Browse Source

initializable final draft, ready for review

teryanarmen 3 years ago
parent
commit
cab8e489b2

+ 41 - 14
certora/applyHarness.patch

@@ -1,12 +1,12 @@
 diff -ruN .gitignore .gitignore
 --- .gitignore	1969-12-31 16:00:00.000000000 -0800
-+++ .gitignore	2022-05-27 01:31:23.000000000 -0700
++++ .gitignore	2022-06-01 15:28:29.000000000 -0700
 @@ -0,0 +1,2 @@
 +*
 +!.gitignore
 diff -ruN access/AccessControl.sol access/AccessControl.sol
 --- access/AccessControl.sol	2022-05-25 09:38:35.000000000 -0700
-+++ access/AccessControl.sol	2022-05-27 01:31:23.000000000 -0700
++++ access/AccessControl.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -93,7 +93,7 @@
       *
       * _Available since v4.6._
@@ -18,7 +18,7 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
  
 diff -ruN governance/Governor.sol governance/Governor.sol
 --- governance/Governor.sol	2022-05-25 09:38:35.000000000 -0700
-+++ governance/Governor.sol	2022-05-27 01:31:23.000000000 -0700
++++ governance/Governor.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -44,7 +44,7 @@
  
      string private _name;
@@ -30,7 +30,7 @@ diff -ruN governance/Governor.sol governance/Governor.sol
      // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
 diff -ruN governance/TimelockController.sol governance/TimelockController.sol
 --- governance/TimelockController.sol	2022-05-25 09:38:35.000000000 -0700
-+++ governance/TimelockController.sol	2022-05-27 01:31:23.000000000 -0700
++++ governance/TimelockController.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -28,10 +28,10 @@
      bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
      bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
@@ -46,7 +46,7 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol
       * @dev Emitted when a call is scheduled as part of operation `id`.
 diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
 --- governance/extensions/GovernorCountingSimple.sol	2022-05-25 09:38:35.000000000 -0700
-+++ governance/extensions/GovernorCountingSimple.sol	2022-05-27 03:15:40.000000000 -0700
++++ governance/extensions/GovernorCountingSimple.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -27,7 +27,7 @@
          mapping(address => bool) hasVoted;
      }
@@ -58,7 +58,7 @@ diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions
       * @dev See {IGovernor-COUNTING_MODE}.
 diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
 --- governance/extensions/GovernorPreventLateQuorum.sol	2022-05-25 09:38:35.000000000 -0700
-+++ governance/extensions/GovernorPreventLateQuorum.sol	2022-05-27 01:31:23.000000000 -0700
++++ governance/extensions/GovernorPreventLateQuorum.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -21,8 +21,8 @@
      using SafeCast for uint256;
      using Timers for Timers.BlockNumber;
@@ -72,7 +72,7 @@ diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensi
      event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
 diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 --- governance/utils/Votes.sol	2022-05-25 09:38:35.000000000 -0700
-+++ governance/utils/Votes.sol	2022-05-27 01:31:23.000000000 -0700
++++ governance/utils/Votes.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -35,7 +35,25 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -145,9 +145,36 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 -    function _getVotingUnits(address) internal view virtual returns (uint256);
 +    function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public
  }
+diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol
+--- proxy/utils/Initializable.sol	2022-05-25 14:01:12.000000000 -0700
++++ proxy/utils/Initializable.sol	2022-06-01 17:10:12.000000000 -0700
+@@ -59,12 +59,12 @@
+      * @dev Indicates that the contract has been initialized.
+      * @custom:oz-retyped-from bool
+      */
+-    uint8 private _initialized;
++    uint8 internal _initialized;
+ 
+     /**
+      * @dev Indicates that the contract is in the process of being initialized.
+      */
+-    bool private _initializing;
++    bool internal _initializing;
+ 
+     /**
+      * @dev Triggered when the contract has been initialized or reinitialized.
+@@ -130,7 +130,7 @@
+         _setInitializedVersion(type(uint8).max);
+     }
+ 
+-    function _setInitializedVersion(uint8 version) private returns (bool) {
++    function _setInitializedVersion(uint8 version) internal returns (bool) {
+         // If the contract is initializing we ignore whether _initialized is set in order to support multiple
+         // inheritance patterns, but we only do this in the context of a constructor, and for the lowest level
+         // of initializers, because in other contexts the contract may have been reentered.
 diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
 --- token/ERC1155/ERC1155.sol	2022-05-25 09:38:35.000000000 -0700
-+++ token/ERC1155/ERC1155.sol	2022-05-27 01:31:23.000000000 -0700
++++ token/ERC1155/ERC1155.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -268,7 +268,7 @@
          uint256 id,
          uint256 amount,
@@ -204,7 +231,7 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
                  bytes4 response
 diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
 --- token/ERC20/ERC20.sol	2022-05-25 09:38:35.000000000 -0700
-+++ token/ERC20/ERC20.sol	2022-05-27 01:31:23.000000000 -0700
++++ token/ERC20/ERC20.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -277,7 +277,7 @@
       * - `account` cannot be the zero address.
       * - `account` must have at least `amount` tokens.
@@ -216,7 +243,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
          _beforeTokenTransfer(account, address(0), amount);
 diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
 --- token/ERC20/extensions/ERC20FlashMint.sol	2022-05-25 09:38:35.000000000 -0700
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2022-05-27 01:31:23.000000000 -0700
++++ token/ERC20/extensions/ERC20FlashMint.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -40,9 +40,11 @@
          require(token == address(this), "ERC20FlashMint: wrong token");
          // silence warning about unused variable without the addition of bytecode.
@@ -232,7 +259,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20
       * implementation returns the address(0) which means the fee amount will be burnt.
 diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
 --- token/ERC20/extensions/ERC20Votes.sol	2022-05-06 13:43:21.000000000 -0700
-+++ token/ERC20/extensions/ERC20Votes.sol	2022-05-27 01:31:23.000000000 -0700
++++ token/ERC20/extensions/ERC20Votes.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -33,8 +33,8 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -255,7 +282,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
          _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount);
 diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
 --- token/ERC20/extensions/ERC20Wrapper.sol	2022-05-25 09:38:35.000000000 -0700
-+++ token/ERC20/extensions/ERC20Wrapper.sol	2022-05-27 01:31:23.000000000 -0700
++++ token/ERC20/extensions/ERC20Wrapper.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -55,7 +55,7 @@
       * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
       * function that can be exposed with access control if desired.
@@ -267,7 +294,7 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr
          return value;
 diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
 --- token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-25 09:38:35.000000000 -0700
-+++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-27 01:31:23.000000000 -0700
++++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -34,7 +34,7 @@
      /**
       * @dev Returns the balance of `account`.
@@ -279,7 +306,7 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/
  }
 diff -ruN utils/Address.sol utils/Address.sol
 --- utils/Address.sol	2022-05-25 09:38:35.000000000 -0700
-+++ utils/Address.sol	2022-05-27 01:31:23.000000000 -0700
++++ utils/Address.sol	2022-06-01 15:28:29.000000000 -0700
 @@ -131,6 +131,7 @@
          uint256 value,
          string memory errorMessage

+ 50 - 12
certora/harnesses/InitializableBasicHarness.sol

@@ -1,35 +1,73 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.2;
 
-import "../munged/proxy/utils/Initializable4.6.sol";
+import "../munged/proxy/utils/Initializable.sol";
 
 contract InitializableBasicHarness is Initializable {
 
-    uint256 public unchangeable;
-    
+    uint256 public val;
+    uint256 public a;
+    uint256 public b;
+
     modifier version1() {
         require(_initialized == 1);
         _;
     }
 
-    modifier version2() {
-        require(_initialized == 2);
+    modifier versionN(uint8 n) {
+        require(_initialized == n);
         _;
     }
 
-    function initialize(uint256 val) public initializer {
-        unchangeable = val;
+    function initialize(uint256 _val, uint256 _a, uint256 _b) public initializer {
+        a = _a;
+        b = _b;
+        val = _val;
     }
 
-    function reinitialize(uint256 val) public reinitializer(2) {
-        unchangeable = val;
+    function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) public reinitializer(n) {
+        a = _a;
+        b = _b;
+        val = _val;
     }
 
+    // Versionede return functions for testing
+
     function returnsV1() public view version1 returns(uint256) {
-        return unchangeable/2;
+        return val/2;
+    }
+
+    function returnsVN(uint8 n) public view versionN(n) returns(uint256) {
+        return val/(n+1);
+    }
+    
+    function returnsAV1() public view version1 returns(uint256) {
+        return a/2;
+    }
+
+    function returnsAVN(uint8 n) public view versionN(n) returns(uint256) {
+        return a/(n+1);
     }
 
-    function returnsV2() public view version2 returns(uint256) {
-        return unchangeable/3;
+    function returnsBV1() public view version1 returns(uint256) {
+        return b/2;
     }
+
+    function returnsBVN(uint8 n) public view versionN(n) returns(uint256) {
+        return b/(n+1);
+    }
+
+    // Harness //
+    function initialized() public view returns(uint8) {
+        return _initialized;
+    }
+
+    function initializing() public view returns(bool) {
+        return _initializing;
+    }
+
+    function thisIsContract() public view returns(bool) {
+        return !Address.isContract(address(this));
+    }
+    
 }

+ 81 - 0
certora/harnesses/InitializableComplexHarness.sol

@@ -0,0 +1,81 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/proxy/utils/Initializable.sol";
+
+contract InitializableA is Initializable {
+    uint256 public a;
+    
+    modifier version1() {
+        require(_initialized == 1);
+        _;
+    }
+
+    modifier versionN(uint8 n) {
+        require(_initialized == n);
+        _;
+    }
+    function __InitializableA_init(uint256 _a) internal onlyInitializing {
+        a = _a;
+    }
+    
+    function returnsAV1() public view version1 returns(uint256) {
+        return a/2;
+    }
+
+    function returnsAVN(uint8 n) public view versionN(n) returns(uint256) {
+        return a/(n+1);
+    }
+}
+
+contract InitializableB is Initializable, InitializableA {
+    uint256 public b;
+    function __InitializableB_init(uint256 _b) internal onlyInitializing {
+        b = _b;
+    }
+
+    function returnsBV1() public view version1 returns(uint256) {
+        return b/2;
+    }
+
+    function returnsBVN(uint8 n) public view versionN(n) returns(uint256) {
+        return b/(n+1);
+    }
+}
+
+contract InitializableComplexHarness is Initializable, InitializableB {
+    uint256 public val;
+
+    function initialize(uint256 _val, uint256 _a, uint256 _b) initializer public {
+        val = _val;
+        __InitializableA_init(_a);
+        __InitializableB_init(_b);
+    }
+
+    function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) reinitializer(n) public {
+        val = _val;
+        __InitializableA_init(_a);
+        __InitializableB_init(_b);
+    }
+
+    function returnsV1() public view version1 returns(uint256) {
+        return val/2;
+    }
+
+    function returnsVN(uint8 n) public view versionN(n) returns(uint256) {
+        return val/(n+1);
+    }
+
+    // Harness //
+    function initialized() public view returns(uint8) {
+        return _initialized;
+    }
+
+    function initializing() public view returns(bool) {
+        return _initializing;
+    }
+
+    function thisIsContract() public view returns(bool) {
+        return !Address.isContract(address(this));
+    }
+}

+ 0 - 18
certora/harnesses/InitializablrComplexHarness.sol

@@ -1,18 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.2;
-
-import "../munged/proxy/utils/Initializable4.6.sol";
-
-contract InitializableBasicHarness is Initializable {
-
-    uint256 public unchangeable;
-
-    function initialize(uint256 _val) public initializer {
-        unchangeable = _val;
-    }
-    
-    function reinitialize(uint256 _val) public reinitializer(2) {
-        unchangeable = _val;
-    }
-    
-}

+ 18 - 0
certora/harnesses/ReinitializersHarness.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.4;
+
+import "@openzeppelin/contracts-upgradeable/proxy/utils/Initializable.sol";
+import "@openzeppelin/contracts-upgradeable/token/ERC20/ERC20Upgradeable.sol";
+import "@openzeppelin/contracts-upgradeable/token/ERC20/extensions/draft-ERC20PermitUpgradeable.sol";
+
+contract MyTokenV1 is Initializable, ERC20Upgradeable {
+    function initialize() initializer public {
+        __ERC20_init("MyToken", "MTK");
+    }
+}
+
+contract MyTokenV2 is Initializable, ERC20Upgradeable, ERC20PermitUpgradeable {
+    function initializeV2() reinitializer(2) public {
+        __ERC20Permit_init("MyToken");
+    }
+}

+ 2 - 2
certora/scripts/old/verifyAll.sh

@@ -18,7 +18,7 @@ do
                 certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
                 --link ${contractFile%.*}:token=ERC20VotesHarness \
                 --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
+                --solc solc \
                 --staging shelly/forSasha \
                 --disableLocalTypeChecking \
                 --optimistic_loop \
@@ -28,7 +28,7 @@ do
             else
                 certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
                 --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
+                --solc solc \
                 --staging shelly/forSasha \
                 --disableLocalTypeChecking \
                 --optimistic_loop \

+ 2 - 4
certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -3,12 +3,10 @@ certoraRun \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
     --solc solc \
     --optimistic_loop \
-    --staging \
-    --settings -optimisticFallback=true \
+    --rule_sanity advanced \
     --send_only \
     --loop_iter 1 \
-    --rule $1 \
-    --msg "$1" \
+    --msg "all sanity" \
 
 
 

+ 12 - 0
certora/scripts/verifyInitializable.sh

@@ -0,0 +1,12 @@
+certoraRun \
+    certora/harnesses/InitializableComplexHarness.sol \
+    --verify InitializableComplexHarness:certora/specs/Initializable.spec \
+    --solc solc \
+    --optimistic_loop \
+    --send_only \
+    --rule_sanity advanced \
+    --loop_iter 3 \
+    --msg "all complex sanity" \
+
+
+

+ 12 - 0
certora/scripts/verifyInitializableComplex.sh

@@ -0,0 +1,12 @@
+certoraRun \
+    certora/harnesses/InitializableComplexHarness.sol \
+    --verify InitializableComplexHarness:certora/specs/InitializableCompex.spec \
+    --solc solc \
+    --optimistic_loop \
+    --rule_sanity advanced \
+    --send_only \
+    --loop_iter 1 \
+    --msg "all sanity" \
+
+
+

+ 210 - 2
certora/specs/Initializable.spec

@@ -1,3 +1,211 @@
 methods {
-    
-}
+    initialize(uint256, uint256, uint256) envfree
+    reinitialize(uint256, uint256, uint256, uint8) envfree
+    initialized() returns uint8 envfree
+    initializing() returns bool envfree
+    thisIsContract() returns bool envfree
+
+    returnsV1() returns uint256 envfree
+    returnsVN(uint8) returns uint256 envfree
+    returnsAV1() returns uint256 envfree
+    returnsAVN(uint8) returns uint256 envfree
+    returnsBV1() returns uint256 envfree
+    returnsBVN(uint8) returns uint256 envfree
+    a() returns uint256 envfree
+    b() returns uint256 envfree
+    val() returns uint256 envfree
+}
+
+definition isUninitialized() returns bool = initialized() == 0;
+
+definition isInitialized() returns bool = initialized() > 0;
+
+definition isInitializedOnce() returns bool = initialized() == 1;
+
+definition isReinitialized() returns bool = initialized() > 1;
+
+definition isDisabled() returns bool = initialized() == 255;
+
+/*
+idea : need extensive harness to test upgrading with reinitialize 
+
+Setup:
+
+contracts A, B, C
+
+Scenario where B extends A and both are being initialized
+
+Potentially need to summarize ‘isContract’
+
+Multiple Versioning within one contract
+
+ 
+
+Test Cases: 
+
+Simple
+
+1 contract with initialize and reinitialize methods (v 1-3)
+
+Multiple Inheritance 
+
+Contracts A, B, C
+
+C Inherits from B, which Inherits from A
+
+Properties
+
+/// You can only initialize once  
+/// two rules prove initialize is equivalent to reinitialize(1) property (?) -- what other effects from these calls?
+// if reinitialize(1) is called successfully, _initialized is set to 1
+// if initialize is called successfully, _initialized is set to 1
+/// disabled stays disabled
+// invariant
+// or rule?
+/// n increase iff reinitialize succeeds 
+// n only increases
+// reinitialize called => n increases 
+/// You can reinitialize(n) iff n > _initialized && initialized < 256 (maxuint8) 
+// <=
+// =>
+/// can only cal v1 function in v1
+
+Question: can we handle reentrancy?
+*/
+
+// You can only initialize once  
+rule initOnce() {
+    uint256 val; uint256 a; uint256 b;
+
+    require isInitialized();
+    initialize@withrevert(val, a, b);
+    assert lastReverted;
+}
+
+/// two rules prove initialize is equivalent to reinitialize(1) property (?) -- what other effects from these calls?
+
+// if reinitialize(1) is called successfully, _initialized is set to 1
+rule basicReinitializeEffects() {
+    uint256 val; uint256 a; uint256 b;
+
+    reinitialize(val, a, b, 1);
+
+    assert isInitializedOnce();
+}
+
+// if initialize is called successfully, _initialized is set to 1
+rule initalizeEffects(method f) {
+    env e; calldataarg args;
+
+    f(e, args);
+
+    assert f.selector == initialize(uint256, uint256, uint256).selector => isInitializedOnce();
+}
+
+/// disabled stays disabled
+
+// invariant
+invariant disabledStaysDisabledInv()
+    isDisabled() => isDisabled()
+
+// or rule?
+rule disabledStaysDisabled(method f) {
+    env e; calldataarg args; 
+
+    bool disabledBefore = isDisabled();
+    f(e, args);
+    bool disabledAfter = isDisabled();
+
+    assert disabledBefore => disabledAfter;
+}
+
+/// n increase iff reinitialize succeeds 
+
+// n only increases
+rule increasingInitialized(method f) {
+    env e; calldataarg args;
+
+    uint8 initBefore = initialized();
+    f(e, args);
+    uint8 initAfter = initialized();
+    assert initBefore <= initAfter;
+}
+
+// reinitialize called => n increases 
+rule reinitializeIncreasesInit() {
+    uint256 val; uint8 n; uint256 a; uint256 b;
+
+    uint8 initBefore = initialized();
+    reinitialize(val, a, b, n);
+    uint8 initAfter = initialized();
+
+    assert initAfter > initBefore;
+}
+
+/// You can reinitialize(n) iff n > _initialized && initialized < 256 (maxuint8) 
+
+// <=
+rule reinitializeLiveness() {
+    env e; uint256 val; uint8 n; uint256 a; uint256 b;
+
+    require !initializing();
+    uint8 initVal = initialized();
+    reinitialize@withrevert(val, a, b, n);
+
+    assert n > initVal && initVal < 255 => !lastReverted;
+}
+
+// =>
+rule reinitializeRule() {
+    env e; calldataarg args; uint256 val; uint8 n; uint256 a; uint256 b;
+
+    uint8 initBefore = initialized();
+    reinitialize(val, a, b, n);
+    uint8 initAfter = initialized();
+
+    assert initAfter > initBefore => n > initBefore;
+}
+
+// can only call v1 functions in v1
+rule initVersionCheck() {
+    env e; calldataarg args; uint256 val; uint256 a; uint256 b; uint8 n; 
+
+    require n != 1;
+
+    initialize(val, a, b);
+    assert returnsV1() == val / 2;
+    assert returnsAV1() == a / 2;
+    assert returnsBV1() == b / 2;
+    returnsVN@withrevert(n);
+    assert lastReverted;
+    returnsAVN@withrevert(n);
+    assert lastReverted;
+    returnsBVN@withrevert(n);
+    assert lastReverted;
+}
+
+// can only call V_n functions in V_n
+rule reinitVersionCheck() {
+    env e; calldataarg args; uint256 val; uint256 a; uint256 b; uint8 n; uint8 m;
+
+    require n != m;
+
+    reinitialize(val, a, b, n);
+    assert returnsVN(n) == val / (n + 1);
+    assert returnsAVN(n) == a / (n + 1);
+    assert returnsBVN(n) == b / (n + 1);
+
+    returnsVN@withrevert(m);
+    assert lastReverted;
+    returnsAVN@withrevert(m);
+    assert lastReverted;
+    returnsBVN@withrevert(m);
+    assert lastReverted;
+}
+
+rule inheritanceCheck() {
+    env e; calldataarg args; uint256 val; uint8 n; uint256 a; uint256 b;
+
+    initialize(val, a, b);
+    assert val() == val && a() == a && b() == b;
+}

