starting to work on governor specifications

certora/diff/governance_Governor.sol.patch

@@ -0,0 +1,19 @@
+--- governance/Governor.sol	2023-03-07 10:48:47.730155491 +0100
++++ governance/Governor.sol	2023-03-10 10:13:31.926616811 +0100
+@@ -216,6 +216,16 @@
+         return _proposals[proposalId].proposer;
+     }
+ 
++    // FV
++    function _isExecuted(uint256 proposalId) internal view returns (bool) {
++        return _proposals[proposalId].executed;
++    }
++
++    // FV
++    function _isCanceled(uint256 proposalId) internal view returns (bool) {
++        return _proposals[proposalId].canceled;
++    }
++
+     /**
+      * @dev Amount of votes already cast passes the threshold limit.
+      */

certora/harnesses/AccessControlHarness.sol

@@ -1,5 +1,4 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.0;
 
 import "../patched/access/AccessControl.sol";

certora/harnesses/ERC20FlashMintHarness.sol

@@ -1,5 +1,4 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.0;
 
 import "../patched/token/ERC20/ERC20.sol";

certora/harnesses/ERC20PermitHarness.sol

@@ -1,5 +1,4 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.0;
 
 import "../patched/token/ERC20/extensions/ERC20Permit.sol";

certora/harnesses/ERC20VotesHarness.sol

@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/extensions/ERC20Votes.sol";
+
+contract ERC20VotesHarness is ERC20Votes {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
+
+    function mint(address account, uint256 amount) external {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) external {
+        _burn(account, amount);
+    }
+
+    // inspection
+    function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
+        return checkpoints(account, pos).fromBlock;
+    }
+
+    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
+        return checkpoints(account, pos).votes;
+    }
+
+    function maxSupply() public view returns (uint224) {
+        return _maxSupply();
+    }
+}

certora/harnesses/ERC20WrapperHarness.sol

@@ -1,5 +1,4 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.0;
 
 import "../patched/token/ERC20/extensions/ERC20Wrapper.sol";

certora/harnesses/ERC3156FlashBorrowerHarness.sol

@@ -1,9 +1,8 @@
 // SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
 
 import "../patched/interfaces/IERC3156FlashBorrower.sol";
 
-pragma solidity ^0.8.0;
-
 contract ERC3156FlashBorrowerHarness is IERC3156FlashBorrower {
     bytes32 somethingToReturn;
 

certora/harnesses/GovernorHarness.sol

@@ -0,0 +1,160 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../patched/governance/Governor.sol";
+import "../patched/governance/extensions/GovernorCountingSimple.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 GovernorHarness is
+    Governor,
+    GovernorCountingSimple,
+    GovernorTimelockControl,
+    GovernorVotes,
+    GovernorVotesQuorumFraction
+{
+    constructor(IVotes _token, TimelockController _timelock, uint256 _quorumNumeratorValue)
+        Governor("Harness")
+        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);
+    }
+
+    // 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 Certora.
+    // mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+    //
+    // function _castVote(
+    //     uint256 proposalId,
+    //     address account,
+    //     uint8 support,
+    //     string memory reason,
+    //     bytes memory params
+    // ) internal virtual override returns (uint256) {
+    //     uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params);
+    //     ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+    //     return deltaWeight;
+    // }
+
+    // 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 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 _executor() internal view override(Governor, GovernorTimelockControl) returns (address) {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/harnesses/Ownable2StepHarness.sol

@@ -1,5 +1,4 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.0;
 
 import "../patched/access/Ownable2Step.sol";

certora/harnesses/OwnableHarness.sol

@@ -1,5 +1,4 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.0;
 
 import "../patched/access/Ownable.sol";

certora/run.js

@@ -8,26 +8,27 @@
 
 const MAX_PARALLEL = 4;
 
-let specs = require(__dirname + '/specs.json');
-
 const proc = require('child_process');
 const { PassThrough } = require('stream');
 const events = require('events');
 const limit = require('p-limit')(MAX_PARALLEL);
 
+const strToRegex = str => new RegExp(`^${str.replace(/[.+?^${}()|[\]\\]/g, '\\$&').replace(/[*]/g, '.$&')}$`);
+
 let [, , request = '', ...extraOptions] = process.argv;
 if (request.startsWith('-')) {
   extraOptions.unshift(request);
   request = '';
 }
+const [reqSpec, reqContract] = request.split(':').reverse();
 
