diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 1403850fb..a960f6e40 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -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-12 19:13:19.000000000 -0700 ++++ governance/TimelockController.sol 2022-05-15 14:10:49.000000000 -0700 @@ -24,10 +24,10 @@ bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE"); bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); @@ -44,7 +44,7 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol ) private { - (bool success, ) = target.call{value: value}(data); - require(success, "TimelockController: underlying transaction reverted"); -+ return; // can't deal with external calls ++ return; // haven't dealt with external calls yet + // (bool success, ) = target.call{value: value}(data); + // require(success, "TimelockController: underlying transaction reverted"); @@ -401,12 +401,12 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/ } 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 ++++ utils/Address.sol 2022-05-16 14:24:44.000000000 -0700 @@ -131,6 +131,7 @@ uint256 value, string memory errorMessage ) internal returns (bytes memory) { -+ return ""; ++ 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/harnesses/GovernorPreventLateQuorumHarness.sol b/certora/harnesses/GovernorPreventLateQuorumHarness.sol index cd9133e59..773d2ef54 100644 --- a/certora/harnesses/GovernorPreventLateQuorumHarness.sol +++ b/certora/harnesses/GovernorPreventLateQuorumHarness.sol @@ -35,6 +35,10 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G return _extendedDeadlines[id].isUnset(); } + function getExtendedDeadlineIsStarted(uint256 id) public view returns(bool) { + return _extendedDeadlines[id].isStarted(); + } + function getExtendedDeadline(uint256 id) public view returns(uint64) { return _extendedDeadlines[id].getDeadline(); } @@ -49,15 +53,6 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G 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){ diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh index cbea7b40e..72b7fa651 100644 --- a/certora/scripts/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh @@ -1,12 +1,12 @@ certoraRun \ certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ - --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorCountingSimple.spec \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ --solc solc \ --optimistic_loop \ - --loop_iter 1 \ + --disable_auto_cache_key_gen \ --staging \ - --rule_sanity advanced \ --send_only \ + --loop_iter 1 \ --rule $1 \ --msg "$1" \ diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 3936e77c4..83c47dde1 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -70,7 +70,6 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { calldataarg args; f@withrevert(e, args); } - } /* diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index 3660e70b4..20b5d4ede 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -183,7 +183,8 @@ 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"; + // want all vote categories to not decrease and at least one category to increase + assert (!hasVotedBefore && hasVotedAfter) => (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), "no correlation: some category decreased"; } diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index 6ef3745c3..bcadf76da 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -1,22 +1,8 @@ -////////////////////////////////////////////////////////////////////////////// -///////////////////// Governor.sol base definitions ////////////////////////// -////////////////////////////////////////////////////////////////////////////// +import "GovernorCountingSimple.spec" using ERC721VotesHarness as erc721votes -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 - quorumNumerator() returns uint256 envfree quorumDenominator() returns uint256 envfree votingPeriod() returns uint256 envfree lateQuorumVoteExtension() returns uint64 envfree @@ -24,20 +10,12 @@ methods { // harness getExtendedDeadlineIsUnset(uint256) returns bool envfree + getExtendedDeadlineIsStarted(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 + + // more robust check than f.selector == _castVote(...).selector + latestCastVoteCall() returns uint256 envfree - // function summarization - proposalThreshold() returns uint256 envfree - - // erc20votes dispatch - getVotes(address, uint256) returns uint256 => DISPATCHER(true) - // erc721votes/Votes dispatch - getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true) - getPastVotes(address, uint256) returns uint256 => DISPATCHER(true) // timelock dispatch getMinDelay() returns uint256 => DISPATCHER(true) @@ -46,34 +24,72 @@ methods { scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT } + +////////////////////////////////////////////////////////////////////////////// +///////////////////////////// Helper Functions /////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env e) { + string reason; uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params; + 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 == 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); + } +} + + ////////////////////////////////////////////////////////////////////////////// //////////////////////////////// Definitions ///////////////////////////////// ////////////////////////////////////////////////////////////////////////////// -// where can invariants help? -// can I replace definitions with invariants? +// proposal deadline can be extended (but isn't) +definition deadlineExtendable(env e, uint256 pId) returns bool = + getExtendedDeadlineIsUnset(pId) + && !quorumReached(e, pId); -// create definition for extended -definition deadlineCanBeExtended(uint256 pId) returns bool = - getExtendedDeadlineIsUnset(pId) && - !quorumReached(pId); +// proposal deadline has been extended +definition deadlineExtended(env e, uint256 pId) returns bool = + getExtendedDeadlineIsStarted(pId) + && quorumReached(e, pId); -definition deadlineHasBeenExtended(uint256 pId) returns bool = - !getExtendedDeadlineIsUnset(pId) && - quorumReached(pId); -definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0; +////////////////////////////////////////////////////////////////////////////// +///////////////////////////////// Invariants ///////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +/* + * I1: A propsal must be in state deadlineExtendable or deadlineExtended. + * --INVARIANT PASSING // fails for updateQuorumNumerator + * --ADVANCED SANITY PASSING // can't sanity test failing rules, not sure how it works for invariants + */ +invariant proposalInOneState(env e, uint256 pId) + deadlineExtendable(e, pId) || deadlineExtended(e, pId) + { preserved { require proposalCreated(pId); } } + ////////////////////////////////////////////////////////////////////////////// ////////////////////////////////// Rules ///////////////////////////////////// ////////////////////////////////////////////////////////////////////////////// -// 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 - } { +///////////////////////////// first set of rules ///////////////////////////// + +// R1 and R2 are assumed in R3, so we prove them first +/* + * R1: If deadline increases then we are in deadlineExtended state and castVote was called. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule deadlineChangeEffects(method f) filtered {f -> !f.isView} { env e; calldataarg args; uint256 pId; require (proposalCreated(pId)); @@ -82,10 +98,15 @@ rule deadlineChangeEffects(method f) f(e, args); uint256 deadlineAfter = proposalDeadline(pId); - assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(pId)); + assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId)); } - // 2. cant unextend RULE PASSING*; ADV SANITY PASSING + +/* + * R2: A proposal can't leave deadlineExtended state. + * RULE PASSING* + * ADVANCED SANITY PASSING + */ rule deadlineCantBeUnextended(method f) filtered { f -> !f.isView @@ -93,23 +114,24 @@ rule deadlineCantBeUnextended(method f) } { env e; calldataarg args; uint256 pId; - require(deadlineHasBeenExtended(pId)); + require(deadlineExtended(e, pId)); require(proposalCreated(pId)); f(e, args); - assert(deadlineHasBeenExtended(pId)); + assert(deadlineExtended(e, pId)); } - // 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 - } { + +/* + * R3: A proposal's deadline can't change in deadlineExtended state. + * RULE PASSING* + * ADVANCED SANITY PASSING + */ +rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} { env e; calldataarg args; uint256 pId; - require(deadlineHasBeenExtended(pId)); + require(deadlineExtended(e, pId)); require(proposalCreated(pId)); uint256 deadlineBefore = proposalDeadline(pId); @@ -118,3 +140,145 @@ rule canExtendDeadlineOnce(method f) assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); } + + +//////////////////////////// second set of rules //////////////////////////// + +// HIGH LEVEL RULE R6: deadline can only extended if quorum reached w/ <= timeOfExtension left to vote +// I1, R4 and R5 are assumed in R6 so we prove them first + +/* + * R4: 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 PASSING + * ADVANCED SANITY PASSING + */ +rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isView} { + address acc = e.msg.sender; + + require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power + + uint256 againstBefore = votesAgainst(); + uint256 forBefore = votesFor(); + uint256 abstainBefore = votesAbstain(); + + bool hasVotedBefore = hasVoted(e, pId, acc); + + helperFunctionsWithRevertOnlyCastVote(pId, f, e); + + uint256 againstAfter = votesAgainst(); + uint256 forAfter = votesFor(); + uint256 abstainAfter = votesAbstain(); + + bool hasVotedAfter = hasVoted(e, pId, acc); + + // want all vote categories to not decrease and at least one category to increase + assert + (!hasVotedBefore && hasVotedAfter) => + (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), + "no correlation: some category decreased"; // currently vacous but keeping for CI tests + assert + (!hasVotedBefore && hasVotedAfter) => + (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter), + "no correlation: no category increased"; +} + + +/* + * R5: An against vote does not make a proposal reach quorum. + * RULE PASSING + * --ADVANCED SANITY PASSING vacuous but keeping + */ +rule againstVotesDontCount(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + address acc = e.msg.sender; + + bool quorumBefore = quorumReached(e, pId); + uint256 againstBefore = votesAgainst(); + + f(e, args); + + bool quorumAfter = quorumReached(e, pId); + uint256 againstAfter = votesAgainst(); + + assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum reached with against vote"; +} + +/* + * R6: Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + + // need invariant that proves that a propsal must be in state deadlineExtendable or deadlineExtended + require(deadlineExtended(e, pId) || deadlineExtendable(e, pId)); + require(proposalCreated(pId)); + + bool wasDeadlineExtendable = deadlineExtendable(e, pId); + uint64 extension = lateQuorumVoteExtension(); + uint256 deadlineBefore = proposalDeadline(pId); + f(e, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert(deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline was not extendable"); + assert(deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used"); +} + +/* + * R7: `extendedDeadlineField` is set iff `_castVote` is called and quroum is reached. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + require(deadlineExtended(e, pId) || deadlineExtendable(e, pId)); + + 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" + ); +} + +/* +* R8: If the deadline for a proposal has not been reached, users can still vote. +* --RULE PASSING +* --ADVANCED SANITY PASSING +*/ +rule canVote(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + address acc = e.msg.sender; + uint256 deadline = proposalDeadline(pId); + bool votedBefore = hasVoted(e, pId, acc); + + require(proposalCreated(pId)); + require(deadline >= e.block.number); + // last error? + helperFunctionsWithRevertOnlyCastVote(pId, f, e); + bool votedAfter = hasVoted(e, pId, acc); + + assert !votedBefore && votedAfter => deadline >= e.block.number; +} + +/* + * R9: Deadline can never be reduced. + * RULE PASSING + * ADVANCED SANITY PASSING + */ +rule deadlineNeverReduced(method f) filtered {f -> !f.isView} { + env e; calldataarg args; uint256 pId; + require(proposalCreated(pId)); + + uint256 deadlineBefore = proposalDeadline(pId); + f(e, args); + uint256 deadlineAfter = proposalDeadline(pId); + + assert(deadlineAfter >= deadlineBefore); +} +