From e04f7ded9400e9a9d1335c4fb6bbfbac94064fcf Mon Sep 17 00:00:00 2001 From: teryanarmen <61996358+teryanarmen@users.noreply.github.com> Date: Sun, 27 Nov 2022 15:41:50 -0800 Subject: [PATCH] Fixed GPLQ spec, all rules passing (#3822) Co-authored-by: Michael George Co-authored-by: Nick Armstrong Co-authored-by: Michael George Co-authored-by: Aleksander Kryukov Co-authored-by: Hadrien Croubois --- certora/scripts/passes/verifyAccessControl.sh | 1 - certora/scripts/passes/verifyERC1155.sh | 1 - .../scripts/passes/verifyERC1155Burnable.sh | 1 - .../scripts/passes/verifyERC1155Pausable.sh | 1 - certora/scripts/passes/verifyERC1155Supply.sh | 1 - .../scripts/passes/verifyERC20FlashMint.sh | 1 - certora/scripts/passes/verifyERC20Votes.sh | 1 - certora/scripts/passes/verifyERC20Wrapper.sh | 1 - certora/scripts/passes/verifyERC721Votes.sh | 1 - .../verifyGPLQ_deadlineCantBeUnextended.sh | 12 + .../passes/verifyGPLQ_proposalInOneState.sh | 13 + .../passes/verifyGPLQ_quorumReachedEffect.sh | 12 + certora/scripts/passes/verifyGovernor.sh | 1 - .../passes/verifyGovernorCountingSimple.sh | 1 - .../passes/verifyGovernorPreventLateQuorum.sh | 5 +- certora/scripts/passes/verifyInitializable.sh | 1 - certora/scripts/passes/verifyTimelock.sh | 1 - certora/specs/GovernorPreventLateQuorum.spec | 274 ++++++++---------- 18 files changed, 166 insertions(+), 163 deletions(-) create mode 100644 certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh create mode 100644 certora/scripts/passes/verifyGPLQ_proposalInOneState.sh create mode 100644 certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh diff --git a/certora/scripts/passes/verifyAccessControl.sh b/certora/scripts/passes/verifyAccessControl.sh index 6353cfa72..0702260aa 100644 --- a/certora/scripts/passes/verifyAccessControl.sh +++ b/certora/scripts/passes/verifyAccessControl.sh @@ -5,6 +5,5 @@ set -euxo pipefail certoraRun \ certora/harnesses/AccessControlHarness.sol \ --verify AccessControlHarness:certora/specs/AccessControl.spec \ - --solc solc \ --optimistic_loop \ $@ diff --git a/certora/scripts/passes/verifyERC1155.sh b/certora/scripts/passes/verifyERC1155.sh index 7564598ac..bb436ee2c 100644 --- a/certora/scripts/passes/verifyERC1155.sh +++ b/certora/scripts/passes/verifyERC1155.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC1155/ERC1155Harness.sol \ --verify ERC1155Harness:certora/specs/ERC1155.spec \ - --solc solc \ --optimistic_loop \ --loop_iter 3 \ $@ diff --git a/certora/scripts/passes/verifyERC1155Burnable.sh b/certora/scripts/passes/verifyERC1155Burnable.sh index e6556c3e5..bd0f59598 100644 --- a/certora/scripts/passes/verifyERC1155Burnable.sh +++ b/certora/scripts/passes/verifyERC1155Burnable.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ - --solc solc \ --optimistic_loop \ --loop_iter 3 \ $@ diff --git a/certora/scripts/passes/verifyERC1155Pausable.sh b/certora/scripts/passes/verifyERC1155Pausable.sh index 41f9ad763..beef12ee3 100644 --- a/certora/scripts/passes/verifyERC1155Pausable.sh +++ b/certora/scripts/passes/verifyERC1155Pausable.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ - --solc solc \ --optimistic_loop \ --loop_iter 3 \ $@ diff --git a/certora/scripts/passes/verifyERC1155Supply.sh b/certora/scripts/passes/verifyERC1155Supply.sh index c23c94313..2b88b130b 100644 --- a/certora/scripts/passes/verifyERC1155Supply.sh +++ b/certora/scripts/passes/verifyERC1155Supply.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ - --solc solc \ --optimistic_loop \ --loop_iter 3 \ $@ diff --git a/certora/scripts/passes/verifyERC20FlashMint.sh b/certora/scripts/passes/verifyERC20FlashMint.sh index ff7020733..9fd3e2547 100644 --- a/certora/scripts/passes/verifyERC20FlashMint.sh +++ b/certora/scripts/passes/verifyERC20FlashMint.sh @@ -6,6 +6,5 @@ certoraRun \ certora/harnesses/ERC20FlashMintHarness.sol \ certora/harnesses/IERC3156FlashBorrowerHarness.sol \ --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ - --solc solc \ --optimistic_loop \ $@ diff --git a/certora/scripts/passes/verifyERC20Votes.sh b/certora/scripts/passes/verifyERC20Votes.sh index 7d3980af7..1241eb374 100644 --- a/certora/scripts/passes/verifyERC20Votes.sh +++ b/certora/scripts/passes/verifyERC20Votes.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC20VotesHarness.sol \ --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ - --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ $@ \ No newline at end of file diff --git a/certora/scripts/passes/verifyERC20Wrapper.sh b/certora/scripts/passes/verifyERC20Wrapper.sh index 0a05c60ad..a6d704a3f 100644 --- a/certora/scripts/passes/verifyERC20Wrapper.sh +++ b/certora/scripts/passes/verifyERC20Wrapper.sh @@ -5,6 +5,5 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC20WrapperHarness.sol certora/harnesses/ERC20PermitHarness.sol \ --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ - --solc solc \ --optimistic_loop \ $@ diff --git a/certora/scripts/passes/verifyERC721Votes.sh b/certora/scripts/passes/verifyERC721Votes.sh index 6240cb1c3..06c94c285 100644 --- a/certora/scripts/passes/verifyERC721Votes.sh +++ b/certora/scripts/passes/verifyERC721Votes.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC721VotesHarness.sol certora/munged/utils/Checkpoints.sol \ --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ - --solc solc \ --optimistic_loop \ --disableLocalTypeChecking \ --settings -copyLoopUnroll=4 \ diff --git a/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh b/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh new file mode 100644 index 000000000..a28e75967 --- /dev/null +++ b/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +set -euxo pipefail + +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \ + --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --link GovernorFullHarness:token=ERC20VotesHarness \ + --optimistic_loop \ + --rule deadlineCantBeUnextended \ + --loop_iter 1 \ + $@ diff --git a/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh b/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh new file mode 100644 index 000000000..94754778e --- /dev/null +++ b/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +set -euxo pipefail + +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \ + --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --link GovernorFullHarness:token=ERC20VotesHarness \ + --optimistic_loop \ + --rule proposalInOneState \ + --settings -t=1000 \ + --loop_iter 1 \ + $@ diff --git a/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh b/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh new file mode 100644 index 000000000..2cbebae8f --- /dev/null +++ b/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +set -euxo pipefail + +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \ + --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --link GovernorFullHarness:token=ERC20VotesHarness \ + --optimistic_loop \ + --rule quorumReachedEffect \ + --loop_iter 1 \ + $@ diff --git a/certora/scripts/passes/verifyGovernor.sh b/certora/scripts/passes/verifyGovernor.sh index 3e061745d..02d2b3118 100644 --- a/certora/scripts/passes/verifyGovernor.sh +++ b/certora/scripts/passes/verifyGovernor.sh @@ -10,7 +10,6 @@ certoraRun \ certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ --verify GovernorHarness:certora/specs/GovernorBase.spec \ --link GovernorHarness:token=ERC20VotesHarness \ - --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ $@ \ No newline at end of file diff --git a/certora/scripts/passes/verifyGovernorCountingSimple.sh b/certora/scripts/passes/verifyGovernorCountingSimple.sh index 1112d749c..b774d5fc5 100644 --- a/certora/scripts/passes/verifyGovernorCountingSimple.sh +++ b/certora/scripts/passes/verifyGovernorCountingSimple.sh @@ -7,7 +7,6 @@ certoraRun \ certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ --verify GovernorHarness:certora/specs/GovernorCountingSimple.spec \ --link GovernorHarness:token=ERC20VotesHarness \ - --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ $@ diff --git a/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh b/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh index 35ff726c3..03cbe2ab7 100644 --- a/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh @@ -3,10 +3,11 @@ set -euxo pipefail certoraRun \ - certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ --loop_iter 1 \ - --rule_sanity \ + --send_only \ + --rules deadlineNeverReduced againstVotesDontCount hasVotedCorrelationNonzero canExtendDeadlineOnce deadlineChangeEffects quorumReachedCantChange quorumLengthGt0 cantExtendWhenQuorumUnreached quorumNumerLTEDenom deprecatedQuorumStateIsUninitialized \ $@ diff --git a/certora/scripts/passes/verifyInitializable.sh b/certora/scripts/passes/verifyInitializable.sh index 2e069d984..422f826f4 100644 --- a/certora/scripts/passes/verifyInitializable.sh +++ b/certora/scripts/passes/verifyInitializable.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/InitializableComplexHarness.sol \ --verify InitializableComplexHarness:certora/specs/Initializable.spec \ - --solc solc \ --optimistic_loop \ --loop_iter 3 \ $@ diff --git a/certora/scripts/passes/verifyTimelock.sh b/certora/scripts/passes/verifyTimelock.sh index c515ec9b6..1d11dbcfd 100644 --- a/certora/scripts/passes/verifyTimelock.sh +++ b/certora/scripts/passes/verifyTimelock.sh @@ -5,7 +5,6 @@ set -euxo pipefail certoraRun \ certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \ --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ - --solc solc \ --optimistic_loop \ --loop_iter 3 \ --settings -byteMapHashingPrecision=32 \ diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index 9e1d45dd9..e4ccd85ac 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -10,9 +10,9 @@ feature of giving voters more time to vote in the case that a proposal reaches quorum with less than `voteExtension` amount of time left to vote. ### Assumptions and Simplifications - + None - + #### Harnessing - The contract that the specification was verified against is `GovernorPreventLateQuorumHarness`, which inherits from all of the Governor @@ -25,7 +25,7 @@ None version. This flag stores the `block.number` in a variable `latestCastVoteCall` and is used as a way to check when any of variations of `castVote` are called. - + #### Munging - Various variables' visibility was changed from private to internal or from @@ -44,8 +44,8 @@ methods { // summarized hashProposal(address[],uint256[],bytes[],bytes32) returns (uint256) => NONDET _hashTypedDataV4(bytes32) returns (bytes32) - - // envfree + + // envfree quorumNumerator(uint256) returns uint256 quorumDenominator() returns uint256 envfree votingPeriod() returns uint256 envfree @@ -94,7 +94,7 @@ function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env function setup(env e1, env e2) { require getQuorumNumeratorLength() + 1 < max_uint; require e2.block.number >= e1.block.number; -} +} //////////////////////////////////////////////////////////////////////////////// @@ -119,55 +119,45 @@ definition proposalNotCreated(env e, uint256 pId) returns bool = && getAbstainVotes(pId) == 0 && getForVotes(pId) == 0; - /// Method f is a version of `castVote` whose state changing effects are covered by `castVoteBySig`. -/// @dev castVoteBySig allows anyone to cast a vote for anyone else if they can supply the signature. Specifically, -/// it covers the case where the msg.sender supplies a signature for themselves which is normally done using the normal +/// @dev castVoteBySig allows anyone to cast a vote for anyone else if they can supply the signature. Specifically, +/// it covers the case where the msg.sender supplies a signature for themselves which is normally done using the normal /// `castVote`. definition castVoteSubset(method f) returns bool = f.selector == castVote(uint256, uint8).selector || f.selector == castVoteWithReason(uint256, uint8, string).selector || f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector || f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector; + + //////////////////////////////////////////////////////////////////////////////// //// ### Properties // //////////////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////// // Invariants // //////////////////////////////////////////////////////////////////////////////// /** - * If a proposal has reached quorum then the proposal snapshot (start `block.number`) must be non-zero + * A created proposal must be in state `deadlineExtendable` or `deadlineExtended`. + * @dev We assume the total supply of the voting token is non-zero */ -invariant quorumReachedEffect(env e1, uint256 pId) - quorumReached(e1, pId) && getPastTotalSupply(0) > 0 => proposalCreated(pId) // bug: 0 supply 0 votes => quorumReached - // relay havocs external contracts, changing pastTotalSupply and thus quorumReached +invariant proposalInOneState(env e1, uint256 pId) + getPastTotalSupply(0) > 0 => (proposalNotCreated(e1, pId) || deadlineExtendable(e1, pId) || deadlineExtended(e1, pId)) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } - { + { preserved with (env e2) { setup(e1, e2); } } -/** - * A created proposal must be in state `deadlineExtendable` or `deadlineExtended`. - */ -invariant proposalInOneState(env e1, uint256 pId) - getPastTotalSupply(0) > 0 => (proposalNotCreated(e1, pId) || deadlineExtendable(e1, pId) || deadlineExtended(e1, pId)) - filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } - { - preserved with (env e2) { - require proposalCreated(pId); - setup(e1, e2); - } - } -/** +/** * The quorum numerator is always less than or equal to the quorum denominator. */ invariant quorumNumerLTEDenom(env e1, uint256 blockNumber) quorumNumerator(e1, blockNumber) <= quorumDenominator() - { + { preserved with (env e2) { setup(e1, e2); } @@ -179,6 +169,40 @@ invariant quorumNumerLTEDenom(env e1, uint256 blockNumber) invariant deprecatedQuorumStateIsUninitialized() getDeprecatedQuorumNumerator() == 0 +/** + * If a proposal's deadline has been extended, then the proposal must have been created and reached quorum. + */ +invariant cantExtendWhenQuorumUnreached(env e2, uint256 pId) + getExtendedDeadlineIsStarted(pId) => quorumReached(e2, pId) && proposalCreated(pId) + filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } + { preserved with (env e1) { + require e1.block.number > proposalSnapshot(pId); + setup(e1, e2); + }} + +/** + * The snapshot arrat keeping tracking of quorum numerators must never be uninitialized. + */ +invariant quorumLengthGt0(env e) + getQuorumNumeratorLength() > 0 + filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } + { preserved { + setup(e,e); + }} + +/** + * If a proposal has reached quorum then the proposal snapshot (start `block.number`) must be non-zero + */ +invariant quorumReachedEffect(env e1, uint256 pId) + quorumReached(e1, pId) && getPastTotalSupply(0) > 0 => proposalCreated(pId) + filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } + { + preserved with (env e2) { + setup(e1, e2); + } + } + + ////////////////////////////////////////////////////////////////////////////// // Rules // ////////////////////////////////////////////////////////////////////////////// @@ -187,7 +211,9 @@ invariant deprecatedQuorumStateIsUninitialized() * `updateQuorumNumerator` can only change quorum requirements for future proposals. * @dev In the case that the array containing past quorum numerators overflows, this rule will fail. */ -rule quorumReachedCantChange(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { +rule quorumReachedCantChange(method f) filtered { + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector + } { env e1; uint256 pId; bool _quorumReached = quorumReached(e1, pId); @@ -201,75 +227,12 @@ rule quorumReachedCantChange(method f) filtered { f -> !f.isFallback && !f.isVie assert _quorumReached == quorumReached_, "function changed quorumReached"; } -///////////////////////////// #### first set of rules //////////////////////// - -//// The rules [`deadlineChangeEffects`](#deadlineChangeEffects) and [`deadlineCantBeUnextended`](#deadlineCantBeUnextended) -//// are assumed in rule [`canExtendDeadlineOnce`](#canExtendDeadlineOnce), so we prove them first. - /** - * If deadline increases then we are in `deadlineExtended` state and `castVote` - * was called. + * Casting a vote must not decrease any category's total number of votes and increase at least one category's. */ -rule deadlineChangeEffects(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { - env e; calldataarg args; uint256 pId; - - requireInvariant quorumReachedEffect(e, pId); - - uint256 deadlineBefore = proposalDeadline(pId); - f(e, args); - uint256 deadlineAfter = proposalDeadline(pId); - - assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId)); -} - - -/** - * @title Deadline can't be unextended - * @notice A proposal can't leave `deadlineExtended` state. - */ -rule deadlineCantBeUnextended(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { - env e1; env e2; env e3; env e4; calldataarg args; uint256 pId; - setup(e1, e2); - - require(deadlineExtended(e1, pId)); - requireInvariant quorumReachedEffect(e1, pId); - - f(e2, args); - - assert(deadlineExtended(e1, pId)); -} - - -/** - * A proposal's deadline can't change in `deadlineExtended` state. - */ -rule canExtendDeadlineOnce(method f) filtered {f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector} { - env e1; env e2; calldataarg args; uint256 pId; - - require(deadlineExtended(e1, pId)); - require(proposalSnapshot(pId) > 0); - requireInvariant quorumReachedEffect(e1, pId); - setup(e1, e2); - - uint256 deadlineBefore = proposalDeadline(pId); - f(e2, args); - uint256 deadlineAfter = proposalDeadline(pId); - - assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); -} - - -/////////////////////// #### second set of rules //////////////////////////// - -//// The main rule in this section is [the deadline can only be extended if quorum reached with <= `timeOfExtension` left to vote](#deadlineExtnededIfQuorumReached) -//// The other rules of this section are assumed in the proof, so we prove them -//// first. - -/** - * A change in `hasVoted` must be correlated with an increasing of the vote - * supports, i.e. casting a vote increases the total number of votes. - */ -rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector} { +rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered { + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector + } { address acc = e.msg.sender; require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power @@ -292,7 +255,7 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f. assert (!hasVotedBefore && hasVotedAfter) => (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), - "after a vote is cast, the number of votes for each category must not decrease"; // currently vacous but keeping for CI tests + "after a vote is cast, the number of votes for each category must not decrease"; assert (!hasVotedBefore && hasVotedAfter) => (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter), @@ -300,10 +263,11 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f. } /** - * @title Against votes don't count - * @notice An against vote does not make a proposal reach quorum. + * Voting against a proposal does not count towards quorum. */ -rule againstVotesDontCount(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { +rule againstVotesDontCount(method f) filtered { + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector + } { env e; calldataarg args; uint256 pId; address acc = e.msg.sender; @@ -318,57 +282,12 @@ rule againstVotesDontCount(method f) filtered { f -> !f.isFallback && !f.isView assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum must not be reached with an against vote"; } -/** - * Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote - */ - // not reasonable rule since tool can arbitrarily pick a pre-state where quorum is reached -// rule deadlineExtendedIfQuorumReached(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { -// env e; calldataarg args; uint256 pId; - -// requireInvariant proposalInOneState(e, pId); -// requireInvariant quorumReachedEffect(e, pId); -// require proposalCreated(pId); -// require getPastTotalSupply(proposalSnapshot(pId)) >= 100; -// require quorumNumerator(e, proposalSnapshot(pId)) > 0; - -// bool wasDeadlineExtendable = deadlineExtendable(e, pId); -// uint64 extension = lateQuorumVoteExtension(); -// uint256 deadlineBefore = proposalDeadline(pId); -// f(e, args); -// uint256 deadlineAfter = proposalDeadline(pId); - -// assert deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline must have been extendable for the deadline to be extended"; -// assert deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used"; -// } - -/** - * `extendedDeadlineField` is set if and only if `_castVote` is called and quorum is reached. - */ - // tool picks a state where quorum is unreached but extendedDeadline is set and then casts a vote which causes quorum - // to be reached, so the rule breaks. Need to write a rule that says that if quorum is unreached, then extendedDeadline - // must be unset. -// rule extendedDeadlineValueSetIfQuorumReached(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { -// env e; calldataarg args; uint256 pId; -// setup(e, e); -// requireInvariant proposalInOneState(e, pId); -// require lateQuorumVoteExtension() + e.block.number < max_uint64; - -// bool extendedBefore = deadlineExtended(e, pId); -// f(e, args); -// bool extendedAfter = deadlineExtended(e, pId); -// uint256 extDeadline = getExtendedDeadline(pId); - -// assert( -// !extendedBefore && extendedAfter -// => extDeadline == e.block.number + lateQuorumVoteExtension(), -// "extended deadline was not set" -// ); -// } - /** * Deadline can never be reduced. */ -rule deadlineNeverReduced(method f) filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { +rule deadlineNeverReduced(method f) filtered { + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector + } { env e1; env e2; calldataarg args; uint256 pId; requireInvariant quorumReachedEffect(e1, pId); @@ -381,3 +300,62 @@ rule deadlineNeverReduced(method f) filtered { f -> !f.isFallback && !f.isView & assert(deadlineAfter >= deadlineBefore); } + +//// The rules [`deadlineChangeEffects`](#deadlineChangeEffects) and [`deadlineCantBeUnextended`](#deadlineCantBeUnextended) +//// are assumed in rule [`canExtendDeadlineOnce`](#canExtendDeadlineOnce), so we prove them first. + +/** + * If deadline increases then we are in `deadlineExtended` state and `castVote` + * was called. + */ +rule deadlineChangeEffects(method f) filtered { + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector + } { + env e; calldataarg args; uint256 pId; + + requireInvariant quorumReachedEffect(e, pId); + + uint256 deadlineBefore = proposalDeadline(pId); + f(e, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId)); +} + +/** + * @title Deadline can't be unextended + * @notice A proposal can't leave `deadlineExtended` state. + */ +rule deadlineCantBeUnextended(method f) filtered { + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector + } { + env e1; env e2; env e3; env e4; calldataarg args; uint256 pId; + setup(e1, e2); + + require(deadlineExtended(e1, pId)); + requireInvariant quorumReachedEffect(e1, pId); + + f(e2, args); + + assert(deadlineExtended(e1, pId)); +} + +/** + * A proposal's deadline can't change in `deadlineExtended` state. + */ +rule canExtendDeadlineOnce(method f) filtered { + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector + } { + env e1; env e2; calldataarg args; uint256 pId; + + require(deadlineExtended(e1, pId)); + require(proposalSnapshot(pId) > 0); + requireInvariant quorumReachedEffect(e1, pId); + setup(e1, e2); + + uint256 deadlineBefore = proposalDeadline(pId); + f(e2, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); +} \ No newline at end of file