-if (request) {
-  const [reqSpec, reqContract] = request.split(':').reverse();
-  specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract));
-  if (specs.length === 0) {
-    console.error(`Error: Requested spec '${request}' not found in specs.json`);
-    process.exit(1);
-  }
+const specs = require(__dirname + '/specs.js')
+  .filter(entry => !reqSpec || strToRegex(reqSpec).test(entry.spec))
+  .filter(entry => !reqContract || strToRegex(reqContract).test(entry.contract));
+
+if (specs.length === 0) {
+  console.error(`Error: Requested spec '${request}' not found in specs.json`);
+  process.exit(1);
 }
 
 for (const { spec, contract, files, options = [] } of Object.values(specs)) {

certora/specs.json → certora/specs.js

@@ -1,4 +1,7 @@
-[
+/// This helper will be handy when we want to do cross product. Ex: all governor specs on all variations of the clock mode.
+const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat())));
+
+module.exports = [
   {
     "spec": "AccessControl",
     "contract": "AccessControlHarness",
@@ -45,5 +48,18 @@
     "spec": "Initializable",
     "contract": "InitializableHarness",
     "files": ["certora/harnesses/InitializableHarness.sol"]
-  }
-]
+  },
+  ...[ "GovernorBase", "GovernorInvariants", "GovernorStates", "GovernorFunctions" ].map(spec => ({
+    spec,
+    "contract": "GovernorHarness",
+    "files": [
+      "certora/harnesses/GovernorHarness.sol",
+      "certora/harnesses/ERC20VotesHarness.sol"
+    ],
+    "options": [
+      "--link GovernorHarness:token=ERC20VotesHarness",
+      "--optimistic_loop",
+      "--optimistic_hashing"
+    ]
+  }))
+];

certora/specs/Governor.helpers.spec

@@ -0,0 +1,124 @@
+import "methods/IGovernor.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ States                                                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition UNSET()      returns uint8 = 255;
+definition PENDING()    returns uint8 = 0;
+definition ACTIVE()     returns uint8 = 1;
+definition CANCELED()   returns uint8 = 2;
+definition DEFEATED()   returns uint8 = 3;
+definition SUCCEEDED()  returns uint8 = 4;
+definition QUEUED()     returns uint8 = 5;
+definition EXPIRED()    returns uint8 = 6;
+definition EXECUTED()   returns uint8 = 7;
+
+function safeState(env e, uint256 pId) returns uint8 {
+    uint8 result = state@withrevert(e, pId);
+    return lastReverted ? UNSET() : result;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Filters                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+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;
+
+definition voting(method f) returns bool =
+    f.selector == castVote(uint256,uint8).selector ||
+    f.selector == castVoteWithReason(uint256,uint8,string).selector ||
+    f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helper functions                                                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 support) returns uint256 {
+    string reason; bytes params; uint8 v; bytes32 s; bytes32 r;
+
+    if (f.selector == castVote(uint256,uint8).selector)
+    {
+        require e.msg.sender == voter;
+        return castVote@withrevert(e, pId, support);
+    }
+    else  if (f.selector == castVoteWithReason(uint256,uint8,string).selector)
+    {
+        require e.msg.sender == voter;
+        return castVoteWithReason@withrevert(e, pId, support, reason);
+    }
+    else  if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector)
+    {
+        require e.msg.sender == voter;
+        return castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params);
+    }
+    else
+    {
+        calldataarg args;
+        f@withrevert(e, args);
+        return 0;
+    }
+}
+
+function helperFunctionsWithRevert(env e, method f, uint256 pId) {
+    if (f.selector == propose(address[], uint256[], bytes[], string).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; string description;
+        require pId == propose@withrevert(e, targets, values, calldatas, description);
+    }
+    else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 description;
+        require pId == queue@withrevert(e, targets, values, calldatas, description);
+    }
+    else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 description;
+        require pId == execute@withrevert(e, targets, values, calldatas, description);
+    }
+    else if (f.selector == cancel(address[], uint256[], bytes[], bytes32).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 description;
+        require pId == cancel@withrevert(e, targets, values, calldatas, description);
+    }
+    else if (f.selector == castVote(uint256, uint8).selector)
+    {
+        uint8 support;
+        castVote@withrevert(e, pId, support);
+    }
+    else if  (f.selector == castVoteWithReason(uint256, uint8, string).selector)
+    {
+        uint8 support; string reason;
+        castVoteWithReason@withrevert(e, pId, support, reason);
+    }
+    else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector)
+    {
+        uint8 support; string reason; bytes params;
+        castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params);
+    }
+    else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector)
+    {
+        uint8 support; uint8 v; bytes32 r; bytes32 s;
+        castVoteBySig@withrevert(e, pId, support, v, r, s);
+    }
+    else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector)
+    {
+        uint8 support; string reason; bytes params; uint8 v; bytes32 r; bytes32 s;
+        castVoteWithReasonAndParamsBySig@withrevert(e, pId, support, reason, params, v, r, s);
+    }
+    else
+    {
+        calldataarg args;
+        f@withrevert(e, args);
+    }
+}

