Merge branch 'master' into fv/Governor

certora/diff/governance_Governor.sol.patch

@@ -0,0 +1,24 @@
+--- governance/Governor.sol	2023-05-03 09:17:45.566699712 +0200
++++ governance/Governor.sol	2023-05-04 15:18:42.667741565 +0200
+@@ -224,6 +224,21 @@
+         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;
++    }
++
++    // FV
++    function _governanceCallLength() internal view returns (uint256) {
++        return _governanceCall.length();
++    }
++
+     /**
+      * @dev Amount of votes already cast passes the threshold limit.
+      */

certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch

@@ -0,0 +1,14 @@
+--- governance/extensions/GovernorPreventLateQuorum.sol	2023-05-03 09:17:45.566699712 +0200
++++ governance/extensions/GovernorPreventLateQuorum.sol	2023-05-04 15:18:42.657742113 +0200
+@@ -82,6 +82,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/diff/governance_extensions_GovernorTimelockControl.sol.patch

@@ -0,0 +1,33 @@
+--- governance/extensions/GovernorTimelockControl.sol	2023-05-04 11:44:55.587737817 +0200
++++ governance/extensions/GovernorTimelockControl.sol	2023-05-04 15:18:42.661075263 +0200
+@@ -24,7 +24,7 @@
+  * _Available since v4.3._
+  */
+ abstract contract GovernorTimelockControl is IGovernorTimelock, Governor {
+-    TimelockController private _timelock;
++    TimelockController public _timelock; // FV: public for link
+     mapping(uint256 => bytes32) private _timelockIds;
+ 
+     /**
+@@ -84,6 +84,11 @@
+         return eta == 1 ? 0 : eta; // _DONE_TIMESTAMP (1) should be replaced with a 0 value
+     }
+ 
++    // FV
++    function _proposalQueueId(uint256 proposalId) internal view returns (bytes32) {
++        return _timelockIds[proposalId];
++    }
++
+     /**
+      * @dev Function to queue a proposal to the timelock.
+      */
+@@ -163,4 +168,9 @@
+         emit TimelockChange(address(_timelock), address(newTimelock));
+         _timelock = newTimelock;
+     }
++
++    // FV
++    function timelockId(uint256 proposalId) public view returns (bytes32) {
++        return _timelockIds[proposalId];
++    }
+ }

certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch

@@ -0,0 +1,14 @@
+--- governance/extensions/GovernorVotesQuorumFraction.sol	2023-05-03 09:17:45.570033048 +0200
++++ governance/extensions/GovernorVotesQuorumFraction.sol	2023-05-04 15:18:42.664408414 +0200
+@@ -61,6 +61,11 @@
+         return _quorumNumeratorHistory.upperLookupRecent(SafeCast.toUint32(timepoint));
+     }
+ 
++    // FV
++    function quorumNumeratorLength() public view returns (uint256) {
++        return _quorumNumeratorHistory._checkpoints.length;
++    }
++
+     /**
+      * @dev Returns the quorum denominator. Defaults to 100, but may be overridden.
+      */

certora/diff/token_ERC721_ERC721.sol.patch

@@ -1,5 +1,5 @@
---- token/ERC721/ERC721.sol	2023-03-07 10:48:47.736822221 +0100
-+++ token/ERC721/ERC721.sol	2023-03-09 19:49:39.669338673 +0100
+--- token/ERC721/ERC721.sol	2023-04-27 22:16:54.864065073 +0200
++++ token/ERC721/ERC721.sol	2023-05-04 15:18:42.671074716 +0200
 @@ -199,6 +199,11 @@
          return _owners[tokenId];
      }

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/ERC20VotesBlocknumberHarness.sol

@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/extensions/ERC20Votes.sol";
+
+contract ERC20VotesBlocknumberHarness 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/ERC20VotesTimestampHarness.sol

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/extensions/ERC20Votes.sol";
+
+contract ERC20VotesTimestampHarness 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();
+    }
+
+    // clock
+    function clock() public view override returns (uint48) {
+        return uint48(block.timestamp);
+    }
+
+    // solhint-disable-next-line func-name-mixedcase
+    function CLOCK_MODE() public view virtual override returns (string memory) {
+        return "mode=timestamp";
+    }
+}

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,153 @@
+// 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 hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public pure returns (uint256) {
+        return hashProposal(targets, values, calldatas, keccak256(bytes(description)));
+    }
+
+    function getExecutor() public view returns (address) {
+        return _executor();
+    }
+
+    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 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 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/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 hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public pure returns (uint256) {
+        return hashProposal(targets, values, calldatas, keccak256(bytes(description)));
+    }
+
+    function getExecutor() public view returns (address) {
+        return _executor();
+    }
+
+    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/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

