add PreventLateQuorum specs

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.

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);
+    }
+}

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'],
+  })),
 ];

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;

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;
 
-    castVote@withrevert(e, pId, sup);
+    bool votedCheck = hasVoted(pId, voter);
+
+    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                              │

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                                                                                        │

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;
+}

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)
+    );
+}