diff --git a/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch new file mode 100644 index 000000000..776a15394 --- /dev/null +++ b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch @@ -0,0 +1,14 @@ +--- governance/extensions/GovernorPreventLateQuorum.sol 2023-03-07 10:48:47.733488857 +0100 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2023-03-15 14:14:59.121060484 +0100 +@@ -84,6 +84,11 @@ + return _voteExtension; + } + ++ // FV ++ function _getExtendedDeadline(uint256 proposalId) internal view returns (uint64) { ++ return _extendedDeadlines[proposalId]; ++ } ++ + /** + * @dev Changes the {lateQuorumVoteExtension}. This operation can only be performed by the governance executor, + * generally through a governance proposal. diff --git a/certora/harnesses/GovernorPreventLateHarness.sol b/certora/harnesses/GovernorPreventLateHarness.sol new file mode 100644 index 000000000..048ceae3c --- /dev/null +++ b/certora/harnesses/GovernorPreventLateHarness.sol @@ -0,0 +1,176 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../patched/governance/Governor.sol"; +import "../patched/governance/extensions/GovernorCountingSimple.sol"; +import "../patched/governance/extensions/GovernorPreventLateQuorum.sol"; +import "../patched/governance/extensions/GovernorTimelockControl.sol"; +import "../patched/governance/extensions/GovernorVotes.sol"; +import "../patched/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract GovernorPreventLateHarness is + Governor, + GovernorCountingSimple, + GovernorPreventLateQuorum, + GovernorTimelockControl, + GovernorVotes, + GovernorVotesQuorumFraction +{ + constructor(IVotes _token, TimelockController _timelock, uint256 _quorumNumeratorValue, uint64 _initialVoteExtension) + Governor("Harness") + GovernorPreventLateQuorum(_initialVoteExtension) + GovernorTimelockControl(_timelock) + GovernorVotes(_token) + GovernorVotesQuorumFraction(_quorumNumeratorValue) + {} + + // Harness from Votes + function token_getPastTotalSupply(uint256 blockNumber) public view returns(uint256) { + return token.getPastTotalSupply(blockNumber); + } + + function token_getPastVotes(address account, uint256 blockNumber) public view returns(uint256) { + return token.getPastVotes(account, blockNumber); + } + + function token_clock() public view returns (uint48) { + return token.clock(); + } + + function token_CLOCK_MODE() public view returns (string memory) { + return token.CLOCK_MODE(); + } + + // Harness from Governor + function getExecutor() public view returns (address) { + return _executor(); + } + + function proposalProposer(uint256 proposalId) public view returns (address) { + return _proposalProposer(proposalId); + } + + function quorumReached(uint256 proposalId) public view returns (bool) { + return _quorumReached(proposalId); + } + + function voteSucceeded(uint256 proposalId) public view returns (bool) { + return _voteSucceeded(proposalId); + } + + function isExecuted(uint256 proposalId) public view returns (bool) { + return _isExecuted(proposalId); + } + + function isCanceled(uint256 proposalId) public view returns (bool) { + return _isCanceled(proposalId); + } + + function isQueued(uint256 proposalId) public view returns (bool) { + return _proposalQueueId(proposalId) != bytes32(0); + } + + function governanceCallLength() public view returns (uint256) { + return _governanceCallLength(); + } + + // Harness from GovernorPreventLateQuorum + function getExtendedDeadline(uint256 proposalId) public view returns (uint64) { + return _getExtendedDeadline(proposalId); + } + + // Harness from GovernorCountingSimple + function getAgainstVotes(uint256 proposalId) public view returns (uint256) { + (uint256 againstVotes,,) = proposalVotes(proposalId); + return againstVotes; + } + + function getForVotes(uint256 proposalId) public view returns (uint256) { + (,uint256 forVotes,) = proposalVotes(proposalId); + return forVotes; + } + + function getAbstainVotes(uint256 proposalId) public view returns (uint256) { + (,,uint256 abstainVotes) = proposalVotes(proposalId); + return abstainVotes; + } + + // The following functions are overrides required by Solidity added by OZ Wizard. + function votingDelay() public pure override returns (uint256) { + return 1; // 1 block + } + + function votingPeriod() public pure override returns (uint256) { + return 45818; // 1 week + } + + function quorum(uint256 blockNumber) + public + view + override(IGovernor, GovernorVotesQuorumFraction) + returns (uint256) + { + return super.quorum(blockNumber); + } + + function state(uint256 proposalId) public view override(Governor, GovernorTimelockControl) returns (ProposalState) { + return super.state(proposalId); + } + + function proposalDeadline(uint256 proposalId) public view override(IGovernor, Governor, GovernorPreventLateQuorum) returns (uint256) { + return super.proposalDeadline(proposalId); + } + + function propose( + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + string memory description + ) public override(Governor, IGovernor) returns (uint256) { + return super.propose(targets, values, calldatas, description); + } + + function _execute( + uint256 proposalId, + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + bytes32 descriptionHash + ) internal override(Governor, GovernorTimelockControl) { + super._execute(proposalId, targets, values, calldatas, descriptionHash); + } + + function _cancel( + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + bytes32 descriptionHash + ) internal override(Governor, GovernorTimelockControl) returns (uint256) { + return super._cancel(targets, values, calldatas, descriptionHash); + } + + function _castVote( + uint256 proposalId, + address account, + uint8 support, + string memory reason, + bytes memory params + ) internal override(Governor, GovernorPreventLateQuorum) returns (uint256) { + return super._castVote(proposalId, account, support, reason, params); + } + + function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) { + return super._executor(); + } + + function supportsInterface(bytes4 interfaceId) + public + view + virtual + override(Governor, GovernorTimelockControl) + returns (bool) + { + return super.supportsInterface(interfaceId); + } +} diff --git a/certora/specs.js b/certora/specs.js index 3ab802a14..e013e8891 100644 --- a/certora/specs.js +++ b/certora/specs.js @@ -66,4 +66,11 @@ module.exports = [ files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`], options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'], })), + // WIP prevent late quorum + ...product(['GovernorPreventLateQuorum'], ['ERC20VotesBlocknumberHarness']).map(([spec, token]) => ({ + spec, + contract: 'GovernorPreventLateHarness', + files: ['certora/harnesses/GovernorPreventLateHarness.sol', `certora/harnesses/${token}.sol`], + options: [`--link GovernorPreventLateHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'], + })), ]; diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec index 59fe8373a..ec7b610a7 100644 --- a/certora/specs/Governor.helpers.spec +++ b/certora/specs/Governor.helpers.spec @@ -57,7 +57,6 @@ definition skip(method f) returns bool = f.isView || f.isFallback || f.selector == relay(address,uint256,bytes).selector || - f.selector == 0xb9a61961 || // __acceptAdmin() f.selector == onERC721Received(address,address,uint256,bytes).selector || f.selector == onERC1155Received(address,address,uint256,uint256,bytes).selector || f.selector == onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector; diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec index a49206b56..436fc273d 100644 --- a/certora/specs/GovernorBaseRules.spec +++ b/certora/specs/GovernorBaseRules.spec @@ -55,14 +55,35 @@ rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldata │ (calling a view function), and we do not desire to check the signature verification. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule noDoubleVoting(uint256 pId, env e, uint8 sup) { - bool votedCheck = hasVoted(pId, e.msg.sender); +rule noDoubleVoting(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + address voter; + uint8 support; + + bool votedCheck = hasVoted(pId, voter); - castVote@withrevert(e, pId, sup); + helperVoteWithRevert(e, f, pId, voter, support); assert votedCheck => lastReverted, "double voting occurred"; } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Voting against a proposal does not count towards quorum. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule againstVotesDontCountTowardsQuorum(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + address voter; + uint8 support = 0; // Against + + helperVoteWithRevert(e, f, pId, voter, support); + + assert quorumReached(pId) == quorumBefore, "quorum must not be reached with an against vote"; +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: A proposal could be executed only if quorum was reached and vote succeeded │ @@ -90,7 +111,9 @@ rule noStartBeforeCreation(uint256 pId, env e, method f, calldataarg args) filtered { f -> !skip(f) } { require !proposalCreated(pId); + f(e, args); + assert proposalCreated(pId) => proposalSnapshot(pId) >= clock(e), "starts before proposal"; } @@ -103,10 +126,26 @@ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) filtered { f -> !skip(f) } { require !isExecuted(pId); + f(e, args); + assert isExecuted(pId) => proposalDeadline(pId) <= clock(e), "executed before deadline"; } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: The quorum numerator is always less than or equal to the quorum denominator │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant quorumRatioLessThanOne(env e, uint256 blockNumber) + quorumNumerator(e, blockNumber) <= quorumDenominator() + filtered { f -> !skip(f) } + { + preserved { + require clockSanity(e); + } + } + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: All proposal specific (non-view) functions should revert if proposal is executed │ diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec index 1247789fa..d66bd591b 100644 --- a/certora/specs/GovernorInvariants.spec +++ b/certora/specs/GovernorInvariants.spec @@ -35,6 +35,21 @@ invariant proposalStateConsistency(uint256 pId) } } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: votes recorded => proposal snapshot is in the past │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant votesImplySnapshotPassed(env e, uint256 pId) + getAgainstVotes(pId) == 0 => proposalSnapshot(pId) < clock(e) && + getForVotes(pId) == 0 => proposalSnapshot(pId) < clock(e) && + getAbstainVotes(pId) == 0 => proposalSnapshot(pId) < clock(e) + { + preserved { + require clockSanity(e); + } + } + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: cancel => created │ diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec new file mode 100644 index 000000000..d8df72f94 --- /dev/null +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -0,0 +1,68 @@ +import "helpers.spec" +import "methods/IGovernor.spec" +import "Governor.helpers.spec" +import "GovernorInvariants.spec" + +methods { + lateQuorumVoteExtension() returns uint64 envfree + getExtendedDeadline(uint256) returns uint64 envfree +} + +use invariant proposalStateConsistency +use invariant votesImplySnapshotPassed + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: │ +│ * Deadline can never be reduced │ +│ * If deadline increases then we are in `deadlineExtended` state and `castVote` was called. │ +│ * A proposal's deadline can't change in `deadlineExtended` state. │ +│ * A proposal's deadline can't be unextended. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !skip(f) } +{ + requireInvariant proposalStateConsistency(pId); + requireInvariant votesImplySnapshotPassed(pId); + + // This should be a direct consequence of the invariant: `getExtendedDeadline(pId) > 0 => quorumReached(pId)` + // But this is not (easily) provable because the prover think `_totalSupplyCheckpoints` can arbitrarily change, + // which causes the quorum() to change. Not sure how to fix that. + require !quorumReached(pId) => getExtendedDeadline(pId) == 0; + + uint256 deadlineBefore = proposalDeadline(pId); + bool deadlineExtendedBefore = getExtendedDeadline(pId) > 0; + bool quorumReachedBefore = quorumReached(pId); + + f(e, args); + + uint256 deadlineAfter = proposalDeadline(pId); + bool deadlineExtendedAfter = getExtendedDeadline(pId) > 0; + bool quorumReachedAfter = quorumReached(pId); + + // deadline can never be reduced + assert deadlineBefore <= proposalDeadline(pId); + + // deadline can only be extended in proposal or on cast vote + assert deadlineAfter != deadlineBefore => ( + ( + !deadlineExtendedBefore && + !deadlineExtendedAfter && + f.selector == propose(address[], uint256[], bytes[], string).selector + ) || ( + !deadlineExtendedBefore && + deadlineExtendedAfter && + !quorumReachedBefore && + quorumReachedAfter && + deadlineAfter == clock(e) + lateQuorumVoteExtension() && + votingAll(f) + ) + ); + + // a deadline can only be extended once + assert deadlineExtendedBefore => deadlineBefore == deadlineAfter; + + // a deadline cannot be un-extended + assert deadlineExtendedBefore => deadlineExtendedAfter; +} diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index 417b7b0c6..9488163cd 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -128,3 +128,23 @@ rule stateIsConsistentWithVotes(uint256 pId, env e) { ) ); } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: `updateQuorumNumerator` cannot cause quorumReached to change. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !skip(f) } +{ + require clockSanity(e); + + bool quorumReachedBefore = quorumReached(e, pId); + + f(e, args); + + assert quorumReached(e, pId) != quorumReachedBefore => ( + !quorumReachedBefore && + votingAll(f) + ); +}