@@ -21,7 +21,7 @@ const argv = require('yargs')
     spec: {
       alias: 's',
       type: 'string',
-      default: __dirname + '/specs.json',
+      default: __dirname + '/specs.js',
     },
     parallel: {
       alias: 'p',
@@ -59,12 +59,17 @@ if (process.exitCode) {
 }
 
 for (const { spec, contract, files, options = [] } of specs) {
-  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]);
+  limit(runCertora, spec, contract, files, [...options, ...argv.options]);
 }
 
 // Run certora, aggregate the output and print it at the end
 async function runCertora(spec, contract, files, options = []) {
-  const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
+  const args = [
+    ...files,
+    '--verify',
+    `${contract}:certora/specs/${spec}.spec`,
+    ...options.flatMap(opt => opt.split(' ')),
+  ];
   const child = proc.spawn('certoraRun', args);
 
   const stream = new PassThrough();

certora/specs.js

@@ -0,0 +1,129 @@
+const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat())));
+
+module.exports = [].concat(
+  // AccessControl
+  {
+    spec: 'AccessControl',
+    contract: 'AccessControlHarness',
+    files: ['certora/harnesses/AccessControlHarness.sol'],
+  },
+  {
+    spec: 'AccessControlDefaultAdminRules',
+    contract: 'AccessControlDefaultAdminRulesHarness',
+    files: ['certora/harnesses/AccessControlDefaultAdminRulesHarness.sol'],
+  },
+  {
+    spec: 'Ownable',
+    contract: 'OwnableHarness',
+    files: ['certora/harnesses/OwnableHarness.sol'],
+  },
+  {
+    spec: 'Ownable2Step',
+    contract: 'Ownable2StepHarness',
+    files: ['certora/harnesses/Ownable2StepHarness.sol'],
+  },
+  // Tokens
+  {
+    spec: 'ERC20',
+    contract: 'ERC20PermitHarness',
+    files: ['certora/harnesses/ERC20PermitHarness.sol'],
+    options: ['--optimistic_loop'],
+  },
+  {
+    spec: 'ERC20FlashMint',
+    contract: 'ERC20FlashMintHarness',
+    files: ['certora/harnesses/ERC20FlashMintHarness.sol', 'certora/harnesses/ERC3156FlashBorrowerHarness.sol'],
+    options: ['--optimistic_loop'],
+  },
+  {
+    spec: 'ERC20Wrapper',
+    contract: 'ERC20WrapperHarness',
+    files: ['certora/harnesses/ERC20PermitHarness.sol', 'certora/harnesses/ERC20WrapperHarness.sol'],
+    options: ['--link ERC20WrapperHarness:_underlying=ERC20PermitHarness', '--optimistic_loop'],
+  },
+  {
+    spec: 'ERC721',
+    contract: 'ERC721Harness',
+    files: ['certora/harnesses/ERC721Harness.sol', 'certora/harnesses/ERC721ReceiverHarness.sol'],
+    options: ['--optimistic_loop'],
+  },
+  // Security
+  {
+    spec: 'Pausable',
+    contract: 'PausableHarness',
+    files: ['certora/harnesses/PausableHarness.sol'],
+  },
+  // Proxy
+  {
+    spec: 'Initializable',
+    contract: 'InitializableHarness',
+    files: ['certora/harnesses/InitializableHarness.sol'],
+  },
+  // Structures
+  {
+    spec: 'DoubleEndedQueue',
+    contract: 'DoubleEndedQueueHarness',
+    files: ['certora/harnesses/DoubleEndedQueueHarness.sol'],
+  },
+  {
+    spec: 'EnumerableSet',
+    contract: 'EnumerableSetHarness',
+    files: ['certora/harnesses/EnumerableSetHarness.sol'],
+  },
+  {
+    spec: 'EnumerableMap',
+    contract: 'EnumerableMapHarness',
+    files: ['certora/harnesses/EnumerableMapHarness.sol'],
+  },
+  // Governance
+  {
+    spec: 'TimelockController',
+    contract: 'TimelockControllerHarness',
+    files: ['certora/harnesses/TimelockControllerHarness.sol'],
+    options: ['--optimistic_hashing', '--optimistic_loop'],
+  },
+  // Governor
+  product(
+    [
+      ...product(['GovernorHarness'], ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates']),
+      ...product(['GovernorPreventLateHarness'], ['GovernorPreventLateQuorum']),
+    ],
+    ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
+  ).map(([contract, spec, token]) => ({
+    spec,
+    contract,
+    files: [
+      `certora/harnesses/${contract}.sol`,
+      `certora/harnesses/${token}.sol`,
+      `certora/harnesses/TimelockControllerHarness.sol`,
+    ],
+    options: [
+      `--link ${contract}:token=${token}`,
+      `--link ${contract}:_timelock=TimelockControllerHarness`,
+      '--optimistic_hashing',
+      '--optimistic_loop',
+    ],
+  })),
+  product(
+    ['GovernorHarness'],
+    ['GovernorFunctions'],
+    ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
+    ['castVote', 'execute'], // 'propose', 'queue', 'cancel' // these rules timeout/fail
+  ).map(([contract, spec, token, fn]) => ({
+    spec,
+    contract,
+    files: [
+      `certora/harnesses/${contract}.sol`,
+      `certora/harnesses/${token}.sol`,
+      `certora/harnesses/TimelockControllerHarness.sol`,
+    ],
+    options: [
+      `--link ${contract}:token=${token}`,
+      `--link ${contract}:_timelock=TimelockControllerHarness`,
+      '--optimistic_hashing',
+      '--optimistic_loop',
+      '--rules',
+      ...['liveness', 'effect', 'sideeffect'].map(kind => `${fn}_${kind}`),
+    ],
+  })),
+);

certora/specs.json

@@ -1,86 +0,0 @@
-[
-  {
-    "spec": "Pausable",
-    "contract": "PausableHarness",
-    "files": ["certora/harnesses/PausableHarness.sol"]
-  },
-  {
-    "spec": "AccessControl",
-    "contract": "AccessControlHarness",
-    "files": ["certora/harnesses/AccessControlHarness.sol"]
-  },
-  {
-    "spec": "AccessControlDefaultAdminRules",
-    "contract": "AccessControlDefaultAdminRulesHarness",
-    "files": ["certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"]
-  },
-  {
-    "spec": "DoubleEndedQueue",
-    "contract": "DoubleEndedQueueHarness",
-    "files": ["certora/harnesses/DoubleEndedQueueHarness.sol"]
-  },
-  {
-    "spec": "Ownable",
-    "contract": "OwnableHarness",
-    "files": ["certora/harnesses/OwnableHarness.sol"]
-  },
-  {
-    "spec": "Ownable2Step",
-    "contract": "Ownable2StepHarness",
-    "files": ["certora/harnesses/Ownable2StepHarness.sol"]
-  },
-  {
-    "spec": "ERC20",
-    "contract": "ERC20PermitHarness",
-    "files": ["certora/harnesses/ERC20PermitHarness.sol"],
-    "options": ["--optimistic_loop"]
-  },
-  {
-    "spec": "ERC20FlashMint",
-    "contract": "ERC20FlashMintHarness",
-    "files": [
-      "certora/harnesses/ERC20FlashMintHarness.sol",
-      "certora/harnesses/ERC3156FlashBorrowerHarness.sol"
-    ],
-    "options": ["--optimistic_loop"]
-  },
-  {
-    "spec": "ERC20Wrapper",
-    "contract": "ERC20WrapperHarness",
-    "files": [
-      "certora/harnesses/ERC20PermitHarness.sol",
-      "certora/harnesses/ERC20WrapperHarness.sol"
-    ],
-    "options": [
-      "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
-      "--optimistic_loop"
-    ]
-  },
-  {
-    "spec": "ERC721",
-    "contract": "ERC721Harness",
-    "files": ["certora/harnesses/ERC721Harness.sol", "certora/harnesses/ERC721ReceiverHarness.sol"],
-    "options": ["--optimistic_loop"]
-  },
-  {
-    "spec": "Initializable",
-    "contract": "InitializableHarness",
-    "files": ["certora/harnesses/InitializableHarness.sol"]
-  },
-  {
-    "spec": "EnumerableSet",
-    "contract": "EnumerableSetHarness",
-    "files": ["certora/harnesses/EnumerableSetHarness.sol"]
-  },
-  {
-    "spec": "EnumerableMap",
-    "contract": "EnumerableMapHarness",
-    "files": ["certora/harnesses/EnumerableMapHarness.sol"]
-  },
-  {
-    "spec": "TimelockController",
-    "contract": "TimelockControllerHarness",
-    "files": ["certora/harnesses/TimelockControllerHarness.sol"],
-    "options": ["--optimistic_hashing", "--optimistic_loop"]
-  }
-]

certora/specs/GovernorBaseRules.spec

@@ -0,0 +1,202 @@
+import "helpers/helpers.spec"
+import "helpers/Governor.helpers.spec"
+import "GovernorInvariants.spec"
+
+use invariant proposalStateConsistency
+use invariant canceledImplyCreated
+use invariant executedImplyCreated
+use invariant noBothExecutedAndCanceled
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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 args)
+    filtered { f -> !assumedSafe(f) }
+{
+    require proposalCreated(pId);
+
+    uint256 voteStart = proposalSnapshot(pId);
+    uint256 voteEnd   = proposalDeadline(pId);
+    address proposer  = proposalProposer(pId);
+
+    f(e, args);
+
+    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                                                                                      │
+│                                                                                                                     │
+│ This rule is checked for castVote, castVoteWithReason and castVoteWithReasonAndParams. For the signature variants   │
+│ (castVoteBySig and castVoteWithReasonAndParamsBySig) we basically assume that the signature referendum is correct   │
+│ without checking it.                                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDoubleVoting(uint256 pId, env e, method f)
+    filtered { f -> voting(f) }
+{
+    address voter;
+    uint8   support;
+
+    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)
+{
+    bool quorumReachedBefore = quorumReached(pId);
+
+    // Ideally we would use `helperVoteWithRevert` here, but it causes timeout. Consider changing it if/when the prover improves.
+    castVote(e, pId, 0);
+
+    assert quorumReached(pId) == quorumReachedBefore, "quorum must not be reached with an against vote";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A proposal could be executed only if quorum was reached and vote succeeded                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, calldataarg args)
+    filtered { f -> !assumedSafe(f) }
+{
+    require !isExecuted(pId);
+
+    bool quorumReachedBefore = quorumReached(pId);
+    bool voteSucceededBefore = voteSucceeded(pId);
+
+    f(e, args);
+
+    assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum not met or vote not successful";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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)
+    filtered { f -> !assumedSafe(f) }
+{
+    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)
+    filtered { f -> !assumedSafe(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()
+    quorumNumerator() <= quorumDenominator()
+    filtered { f -> !assumedSafe(f) }
+    {
+        preserved {
+            require quorumNumeratorLength() < max_uint256;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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, none of the      │
+│ proposal specific functions can make changes again. Note that we prove that only the `execute()` function can set   |
+| isExecuted() to true in in `GorvernorChanges.spec`.                                                                 |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args)
+    filtered { f -> operateOnProposal(f) }
+{
+    require isExecuted(pId);
+    requireInvariant noBothExecutedAndCanceled(pId);
+    requireInvariant executedImplyCreated(pId);
+
+    helperFunctionsWithRevert(e, f, pId);
+
+    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. Note that we prove that only the `execute()` function can set   |
+| isExecuted() to true in in `GorvernorChanges.spec`.                                                                 |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args)
+    filtered { f -> operateOnProposal(f) }
+{
+    require isCanceled(pId);
+    requireInvariant noBothExecutedAndCanceled(pId);
+    requireInvariant canceledImplyCreated(pId);
+
+    helperFunctionsWithRevert(e, f, pId);
+
+    assert lastReverted, "Function was not reverted";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Update operation are restricted to executor                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule privilegedUpdate(env e, method f, calldataarg args)
+    filtered { f -> !assumedSafe(f) }
+{
+    address executorBefore        = getExecutor();
+    uint256 quorumNumeratorBefore = quorumNumerator();
+    address timelockBefore        = timelock();
+
+    f(e, args);
+
+    assert quorumNumerator() != quorumNumeratorBefore => e.msg.sender == executorBefore;
+    assert timelock()        != timelockBefore        => e.msg.sender == executorBefore;
+}

certora/specs/GovernorChanges.spec

@@ -0,0 +1,56 @@
+import "helpers/helpers.spec"
+import "helpers/Governor.helpers.spec"
+import "GovernorInvariants.spec"
+
+use invariant proposalStateConsistency
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Proposal can be switched state only by specific functions                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule changes(uint256 pId, env e, method f, calldataarg args)
+    filtered { f -> !assumedSafe(f) }
+{
+    require clockSanity(e);
+    requireInvariant proposalStateConsistency(pId);
+
+    address user;
+
+    bool    existBefore        = proposalCreated(pId);
+    bool    isExecutedBefore   = isExecuted(pId);
+    bool    isCanceledBefore   = isCanceled(pId);
+    bool    isQueuedBefore     = isQueued(pId);
+    bool    hasVotedBefore     = hasVoted(pId, user);
+    uint256 votesAgainstBefore = getAgainstVotes(pId);
+    uint256 votesForBefore     = getForVotes(pId);
+    uint256 votesAbstainBefore = getAbstainVotes(pId);
+
+    f(e, args);
+
+    bool    existAfter        = proposalCreated(pId);
+    bool    isExecutedAfter   = isExecuted(pId);
+    bool    isCanceledAfter   = isCanceled(pId);
+    bool    isQueuedAfter     = isQueued(pId);
+    bool    hasVotedAfter     = hasVoted(pId, user);
+    uint256 votesAgainstAfter = getAgainstVotes(pId);
+    uint256 votesForAfter     = getForVotes(pId);
+    uint256 votesAbstainAfter = getAbstainVotes(pId);
+
+    // propose, execute, cancel
+    assert existAfter      != existBefore      => (!existBefore      && f.selector == propose(address[],uint256[],bytes[],string).selector);
+    assert isExecutedAfter != isExecutedBefore => (!isExecutedBefore && f.selector == execute(address[],uint256[],bytes[],bytes32).selector);
+    assert isCanceledAfter != isCanceledBefore => (!isCanceledBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector);
+
+    // queue is cleared on cancel
+    assert isQueuedAfter != isQueuedBefore => (
+        (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) ||
+        (isQueuedBefore  && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector)
+    );
+
+    // votes
+    assert hasVotedAfter     != hasVotedBefore     => (!hasVotedBefore                        && votingAll(f));
+    assert votesAgainstAfter != votesAgainstBefore => (votesAgainstAfter > votesAgainstBefore && votingAll(f));
+    assert votesForAfter     != votesForBefore     => (votesForAfter     > votesForBefore     && votingAll(f));
+    assert votesAbstainAfter != votesAbstainBefore => (votesAbstainAfter > votesAbstainBefore && votingAll(f));
+}

certora/specs/GovernorFunctions.spec

@@ -0,0 +1,276 @@
+import "helpers/helpers.spec"
+import "helpers/Governor.helpers.spec"
+import "GovernorInvariants.spec"
+
+use invariant proposalStateConsistency
+use invariant queuedImplyDeadlineOver
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: propose effect and liveness. Includes "no double proposition"                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule propose_liveness(uint256 pId, env e) {
+    require nonpayable(e);
+    require clockSanity(e);
+
+    uint8 stateBefore = state(e, pId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string descr;
+    require pId == hashProposal(targets, values, calldatas, descr);
+
+    propose@withrevert(e, targets, values, calldatas, descr);
+
+    // liveness & double proposal
+    assert !lastReverted <=> (
+        stateBefore == UNSET() &&
+        validProposal(targets, values, calldatas)
+    );
+}
+
+rule propose_effect(uint256 pId, env e) {
+    address[] targets; uint256[] values; bytes[] calldatas; string descr;
+    require pId == hashProposal(targets, values, calldatas, descr);
+
+    propose(e, targets, values, calldatas, descr);
+
+    // effect
+    assert state(e, pId)         == PENDING();
+    assert proposalProposer(pId) == e.msg.sender;
+    assert proposalSnapshot(pId) == clock(e) + votingDelay();
+    assert proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod();
+}
+
+rule propose_sideeffect(uint256 pId, env e, uint256 otherId) {
+    uint8   otherStateBefore = state(e, otherId);
+    uint256 otherVoteStart   = proposalSnapshot(otherId);
+    uint256 otherVoteEnd     = proposalDeadline(otherId);
+    address otherProposer    = proposalProposer(otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string descr;
+    require pId == hashProposal(targets, values, calldatas, descr);
+
+    propose(e, targets, values, calldatas, descr);
+
+    // 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_liveness(uint256 pId, env e, method f)
+    filtered { f -> voting(f) }
+{
+    require nonpayable(e);
+    require clockSanity(e);
+
+    uint8   support;
+    address voter;
+
+    uint8   stateBefore    = state(e, pId);
+    bool    hasVotedBefore = hasVoted(pId, voter);
+    uint256 voterWeight    = token_getPastVotes(voter, proposalSnapshot(pId));
+
+    // voting weight overflow check
+    require getAgainstVotes(pId) + voterWeight <= max_uint256;
+    require getForVotes(pId)     + voterWeight <= max_uint256;
+    require getAbstainVotes(pId) + voterWeight <= max_uint256;
+
+    helperVoteWithRevert(e, f, pId, voter, support);
+
+    assert !lastReverted <=> (
+        stateBefore == ACTIVE() &&
+        !hasVotedBefore &&
+        (support == 0 || support == 1 || support == 2)
+    );
+}
+
+rule castVote_effect(uint256 pId, env e, method f)
+    filtered { f -> voting(f) }
+{
+    uint8   support;
+    address voter;
+
+    uint256 againstVotesBefore = getAgainstVotes(pId);
+    uint256 forVotesBefore     = getForVotes(pId);
+    uint256 abstainVotesBefore = getAbstainVotes(pId);
+    uint256 voterWeight        = token_getPastVotes(voter, proposalSnapshot(pId));
+
+    uint256 weight = helperVoteWithRevert(e, f, pId, voter, support);
+    require !lastReverted;
+
+    assert state(e, pId)        == ACTIVE();
+    assert voterWeight          == weight;
+    assert getAgainstVotes(pId) == againstVotesBefore + (support == 0 ? weight : 0);
+    assert getForVotes(pId)     == forVotesBefore     + (support == 1 ? weight : 0);
+    assert getAbstainVotes(pId) == abstainVotesBefore + (support == 2 ? weight : 0);
+    assert hasVoted(pId, voter);
+}
+
+rule castVote_sideeffect(uint256 pId, env e, method f)
+    filtered { f -> voting(f) }
+{
+    uint8   support;
+    address voter;
+    address otherVoter;
+    uint256 otherId;
+
+    bool    otherVotedBefore        = hasVoted(otherId, otherVoter);
+    uint256 otherAgainstVotesBefore = getAgainstVotes(otherId);
+    uint256 otherForVotesBefore     = getForVotes(otherId);
+    uint256 otherAbstainVotesBefore = getAbstainVotes(otherId);
+
+    helperVoteWithRevert(e, f, pId, voter, support);
+    require !lastReverted;
+
+    // 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);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: queue effect and liveness.                                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule queue_liveness(uint256 pId, env e) {
+    require nonpayable(e);
+    require clockSanity(e);
+
+    uint8 stateBefore = state(e, pId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    queue@withrevert(e, targets, values, calldatas, descrHash);
+
+    // liveness
+    assert !lastReverted <=> stateBefore == SUCCEEDED();
+}
+
+rule queue_effect(uint256 pId, env e) {
+    uint8 stateBefore  = state(e, pId);
+    bool  queuedBefore = isQueued(pId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    queue(e, targets, values, calldatas, descrHash);
+
+    assert state(e, pId) == QUEUED();
+    assert isQueued(pId);
+    assert !queuedBefore;
+}
+
+rule queue_sideeffect(uint256 pId, env e, uint256 otherId) {
+    uint8 otherStateBefore  = state(e, otherId);
+    bool  otherQueuedBefore = isQueued(otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    queue(e, targets, values, calldatas, descrHash);
+
+    // no side-effect
+    assert state(e, otherId) != otherStateBefore  => otherId == pId;
+    assert isQueued(otherId) != otherQueuedBefore => otherId == pId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: execute effect and liveness.                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule execute_liveness(uint256 pId, env e) {
+    require nonpayable(e);
+    require clockSanity(e);
+
+    uint8 stateBefore = state(e, pId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    execute@withrevert(e, targets, values, calldatas, descrHash);
+
+    // liveness: can't check full equivalence because of execution call reverts
+    assert !lastReverted => (stateBefore == SUCCEEDED() || stateBefore == QUEUED());
+}
+
+rule execute_effect(uint256 pId, env e) {
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    execute(e, targets, values, calldatas, descrHash);
+
+    // effect
+    assert state(e, pId) == EXECUTED();
+}
+
+rule execute_sideeffect(uint256 pId, env e, uint256 otherId) {
+    uint8 otherStateBefore = state(e, otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    execute(e, targets, values, calldatas, descrHash);
+
+    // no side-effect
+    assert state(e, otherId) != otherStateBefore => otherId == pId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: cancel (public) effect and liveness.                                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cancel_liveness(uint256 pId, env e) {
+    require nonpayable(e);
+    require clockSanity(e);
+    requireInvariant queuedImplyDeadlineOver(e, pId);
+
+    uint8 stateBefore = state(e, pId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    cancel@withrevert(e, targets, values, calldatas, descrHash);
+
+    // liveness
+    assert !lastReverted <=> (
+        stateBefore == PENDING() &&
+        e.msg.sender == proposalProposer(pId)
+    );
+}
+
+rule cancel_effect(uint256 pId, env e) {
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    cancel(e, targets, values, calldatas, descrHash);
+
+    // effect
+    assert state(e, pId) == CANCELED();
+    assert !isQueued(pId); // cancel resets timelockId
+}
+
+rule cancel_sideeffect(uint256 pId, env e, uint256 otherId) {
+    uint8 otherStateBefore  = state(e, otherId);
+    bool  otherQueuedBefore = isQueued(otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+    require pId == hashProposal(targets, values, calldatas, descrHash);
+
+    cancel(e, targets, values, calldatas, descrHash);
+
+    // no side-effect
+    assert state(e, otherId) != otherStateBefore  => otherId == pId;
+    assert isQueued(otherId) != otherQueuedBefore => otherId == pId;
+}

certora/specs/GovernorInvariants.spec

@@ -0,0 +1,153 @@
+import "helpers/helpers.spec"
+import "helpers/Governor.helpers.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: clock is consistent between the goernor and the token                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule clockMode(env e) {
+    require clockSanity(e);
+
+    assert clock(e) == e.block.number || clock(e) == e.block.timestamp;
+    assert clock(e) == token_clock(e);
+
+    /// This causes a failure in the prover
+    // assert CLOCK_MODE(e) == token_CLOCK_MODE(e);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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 clockSanity(e);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: votes recorded => created                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant votesImplyCreated(uint256 pId)
+    (
+        getAgainstVotes(pId) > 0 ||
+        getForVotes(pId)     > 0 ||
+        getAbstainVotes(pId) > 0
+    ) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            require clockSanity(e);
+            requireInvariant proposalStateConsistency(pId);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: cancel => created                                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant canceledImplyCreated(uint pId)
+    isCanceled(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            require clockSanity(e);
+            requireInvariant proposalStateConsistency(pId);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: executed => created                                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant executedImplyCreated(uint pId)
+    isExecuted(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            require clockSanity(e);
+            requireInvariant proposalStateConsistency(pId);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: queued => created                                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant queuedImplyCreated(uint pId)
+    isQueued(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            require clockSanity(e);
+            requireInvariant proposalStateConsistency(pId);
+        }
+    }
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: timings                                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant votesImplySnapshotPassed(env e, uint256 pId)
+    (
+        getAgainstVotes(pId) > 0 ||
+        getForVotes(pId)     > 0 ||
+        getAbstainVotes(pId) > 0
+    ) => proposalSnapshot(pId) < clock(e)
+    {
+        preserved with (env e2) {
+            // In this invariant, `env e` is representing the present. And `clock(e)` the current timestamp.
+            // It should hold for any transitions in the pasts
+            require clock(e2) <= clock(e);
+        }
+    }
+
+invariant queuedImplyDeadlineOver(env e, uint pId)
+    isQueued(pId) => proposalDeadline(pId) < clock(e)
+    {
+        preserved {
+            require clockSanity(e);
+            requireInvariant proposalStateConsistency(pId);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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)
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: the "governance call" dequeue is empty                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant governanceCallLength()
+    governanceCallLength() == 0

certora/specs/GovernorPreventLateQuorum.spec

@@ -0,0 +1,68 @@
+import "helpers/helpers.spec"
+import "helpers/Governor.helpers.spec"
+import "GovernorInvariants.spec"
+
+methods {
+    lateQuorumVoteExtension()    returns uint64 envfree
+    getExtendedDeadline(uint256) returns uint64 envfree
+}
+
+use invariant proposalStateConsistency
+use invariant votesImplySnapshotPassed
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ This is not (easily) provable as an invariant because the prover think `_totalSupplyCheckpoints` can arbitrarily    │
+│ change, which causes the quorum() to change. Not sure how to fix that.                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+// invariant deadlineExtendedEquivQuorumReached(uint256 pId)
+//     getExtendedDeadline(pId) > 0 <=> (quorumReached(pId) && !isCanceled(pId))
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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 -> !assumedSafe(f) }
+{
+    require clockSanity(e);
+    requireInvariant proposalStateConsistency(pId);
+    requireInvariant votesImplySnapshotPassed(e, pId);
+
+    uint256 deadlineBefore         = proposalDeadline(pId);
+    bool    deadlineExtendedBefore = getExtendedDeadline(pId) > 0;
+
+    f(e, args);
+
+    uint256 deadlineAfter         = proposalDeadline(pId);
+    bool    deadlineExtendedAfter = getExtendedDeadline(pId) > 0;
+
+    // deadline can never be reduced
+    assert deadlineBefore <= deadlineAfter;
+
+    // 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 &&
+            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

@@ -0,0 +1,238 @@
+import "helpers/helpers.spec"
+import "helpers/Governor.helpers.spec"
+import "GovernorInvariants.spec"
+
+use invariant proposalStateConsistency
+use invariant votesImplySnapshotPassed
+
+definition assumedSafeOrDuplicate(method f) returns bool =
+    assumedSafe(f)
+    || f.selector == castVoteWithReason(uint256,uint8,string).selector
+    || f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector
+    || f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector
+    || f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: state returns one of the value in the enumeration                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateDomain(env e, uint256 pId) {
+    uint8 result = safeState(e, pId);
+    assert (
+        result == UNSET()     ||
+        result == PENDING()   ||
+        result == ACTIVE()    ||
+        result == CANCELED()  ||
+        result == DEFEATED()  ||
+        result == SUCCEEDED() ||
+        result == QUEUED()    ||
+        result == EXECUTED()
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ [DISABLED] Rule: State transitions caused by function calls                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+/// Previous version that results in the prover timing out.
+// rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args)
+//     filtered { f -> !assumedSafeOrDuplicate(f) }
+// {
+//     require clockSanity(e);
+//     require quorumNumeratorLength() < max_uint256; // sanity
+//
+//     uint8 stateBefore = safeState(e, pId);
+//     f(e, args);
+//     uint8 stateAfter  = safeState(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  ) ||
+//         (stateBefore == SUCCEEDED() && stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) ||
+//         (stateBefore == QUEUED()    && stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector)
+//     );
+// }
+
+/// This version also causes a lot of timeouts so we comment it out of now
+// function stateTransitionFnHelper(method f, uint8 s) returns uint8 {
+//     uint256 pId; env e; calldataarg args;
+//
+//     require clockSanity(e);
+//     require quorumNumeratorLength() < max_uint256; // sanity
+//
+//     require safeState(e, pId) == s; // constrain state before
+//     f(e, args);
+//     require safeState(e, pId) != s; // constrain state after
+//
+//     return safeState(e, pId);
+// }
+//
+// rule stateTransitionFn_UNSET(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, UNSET());
+//     assert stateAfter == PENDING() && f.selector == propose(address[],uint256[],bytes[],string).selector;
+// }
+//
+// rule stateTransitionFn_PENDING(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, PENDING());
+//     assert stateAfter == CANCELED() && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector;
+// }
+//
+// rule stateTransitionFn_ACTIVE(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, ACTIVE());
+//     assert false;
+// }
+//
+// rule stateTransitionFn_CANCELED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, CANCELED());
+//     assert false;
+// }
+//
+// rule stateTransitionFn_DEFEATED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, DEFEATED());
+//     assert false;
+// }
+//
+// rule stateTransitionFn_SUCCEEDED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, SUCCEEDED());
+//     assert (
+//         (stateAfter == QUEUED()   && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) ||
+//         (stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector)
+//     );
+// }
+//
+// rule stateTransitionFn_QUEUED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, QUEUED());
+//     assert stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector;
+// }
+//
+// rule stateTransitionFn_EXECUTED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } {
+//     uint8 stateAfter = stateTransitionFnHelper(f, EXECUTED());
+//     assert false;
+// }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: State transitions caused by time passing                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+// The timelockId can be set in states QUEUED, EXECUTED and CANCELED. However, checking the full scope of this results
+// in a timeout. This is a weaker version that is still useful. Ideally we would check `safeState`.
+invariant noTimelockBeforeEndOfVote(env e, uint256 pId)
+    state(e, pId) == ACTIVE() => timelockId(pId) == 0
+
+rule stateTransitionWait(uint256 pId, env e1, env e2) {
+    require clockSanity(e1);
+    require clockSanity(e2);
+    require clock(e2) > clock(e1);
+
+    // Force the state to be consistent with e1 (before). We want the storage related to `pId` to match what is
+    // possible before the time passes. We don't want the state transition include elements that cannot have happened
+    // before e1. This ensure that the e1 → e2 state transition is purelly a consequence of time passing.
+    requireInvariant votesImplySnapshotPassed(e1, pId);
+    requireInvariant noTimelockBeforeEndOfVote(e1, pId);
+
+    uint8 stateBefore = state(e1, pId); // Ideally we would use "safeState(e1, pId)"
+    uint8 stateAfter  = state(e2, pId); // Ideally we would use "safeState(e2, pId)"
+
+    assert (stateBefore != stateAfter) => (
+        (stateBefore == PENDING() && stateAfter == ACTIVE()   ) ||
+        (stateBefore == PENDING() && stateAfter == DEFEATED() ) ||
+        (stateBefore == ACTIVE()  && stateAfter == SUCCEEDED()) ||
+        (stateBefore == ACTIVE()  && stateAfter == DEFEATED() )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: State corresponds to the vote timing and results                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateIsConsistentWithVotes(uint256 pId, env e) {
+    require clockSanity(e);
+    requireInvariant proposalStateConsistency(pId);
+
+    uint48  currentClock  = clock(e);
+    uint8   currentState  = safeState(e, pId);
+    uint256 snapshot      = proposalSnapshot(pId);
+    uint256 deadline      = proposalDeadline(pId);
+    bool    quorumSuccess = quorumReached(pId);
+    bool    voteSuccess   = voteSucceeded(pId);
+
+    // Pending: before vote starts
+    assert currentState == PENDING() => (
+        snapshot >= currentClock
+    );
+
+    // Active: after vote starts & before vote ends
+    assert currentState == ACTIVE() => (
+        snapshot < currentClock &&
+        deadline >= currentClock
+    );
+
+    // Succeeded: after vote end, with vote successful and quorum reached
+    assert currentState == SUCCEEDED() => (
+        deadline < currentClock &&
+        (
+            quorumSuccess &&
+            voteSuccess
+        )
+    );
+
+    // Defeated: after vote end, with vote not successful or quorum not reached
+    assert currentState == DEFEATED() => (
+        deadline < currentClock &&
+        (
+            !quorumSuccess ||
+            !voteSuccess
+        )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ [NEED WORK] Rule: `updateQuorumNumerator` cannot cause quorumReached to change.                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+//// This would be nice, but its way to slow to run because "quorumReached" is a FV nightmare
+//// Also, for it to work we need to prove that the checkpoints have (strictly) increasing keys.
+// rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg args)
+//     filtered { f -> !assumedSafeOrDuplicate(f) }
+// {
+//     require clockSanity(e);
+//     require clock(e) > proposalSnapshot(pId); // vote has started
+//     require quorumNumeratorLength() < max_uint256; // sanity
+//
+//     bool quorumReachedBefore = quorumReached(pId);
+//
+//     uint256 snapshot    = proposalSnapshot(pId);
+//     uint256 totalSupply = token_getPastTotalSupply(snapshot);
+//
+//     f(e, args);
+//
+//     // Needed because the prover doesn't understand the checkpoint properties of the voting token.
+//     require clock(e) > snapshot => token_getPastTotalSupply(snapshot) == totalSupply;
+//
+//     assert quorumReached(pId) != quorumReachedBefore => (
+//         !quorumReachedBefore &&
+//         votingAll(f)
+//     );
+// }
+
+//// To prove that, we need to prove that the checkpoints have (strictly) increasing keys.
+//// otherwise it gives us counter example where the checkpoint history has keys:
+//// [ 12,12,13,13,12] and the lookup obviously fail to get the correct value
+// rule quorumUpdateDoesntAffectPastProposals(uint256 pId, env e) {
+//     require clockSanity(e);
+//     require clock(e) > proposalSnapshot(pId); // vote has started
+//     require quorumNumeratorLength() < max_uint256; // sanity
+//
+//     bool quorumReachedBefore = quorumReached(pId);
+//
+//     uint256 newQuorumNumerator;
+//     updateQuorumNumerator(e, newQuorumNumerator);
+//
+//     assert quorumReached(pId) == quorumReachedBefore;
+// }

certora/specs/TimelockController.spec

@@ -1,29 +1,6 @@
 import "helpers/helpers.spec"
 import "methods/IAccessControl.spec"
-
-methods {
-    TIMELOCK_ADMIN_ROLE()       returns (bytes32) envfree
-    PROPOSER_ROLE()             returns (bytes32) envfree
-    EXECUTOR_ROLE()             returns (bytes32) envfree
-    CANCELLER_ROLE()            returns (bytes32) envfree
-    isOperation(bytes32)        returns (bool)    envfree
-    isOperationPending(bytes32) returns (bool)    envfree
-    isOperationReady(bytes32)   returns (bool)
-    isOperationDone(bytes32)    returns (bool)    envfree
-    getTimestamp(bytes32)       returns (uint256) envfree
-    getMinDelay()               returns (uint256) envfree
-
-    hashOperation(address, uint256, bytes, bytes32, bytes32)            returns(bytes32) envfree
-    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree
-
-    schedule(address, uint256, bytes, bytes32, bytes32, uint256)
-    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256)
-    execute(address, uint256, bytes, bytes32, bytes32)
-    executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
-    cancel(bytes32)
-
-    updateDelay(uint256)
-}
+import "methods/ITimelockController.spec"
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐

certora/specs/helpers/Governor.helpers.spec

@@ -0,0 +1,186 @@
+import "helpers.spec"
+import "../methods/IGovernor.spec"
+import "../methods/ITimelockController.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Sanity                                                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function clockSanity(env e) returns bool {
+    return e.block.number    < max_uint48()
+        && e.block.timestamp < max_uint48()
+        && clock(e) > 0;
+}
+
+function validProposal(address[] targets, uint256[] values, bytes[] calldatas) returns bool {
+    return targets.length > 0
+        && targets.length == values.length
+        && targets.length == calldatas.length;
+}
+
+function sanityString(string s) returns bool {
+    return s.length < 0xffff;
+}
+
+function sanityBytes(bytes b) returns bool {
+    return b.length < 0xffff;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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;
+
+// This helper is an alternative to state(e, pId) that will return UNSET() instead of reverting when then proposal
+// does not exist (not created yet)
+function safeState(env e, uint256 pId) returns uint8 {
+    return proposalCreated(pId) ? state(e, pId): UNSET();
+}
+
+definition proposalCreated(uint256 pId) returns bool =
+    proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Filters                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition assumedSafe(method f) returns bool =
+    f.isView ||
+    f.isFallback ||
+    f.selector == relay(address,uint256,bytes).selector ||
+    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;
+
+// These function are covered by helperFunctionsWithRevert
+definition operateOnProposal(method f) returns bool =
+    f.selector == propose(address[],uint256[],bytes[],string).selector ||
+    f.selector == queue(address[],uint256[],bytes[],bytes32).selector ||
+    f.selector == execute(address[],uint256[],bytes[],bytes32).selector ||
+    f.selector == cancel(address[],uint256[],bytes[],bytes32).selector ||
+    f.selector == castVote(uint256,uint8).selector ||
+    f.selector == castVoteWithReason(uint256,uint8,string).selector ||
+    f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector ||
+    f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector ||
+    f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector;
+
+// These function are covered by helperVoteWithRevert
+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;
+
+definition votingBySig(method f) returns bool =
+    f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector ||
+    f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector;
+
+definition votingAll(method f) returns bool =
+    voting(f) || votingBySig(f);
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helper functions                                                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 support) returns uint256 {
+    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)
+    {
+        string reason;
+        require e.msg.sender == voter && sanityString(reason);
+        return castVoteWithReason@withrevert(e, pId, support, reason);
+    }
+    else  if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector)
+    {
+        string reason; bytes params;
+        require e.msg.sender == voter && sanityString(reason) && sanityBytes(params);
+        return castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params);
+    }
+    else
+    {
+        calldataarg args;
+        f(e, args);
+        return 0;
+    }
+}
+
+// Governor function that operates on a given proposalId may or may not include the proposalId in the arguments. This
+// helper restricts the call to method `f` in a way that it's operating on a specific proposal.
+//
+// This can be used to say "consider any function call that operates on proposal `pId`" or "consider a propose call
+// that corresponds to a given pId".
+//
+// This is for example used when proving that not 2 proposals can be proposed with the same id: Once the proposal is
+// proposed a first time, we want to prove that "any propose call that corresponds to the same id should revert".
+function helperFunctionsWithRevert(env e, method f, uint256 pId) {
+    if (f.selector == propose(address[],uint256[],bytes[],string).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; string descr;
+        require pId == hashProposal(targets, values, calldatas, descr);
+        propose@withrevert(e, targets, values, calldatas, descr);
+    }
+    else if (f.selector == queue(address[],uint256[],bytes[],bytes32).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+        require pId == hashProposal(targets, values, calldatas, descrHash);
+        queue@withrevert(e, targets, values, calldatas, descrHash);
+    }
+    else if (f.selector == execute(address[],uint256[],bytes[],bytes32).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+        require pId == hashProposal(targets, values, calldatas, descrHash);
+        execute@withrevert(e, targets, values, calldatas, descrHash);
+    }
+    else if (f.selector == cancel(address[],uint256[],bytes[],bytes32).selector)
+    {
+        address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
+        require pId == hashProposal(targets, values, calldatas, descrHash);
+        cancel@withrevert(e, targets, values, calldatas, descrHash);
+    }
+    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(e, args);
+    }
+}

certora/specs/methods/IGovernor.spec

@@ -0,0 +1,56 @@
+// includes some non standard (from extension) and harness functions
+methods {
+    name()                                            returns string  envfree
+    version()                                         returns string  envfree
+    token()                                           returns address envfree
+    timelock()                                        returns address 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
+    quorumNumerator()                                 returns uint256 envfree
+    quorumNumerator(uint256)                          returns uint256 envfree
+    quorumDenominator()                               returns uint256 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)
+    updateTimelock(address)
+
+    // harness
+    token_getPastTotalSupply(uint256)                returns uint256 envfree
+    token_getPastVotes(address,uint256)              returns uint256 envfree
+    token_clock()                                    returns uint48
+    token_CLOCK_MODE()                               returns string
+    hashProposal(address[],uint256[],bytes[],string) returns uint256 envfree
+    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
+    isQueued(uint256)                                returns bool    envfree
+    governanceCallLength()                           returns uint256 envfree
+    getAgainstVotes(uint256)                         returns uint256 envfree
+    getForVotes(uint256)                             returns uint256 envfree
+    getAbstainVotes(uint256)                         returns uint256 envfree
+    quorumNumeratorLength()                          returns uint256 envfree
+    timelockId(uint256)                              returns bytes32 envfree
+}

certora/specs/methods/ITimelockController.spec

@@ -0,0 +1,22 @@
+methods {
+    TIMELOCK_ADMIN_ROLE()       returns (bytes32) envfree => DISPATCHER(true)
+    PROPOSER_ROLE()             returns (bytes32) envfree => DISPATCHER(true)
+    EXECUTOR_ROLE()             returns (bytes32) envfree => DISPATCHER(true)
+    CANCELLER_ROLE()            returns (bytes32) envfree => DISPATCHER(true)
+    isOperation(bytes32)        returns (bool)    envfree => DISPATCHER(true)
+    isOperationPending(bytes32) returns (bool)    envfree => DISPATCHER(true)
+    isOperationReady(bytes32)   returns (bool)            => DISPATCHER(true)
+    isOperationDone(bytes32)    returns (bool)    envfree => DISPATCHER(true)
+    getTimestamp(bytes32)       returns (uint256) envfree => DISPATCHER(true)
+    getMinDelay()               returns (uint256) envfree => DISPATCHER(true)
+
+    hashOperation(address, uint256, bytes, bytes32, bytes32)            returns(bytes32) envfree => DISPATCHER(true)
+    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree => DISPATCHER(true)
+
+    schedule(address, uint256, bytes, bytes32, bytes32, uint256)            => DISPATCHER(true)
+    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => DISPATCHER(true)
+    execute(address, uint256, bytes, bytes32, bytes32)                      => DISPATCHER(true)
+    executeBatch(address[], uint256[], bytes[], bytes32, bytes32)           => DISPATCHER(true)
+    cancel(bytes32)                                                         => DISPATCHER(true)
+    updateDelay(uint256)                                                    => DISPATCHER(true)
+}

requirements.txt

@@ -1 +1 @@
-certora-cli==3.6.4
+certora-cli==3.6.8