From bf73fb40138c6af3927b108ec966c8dfa41dc257 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 28 Feb 2023 18:35:03 +0100 Subject: [PATCH] fix GovernorPreventLateQuorum.spec --- .../passes/verifyGovernorPreventLateQuorum.sh | 1 - certora/specs/GovernorPreventLateQuorum.spec | 52 +++++++++---------- 2 files changed, 24 insertions(+), 29 deletions(-) diff --git a/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh b/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh index 03cbe2ab7..ea45aab5a 100644 --- a/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/passes/verifyGovernorPreventLateQuorum.sh @@ -8,6 +8,5 @@ certoraRun \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ --loop_iter 1 \ - --send_only \ --rules deadlineNeverReduced againstVotesDontCount hasVotedCorrelationNonzero canExtendDeadlineOnce deadlineChangeEffects quorumReachedCantChange quorumLengthGt0 cantExtendWhenQuorumUnreached quorumNumerLTEDenom deprecatedQuorumStateIsUninitialized \ $@ diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index e4ccd85ac..5033bd17b 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,13 +44,12 @@ 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 lateQuorumVoteExtension() returns uint64 envfree - propose(address[], uint256[], bytes[], string) // harness getDeprecatedQuorumNumerator() returns uint256 envfree @@ -59,9 +58,6 @@ methods { getExtendedDeadlineIsUnset(uint256) returns bool envfree getExtendedDeadlineIsStarted(uint256) returns bool envfree getExtendedDeadline(uint256) returns uint64 envfree - getAgainstVotes(uint256) returns uint256 envfree - getAbstainVotes(uint256) returns uint256 envfree - getForVotes(uint256) returns uint256 envfree getPastTotalSupply(uint256) returns (uint256) envfree // more robust check than f.selector == _castVote(...).selector @@ -94,7 +90,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; -} +} //////////////////////////////////////////////////////////////////////////////// @@ -120,8 +116,8 @@ definition proposalNotCreated(env e, uint256 pId) returns bool = && 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 || @@ -146,18 +142,18 @@ definition castVoteSubset(method f) returns bool = 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); } } -/** +/** * 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); } @@ -211,8 +207,8 @@ invariant quorumReachedEffect(env e1, uint256 pId) * `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); @@ -241,7 +237,7 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered { uint256 forBefore = votesFor(); uint256 abstainBefore = votesAbstain(); - bool hasVotedBefore = hasVoted(e, pId, acc); + bool hasVotedBefore = hasVoted(pId, acc); helperFunctionsWithRevertOnlyCastVote(pId, f, e); // should be f(e, args) @@ -249,7 +245,7 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered { uint256 forAfter = votesFor(); uint256 abstainAfter = votesAbstain(); - bool hasVotedAfter = hasVoted(e, pId, acc); + bool hasVotedAfter = hasVoted(pId, acc); // want all vote categories to not decrease and at least one category to increase assert @@ -265,8 +261,8 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered { /** * 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; @@ -285,8 +281,8 @@ rule againstVotesDontCount(method f) filtered { /** * 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; @@ -307,9 +303,9 @@ rule deadlineNeverReduced(method f) filtered { /** * 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 + f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector } { env e; calldataarg args; uint256 pId; @@ -325,7 +321,7 @@ rule deadlineChangeEffects(method f) filtered { /** * @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 } { @@ -342,7 +338,7 @@ rule deadlineCantBeUnextended(method f) filtered { /** * 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 } { @@ -351,7 +347,7 @@ rule canExtendDeadlineOnce(method f) filtered { require(deadlineExtended(e1, pId)); require(proposalSnapshot(pId) > 0); requireInvariant quorumReachedEffect(e1, pId); - setup(e1, e2); + setup(e1, e2); uint256 deadlineBefore = proposalDeadline(pId); f(e2, args);