From 793b88efd8eedda38dbe6e04d20342a1277ade08 Mon Sep 17 00:00:00 2001 From: teryanarmen Date: Mon, 16 May 2022 14:26:31 -0700 Subject: [PATCH] finalize fist 3 rules; fix old governor spec --- .vscode/settings.json | 3 + certora/applyHarness.patch | 50 +++++-- .../GovernorPreventLateQuorumHarness.sol | 32 ++++- .../munged/governance/TimelockController.sol | 7 +- certora/munged/utils/Address.sol | 1 + .../verifyGovernorPreventLateQuorum.sh | 15 ++- certora/specs/GovernorBase.spec | 23 ++-- certora/specs/GovernorCountingSimple.spec | 3 +- certora/specs/GovernorPreventLateQuorum.spec | 123 +++++++++--------- 9 files changed, 165 insertions(+), 92 deletions(-) create mode 100644 .vscode/settings.json diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 000000000..5120aebf5 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,3 @@ +{ + "solidity.compileUsingRemoteVersion": "v0.8.2+commit.661d1103" +} \ No newline at end of file diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 32adf065f..1403850fb 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,6 +1,6 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol --- access/AccessControl.sol 2022-05-06 13:44:28.000000000 -0700 -+++ access/AccessControl.sol 2022-05-09 09:49:26.000000000 -0700 ++++ access/AccessControl.sol 2022-05-11 11:17:20.000000000 -0700 @@ -93,7 +93,7 @@ * * _Available since v4.6._ @@ -12,7 +12,7 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol diff -ruN governance/Governor.sol governance/Governor.sol --- governance/Governor.sol 2022-05-09 09:11:10.000000000 -0700 -+++ governance/Governor.sol 2022-05-09 09:49:26.000000000 -0700 ++++ governance/Governor.sol 2022-05-11 11:17:20.000000000 -0700 @@ -42,7 +42,7 @@ string private _name; @@ -24,7 +24,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-06 13:44:28.000000000 -0700 -+++ governance/TimelockController.sol 2022-05-09 09:49:26.000000000 -0700 ++++ governance/TimelockController.sol 2022-05-12 19:13:19.000000000 -0700 @@ -24,10 +24,10 @@ bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE"); bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); @@ -38,7 +38,22 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol /** * @dev Emitted when a call is scheduled as part of operation `id`. -@@ -353,4 +353,4 @@ +@@ -332,10 +332,11 @@ + uint256 value, + bytes calldata data + ) private { +- (bool success, ) = target.call{value: value}(data); +- require(success, "TimelockController: underlying transaction reverted"); ++ return; // can't deal with external calls ++ // (bool success, ) = target.call{value: value}(data); ++ // require(success, "TimelockController: underlying transaction reverted"); + +- emit CallExecuted(id, index, target, value, data); ++ // emit CallExecuted(id, index, target, value, data); + } + + /** +@@ -353,4 +354,4 @@ emit MinDelayChange(_minDelay, newDelay); _minDelay = newDelay; } @@ -46,7 +61,7 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol +} diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol --- governance/extensions/GovernorPreventLateQuorum.sol 2022-05-09 09:11:01.000000000 -0700 -+++ governance/extensions/GovernorPreventLateQuorum.sol 2022-05-09 09:49:26.000000000 -0700 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2022-05-11 11:17:20.000000000 -0700 @@ -21,8 +21,8 @@ using SafeCast for uint256; using Timers for Timers.BlockNumber; @@ -60,7 +75,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-06 13:44:28.000000000 -0700 -+++ governance/utils/Votes.sol 2022-05-09 09:49:26.000000000 -0700 ++++ governance/utils/Votes.sol 2022-05-11 11:17:20.000000000 -0700 @@ -35,7 +35,25 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -135,7 +150,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol } diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol --- token/ERC1155/ERC1155.sol 2022-05-06 13:44:28.000000000 -0700 -+++ token/ERC1155/ERC1155.sol 2022-05-09 09:49:26.000000000 -0700 ++++ token/ERC1155/ERC1155.sol 2022-05-11 11:17:20.000000000 -0700 @@ -268,7 +268,7 @@ uint256 id, uint256 amount, @@ -192,7 +207,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-06 13:44:28.000000000 -0700 -+++ token/ERC20/ERC20.sol 2022-05-09 09:49:26.000000000 -0700 ++++ token/ERC20/ERC20.sol 2022-05-11 11:17:20.000000000 -0700 @@ -277,7 +277,7 @@ * - `account` cannot be the zero address. * - `account` must have at least `amount` tokens. @@ -213,7 +228,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol /** diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol --- token/ERC20/extensions/ERC20FlashMint.sol 2022-05-06 13:44:28.000000000 -0700 -+++ token/ERC20/extensions/ERC20FlashMint.sol 2022-05-09 09:49:26.000000000 -0700 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2022-05-11 11:17:20.000000000 -0700 @@ -40,9 +40,11 @@ require(token == address(this), "ERC20FlashMint: wrong token"); // silence warning about unused variable without the addition of bytecode. @@ -229,7 +244,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 * `receiver`, who is required to implement the {IERC3156FlashBorrower} 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-09 09:49:26.000000000 -0700 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-05-11 11:17:20.000000000 -0700 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -362,7 +377,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote } diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol --- token/ERC20/extensions/ERC20Wrapper.sol 2022-05-06 13:44:28.000000000 -0700 -+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-05-09 09:49:26.000000000 -0700 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-05-11 11:17:20.000000000 -0700 @@ -44,7 +44,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. @@ -374,7 +389,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-06 13:44:28.000000000 -0700 -+++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-05-09 09:49:26.000000000 -0700 ++++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-05-11 11:17:20.000000000 -0700 @@ -34,7 +34,7 @@ /** * @dev Returns the balance of `account`. @@ -384,3 +399,14 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/ return balanceOf(account); } } +diff -ruN utils/Address.sol utils/Address.sol +--- utils/Address.sol 2022-05-06 13:43:21.000000000 -0700 ++++ utils/Address.sol 2022-05-15 10:58:38.000000000 -0700 +@@ -131,6 +131,7 @@ + uint256 value, + string memory errorMessage + ) internal returns (bytes memory) { ++ return ""; + require(address(this).balance >= value, "Address: insufficient balance for call"); + require(isContract(target), "Address: call to non-contract"); + diff --git a/certora/harnesses/GovernorPreventLateQuorumHarness.sol b/certora/harnesses/GovernorPreventLateQuorumHarness.sol index e13bb62e5..cd9133e59 100644 --- a/certora/harnesses/GovernorPreventLateQuorumHarness.sol +++ b/certora/harnesses/GovernorPreventLateQuorumHarness.sol @@ -20,6 +20,8 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G GovernorPreventLateQuorum(initialVoteExtension) {} + mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; + // variable added to check when _castVote is called uint256 public latestCastVoteCall; @@ -39,12 +41,29 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G // Harness from GovernorCountingSimple // - function quorumReached(uint256 proposalId) public view returns(bool) { + function quorumReached(uint256 proposalId) public view returns(bool) { return _quorumReached(proposalId); } + function voteSucceeded(uint256 proposalId) public view returns(bool) { + return _voteSucceeded(proposalId); + } + + function countVote(uint256 proposalId, + address account, + uint8 support, + uint256 weight, + bytes memory // params + ) public view { + return _countVote(proposalId,account,support,weight,""); + } + // Harness from Governor // + function getExecutor() public view returns (address){ + return _executor(); + } + function isExecuted(uint256 proposalId) public view returns (bool) { return _proposals[proposalId].executed; } @@ -66,10 +85,16 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G string memory reason, bytes memory params ) internal virtual override(Governor, GovernorPreventLateQuorum) returns (uint256) { + // flag for when _castVote is called latestCastVoteCall = block.number; - return super._castVote(proposalId, account, support, reason, params); - } + // added to run GovernorCountingSimple.spec + uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params); + ghost_sum_vote_power_by_id[proposalId] += deltaWeight; + + return deltaWeight; + } + /* function castVote( uint256 proposalId, address account, @@ -79,6 +104,7 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G ) public returns(uint256) { return _castVote(proposalId, account, support, reason, params); } + */ function lateQuorumVoteExtension() public view virtual override returns (uint64) { return super.lateQuorumVoteExtension(); diff --git a/certora/munged/governance/TimelockController.sol b/certora/munged/governance/TimelockController.sol index da38df8f3..b8278ff4d 100644 --- a/certora/munged/governance/TimelockController.sol +++ b/certora/munged/governance/TimelockController.sol @@ -332,10 +332,11 @@ contract TimelockController is AccessControl { uint256 value, bytes calldata data ) private { - (bool success, ) = target.call{value: value}(data); - require(success, "TimelockController: underlying transaction reverted"); + return; // haven't dealt with external calls yet + // (bool success, ) = target.call{value: value}(data); + // require(success, "TimelockController: underlying transaction reverted"); - emit CallExecuted(id, index, target, value, data); + // emit CallExecuted(id, index, target, value, data); } /** diff --git a/certora/munged/utils/Address.sol b/certora/munged/utils/Address.sol index daea7f31e..c4da2a463 100644 --- a/certora/munged/utils/Address.sol +++ b/certora/munged/utils/Address.sol @@ -131,6 +131,7 @@ library Address { uint256 value, string memory errorMessage ) internal returns (bytes memory) { + return ""; // external calls havoc require(address(this).balance >= value, "Address: insufficient balance for call"); require(isContract(target), "Address: call to non-contract"); diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh index ed102853c..cbea7b40e 100644 --- a/certora/scripts/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh @@ -1,9 +1,14 @@ certoraRun \ - certora/harnesses/ERC721VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ - --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ + certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorCountingSimple.spec \ --solc solc \ --optimistic_loop \ - --loop_iter 3 \ - --cloud \ + --loop_iter 1 \ + --staging \ + --rule_sanity advanced \ + --send_only \ --rule $1 \ - --msg "GovernorPreventLateQuorum $1" \ No newline at end of file + --msg "$1" \ + + + diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 031b2680e..3936e77c4 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -17,16 +17,16 @@ methods { queue(address[], uint256[], bytes[], bytes32) returns uint256 // internal functions made public in harness: - _quorumReached(uint256) returns bool - _voteSucceeded(uint256) returns bool envfree + 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 + getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true) + getPastVotes(address, uint256) returns uint256 => DISPATCHER(true) //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true) //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) @@ -47,7 +47,7 @@ definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0 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; + uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params; if (f.selector == propose(address[], uint256[], bytes[], string).selector) { uint256 result = propose@withrevert(e, targets, values, calldatas, reason); require(result == proposalId); @@ -62,10 +62,15 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { 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 { + } else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) { + castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s); + } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) { + castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params); + } else { calldataarg args; f@withrevert(e, args); } + } /* @@ -152,8 +157,8 @@ invariant noBothExecutedAndCanceled(uint256 pId) */ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){ bool isExecutedBefore = isExecuted(pId); - bool quorumReachedBefore = _quorumReached(e, pId); - bool voteSucceededBefore = _voteSucceeded(pId); + bool quorumReachedBefore = quorumReached(e, pId); + bool voteSucceededBefore = voteSucceeded(pId); calldataarg args; f(e, args); @@ -283,6 +288,7 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f -> && f.selector != queue(address[],uint256[],bytes[],bytes32).selector && f.selector != relay(address,uint256,bytes).selector && f.selector != 0xb9a61961 // __acceptAdmin() + && f.selector != setLateQuorumVoteExtension(uint64).selector } { env e; calldataarg args; uint256 pId; @@ -305,6 +311,7 @@ rule allFunctionsRevertIfCanceled(method f) filtered { && f.selector != queue(address[],uint256[],bytes[],bytes32).selector && f.selector != relay(address,uint256,bytes).selector && f.selector != 0xb9a61961 // __acceptAdmin() + && f.selector != setLateQuorumVoteExtension(uint64).selector } { env e; calldataarg args; uint256 pId; diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index c5dcecddf..3660e70b4 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -7,7 +7,6 @@ methods { proposalVotes(uint256) returns (uint256, uint256, uint256) envfree quorumNumerator() returns uint256 - _executor() returns address getExecutor() returns address @@ -184,7 +183,7 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) { bool hasVotedAfter = hasVoted(e, pId, acc); - assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation"; + assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter, "no correlation"; } diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index 885c665ed..6ef3745c3 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -3,6 +3,7 @@ ////////////////////////////////////////////////////////////////////////////// using ERC721VotesHarness as erc721votes +using ERC20VotesHarness as erc20votes methods { proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart @@ -19,97 +20,101 @@ methods { quorumDenominator() returns uint256 envfree votingPeriod() returns uint256 envfree lateQuorumVoteExtension() returns uint64 envfree + propose(address[], uint256[], bytes[], string) // harness getExtendedDeadlineIsUnset(uint256) returns bool envfree getExtendedDeadline(uint256) returns uint64 envfree quorumReached(uint256) returns bool envfree + voteSucceeded(uint256) returns bool envfree + quorum(uint256) returns uint256 latestCastVoteCall() returns uint256 envfree // more robust check than f.selector == _castVote(...).selector // function summarization proposalThreshold() returns uint256 envfree + // erc20votes dispatch 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 + // erc721votes/Votes dispatch + getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true) + getPastVotes(address, uint256) returns uint256 => DISPATCHER(true) + // timelock dispatch + getMinDelay() returns uint256 => DISPATCHER(true) + + hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) + executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => CONSTANT + scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT } ////////////////////////////////////////////////////////////////////////////// //////////////////////////////// Definitions ///////////////////////////////// ////////////////////////////////////////////////////////////////////////////// +// where can invariants help? +// can I replace definitions with invariants? + // create definition for extended -definition deadlineCanBeExtended(uint256 id) returns bool = - getExtendedDeadlineIsUnset(id) && - getExtendedDeadline(id) == 0 && - !quorumReached(id); +definition deadlineCanBeExtended(uint256 pId) returns bool = + getExtendedDeadlineIsUnset(pId) && + !quorumReached(pId); -definition deadlineHasBeenExtended(uint256 id) returns bool = - !getExtendedDeadlineIsUnset(id) && - getExtendedDeadline(id) > 0 && - quorumReached(id); +definition deadlineHasBeenExtended(uint256 pId) returns bool = + !getExtendedDeadlineIsUnset(pId) && + quorumReached(pId); +definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0; +////////////////////////////////////////////////////////////////////////////// +////////////////////////////////// Rules ///////////////////////////////////// +////////////////////////////////////////////////////////////////////////////// -// RULE deadline can only be extended once - // 1. if deadline changes then we have state transition from deadlineCanBeExtended to deadlineHasBeenExtended -rule deadlineChangeEffects(method f) filtered {f -> !f.isView /* bottleneck, restrict for faster testing && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } { - env e; calldataarg args; uint256 id; +// RULE deadline can only be extended only once PASSING but vacuous + // 1. if deadline changes then we have state transition to deadlineHasBeenExtended RULE PASSING; ADV SANITY PASSING +rule deadlineChangeEffects(method f) + filtered { + f -> !f.isView + } { + env e; calldataarg args; uint256 pId; - require (latestCastVoteCall() < e.block.number); - require (quorumNumerator() <= quorumDenominator()); - require deadlineCanBeExtended(id); - require (proposalDeadline(id) > e.block.number - && proposalDeadline(id) >= proposalSnapshot(id) + votingPeriod() - && proposalSnapshot(id) < e.block.number); + require (proposalCreated(pId)); - uint256 deadlineBefore = proposalDeadline(id); + uint256 deadlineBefore = proposalDeadline(pId); f(e, args); - uint256 deadlineAfter = proposalDeadline(id); + uint256 deadlineAfter = proposalDeadline(pId); - assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(id)); + assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(pId)); } - // 2. cant unextend -rule deadlineCantBeUnextended(method f) filtered {f -> !f.isView /* && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } { - env e; calldataarg args; uint256 id; - require(deadlineHasBeenExtended(id)); + // 2. cant unextend RULE PASSING*; ADV SANITY PASSING +rule deadlineCantBeUnextended(method f) + filtered { + f -> !f.isView + && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function + } { + env e; calldataarg args; uint256 pId; + + require(deadlineHasBeenExtended(pId)); + require(proposalCreated(pId)); + f(e, args); - assert(deadlineHasBeenExtended(id)); + + assert(deadlineHasBeenExtended(pId)); } - // 3. extended => can't change deadline + // 3. extended => can't change deadline RULE PASSING; ADV SANITY PASSING //@note if deadline changed, then it wasnt extended and castvote was called -rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView /* && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } { - env e; calldataarg args; - uint256 id; - require(deadlineHasBeenExtended(id)); // stays true - require (proposalDeadline(id) > e.block.number - && proposalDeadline(id) >= proposalSnapshot(id) + votingPeriod() - && proposalSnapshot(id) < e.block.number); - uint256 deadlineBefore = proposalDeadline(id); +rule canExtendDeadlineOnce(method f) + filtered { + f -> !f.isView + } { + env e; calldataarg args; uint256 pId; + + require(deadlineHasBeenExtended(pId)); + require(proposalCreated(pId)); + + uint256 deadlineBefore = proposalDeadline(pId); f(e, args); - uint256 deadlineAfter = proposalDeadline(id); + uint256 deadlineAfter = proposalDeadline(pId); + assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); } - - -// RULE deadline can only extended if quorum reached w/ <= timeOfExtension left to vote -// 3 rules - // 1. voting increases total votes - // 2. number of votes > quorum => quorum reached - // 3. deadline can only extended if quorum reached w/ <= timeOfExtension left to vote -rule deadlineCanOnlyBeExtenededIfQuorumReached() { - env e; method f; calldataarg args; - uint256 id; - require(getExtendedDeadlineIsUnset(id)); - f(e, args); - assert(false); -} - -// RULE extendedDeadline is used iff quorum is reached w/ <= extensionTime left to vote - -// RULE extendedDeadlineField is set iff quroum is reached - -// RULE if the deadline/extendedDeadline has not been reached, you can still vote (base) \ No newline at end of file