+ 0 - 334
certora/specs/governor/GovernorBase.spec

@@ -1,334 +0,0 @@
-//////////////////////////////////////////////////////////////////////////////
-///////////////////// Governor.sol base definitions //////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
-    proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd
-    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
-    isExecuted(uint256) returns bool envfree
-    isCanceled(uint256) returns bool envfree
-    execute(address[], uint256[], bytes[], bytes32) returns uint256
-    hasVoted(uint256, address) returns bool
-    castVote(uint256, uint8) returns uint256
-    updateQuorumNumerator(uint256)
-    queue(address[], uint256[], bytes[], bytes32) returns uint256
-
-    // internal functions made public in harness:
-    _quorumReached(uint256) returns bool
-    _voteSucceeded(uint256) returns bool envfree
-
-    // function summarization
-    proposalThreshold() returns uint256 envfree
-
-    getVotes(address, uint256) returns uint256 => DISPATCHER(true)
-
-    getPastTotalSupply(uint256 t) returns uint256      => PER_CALLEE_CONSTANT
-    getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT
-
-    //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
-    //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
-}
-
-//////////////////////////////////////////////////////////////////////////////
-//////////////////////////////// Definitions /////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-// proposal was created - relation proved in noStartBeforeCreation
-definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////// Helper Functions ///////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
-    address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash;
-    uint8 support; uint8 v; bytes32 r; bytes32 s;
-	if (f.selector == propose(address[], uint256[], bytes[], string).selector) {
-		uint256 result = propose@withrevert(e, targets, values, calldatas, reason);
-        require(result == proposalId);
-	} else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) {
-		uint256 result = execute@withrevert(e, targets, values, calldatas, descriptionHash);
-        require(result == proposalId);
-	} else if (f.selector == castVote(uint256, uint8).selector) {
-		castVote@withrevert(e, proposalId, support);
-	} else if  (f.selector == castVoteWithReason(uint256, uint8, string).selector) {
-        castVoteWithReason@withrevert(e, proposalId, support, reason);
-	} else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) {
-		castVoteBySig@withrevert(e, proposalId, support, v, r, s);
-    } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) {
-        queue@withrevert(e, targets, values, calldatas, descriptionHash);
-	} else {
-        calldataarg args;
-        f@withrevert(e, args);
-    }
-}
-
-/*
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
- ///////////////////////////////////////////////////// State Diagram //////////////////////////////////////////////////////////
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
- //                                                                                                                          //
- //                                                                castVote(s)()                                             //
- //  -------------  propose()  ----------------------  time pass  ---------------       time passes         -----------      //
- // | No Proposal | --------> | Before Start (Delay) | --------> | Voting Period | ----------------------> | execute() |     //
- //  -------------             ----------------------             --------------- -> Executed/Canceled      -----------      //
- //  ------------------------------------------------------------|---------------|-------------------------|-------------->  //
- // t                                                          start            end                     timelock             //
- //                                                                                                                          //
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-*/
-
-
-///////////////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// Global Valid States /////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * Start and end date are either initialized (non zero) or uninitialized (zero) simultaneously
- * This invariant assumes that the block number cannot be 0 at any stage of the contract cycle
- * This is very safe assumption as usually the 0 block is genesis block which is uploaded with data
- * by the developers and will not be valid to raise proposals (at the current way that block chain is functioning)
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant startAndEndDatesNonZero(uint256 pId)
-        proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0
-        { preserved with (env e){   
-                require e.block.number > 0;
-        }}
-        
-
-/*
- * If a proposal is canceled it must have a start and an end date 
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant canceledImplyStartAndEndDateNonZero(uint pId)
-        isCanceled(pId) => proposalSnapshot(pId) != 0
-        {preserved with (env e){               
-                require e.block.number > 0;
-        }}
-
-
-/*
- * If a proposal is executed it must have a start and an end date 
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking] 
-invariant executedImplyStartAndEndDateNonZero(uint pId)
-        isExecuted(pId) => proposalSnapshot(pId) != 0
-        { preserved with (env e){
-            requireInvariant startAndEndDatesNonZero(pId);
-            require e.block.number > 0;
-        }}
-
-
-/*
- * A proposal starting block number must be less or equal than the proposal end date
- */
-invariant voteStartBeforeVoteEnd(uint256 pId)
-        // from < to <= because snapshot and deadline can be the same block number if delays are set to 0
-        // This is possible before the integration of GovernorSettings.sol to the system.
-        // After integration of GovernorSettings.sol the invariant expression should be changed from <= to <
-        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) <= proposalDeadline(pId))
-        // (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) <= proposalDeadline(pId))
-        { preserved {
-            requireInvariant startAndEndDatesNonZero(pId);
-        }}
-
-
-/*
- * A proposal cannot be both executed and canceled simultaneously.
- */
-invariant noBothExecutedAndCanceled(uint256 pId) 
-        !isExecuted(pId) || !isCanceled(pId)
-
-
-/*
- * A proposal could be executed only if quorum was reached and vote succeeded
- */
-rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){
-    bool isExecutedBefore = isExecuted(pId);
-    bool quorumReachedBefore = _quorumReached(e, pId);
-    bool voteSucceededBefore = _voteSucceeded(pId);
-    
-    calldataarg args;
-    f(e, args);
-    
-    bool isExecutedAfter = isExecuted(pId);
-    assert (!isExecutedBefore && isExecutedAfter) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed";
-}
-
-///////////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////// In-State Rules /////////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-//==========================================
-//------------- Voting Period --------------
-//==========================================
-
-/*
- * A user cannot vote twice
- */
- // Checked for castVote only. all 3 castVote functions call _castVote, so the completness of the verification is counted on
- // the fact that the 3 functions themselves makes no chages, but rather call an internal function to execute.
- // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
- // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
- // We could check each function seperately and pass the rule, but that would have uglyfied the code with no concrete 
- // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
-rule doubleVoting(uint256 pId, uint8 sup, method f) {
-    env e;
-    address user = e.msg.sender;        
-    bool votedCheck = hasVoted(e, pId, user);
-
-    castVote@withrevert(e, pId, sup);
-
-    assert votedCheck => lastReverted, "double voting accured";
-}
-
-
-///////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////// State Transitions Rules //////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-//===========================================
-//-------- Propose() --> End of Time --------
-//===========================================
-
-
-/*
- * Once a proposal is created, voteStart and voteEnd are immutable
- */
-rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
-    uint256 _voteStart = proposalSnapshot(pId);
-    uint256 _voteEnd = proposalDeadline(pId);
-
-    require proposalCreated(pId); // startDate > 0
-    
-    env e; calldataarg arg;
-    f(e, arg);
-
-    uint256 voteStart_ = proposalSnapshot(pId);
-    uint256 voteEnd_ = proposalDeadline(pId);
-    assert _voteStart == voteStart_, "Start date was changed";
-    assert _voteEnd == voteEnd_, "End date was changed";
-}
-
-
-/*
- * Voting cannot start at a block number prior to proposal’s creation block number
- */
-rule noStartBeforeCreation(uint256 pId) {
-    uint256 previousStart = proposalSnapshot(pId);
-    // This line makes sure that we see only cases where start date is changed from 0, i.e. creation of proposal
-    // We proved in immutableFieldsAfterProposalCreation that once dates set for proposal, it cannot be changed
-    require !proposalCreated(pId); // previousStart == 0;
-    
-    env e; calldataarg args;
-    propose(e, args);
-
-    uint256 newStart = proposalSnapshot(pId);
-    // if created, start is after current block number (creation block)
-    assert(newStart != previousStart => newStart >= e.block.number);
-}
-
-
-//============================================
-//--- End of Voting Period --> End of Time ---
-//============================================
-
-
-/*
- * A proposal can neither be executed nor canceled before it ends
- */
- // By induction it cannot be executed nor canceled before it starts, due to voteStartBeforeVoteEnd
-rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
-    require !isExecuted(pId) && !isCanceled(pId);
-
-    env e; calldataarg args;
-    f(e, args);
-
-    assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline";
-}
-
-////////////////////////////////////////////////////////////////////////////////
-////////////////////// Integrity Of Functions (Unit Tests) /////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////// High Level Rules ////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////////////
-///////////////////////////// Not Categorized Yet //////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * All proposal specific (non-view) functions should revert if proposal is executed
- */
- // In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID,
- // non of the proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc 
- // we connected the executed attribute to the execute() function, showing that only execute() can
- // change it, and that it will always change it.
-rule allFunctionsRevertIfExecuted(method f) filtered { f ->
-    !f.isView && !f.isFallback
-      && f.selector != updateTimelock(address).selector
-      && f.selector != updateQuorumNumerator(uint256).selector
-      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
-      && f.selector != relay(address,uint256,bytes).selector
-      && f.selector != 0xb9a61961 // __acceptAdmin()
-} {
-    env e; calldataarg args;
-    uint256 pId;
-    require(isExecuted(pId));
-    requireInvariant noBothExecutedAndCanceled(pId);
-    requireInvariant executedImplyStartAndEndDateNonZero(pId);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    assert(lastReverted, "Function was not reverted");
-}
-
-/*
- * All proposal specific (non-view) functions should revert if proposal is canceled
- */
-rule allFunctionsRevertIfCanceled(method f) filtered {
-    f -> !f.isView && !f.isFallback
-      && f.selector != updateTimelock(address).selector
-      && f.selector != updateQuorumNumerator(uint256).selector
-      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
-      && f.selector != relay(address,uint256,bytes).selector
-      && f.selector != 0xb9a61961 // __acceptAdmin()
-} {
-    env e; calldataarg args;
-    uint256 pId;
-    require(isCanceled(pId));
-    requireInvariant noBothExecutedAndCanceled(pId);
-    requireInvariant canceledImplyStartAndEndDateNonZero(pId);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    assert(lastReverted, "Function was not reverted");
-}
-
-/*
- * Proposal can be switched to executed only via execute() function
- */
-rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) {
-    env e; calldataarg args;
-    uint256 pId;
-    bool executedBefore = isExecuted(pId);
-    require(!executedBefore);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    bool executedAfter = isExecuted(pId);
-    assert(executedAfter != executedBefore => f.selector == execute(address[], uint256[], bytes[], bytes32).selector, "isExecuted only changes in the execute method");
-}
-