certora/specs/GovernorBase.spec

@@ -0,0 +1,250 @@
+import "methods/IGovernor.spec"
+import "Governor.helpers.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+definition proposalCreated(uint256 pId) returns bool =
+    proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Votes start and end are either initialized (non zero) or uninitialized (zero) simultaneously             │
+│                                                                                                                     │
+│ This invariant assumes that the block number cannot be 0 at any stage of the contract cycle                         │
+│ This is very safe assumption as usually the 0 block is genesis block which is uploaded with data                    │
+│ by the developers and will not be valid to raise proposals (at the current way that block chain is functioning)     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant proposalStateConsistency(uint256 pId)
+    (proposalProposer(pId) != 0 <=> proposalSnapshot(pId) != 0) && (proposalProposer(pId) != 0 <=> proposalDeadline(pId) != 0)
+    {
+        preserved with (env e) {
+            require clock(e) > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: cancel => created                                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant canceledImplyCreated(uint pId)
+    isCanceled(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            requireInvariant proposalStateConsistency(pId);
+            require clock(e) > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: executed => created                                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant executedImplyCreated(uint pId)
+    isExecuted(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            requireInvariant proposalStateConsistency(pId);
+            require clock(e) > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Votes start before it ends                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant voteStartBeforeVoteEnd(uint256 pId)
+    proposalSnapshot(pId) <= proposalDeadline(pId)
+    {
+        preserved {
+            requireInvariant proposalStateConsistency(pId);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A proposal cannot be both executed and canceled simultaneously                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant noBothExecutedAndCanceled(uint256 pId)
+    !isExecuted(pId) || !isCanceled(pId)
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: No double proposition                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDoublePropose(uint256 pId, env e) {
+    require proposalCreated(pId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string reason;
+    uint256 result = propose(e, targets, values, calldatas, reason);
+
+    assert result != pId, "double proposal";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg) {
+    require proposalCreated(pId);
+
+    uint256 voteStart = proposalSnapshot(pId);
+    uint256 voteEnd = proposalDeadline(pId);
+    address proposer = proposalProposer(pId);
+
+    f(e, arg);
+
+    assert voteStart == proposalSnapshot(pId), "Start date was changed";
+    assert voteEnd == proposalDeadline(pId), "End date was changed";
+    assert proposer == proposalProposer(pId), "Proposer was changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A user cannot vote twice                                                                                      │
+│                                                                                                                     │
+│ Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is      │
+│ counted on the fact that the 3 functions themselves makes no changes, but rather call an internal function to       │
+│ execute. That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it   │
+│ is quite trivial to understand why this is ok. For castVoteBySig we basically assume that the signature referendum  │
+│ is correct without checking it. We could check each function separately and pass the rule, but that would have      │
+│ uglyfied the code with no concrete benefit, as it is evident that nothing is happening in the first 2 functions     │
+│ (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);
+
+    castVote@withrevert(e, pId, sup);
+
+    assert votedCheck => lastReverted, "double voting occurred";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A proposal could be executed only if quorum was reached and vote succeeded                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, calldataarg args) {
+    require !isExecuted(pId);
+
+    bool quorumReachedBefore = quorumReached(pId);
+    bool voteSucceededBefore = voteSucceeded(pId);
+
+    f(e, args);
+
+    assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Voting cannot start at a block number prior to proposal’s creation block number                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noStartBeforeCreation(uint256 pId, env e, method f, calldataarg args){
+    require !proposalCreated(pId);
+    f(e, args);
+    assert proposalCreated(pId) => proposalSnapshot(pId) >= clock(e), "starts before proposal";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A proposal cannot be executed before it ends                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) {
+    require !isExecuted(pId);
+    f(e, args);
+    assert isExecuted(pId) => proposalDeadline(pId) <= clock(e), "executed before deadline";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: All proposal specific (non-view) functions should revert if proposal is executed                              │
+│                                                                                                                     │
+│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, non of the       │
+│ proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc we connected the executed       │
+│ attribute to the execute() function, showing that only execute() can change it, and that it will always change it.  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args) filtered {
+    f -> !f.isView && !f.isFallback
+    && f.selector != updateTimelock(address).selector
+    && f.selector != updateQuorumNumerator(uint256).selector
+    && 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
+} {
+    require isExecuted(pId);
+    requireInvariant noBothExecutedAndCanceled(pId);
+    requireInvariant executedImplyCreated(pId);
+
+    helperFunctionsWithRevert(pId, f, e);
+
+    assert lastReverted, "Function was not reverted";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: All proposal specific (non-view) functions should revert if proposal is canceled                              │
+│                                                                                                                     │
+│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, non of the       │
+│ proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc we connected the executed       │
+│ attribute to the execute() function, showing that only execute() can change it, and that it will always change it.  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args) filtered {
+    f -> !f.isView && !f.isFallback
+    && f.selector != updateTimelock(address).selector
+    && f.selector != updateQuorumNumerator(uint256).selector
+    && 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
+} {
+    require isCanceled(pId);
+    requireInvariant noBothExecutedAndCanceled(pId);
+    requireInvariant canceledImplyCreated(pId);
+
+    helperFunctionsWithRevert(pId, f, e);
+
+    assert lastReverted, "Function was not reverted";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Proposal can be switched state only by specific functions                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateOnlyAfterFunc(uint256 pId, env e, method f) {
+    bool createdBefore = proposalCreated(pId);
+    bool executedBefore = isExecuted(pId);
+    bool canceledBefore = isCanceled(pId);
+
+    helperFunctionsWithRevert(pId, f, e);
+
+    assert (proposalCreated(pId) != createdBefore)
+        => (createdBefore == false && f.selector == propose(address[], uint256[], bytes[], string).selector),
+        "proposalCreated only changes in the propose method";
+
+    assert (isExecuted(pId) != executedBefore)
+        => (executedBefore == false && f.selector == execute(address[], uint256[], bytes[], bytes32).selector),
+        "isExecuted only changes in the execute method";
+
+    assert (isCanceled(pId) != canceledBefore)
+        => (canceledBefore == false && f.selector == cancel(address[], uint256[], bytes[], bytes32).selector),
+        "isCanceled only changes in the cancel method";
+}

certora/specs/GovernorFunctions.spec

@@ -0,0 +1,97 @@
+import "helpers.spec"
+import "methods/IGovernor.spec"
+import "Governor.helpers.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: propose effect and liveness. Includes "no double proposition"                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule propose(uint256 pId, env e) {
+    require nonpayable(e);
+
+    uint256 otherId;
+
+    uint8   stateBefore      = state(e, pId);
+    uint8   otherStateBefore = state(e, otherId);
+    uint256 otherVoteStart   = proposalSnapshot(otherId);
+    uint256 otherVoteEnd     = proposalDeadline(otherId);
+    address otherProposer    = proposalProposer(otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string reason;
+    require pId == propose@withrevert(e, targets, values, calldatas, reason);
+    bool success = !lastReverted;
+
+    // liveness & double proposal
+    assert success <=> stateBefore == UNSET();
+
+    // effect
+    assert success => (
+        state(e, pId)         == PENDING()    &&
+        proposalProposer(pId) == e.msg.sender &&
+        proposalSnapshot(pId) == clock(e) + votingDelay() &&
+        proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod()
+    );
+
+    // no side-effect
+    assert state(e, otherId)         != otherStateBefore => otherId == pId;
+    assert proposalSnapshot(otherId) == otherVoteStart;
+    assert proposalDeadline(otherId) == otherVoteEnd;
+    assert proposalProposer(otherId) == otherProposer;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: votes effect and liveness. Includes "A user cannot vote twice"                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule castVote(uint256 pId, env e, method f)
+    filtered { f -> voting(f) }
+{
+    require nonpayable(e);
+
+    uint8   support;
+    address voter;
+    address otherVoter;
+    uint256 otherId;
+
+    uint8   stateBefore             = state(e, pId);
+    bool    hasVotedBefore          = hasVoted(pId, voter);
+    bool    otherVotedBefore        = hasVoted(otherId, otherVoter);
+    uint256 againstVotesBefore      = getAgainstVotes(pId);
+    uint256 forVotesBefore          = getForVotes(pId);
+    uint256 abstainVotesBefore      = getAbstainVotes(pId);
+    uint256 otherAgainstVotesBefore = getAgainstVotes(otherId);
+    uint256 otherForVotesBefore     = getForVotes(otherId);
+    uint256 otherAbstainVotesBefore = getAbstainVotes(otherId);
+
+    // voting weight overflow check
+    uint256 voterWeight = token_getPastVotes(voter, proposalSnapshot(pId));
+    require againstVotesBefore + voterWeight <= max_uint256;
+    require forVotesBefore     + voterWeight <= max_uint256;
+    require abstainVotesBefore + voterWeight <= max_uint256;
+
+    uint256 weight = helperVoteWithRevert(e, f, pId, voter, support);
+    bool success = !lastReverted;
+
+    assert success <=> (
+        stateBefore == ACTIVE() &&
+        !hasVotedBefore &&
+        (support == 0 || support == 1 || support == 2)
+    );
+
+    assert success => (
+        state(e, pId)        == ACTIVE() &&
+        voterWeight          == weight &&
+        getAgainstVotes(pId) == againstVotesBefore + (support == 0 ? weight : 0) &&
+        getForVotes(pId)     == forVotesBefore     + (support == 1 ? weight : 0) &&
+        getAbstainVotes(pId) == abstainVotesBefore + (support == 2 ? weight : 0) &&
+        hasVoted(pId, voter)
+    );
+
+    // no side-effect
+    assert hasVoted(otherId, otherVoter) != otherVotedBefore        => (otherId == pId && otherVoter == voter);
+    assert getAgainstVotes(otherId)      != otherAgainstVotesBefore => (otherId == pId);
+    assert getForVotes(otherId)          != otherForVotesBefore     => (otherId == pId);
+    assert getAbstainVotes(otherId)      != otherAbstainVotesBefore => (otherId == pId);
+}

certora/specs/GovernorInvariants.spec

@@ -0,0 +1,72 @@
+import "helpers.spec"
+import "methods/IGovernor.spec"
+import "Governor.helpers.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: clock is consistent between the goernor and the token                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule clockMode(env e) {
+    assert clock(e) == e.block.number || clock(e) == e.block.timestamp;
+    assert clock(e) == token_clock(e);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Proposal is UNSET iff the proposer, the snapshot and the deadline are unset.                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant createdConsistency(env e, uint256 pId)
+    safeState(e, pId) == UNSET() <=> proposalProposer(pId) == 0 &&
+    safeState(e, pId) == UNSET() <=> proposalSnapshot(pId) == 0 &&
+    safeState(e, pId) == UNSET() <=> proposalDeadline(pId) == 0 &&
+    safeState(e, pId) == UNSET() =>  !isExecuted(pId) &&
+    safeState(e, pId) == UNSET() =>  !isCanceled(pId)
+    {
+        preserved {
+            require clock(e) > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Votes start before it ends                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant voteStartBeforeVoteEnd(uint256 pId)
+    proposalSnapshot(pId) <= proposalDeadline(pId)
+    {
+        preserved with (env e) {
+            requireInvariant createdConsistency(e, pId);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A proposal cannot be both executed and canceled simultaneously                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant noBothExecutedAndCanceled(uint256 pId)
+    !isExecuted(pId) || !isCanceled(pId)
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg)
+    filtered { f -> !skip(f) }
+{
+    require state(e, pId) != UNSET();
+
+    uint256 voteStart = proposalSnapshot(pId);
+    uint256 voteEnd   = proposalDeadline(pId);
+    address proposer  = proposalProposer(pId);
+
+    f(e, arg);
+
+    assert voteStart == proposalSnapshot(pId), "Start date was changed";
+    assert voteEnd   == proposalDeadline(pId), "End date was changed";
+    assert proposer  == proposalProposer(pId), "Proposer was changed";
+}

certora/specs/GovernorStates.spec

@@ -0,0 +1,212 @@
+import "helpers.spec"
+import "methods/IGovernor.spec"
+import "Governor.helpers.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: state returns one of the value in the enumeration                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateConsistency(env e, uint256 pId) {
+    uint8 result = state(e, pId);
+    assert (
+        result == PENDING()   ||
+        result == ACTIVE()    ||
+        result == CANCELED()  ||
+        result == DEFEATED()  ||
+        result == SUCCEEDED() ||
+        result == QUEUED()    ||
+        result == EXECUTED()
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: State transition                                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args)
+    filtered { f -> !skip(f) }
+{
+    require clock(e) > 0; // Sanity
+
+    uint8 stateBefore = state(e, pId);
+    f(e, args);
+    uint8 stateAfter  = state(e, pId);
+
+    assert (stateBefore != stateAfter) => (
+        stateBefore == UNSET() => (
+            stateAfter == PENDING() && f.selector == propose(address[],uint256[],bytes[],string).selector
+        ) &&
+        stateBefore == PENDING() => (
+            (stateAfter == CANCELED() && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector)
+        ) &&
+        stateBefore == SUCCEEDED() => (
+            (stateAfter == QUEUED()   && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) ||
+            (stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector)
+        ) &&
+        stateBefore == QUEUED() => (
+            (stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector)
+        ) &&
+        stateBefore == ACTIVE()    => false &&
+        stateBefore == CANCELED()  => false &&
+        stateBefore == DEFEATED()  => false &&
+        stateBefore == EXECUTED()  => false
+    );
+}
+
+rule stateTransitionWait(uint256 pId, env e1, env e2) {
+    require clock(e1) > 0; // Sanity
+    require clock(e2) > clock(e1);
+
+    uint8 stateBefore = state(e1, pId);
+    uint8 stateAfter  = state(e2, pId);
+
+    assert (stateBefore != stateAfter) => (
+        stateBefore == PENDING() => (
+            stateAfter == ACTIVE()
+        ) &&
+        stateBefore == ACTIVE() => (
+            stateAfter == SUCCEEDED() ||
+            stateAfter == DEFEATED()
+        ) &&
+        stateBefore == UNSET() => false &&
+        stateBefore == SUCCEEDED() => false &&
+        stateBefore == QUEUED()    => false &&
+        stateBefore == CANCELED()  => false &&
+        stateBefore == DEFEATED()  => false &&
+        stateBefore == EXECUTED()  => false
+    );
+}
+
+
+
+
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg)
+    filtered { f -> !skip(f) }
+{
+    require state(e, pId) != UNSET();
+
+    uint256 voteStart = proposalSnapshot(pId);
+    uint256 voteEnd   = proposalDeadline(pId);
+    address proposer  = proposalProposer(pId);
+
+    f(e, arg);
+
+    assert voteStart == proposalSnapshot(pId), "Start date was changed";
+    assert voteEnd   == proposalDeadline(pId), "End date was changed";
+    assert proposer  == proposalProposer(pId), "Proposer was changed";
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: propose effect and liveness. Includes "no double proposition"                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule propose(uint256 pId, env e) {
+    require nonpayable(e);
+
+    uint256 otherId;
+
+    uint8   stateBefore      = state(e, pId);
+    uint8   otherStateBefore = state(e, otherId);
+    uint256 otherVoteStart   = proposalSnapshot(otherId);
+    uint256 otherVoteEnd     = proposalDeadline(otherId);
+    address otherProposer    = proposalProposer(otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string reason;
+    require pId == propose@withrevert(e, targets, values, calldatas, reason);
+    bool success = !lastReverted;
+
+    // liveness & double proposal
+    assert success <=> stateBefore == UNSET();
+
+    // effect
+    assert success => (
+        state(e, pId)         == PENDING()    &&
+        proposalProposer(pId) == e.msg.sender &&
+        proposalSnapshot(pId) == clock(e) + votingDelay() &&
+        proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod()
+    );
+
+    // no side-effect
+    assert state(e, otherId)         != otherStateBefore => otherId == pId;
+    assert proposalSnapshot(otherId) == otherVoteStart;
+    assert proposalDeadline(otherId) == otherVoteEnd;
+    assert proposalProposer(otherId) == otherProposer;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: votes effect and liveness. Includes "A user cannot vote twice"                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule castVote(uint256 pId, env e, method f)
+    filtered { f -> voting(f) }
+{
+    require nonpayable(e);
+
+    uint8   support;
+    address voter;
+    address otherVoter;
+    uint256 otherId;
+
+    uint8   stateBefore             = state(e, pId);
+    bool    hasVotedBefore          = hasVoted(pId, voter);
+    bool    otherVotedBefore        = hasVoted(otherId, otherVoter);
+    uint256 againstVotesBefore      = getAgainstVotes(pId);
+    uint256 forVotesBefore          = getForVotes(pId);
+    uint256 abstainVotesBefore      = getAbstainVotes(pId);
+    uint256 otherAgainstVotesBefore = getAgainstVotes(otherId);
+    uint256 otherForVotesBefore     = getForVotes(otherId);
+    uint256 otherAbstainVotesBefore = getAbstainVotes(otherId);
+
+    // voting weight overflow check
+    uint256 voterWeight = token_getPastVotes(voter, proposalSnapshot(pId));
+    require againstVotesBefore + voterWeight <= max_uint256;
+    require forVotesBefore     + voterWeight <= max_uint256;
+    require abstainVotesBefore + voterWeight <= max_uint256;
+
+    uint256 weight = helperVoteWithRevert(e, f, pId, voter, support);
+    bool success = !lastReverted;
+
+    assert success <=> (
+        stateBefore == ACTIVE() &&
+        !hasVotedBefore &&
+        (support == 0 || support == 1 || support == 2)
+    );
+
+    assert success => (
+        state(e, pId)        == ACTIVE() &&
+        voterWeight          == weight &&
+        getAgainstVotes(pId) == againstVotesBefore + (support == 0 ? weight : 0) &&
+        getForVotes(pId)     == forVotesBefore     + (support == 1 ? weight : 0) &&
+        getAbstainVotes(pId) == abstainVotesBefore + (support == 2 ? weight : 0) &&
+        hasVoted(pId, voter)
+    );
+
+    // no side-effect
+    assert hasVoted(otherId, otherVoter) != otherVotedBefore        => (otherId == pId && otherVoter == voter);
+    assert getAgainstVotes(otherId)      != otherAgainstVotesBefore => (otherId == pId);
+    assert getForVotes(otherId)          != otherForVotesBefore     => (otherId == pId);
+    assert getAbstainVotes(otherId)      != otherAbstainVotesBefore => (otherId == pId);
+}

certora/specs/methods/IGovernor.spec

@@ -0,0 +1,45 @@
+// includes some non standard (from extension) and harness functions
+methods {
+    name()                                            returns string  envfree
+    version()                                         returns string  envfree
+    clock()                                           returns uint48
+    CLOCK_MODE()                                      returns string
+    COUNTING_MODE()                                   returns string  envfree
+    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
+    state(uint256)                                    returns uint8
+    proposalThreshold()                               returns uint256 envfree
+    proposalSnapshot(uint256)                         returns uint256 envfree
+    proposalDeadline(uint256)                         returns uint256 envfree
+    votingDelay()                                     returns uint256 envfree
+    votingPeriod()                                    returns uint256 envfree
+    quorum(uint256)                                   returns uint256 envfree
+    getVotes(address,uint256)                         returns uint256 envfree
+    getVotesWithParams(address,uint256,bytes)         returns uint256 envfree
+    hasVoted(uint256,address)                         returns bool    envfree
+
+    propose(address[],uint256[],bytes[],string)                                        returns uint256
+    execute(address[],uint256[],bytes[],bytes32)                                       returns uint256
+    queue(address[], uint256[], bytes[], bytes32)                                      returns uint256
+    cancel(address[],uint256[],bytes[],bytes32)                                        returns uint256
+    castVote(uint256,uint8)                                                            returns uint256
+    castVoteWithReason(uint256,uint8,string)                                           returns uint256
+    castVoteWithReasonAndParams(uint256,uint8,string,bytes)                            returns uint256
+    castVoteBySig(uint256,uint8,uint8,bytes32,bytes32)                                 returns uint256
+    castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32) returns uint256
+    updateQuorumNumerator(uint256)
+
+    // harness
+    token_getPastTotalSupply(uint256)   returns uint256 envfree
+    token_getPastVotes(address,uint256) returns uint256 envfree
+    token_clock()                       returns uint48
+    token_CLOCK_MODE()                  returns string
+    getExecutor()                       returns address envfree
+    proposalProposer(uint256)           returns address envfree
+    quorumReached(uint256)              returns bool    envfree
+    voteSucceeded(uint256)              returns bool    envfree
+    isExecuted(uint256)                 returns bool    envfree
+    isCanceled(uint256)                 returns bool    envfree
+    getAgainstVotes(uint256)            returns uint256 envfree
+    getForVotes(uint256)                returns uint256 envfree
+    getAbstainVotes(uint256)            returns uint256 envfree
+}