Add formal verification for the Governor system

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/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,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.js

@@ -0,0 +1,51 @@
+const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat())));
+
+module.exports = [
+  {
+    spec: 'AccessControl',
+    contract: 'AccessControlHarness',
+    files: ['certora/harnesses/AccessControlHarness.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: 'Initializable',
+    contract: 'InitializableHarness',
+    files: ['certora/harnesses/InitializableHarness.sol'],
+  },
+  ...product(
+    ['GovernorBase', 'GovernorInvariants', 'GovernorStates', 'GovernorFunctions'],
+    ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
+  ).map(([spec, token]) => ({
+    spec,
+    contract: 'GovernorHarness',
+    files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
+    options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
+  })),
+];