+ 0 - 221
certora/specs/governor/GovernorCountingSimple.spec

@@ -1,221 +0,0 @@
-import "GovernorBase.spec"
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
-
-    quorum(uint256) returns uint256
-    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
-
-    quorumNumerator() returns uint256
-    _executor() returns address
-
-    erc20votes._getPastVotes(address, uint256) returns uint256
-
-    getExecutor() returns address
-
-    timelock() returns address
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// GHOSTS /////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//////////// ghosts to keep track of votes counting ////////////
-
-/*
- * the sum of voting power of those who voted
- */
-ghost sum_all_votes_power() returns uint256 {
-	init_state axiom sum_all_votes_power() == 0;
-}
-
-hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
-	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
-}
-
-/*
- * sum of all votes casted per proposal
- */
-ghost tracked_weight(uint256) returns uint256 {
-	init_state axiom forall uint256 p. tracked_weight(p) == 0;
-}
-
-/*
- * sum of all votes casted
- */
-ghost sum_tracked_weight() returns uint256 {
-	init_state axiom sum_tracked_weight() == 0;
-}
-
-/*
- * getter for _proposalVotes.againstVotes
- */
-ghost votesAgainst() returns uint256 {
-    init_state axiom votesAgainst() == 0;
-}
-
-/*
- * getter for _proposalVotes.forVotes
- */
-ghost votesFor() returns uint256 {
-    init_state axiom votesFor() == 0;
-}
-
-/*
- * getter for _proposalVotes.abstainVotes
- */
-ghost votesAbstain() returns uint256 {
-    init_state axiom votesAbstain() == 0;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-////////////////////////////// INVARIANTS ////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal
- */
-invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId) 
-	tracked_weight(pId) == ghost_sum_vote_power_by_id(pId)
-
-
-/*
- * sum of all votes casted is equal to the sum of voting power of those who voted
- */
-invariant SumOfVotesCastEqualSumOfPowerOfVoted() 
-	sum_tracked_weight() == sum_all_votes_power()
-
-
-/*
-* sum of all votes casted is greater or equal to the sum of voting power of those who voted at a specific proposal
-*/
-invariant OneIsNotMoreThanAll(uint256 pId) 
-	sum_all_votes_power() >= tracked_weight(pId)
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// RULES //////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * Only sender's voting status can be changed by execution of any cast vote function
- */
-// Checked for castVote only. all 3 castVote functions call _castVote, so the completness of the verification is counted on
- // the fact that the 3 functions themselves makes no chages, but rather call an internal function to execute.
- // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
- // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
- // We could check each function seperately and pass the rule, but that would have uglyfied the code with no concrete 
- // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
-rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) {
-    env e; calldataarg args;
-
-    address voter = e.msg.sender;
-    address user;
-
-    bool hasVotedBefore_User = hasVoted(e, pId, user);
-
-    castVote@withrevert(e, pId, sup);
-    require(!lastReverted);
-
-    bool hasVotedAfter_User = hasVoted(e, pId, user);
-
-    assert user != voter => hasVotedBefore_User == hasVotedAfter_User;
-}
-
-
-/*
-* Total voting tally is monotonically non-decreasing in every operation 
-*/
-rule votingWeightMonotonicity(method f){
-    uint256 votingWeightBefore = sum_tracked_weight();
-
-    env e; 
-    calldataarg args;
-    f(e, args);
-
-    uint256 votingWeightAfter = sum_tracked_weight();
-
-    assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow";
-}
-
-
-/*
-* A change in hasVoted must be correlated with an non-decreasing of the vote supports (nondecrease because user can vote with weight 0)
-*/
-rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
-    address acc = e.msg.sender;
-    
-    uint256 againstBefore = votesAgainst();
-    uint256 forBefore = votesFor();
-    uint256 abstainBefore = votesAbstain();
-
-    bool hasVotedBefore = hasVoted(e, pId, acc);
-
-    helperFunctionsWithRevert(pId, f, e);
-    require(!lastReverted);
-
-    uint256 againstAfter = votesAgainst();
-    uint256 forAfter = votesFor();
-    uint256 abstainAfter = votesAbstain();
-    
-    bool hasVotedAfter = hasVoted(e, pId, acc);
-
-    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
-}
-
-
-/*
-* Only privileged users can execute privileged operations, e.g. change _quorumNumerator or _timelock
-*/
-rule privilegedOnlyNumerator(method f, uint256 newQuorumNumerator){
-    env e;
-    calldataarg arg;
-    uint256 quorumNumBefore = quorumNumerator(e);
-
-    f(e, arg);
-
-    uint256 quorumNumAfter = quorumNumerator(e);
-    address executorCheck = getExecutor(e);
-
-    assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non priveleged user changed quorum numerator";
-}
-
-rule privilegedOnlyTimelock(method f, uint256 newQuorumNumerator){
-    env e;
-    calldataarg arg;
-    uint256 timelockBefore = timelock(e);
-
-    f(e, arg);
-
-    uint256 timelockAfter = timelock(e);
-
-    assert timelockBefore != timelockAfter => e.msg.sender == timelockBefore, "non priveleged user changed timelock";
-}

