diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index a29a34a9a..240711aff 100644 --- a/certora/applyHarness.patch +++ b/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 diff --git a/certora/harnesses/InitializableBasicHarness.sol b/certora/harnesses/InitializableBasicHarness.sol index 08ecbe971..b12b26017 100644 --- a/certora/harnesses/InitializableBasicHarness.sol +++ b/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 returnsV2() public view version2 returns(uint256) { - return unchangeable/3; + 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 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)); + } + } diff --git a/certora/harnesses/InitializableComplexHarness.sol b/certora/harnesses/InitializableComplexHarness.sol new file mode 100644 index 000000000..3e4c0d4b0 --- /dev/null +++ b/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)); + } +} diff --git a/certora/harnesses/InitializablrComplexHarness.sol b/certora/harnesses/InitializablrComplexHarness.sol deleted file mode 100644 index 7a4de57c2..000000000 --- a/certora/harnesses/InitializablrComplexHarness.sol +++ /dev/null @@ -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; - } - -} diff --git a/certora/harnesses/ReinitializersHarness.sol b/certora/harnesses/ReinitializersHarness.sol new file mode 100644 index 000000000..9bf07450b --- /dev/null +++ b/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"); + } +} \ No newline at end of file diff --git a/certora/scripts/old/verifyAll.sh b/certora/scripts/old/verifyAll.sh index 4e04714bb..eb71ead26 100644 --- a/certora/scripts/old/verifyAll.sh +++ b/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 \ diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh index 64952a1d8..4517d161d 100644 --- a/certora/scripts/verifyGovernorPreventLateQuorum.sh +++ b/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" \ diff --git a/certora/scripts/verifyInitializable.sh b/certora/scripts/verifyInitializable.sh new file mode 100644 index 000000000..f302a5c31 --- /dev/null +++ b/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" \ + + + diff --git a/certora/scripts/verifyInitializableComplex.sh b/certora/scripts/verifyInitializableComplex.sh new file mode 100644 index 000000000..2a3da4b2d --- /dev/null +++ b/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" \ + + + diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec index b390da45d..d24d62aa0 100644 --- a/certora/specs/Initializable.spec +++ b/certora/specs/Initializable.spec @@ -1,3 +1,211 @@ methods { - -} \ No newline at end of file + 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; +} diff --git a/certora/specs/governor/GovernorBase.spec b/certora/specs/governor/GovernorBase.spec deleted file mode 100644 index 031b2680e..000000000 --- a/certora/specs/governor/GovernorBase.spec +++ /dev/null @@ -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"); -} - diff --git a/certora/specs/governor/GovernorCountingSimple.spec b/certora/specs/governor/GovernorCountingSimple.spec deleted file mode 100644 index 6d2d5fbb7..000000000 --- a/certora/specs/governor/GovernorCountingSimple.spec +++ /dev/null @@ -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"; -} diff --git a/certora/specs/governor/RulesInProgress.spec b/certora/specs/governor/RulesInProgress.spec deleted file mode 100644 index cbad3336e..000000000 --- a/certora/specs/governor/RulesInProgress.spec +++ /dev/null @@ -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"; -} \ No newline at end of file