+ 0 - 139
certora/specs/governor/RulesInProgress.spec

@@ -1,139 +0,0 @@
-//////////////////////////////////////////////////////////////////////////////
-////////////// THIS SPEC IS A RESERVE FOR NOT IN PROGRESS //////////////
-//////////////////////////////////////////////////////////////////////////////
-
-import "GovernorBase.spec"
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
-
-    quorum(uint256) returns uint256
-    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
-
-    quorumNumerator() returns uint256
-    _executor() returns address
-
-    erc20votes._getPastVotes(address, uint256) returns uint256
-
-    getExecutor() returns address
-
-    timelock() returns address
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// GHOSTS /////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//////////// ghosts to keep track of votes counting ////////////
-
-/*
- * the sum of voting power of those who voted
- */
-ghost sum_all_votes_power() returns uint256 {
-	init_state axiom sum_all_votes_power() == 0;
-}
-
-hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
-	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
-}
-
-/*
- * sum of all votes casted per proposal
- */
-ghost tracked_weight(uint256) returns uint256 {
-	init_state axiom forall uint256 p. tracked_weight(p) == 0;
-}
-
-/*
- * sum of all votes casted
- */
-ghost sum_tracked_weight() returns uint256 {
-	init_state axiom sum_tracked_weight() == 0;
-}
-
-/*
- * getter for _proposalVotes.againstVotes
- */
-ghost votesAgainst() returns uint256 {
-    init_state axiom votesAgainst() == 0;
-}
-
-/*
- * getter for _proposalVotes.forVotes
- */
-ghost votesFor() returns uint256 {
-    init_state axiom votesFor() == 0;
-}
-
-/*
- * getter for _proposalVotes.abstainVotes
- */
-ghost votesAbstain() returns uint256 {
-    init_state axiom votesAbstain() == 0;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-////////////////////////////// INVARIANTS ////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// RULES //////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//NOT FINISHED
-/*
-* the sum of voting power of those who voted is less or equal to the maximum possible votes, per each proposal
-*/
-rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
-
-    // add requireinvariant  for all i, j. i = i - 1 && i < j => checkpointlookup[i] < checkpointlookup[j];
-    require tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId));
-
-    uint256 againstB;
-    uint256 forB;
-    uint256 absatinB;
-    againstB, forB, absatinB = proposalVotes(pId);
-
-    calldataarg args;
-    //f(e, args);
-
-    castVote(e, pId, sup);
-
-    uint256 against;
-    uint256 for;
-    uint256 absatin;
-    against, for, absatin = proposalVotes(pId);
-
-    uint256 ps = proposalSnapshot(pId);
-
-    assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
-}