Formal verification using Certora (#4084)

Co-authored-by: Francisco Giordano <fg@frang.io>

.github/workflows/formal-verification.yml

@@ -0,0 +1,53 @@
+name: formal verification
+
+on:
+  push:
+    branches:
+      - master
+      - release-v*
+  pull_request: {}
+  workflow_dispatch: {}
+
+env:
+  PIP_VERSION: '3.10'
+  JAVA_VERSION: '11'
+  SOLC_VERSION: '0.8.19'
+
+jobs:
+  apply-diff:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Apply patches
+        run: make -C certora apply
+
+  verify:
+    runs-on: ubuntu-latest
+    if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification')
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up environment
+        uses: ./.github/actions/setup
+      - name: Install python
+        uses: actions/setup-python@v4
+        with:
+          python-version: ${{ env.PIP_VERSION }}
+          cache: 'pip'
+      - name: Install python packages
+        run: pip install -r requirements.txt
+      - name: Install java
+        uses: actions/setup-java@v3
+        with:
+          distribution: temurin
+          java-version: ${{ env.JAVA_VERSION }}
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v${{ env.SOLC_VERSION }}/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+          chmod +x /usr/local/bin/solc
+      - name: Verify specification
+        run: |
+          make -C certora apply
+          node certora/run.js >> "$GITHUB_STEP_SUMMARY"
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

certora/.gitignore

@@ -0,0 +1 @@
+patched

certora/Makefile

@@ -1,24 +1,54 @@
 default: help
 
-PATCH         = applyHarness.patch
-CONTRACTS_DIR = ../contracts
-MUNGED_DIR    = munged
+SRC   := ../contracts
+DST   := patched
+DIFF  := diff
+SRCS  := $(shell find $(SRC) -type f)
+DSTS  := $(shell find $(DST) -type f)
+DIFFS := $(shell find $(DIFF) -type f)
 
+###############################################################################
+# Apply all patches in the $DIFF folder to the $DST folder
+apply: $(DST) $(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$(DIFFS)))
+
+# Reset the $DST folder
+$(DST): FORCE
+	@rm -rf $@
+	@cp -r $(SRC) $@
+
+# Update a solidity file in the $DST directory using the corresponding patch
+$(DST)/%.sol: FORCE
+	@echo Applying patch to $@
+	@patch -p0 -d $(DST) < $(patsubst $(DST)_%,$(DIFF)/%.patch,$(subst /,_,$@))
+
+###############################################################################
+# Record all difference between $SRC and $DST in patches
+record: $(DIFF) $(patsubst %,$(DIFF)/%.patch,$(subst /,_,$(subst $(SRC)/,,$(SRCS)) $(subst $(DST)/,,$(DSTS))))
+
+# Create the $DIFF folder
+$(DIFF): FORCE
+	@rm -rf $@
+	@mkdir $@
+
+# Create the patch file by comparing the source and the destination
+$(DIFF)/%.patch: FORCE
+	@echo Generating patch $@
+	@diff -ruN \
+		$(patsubst $(DIFF)/%.patch,$(SRC)/%,$(subst _,/,$@)) \
+		$(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$@)) \
+		| sed 's+$(SRC)/++g' \
+		| sed 's+$(DST)/++g' \
+		> $@
+	@[ -s $@ ] || rm $@
+
+###############################################################################
 help:
 	@echo "usage:"
+	@echo "  make apply:  create $(DST) directory by applying the patches to $(SRC)"
+	@echo "  make record: record the patches capturing the differences between $(SRC) and $(DST)"
 	@echo "  make clean:  remove all generated files (those ignored by git)"
-	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
-	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
-
-munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
-	rm -rf $@
-	cp -r $(CONTRACTS_DIR) $@
-	patch -p0 -d $@ < $(PATCH)
-
-record:
-	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
 
 clean:
 	git clean -fdX
-	touch $(PATCH)
 
+FORCE: ;

certora/applyHarness.patch

@@ -1,101 +0,0 @@
-diff -ruN .gitignore .gitignore
---- .gitignore	1969-12-31 19:00:00.000000000 -0500
-+++ .gitignore	2021-12-09 14:46:33.923637220 -0500
-@@ -0,0 +1,2 @@
-+*
-+!.gitignore
-diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol
---- governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-09 14:46:33.923637220 -0500
-@@ -245,7 +245,7 @@
-     /**
-      * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
-      */
--    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
-         ProposalDetails storage details = _proposalDetails[proposalId];
-         return quorum(proposalSnapshot(proposalId)) <= details.forVotes;
-     }
-@@ -253,7 +253,7 @@
-     /**
-      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
-      */
--    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
-         ProposalDetails storage details = _proposalDetails[proposalId];
-         return details.forVotes > details.againstVotes;
-     }
-diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
---- governance/extensions/GovernorCountingSimple.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/extensions/GovernorCountingSimple.sol	2021-12-09 14:46:33.923637220 -0500
-@@ -64,7 +64,7 @@
-     /**
-      * @dev See {Governor-_quorumReached}.
-      */
--    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
-         ProposalVote storage proposalvote = _proposalVotes[proposalId];
- 
-         return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
-@@ -73,7 +73,7 @@
-     /**
-      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
-      */
--    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
-         ProposalVote storage proposalvote = _proposalVotes[proposalId];
- 
-         return proposalvote.forVotes > proposalvote.againstVotes;
-diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol
---- governance/extensions/GovernorTimelockControl.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/extensions/GovernorTimelockControl.sol	2021-12-09 14:46:33.923637220 -0500
-@@ -111,7 +111,7 @@
-         bytes[] memory calldatas,
-         bytes32 descriptionHash
-     ) internal virtual override {
--        _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
-+         _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
-     }
- 
-     /**
-diff -ruN governance/Governor.sol governance/Governor.sol
---- governance/Governor.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/Governor.sol	2021-12-09 14:46:56.411503587 -0500
-@@ -38,8 +38,8 @@
- 
-     string private _name;
- 
--    mapping(uint256 => ProposalCore) private _proposals;
--
-+    mapping(uint256 => ProposalCore) public _proposals;
-+ 
-     /**
-      * @dev Restrict access to governor executing address. Some module might override the _executor function to make
-      * sure this modifier is consistent with the execution model.
-@@ -167,12 +167,12 @@
-     /**
-      * @dev Amount of votes already cast passes the threshold limit.
-      */
--    function _quorumReached(uint256 proposalId) internal view virtual returns (bool);
-+    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
- 
-     /**
-      * @dev Is the proposal successful or not.
-      */
--    function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
-+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
- 
-     /**
-      * @dev Register a vote with a given support and voting weight.
-diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
---- token/ERC20/extensions/ERC20Votes.sol	2021-12-03 15:24:56.527654330 -0500
-+++ token/ERC20/extensions/ERC20Votes.sol	2021-12-09 14:46:33.927637196 -0500
-@@ -84,7 +84,7 @@
-      *
-      * - `blockNumber` must have been already mined
-      */
--    function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) {
-+    function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) {
-         require(blockNumber < block.number, "ERC20Votes: block not yet mined");
-         return _checkpointsLookup(_checkpoints[account], blockNumber);
-     }

certora/harnesses/AccessControlHarness.sol

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/AccessControl.sol";
+
+contract AccessControlHarness is AccessControl {}

certora/harnesses/ERC20FlashMintHarness.sol

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/ERC20.sol";
+import "../patched/token/ERC20/extensions/ERC20Permit.sol";
+import "../patched/token/ERC20/extensions/ERC20FlashMint.sol";
+
+contract ERC20FlashMintHarness is ERC20, ERC20Permit, ERC20FlashMint {
+    uint256 someFee;
+    address someFeeReceiver;
+
+    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);
+    }
+
+    // public accessor
+    function flashFeeReceiver() public view returns (address) {
+        return someFeeReceiver;
+    }
+
+    // internal hook
+    function _flashFee(address, uint256) internal view override returns (uint256) {
+        return someFee;
+    }
+
+    function _flashFeeReceiver() internal view override returns (address) {
+        return someFeeReceiver;
+    }
+}

certora/harnesses/ERC20PermitHarness.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/ERC20.sol";
+import "../patched/token/ERC20/extensions/ERC20Permit.sol";
+
+contract ERC20PermitHarness is ERC20, ERC20Permit {
+    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);
+    }
+}

certora/harnesses/ERC20VotesHarness.sol

@@ -1,28 +0,0 @@
-import "../munged/token/ERC20/extensions/ERC20Votes.sol";
-
-contract ERC20VotesHarness is ERC20Votes {
-    constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
-
-    mapping(address => mapping(uint256 => uint256)) public _getPastVotes;
-
-    function _afterTokenTransfer(
-        address from,
-        address to,
-        uint256 amount
-    ) internal virtual override {
-        super._afterTokenTransfer(from, to, amount);
-        _getPastVotes[from][block.number] -= amount;
-        _getPastVotes[to][block.number] += amount;
-    }
-
-    /**
-     * @dev Change delegation for `delegator` to `delegatee`.
-     *
-     * Emits events {DelegateChanged} and {DelegateVotesChanged}.
-     */
-    function _delegate(address delegator, address delegatee) internal virtual override{
-        super._delegate(delegator, delegatee);
-        _getPastVotes[delegator][block.number] -= balanceOf(delegator);
-        _getPastVotes[delegatee][block.number] += balanceOf(delegator);
-    }
-}

certora/harnesses/ERC3156FlashBorrowerHarness.sol

@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: MIT
+
+import "../patched/interfaces/IERC3156FlashBorrower.sol";
+
+pragma solidity ^0.8.0;
+
+contract ERC3156FlashBorrowerHarness is IERC3156FlashBorrower {
+    bytes32 somethingToReturn;
+
+    function onFlashLoan(address, address, uint256, uint256, bytes calldata) external view override returns (bytes32) {
+        return somethingToReturn;
+    }
+}

certora/harnesses/WizardControlFirstPriority.sol

@@ -1,150 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.2;
-
-import "../munged/governance/Governor.sol";
-import "../munged/governance/extensions/GovernorCountingSimple.sol";
-import "../munged/governance/extensions/GovernorVotes.sol";
-import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
-import "../munged/governance/extensions/GovernorTimelockControl.sol";
-import "../munged/governance/extensions/GovernorProposalThreshold.sol";
-
-/* 
-Wizard options:
-ProposalThreshhold = 10
-ERC20Votes
-TimelockController
-*/
-
-contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
-    constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction)
-        Governor(name)
-        GovernorVotes(_token)
-        GovernorVotesQuorumFraction(quorumFraction)
-        GovernorTimelockControl(_timelock)
-    {}
-
-    //HARNESS
-
-    function isExecuted(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].executed;
-    }
-    
-    function isCanceled(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].canceled;
-    }
-
-    uint256 _votingDelay;
-
-    uint256 _votingPeriod;
-
-    uint256 _proposalThreshold;
-
-    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
-
-    function _castVote(
-        uint256 proposalId,
-        address account,
-        uint8 support,
-        string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
-        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
-
-        return deltaWeight;        
-    }
-    
-    function snapshot(uint256 proposalId) public view returns (uint64) {
-        return _proposals[proposalId].voteStart._deadline;
-    }
-
-
-    function getExecutor() public view returns (address){
-        return _executor();
-    }
-
-    // original code, harnessed
-
-    function votingDelay() public view override returns (uint256) {     // HARNESS: pure -> view
-        return _votingDelay;                                            // HARNESS: parametric
-    }
-
-    function votingPeriod() public view override returns (uint256) {    // HARNESS: pure -> view
-        return _votingPeriod;                                           // HARNESS: parametric
-    }
-
-    function proposalThreshold() public view override returns (uint256) {   // HARNESS: pure -> view
-        return _proposalThreshold;                                          // HARNESS: parametric
-    }
-
-    // original code, not harnessed
-    // The following functions are overrides required by Solidity.
-
-    function quorum(uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotesQuorumFraction)
-        returns (uint256)
-    {
-        return super.quorum(blockNumber);
-    }
-
-    function getVotes(address account, uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotes)
-        returns (uint256)
-    {
-        return super.getVotes(account, 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, GovernorProposalThreshold, 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/WizardFirstTry.sol

@@ -1,141 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.2;
-
-import "../munged/governance/Governor.sol";
-import "../munged/governance/extensions/GovernorCountingSimple.sol";
-import "../munged/governance/extensions/GovernorVotes.sol";
-import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
-import "../munged/governance/extensions/GovernorTimelockCompound.sol";
-
-/* 
-Wizard options:
-ERC20Votes
-TimelockCompound
-*/
-
-contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
-    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
-        Governor(name)
-        GovernorVotes(_token)
-        GovernorVotesQuorumFraction(quorumFraction)
-        GovernorTimelockCompound(_timelock)
-    {}
-
-    //HARNESS
-
-    function isExecuted(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].executed;
-    }
-    
-    function isCanceled(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].canceled;
-    }
-
-    function snapshot(uint256 proposalId) public view returns (uint64) {
-        return _proposals[proposalId].voteStart._deadline;
-    }
-
-    function getExecutor() public view returns (address){
-        return _executor();
-    }
-
-    uint256 _votingDelay;
-
-    uint256 _votingPeriod;
-
-    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
-
-    function _castVote(
-        uint256 proposalId,
-        address account,
-        uint8 support,
-        string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
-        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
-
-        return deltaWeight;        
-    }
-
-    // original code, harnessed
-
-    function votingDelay() public view override virtual returns (uint256) {     // HARNESS: pure -> view
-        return _votingDelay;                                                    // HARNESS: parametric
-    }
-
-    function votingPeriod() public view override virtual returns (uint256) {    // HARNESS: pure -> view
-        return _votingPeriod;                                                   // HARNESS: parametric
-    }
-
-    // original code, not harnessed
-    // The following functions are overrides required by Solidity.
-
-    function quorum(uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotesQuorumFraction)
-        returns (uint256)
-    {
-        return super.quorum(blockNumber);
-    }
-
-    function getVotes(address account, uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotes)
-        returns (uint256)
-    {
-        return super.getVotes(account, blockNumber);
-    }
-
-    function state(uint256 proposalId)
-        public
-        view
-        override(Governor, GovernorTimelockCompound)
-        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, GovernorTimelockCompound)
-    {
-        super._execute(proposalId, targets, values, calldatas, descriptionHash);
-    }
-
-    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockCompound)
-        returns (uint256)
-    {
-        return super._cancel(targets, values, calldatas, descriptionHash);
-    }
-
-    function _executor()
-        internal
-        view
-        override(Governor, GovernorTimelockCompound)
-        returns (address)
-    {
-        return super._executor();
-    }
-
-    function supportsInterface(bytes4 interfaceId)
-        public
-        view
-        override(Governor, GovernorTimelockCompound)
-        returns (bool)
-    {
-        return super.supportsInterface(interfaceId);
-    }
-}

certora/munged/.gitignore

@@ -1,2 +0,0 @@
-*
-!.gitignore

certora/run.js

@@ -0,0 +1,109 @@
+#!/usr/bin/env node
+
+// USAGE:
+//    node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...]
+// EXAMPLES:
+//    node certora/run.js AccessControl
+//    node certora/run.js AccessControlHarness:AccessControl
+
+const MAX_PARALLEL = 4;
+
+const 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);
+
+let [, , request = '', ...extraOptions] = process.argv;
+if (request.startsWith('-')) {
+  extraOptions.unshift(request);
+  request = '';
+}
+const [reqSpec, reqContract] = request.split(':').reverse();
+
+for (const { spec, contract, files, options = [] } of Object.values(specs)) {
+  if ((!reqSpec || reqSpec === spec) && (!reqContract || reqContract === contract)) {
+    limit(runCertora, spec, contract, files, [...options, ...extraOptions]);
+  }
+}
+
+// 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 child = proc.spawn('certoraRun', args);
+
+  const stream = new PassThrough();
+  const output = collect(stream);
+
+  child.stdout.pipe(stream, { end: false });
+  child.stderr.pipe(stream, { end: false });
+
+  // as soon as we have a jobStatus link, print it
+  stream.on('data', function logStatusUrl(data) {
+    const urls = data.toString('utf8').match(/https?:\S*/g);
+    for (const url of urls ?? []) {
+      if (url.includes('/jobStatus/')) {
+        console.error(`[${spec}] ${url}`);
+        stream.off('data', logStatusUrl);
+        break;
+      }
+    }
+  });
+
+  // wait for process end
+  const [code, signal] = await events.once(child, 'exit');
+
+  // error
+  if (code || signal) {
+    console.error(`[${spec}] Exited with code ${code || signal}`);
+    process.exitCode = 1;
+  }
+
+  // get all output
+  stream.end();
+
+  // write results in markdown format
+  writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)[0]);
+
+  // write all details
+  console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));
+}
+
+// Collects stream data into a string
+async function collect(stream) {
+  const buffers = [];
+  for await (const data of stream) {
+    const buf = Buffer.isBuffer(data) ? data : Buffer.from(data);
+    buffers.push(buf);
+  }
+  return Buffer.concat(buffers).toString('utf8');
+}
+
+// Formatting
+let hasHeader = false;
+
+function formatRow(...array) {
+  return ['', ...array, ''].join(' | ');
+}
+
+function writeHeader() {
+  console.log(formatRow('spec', 'contract', 'result', 'status', 'output'));
+  console.log(formatRow('-', '-', '-', '-', '-'));
+}
+
+function writeEntry(spec, contract, success, url) {
+  if (!hasHeader) {
+    hasHeader = true;
+    writeHeader();
+  }
+  console.log(
+    formatRow(
+      spec,
+      contract,
+      success ? ':x:' : ':heavy_check_mark:',
+      `[link](${url})`,
+      `[link](${url.replace('/jobStatus/', '/output/')})`,
+    ),
+  );
+}

certora/scripts/Governor.sh

@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
-    --verify GovernorHarness:certora/specs/GovernorBase.spec \
-    --solc solc8.0 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule voteStartBeforeVoteEnd \
-    --msg "$1"

certora/scripts/GovernorCountingSimple-counting.sh

@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
-    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
-    --solc solc8.2 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule hasVotedCorrelation \
-    --msg "$1"

certora/scripts/WizardControlFirstPriority.sh

@@ -1,12 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
-    --link WizardControlFirstPriority:token=ERC20VotesHarness \
-    --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
-    --solc solc8.2 \
-    --disableLocalTypeChecking \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule canVoteDuringVotingPeriod \
-    --msg "$1"

certora/scripts/WizardFirstTry.sh

@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
-    --verify WizardFirstTry:certora/specs/GovernorBase.spec \
-    --solc solc8.2 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --disableLocalTypeChecking \
-    --settings -copyLoopUnroll=4 \
-    --msg "$1"

certora/scripts/sanity.sh

@@ -1,14 +0,0 @@
-make -C certora munged
-
-for f in certora/harnesses/Wizard*.sol
-do
-    echo "Processing $f"
-    file="$(basename $f)"
-    echo ${file%.*}
-    certoraRun certora/harnesses/$file \
-    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
-    --solc solc8.2 --staging shelly/forSasha \
-    --optimistic_loop \
-    --msg "checking sanity on ${file%.*}"
-    --settings -copyLoopUnroll=4
-done

certora/scripts/verifyAll.sh

@@ -1,39 +0,0 @@
-#!/bin/bash
-
-make -C certora munged
-
-for contract in certora/harnesses/Wizard*.sol;
-do
-    for spec in certora/specs/*.spec;
-    do      
-        contractFile="$(basename $contract)"
-        specFile="$(basename $spec)"
-        if [[ "${specFile%.*}" != "RulesInProgress" ]];
-        then
-            echo "Processing ${contractFile%.*} with $specFile"
-            if [[ "${contractFile%.*}" = *"WizardControl"* ]];
-            then
-                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
-                --link ${contractFile%.*}:token=ERC20VotesHarness \
-                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
-                --staging shelly/forSasha \
-                --disableLocalTypeChecking \
-                --optimistic_loop \
-                --settings -copyLoopUnroll=4 \
-                --send_only \
-                --msg "checking $specFile on ${contractFile%.*}"
-            else
-                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
-                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
-                --staging shelly/forSasha \
-                --disableLocalTypeChecking \
-                --optimistic_loop \
-                --settings -copyLoopUnroll=4 \
-                --send_only \
-                --msg "checking $specFile on ${contractFile%.*}"
-            fi
-        fi
-    done
-done

certora/specs.json

@@ -0,0 +1,22 @@
+[
+  {
+    "spec": "AccessControl",
+    "contract": "AccessControlHarness",
+    "files": ["certora/harnesses/AccessControlHarness.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"]
+  }
+]

certora/specs/AccessControl.spec

@@ -0,0 +1,114 @@
+import "helpers.spec"
+
+methods {
+    hasRole(bytes32, address) returns(bool) envfree
+    getRoleAdmin(bytes32) returns(bytes32) envfree
+    grantRole(bytes32, address)
+    revokeRole(bytes32, address)
+    renounceRole(bytes32, address)
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyGrantCanGrant(env e, bytes32 role, address account) {
+    method f; calldataarg args;
+
+    bool hasRoleBefore = hasRole(role, account);
+    f(e, args);
+    bool hasRoleAfter = hasRole(role, account);
+
+    assert (
+        !hasRoleBefore &&
+        hasRoleAfter
+    ) => (
+        f.selector == grantRole(bytes32, address).selector
+    );
+
+    assert (
+        hasRoleBefore &&
+        !hasRoleAfter
+    ) => (
+        f.selector == revokeRole(bytes32, address).selector ||
+        f.selector == renounceRole(bytes32, address).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: grantRole only affects the specified user/role combo                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule grantRoleEffect(env e) {
+    require nonpayable(e);
+
+    bytes32 role1; bytes32 role2;
+    address account1; address account2;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
+    bool hasRoleBefore = hasRole(role1, account1);
+
+    grantRole@withrevert(e, role2, account2);
+    assert !lastReverted <=> isCallerAdmin;
+
+    bool hasRoleAfter = hasRole(role1, account1);
+
+    assert (
+        hasRoleBefore != hasRoleAfter
+    ) => (
+        hasRoleAfter == true && role1 == role2 && account1 == account2
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: revokeRole only affects the specified user/role combo                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule revokeRoleEffect(env e) {
+    require nonpayable(e);
+
+    bytes32 role1; bytes32 role2;
+    address account1; address account2;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
+    bool hasRoleBefore = hasRole(role1, account1);
+
+    revokeRole@withrevert(e, role2, account2);
+    assert !lastReverted <=> isCallerAdmin;
+
+    bool hasRoleAfter = hasRole(role1, account1);
+
+    assert (
+        hasRoleBefore != hasRoleAfter
+    ) => (
+        hasRoleAfter == false && role1 == role2 && account1 == account2
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceRole only affects the specified user/role combo                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceRoleEffect(env e) {
+    require nonpayable(e);
+
+    bytes32 role1; bytes32 role2;
+    address account1; address account2;
+
+    bool hasRoleBefore = hasRole(role1, account1);
+
+    renounceRole@withrevert(e, role2, account2);
+    assert !lastReverted <=> account2 == e.msg.sender;
+
+    bool hasRoleAfter = hasRole(role1, account1);
+
+    assert (
+        hasRoleBefore != hasRoleAfter
+    ) => (
+        hasRoleAfter == false && role1 == role2 && account1 == account2
+    );
+}

certora/specs/ERC20.spec

@@ -0,0 +1,414 @@
+import "helpers.spec"
+import "methods/IERC20.spec"
+import "methods/IERC2612.spec"
+
+methods {
+    // non standard ERC20 functions
+    increaseAllowance(address,uint256) returns (bool)
+    decreaseAllowance(address,uint256) returns (bool)
+
+    // exposed for FV
+    mint(address,uint256)
+    burn(address,uint256)
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost & hooks: sum of all balances                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost sumOfBalances() returns uint256 {
+  init_state axiom sumOfBalances() == 0;
+}
+
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: totalSupply is the sum of all balances                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant totalSupplyIsSumOfBalances()
+    totalSupply() == sumOfBalances()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: balance of address(0) is 0                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant zeroAddressNoBalance()
+    balanceOf(0) == 0
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only mint and burn can change total supply                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noChangeTotalSupply(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    method f;
+    calldataarg args;
+
+    uint256 totalSupplyBefore = totalSupply();
+    f(e, args);
+    uint256 totalSupplyAfter = totalSupply();
+
+    assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector;
+    assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAuthorizedCanTransfer(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    method f;
+    calldataarg args;
+    address account;
+
+    uint256 allowanceBefore = allowance(account, e.msg.sender);
+    uint256 balanceBefore   = balanceOf(account);
+    f(e, args);
+    uint256 balanceAfter    = balanceOf(account);
+
+    assert (
+        balanceAfter < balanceBefore
+    ) => (
+        f.selector == burn(address,uint256).selector ||
+        e.msg.sender == account ||
+        balanceBefore - balanceAfter <= allowanceBefore
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder (or a permit) can increase allowance. The spender can decrease it by using it          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyHolderOfSpenderCanChangeAllowance(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    method f;
+    calldataarg args;
+    address holder;
+    address spender;
+
+    uint256 allowanceBefore = allowance(holder, spender);
+    f(e, args);
+    uint256 allowanceAfter = allowance(holder, spender);
+
+    assert (
+        allowanceAfter > allowanceBefore
+    ) => (
+        (f.selector == approve(address,uint256).selector           && e.msg.sender == holder) ||
+        (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
+        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+    );
+
+    assert (
+        allowanceAfter < allowanceBefore
+    ) => (
+        (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
+        (f.selector == approve(address,uint256).selector              && e.msg.sender == holder ) ||
+        (f.selector == decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
+        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: mint behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mint(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address to;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 toBalanceBefore    = balanceOf(to);
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // run transaction
+    mint@withrevert(e, to, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert to == 0 || totalSupplyBefore + amount > max_uint256;
+    } else {
+        // updates balance and totalSupply
+        assert balanceOf(to) == toBalanceBefore   + amount;
+        assert totalSupply() == totalSupplyBefore + amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == to;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: burn behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule burn(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address from;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 fromBalanceBefore  = balanceOf(from);
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // run transaction
+    burn@withrevert(e, from, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert from == 0 || fromBalanceBefore < amount;
+    } else {
+        // updates balance and totalSupply
+        assert balanceOf(from) == fromBalanceBefore   - amount;
+        assert totalSupply()   == totalSupplyBefore - amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == from;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transfer behavior and side effects                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transfer(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address recipient;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 holderBalanceBefore    = balanceOf(holder);
+    uint256 recipientBalanceBefore = balanceOf(recipient);
+    uint256 otherBalanceBefore     = balanceOf(other);
+
+    // run transaction
+    transfer@withrevert(e, recipient, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || recipient == 0 || amount > holderBalanceBefore;
+    } else {
+        // balances of holder and recipient are updated
+        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transferFrom behavior and side effects                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferFrom(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address spender = e.msg.sender;
+    address holder;
+    address recipient;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 allowanceBefore        = allowance(holder, spender);
+    uint256 holderBalanceBefore    = balanceOf(holder);
+    uint256 recipientBalanceBefore = balanceOf(recipient);
+    uint256 otherBalanceBefore     = balanceOf(other);
+
+    // run transaction
+    transferFrom@withrevert(e, holder, recipient, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore;
+    } else {
+        // allowance is valid & updated
+        assert allowanceBefore            >= amount;
+        assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
+
+        // balances of holder and recipient are updated
+        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: approve behavior and side effects                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approve(env e) {
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // cache state
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    approve@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || spender == 0;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: increaseAllowance behavior and side effects                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule increaseAllowance(env e) {
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    increaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == allowanceBefore + amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: decreaseAllowance behavior and side effects                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule decreaseAllowance(env e) {
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    decreaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || spender == 0 || allowanceBefore < amount;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == allowanceBefore - amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: permit behavior and side effects                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule permit(env e) {
+    require nonpayable(e);
+
+    address holder;
+    address spender;
+    uint256 amount;
+    uint256 deadline;
+    uint8 v;
+    bytes32 r;
+    bytes32 s;
+
+    address account1;
+    address account2;
+    address account3;
+
+    // cache state
+    uint256 nonceBefore          = nonces(holder);
+    uint256 otherNonceBefore     = nonces(account1);
+    uint256 otherAllowanceBefore = allowance(account2, account3);
+
+    // sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice
+    require nonceBefore      < max_uint256;
+    require otherNonceBefore < max_uint256;
+
+    // run transaction
+    permit@withrevert(e, holder, spender, amount, deadline, v, r, s);
+
+    // check outcome
+    if (lastReverted) {
+        // Without formally checking the signature, we can't verify exactly the revert causes
+        assert true;
+    } else {
+        // allowance and nonce are updated
+        assert allowance(holder, spender) == amount;
+        assert nonces(holder) == nonceBefore + 1;
+
+        // deadline was respected
+        assert deadline >= e.block.timestamp;
+
+        // no other allowance or nonce is modified
+        assert nonces(account1)              != otherNonceBefore     => account1 == holder;
+        assert allowance(account2, account3) != otherAllowanceBefore => (account2 == holder && account3 == spender);
+    }
+}

certora/specs/ERC20FlashMint.spec

@@ -0,0 +1,48 @@
+import "helpers.spec"
+import "methods/IERC20.spec"
+import "methods/IERC3156.spec"
+
+methods {
+    // non standard ERC3156 functions
+    flashFeeReceiver() returns (address) envfree
+
+    // function summaries below
+    _mint(address account, uint256 amount)              => specMint(account, amount)
+    _burn(address account, uint256 amount)              => specBurn(account, amount)
+    _transfer(address from, address to, uint256 amount) => specTransfer(from, to, amount)
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost: track mint and burns in the CVL                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost mapping(address => uint256)                     trackedMintAmount;
+ghost mapping(address => uint256)                     trackedBurnAmount;
+ghost mapping(address => mapping(address => uint256)) trackedTransferedAmount;
+
+function specMint(address account, uint256 amount)              returns bool { trackedMintAmount[account] = amount;        return true; }
+function specBurn(address account, uint256 amount)              returns bool { trackedBurnAmount[account] = amount;        return true; }
+function specTransfer(address from, address to, uint256 amount) returns bool { trackedTransferedAmount[from][to] = amount; return true; }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: When doing a flashLoan, "amount" is minted and burnt, additionally, the fee is either burnt                   │
+│ (if the fee recipient is 0) or transferred (if the fee recipient is not 0)                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule checkMintAndBurn(env e) {
+    address receiver;
+    address token;
+    uint256 amount;
+    bytes data;
+
+    uint256 fees = flashFee(token, amount);
+    address recipient = flashFeeReceiver();
+
+    flashLoan(e, receiver, token, amount, data);
+
+    assert trackedMintAmount[receiver] == amount;
+    assert trackedBurnAmount[receiver] == amount + (recipient == 0 ? fees : 0);
+    assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == fees;
+}

certora/specs/GovernorBase.spec

@@ -1,333 +0,0 @@
-//////////////////////////////////////////////////////////////////////////////
-///////////////////// Governor.sol base definitions //////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
-    proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd
-    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
-    isExecuted(uint256) returns bool envfree
-    isCanceled(uint256) returns bool envfree
-    execute(address[], uint256[], bytes[], bytes32) returns uint256
-    hasVoted(uint256, address) returns bool
-    castVote(uint256, uint8) returns uint256
-    updateQuorumNumerator(uint256)
-    queue(address[], uint256[], bytes[], bytes32) returns uint256
-
-    // internal functions made public in harness:
-    _quorumReached(uint256) returns bool
-    _voteSucceeded(uint256) returns bool envfree
-
-    // function summarization
-    proposalThreshold() returns uint256 envfree
-
-    getVotes(address, uint256) returns uint256 => DISPATCHER(true)
-
-    getPastTotalSupply(uint256 t) returns uint256      => PER_CALLEE_CONSTANT
-    getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT
-
-    //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
-    //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
-}
-
-//////////////////////////////////////////////////////////////////////////////
-//////////////////////////////// Definitions /////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-// proposal was created - relation proved in noStartBeforeCreation
-definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////// Helper Functions ///////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
-    address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash;
-    uint8 support; uint8 v; bytes32 r; bytes32 s;
-	if (f.selector == propose(address[], uint256[], bytes[], string).selector) {
-		uint256 result = propose@withrevert(e, targets, values, calldatas, reason);
-        require(result == proposalId);
-	} else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) {
-		uint256 result = execute@withrevert(e, targets, values, calldatas, descriptionHash);
-        require(result == proposalId);
-	} else if (f.selector == castVote(uint256, uint8).selector) {
-		castVote@withrevert(e, proposalId, support);
-	} else if  (f.selector == castVoteWithReason(uint256, uint8, string).selector) {
-        castVoteWithReason@withrevert(e, proposalId, support, reason);
-	} else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) {
-		castVoteBySig@withrevert(e, proposalId, support, v, r, s);
-    } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) {
-        queue@withrevert(e, targets, values, calldatas, descriptionHash);
-	} else {
-        calldataarg args;
-        f@withrevert(e, args);
-    }
-}
-
-/*
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
- ///////////////////////////////////////////////////// State Diagram //////////////////////////////////////////////////////////
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
- //                                                                                                                          //
- //                                                                castVote(s)()                                             //
- //  -------------  propose()  ----------------------  time pass  ---------------       time passes         -----------      //
- // | No Proposal | --------> | Before Start (Delay) | --------> | Voting Period | ----------------------> | execute() |     //
- //  -------------             ----------------------             --------------- -> Executed/Canceled      -----------      //
- //  ------------------------------------------------------------|---------------|-------------------------|-------------->  //
- // t                                                          start            end                     timelock             //
- //                                                                                                                          //
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-*/
-
-
-///////////////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// Global Valid States /////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * Start and end date 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)
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant startAndEndDatesNonZero(uint256 pId)
-        proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0
-        { preserved with (env e){
-                require e.block.number > 0;
-        }}
-
-
-/*
- * If a proposal is canceled it must have a start and an end date
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant canceledImplyStartAndEndDateNonZero(uint pId)
-        isCanceled(pId) => proposalSnapshot(pId) != 0
-        {preserved with (env e){
-                require e.block.number > 0;
-        }}
-
-
-/*
- * If a proposal is executed it must have a start and an end date
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant executedImplyStartAndEndDateNonZero(uint pId)
-        isExecuted(pId) => proposalSnapshot(pId) != 0
-        { preserved with (env e){
-            requireInvariant startAndEndDatesNonZero(pId);
-            require e.block.number > 0;
-        }}
-
-
-/*
- * A proposal starting block number must be less or equal than the proposal end date
- */
-invariant voteStartBeforeVoteEnd(uint256 pId)
-        // from < to <= because snapshot and deadline can be the same block number if delays are set to 0
-        // This is possible before the integration of GovernorSettings.sol to the system.
-        // After integration of GovernorSettings.sol the invariant expression should be changed from <= to <
-        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) <= proposalDeadline(pId))
-        // (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) <= proposalDeadline(pId))
-        { preserved {
-            requireInvariant startAndEndDatesNonZero(pId);
-        }}
-
-
-/*
- * A proposal cannot be both executed and canceled simultaneously.
- */
-invariant noBothExecutedAndCanceled(uint256 pId)
-        !isExecuted(pId) || !isCanceled(pId)
-
-
-/*
- * A proposal could be executed only if quorum was reached and vote succeeded
- */
-rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){
-    bool isExecutedBefore = isExecuted(pId);
-    bool quorumReachedBefore = _quorumReached(e, pId);
-    bool voteSucceededBefore = _voteSucceeded(pId);
-
-    calldataarg args;
-    f(e, args);
-
-    bool isExecutedAfter = isExecuted(pId);
-    assert (!isExecutedBefore && isExecutedAfter) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed";
-}
-
-///////////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////// In-State Rules /////////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-//==========================================
-//------------- Voting Period --------------
-//==========================================
-
-/*
- * A user cannot vote twice
- */
- // Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on
- // the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute.
- // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
- // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
- // We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete
- // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
-rule doubleVoting(uint256 pId, uint8 sup, method f) {
-    env e;
-    address user = e.msg.sender;
-    bool votedCheck = hasVoted(e, pId, user);
-
-    castVote@withrevert(e, pId, sup);
-
-    assert votedCheck => lastReverted, "double voting occurred";
-}
-
-
-///////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////// State Transitions Rules //////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-//===========================================
-//-------- Propose() --> End of Time --------
-//===========================================
-
-
-/*
- * Once a proposal is created, voteStart and voteEnd are immutable
- */
-rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
-    uint256 _voteStart = proposalSnapshot(pId);
-    uint256 _voteEnd = proposalDeadline(pId);
-
-    require proposalCreated(pId); // startDate > 0
-
-    env e; calldataarg arg;
-    f(e, arg);
-
-    uint256 voteStart_ = proposalSnapshot(pId);
-    uint256 voteEnd_ = proposalDeadline(pId);
-    assert _voteStart == voteStart_, "Start date was changed";
-    assert _voteEnd == voteEnd_, "End date was changed";
-}
-
-
-/*
- * Voting cannot start at a block number prior to proposal’s creation block number
- */
-rule noStartBeforeCreation(uint256 pId) {
-    uint256 previousStart = proposalSnapshot(pId);
-    // This line makes sure that we see only cases where start date is changed from 0, i.e. creation of proposal
-    // We proved in immutableFieldsAfterProposalCreation that once dates set for proposal, it cannot be changed
-    require !proposalCreated(pId); // previousStart == 0;
-
-    env e; calldataarg args;
-    propose(e, args);
-
-    uint256 newStart = proposalSnapshot(pId);
-    // if created, start is after current block number (creation block)
-    assert(newStart != previousStart => newStart >= e.block.number);
-}
-
-
-//============================================
-//--- End of Voting Period --> End of Time ---
-//============================================
-
-
-/*
- * A proposal can neither be executed nor canceled before it ends
- */
- // By induction it cannot be executed nor canceled before it starts, due to voteStartBeforeVoteEnd
-rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
-    require !isExecuted(pId) && !isCanceled(pId);
-
-    env e; calldataarg args;
-    f(e, args);
-
-    assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline";
-}
-
-////////////////////////////////////////////////////////////////////////////////
-////////////////////// Integrity Of Functions (Unit Tests) /////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////// High Level Rules ////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////////////
-///////////////////////////// Not Categorized Yet //////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * All proposal specific (non-view) functions should revert if proposal is executed
- */
- // In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID,
- // non of the proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc
- // we connected the executed attribute to the execute() function, showing that only execute() can
- // change it, and that it will always change it.
-rule allFunctionsRevertIfExecuted(method f) filtered { f ->
-    !f.isView && !f.isFallback
-      && f.selector != updateTimelock(address).selector
-      && f.selector != updateQuorumNumerator(uint256).selector
-      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
-      && f.selector != relay(address,uint256,bytes).selector
-      && f.selector != 0xb9a61961 // __acceptAdmin()
-} {
-    env e; calldataarg args;
-    uint256 pId;
-    require(isExecuted(pId));
-    requireInvariant noBothExecutedAndCanceled(pId);
-    requireInvariant executedImplyStartAndEndDateNonZero(pId);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    assert(lastReverted, "Function was not reverted");
-}
-
-/*
- * All proposal specific (non-view) functions should revert if proposal is canceled
- */
-rule allFunctionsRevertIfCanceled(method f) filtered {
-    f -> !f.isView && !f.isFallback
-      && f.selector != updateTimelock(address).selector
-      && f.selector != updateQuorumNumerator(uint256).selector
-      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
-      && f.selector != relay(address,uint256,bytes).selector
-      && f.selector != 0xb9a61961 // __acceptAdmin()
-} {
-    env e; calldataarg args;
-    uint256 pId;
-    require(isCanceled(pId));
-    requireInvariant noBothExecutedAndCanceled(pId);
-    requireInvariant canceledImplyStartAndEndDateNonZero(pId);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    assert(lastReverted, "Function was not reverted");
-}
-
-/*
- * Proposal can be switched to executed only via execute() function
- */
-rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) {
-    env e; calldataarg args;
-    uint256 pId;
-    bool executedBefore = isExecuted(pId);
-    require(!executedBefore);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    bool executedAfter = isExecuted(pId);
-    assert(executedAfter != executedBefore => f.selector == execute(address[], uint256[], bytes[], bytes32).selector, "isExecuted only changes in the execute method");
-}

certora/specs/GovernorCountingSimple.spec

@@ -1,221 +0,0 @@
-import "GovernorBase.spec"
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
-
-    quorum(uint256) returns uint256
-    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
-
-    quorumNumerator() returns uint256
-    _executor() returns address
-
-    erc20votes._getPastVotes(address, uint256) returns uint256
-
-    getExecutor() returns address
-
-    timelock() returns address
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// GHOSTS /////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//////////// ghosts to keep track of votes counting ////////////
-
-/*
- * the sum of voting power of those who voted
- */
-ghost sum_all_votes_power() returns uint256 {
-	init_state axiom sum_all_votes_power() == 0;
-}
-
-hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
-	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
-}
-
-/*
- * sum of all votes casted per proposal
- */
-ghost tracked_weight(uint256) returns uint256 {
-	init_state axiom forall uint256 p. tracked_weight(p) == 0;
-}
-
-/*
- * sum of all votes casted
- */
-ghost sum_tracked_weight() returns uint256 {
-	init_state axiom sum_tracked_weight() == 0;
-}
-
-/*
- * getter for _proposalVotes.againstVotes
- */
-ghost votesAgainst() returns uint256 {
-    init_state axiom votesAgainst() == 0;
-}
-
-/*
- * getter for _proposalVotes.forVotes
- */
-ghost votesFor() returns uint256 {
-    init_state axiom votesFor() == 0;
-}
-
-/*
- * getter for _proposalVotes.abstainVotes
- */
-ghost votesAbstain() returns uint256 {
-    init_state axiom votesAbstain() == 0;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-////////////////////////////// INVARIANTS ////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal
- */
-invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId) 
-	tracked_weight(pId) == ghost_sum_vote_power_by_id(pId)
-
-
-/*
- * sum of all votes casted is equal to the sum of voting power of those who voted
- */
-invariant SumOfVotesCastEqualSumOfPowerOfVoted() 
-	sum_tracked_weight() == sum_all_votes_power()
-
-
-/*
-* sum of all votes casted is greater or equal to the sum of voting power of those who voted at a specific proposal
-*/
-invariant OneIsNotMoreThanAll(uint256 pId) 
-	sum_all_votes_power() >= tracked_weight(pId)
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// RULES //////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * Only sender's voting status can be changed by execution of any cast vote function
- */
-// Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on
- // the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute.
- // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
- // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
- // We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete 
- // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
-rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) {
-    env e; calldataarg args;
-
-    address voter = e.msg.sender;
-    address user;
-
-    bool hasVotedBefore_User = hasVoted(e, pId, user);
-
-    castVote@withrevert(e, pId, sup);
-    require(!lastReverted);
-
-    bool hasVotedAfter_User = hasVoted(e, pId, user);
-
-    assert user != voter => hasVotedBefore_User == hasVotedAfter_User;
-}
-
-
-/*
-* Total voting tally is monotonically non-decreasing in every operation 
-*/
-rule votingWeightMonotonicity(method f){
-    uint256 votingWeightBefore = sum_tracked_weight();
-
-    env e; 
-    calldataarg args;
-    f(e, args);
-
-    uint256 votingWeightAfter = sum_tracked_weight();
-
-    assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow";
-}
-
-
-/*
-* A change in hasVoted must be correlated with an non-decreasing of the vote supports (nondecrease because user can vote with weight 0)
-*/
-rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
-    address acc = e.msg.sender;
-    
-    uint256 againstBefore = votesAgainst();
-    uint256 forBefore = votesFor();
-    uint256 abstainBefore = votesAbstain();
-
-    bool hasVotedBefore = hasVoted(e, pId, acc);
-
-    helperFunctionsWithRevert(pId, f, e);
-    require(!lastReverted);
-
-    uint256 againstAfter = votesAgainst();
-    uint256 forAfter = votesFor();
-    uint256 abstainAfter = votesAbstain();
-    
-    bool hasVotedAfter = hasVoted(e, pId, acc);
-
-    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
-}
-
-
-/*
-* Only privileged users can execute privileged operations, e.g. change _quorumNumerator or _timelock
-*/
-rule privilegedOnlyNumerator(method f, uint256 newQuorumNumerator){
-    env e;
-    calldataarg arg;
-    uint256 quorumNumBefore = quorumNumerator(e);
-
-    f(e, arg);
-
-    uint256 quorumNumAfter = quorumNumerator(e);
-    address executorCheck = getExecutor(e);
-
-    assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non privileged user changed quorum numerator";
-}
-
-rule privilegedOnlyTimelock(method f, uint256 newQuorumNumerator){
-    env e;
-    calldataarg arg;
-    uint256 timelockBefore = timelock(e);
-
-    f(e, arg);
-
-    uint256 timelockAfter = timelock(e);
-
-    assert timelockBefore != timelockAfter => e.msg.sender == timelockBefore, "non privileged user changed timelock";
-}

certora/specs/RulesInProgress.spec

@@ -1,139 +0,0 @@
-//////////////////////////////////////////////////////////////////////////////
-////////////// THIS SPEC IS A RESERVE FOR NOT IN PROGRESS //////////////
-//////////////////////////////////////////////////////////////////////////////
-
-import "GovernorBase.spec"
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
-
-    quorum(uint256) returns uint256
-    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
-
-    quorumNumerator() returns uint256
-    _executor() returns address
-
-    erc20votes._getPastVotes(address, uint256) returns uint256
-
-    getExecutor() returns address
-
-    timelock() returns address
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// GHOSTS /////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//////////// ghosts to keep track of votes counting ////////////
-
-/*
- * the sum of voting power of those who voted
- */
-ghost sum_all_votes_power() returns uint256 {
-	init_state axiom sum_all_votes_power() == 0;
-}
-
-hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
-	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
-}
-
-/*
- * sum of all votes casted per proposal
- */
-ghost tracked_weight(uint256) returns uint256 {
-	init_state axiom forall uint256 p. tracked_weight(p) == 0;
-}
-
-/*
- * sum of all votes casted
- */
-ghost sum_tracked_weight() returns uint256 {
-	init_state axiom sum_tracked_weight() == 0;
-}
-
-/*
- * getter for _proposalVotes.againstVotes
- */
-ghost votesAgainst() returns uint256 {
-    init_state axiom votesAgainst() == 0;
-}
-
-/*
- * getter for _proposalVotes.forVotes
- */
-ghost votesFor() returns uint256 {
-    init_state axiom votesFor() == 0;
-}
-
-/*
- * getter for _proposalVotes.abstainVotes
- */
-ghost votesAbstain() returns uint256 {
-    init_state axiom votesAbstain() == 0;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-////////////////////////////// INVARIANTS ////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// RULES //////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//NOT FINISHED
-/*
-* the sum of voting power of those who voted is less or equal to the maximum possible votes, per each proposal
-*/
-rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
-
-    // add requireinvariant  for all i, j. i = i - 1 && i < j => checkpointlookup[i] < checkpointlookup[j];
-    require tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId));
-
-    uint256 againstB;
-    uint256 forB;
-    uint256 absatinB;
-    againstB, forB, absatinB = proposalVotes(pId);
-
-    calldataarg args;
-    //f(e, args);
-
-    castVote(e, pId, sup);
-
-    uint256 against;
-    uint256 for;
-    uint256 absatin;
-    against, for, absatin = proposalVotes(pId);
-
-    uint256 ps = proposalSnapshot(pId);
-
-    assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
-}

certora/specs/helpers.spec

@@ -0,0 +1 @@
+definition nonpayable(env e) returns bool = e.msg.value == 0;

certora/specs/methods/IERC20.spec

@@ -0,0 +1,11 @@
+methods {
+    name()                                returns (string)  envfree => DISPATCHER(true)
+    symbol()                              returns (string)  envfree => DISPATCHER(true)
+    decimals()                            returns (uint8)   envfree => DISPATCHER(true)
+    totalSupply()                         returns (uint256) envfree => DISPATCHER(true)
+    balanceOf(address)                    returns (uint256) envfree => DISPATCHER(true)
+    allowance(address,address)            returns (uint256) envfree => DISPATCHER(true)
+    approve(address,uint256)              returns (bool)            => DISPATCHER(true)
+    transfer(address,uint256)             returns (bool)            => DISPATCHER(true)
+    transferFrom(address,address,uint256) returns (bool)            => DISPATCHER(true)
+}

certora/specs/methods/IERC2612.spec

@@ -0,0 +1,5 @@
+methods {
+    permit(address,address,uint256,uint256,uint8,bytes32,bytes32) => DISPATCHER(true)
+    nonces(address)    returns (uint256) envfree                  => DISPATCHER(true)
+    DOMAIN_SEPARATOR() returns (bytes32) envfree                  => DISPATCHER(true)
+}

certora/specs/methods/IERC3156.spec

@@ -0,0 +1,5 @@
+methods {
+    maxFlashLoan(address)                    returns (uint256) envfree => DISPATCHER(true)
+    flashFee(address,uint256)                returns (uint256) envfree => DISPATCHER(true)
+    flashLoan(address,address,uint256,bytes) returns (bool)            => DISPATCHER(true)
+}

certora/specs/sanity.spec

@@ -1,14 +0,0 @@
-/*
-This rule looks for a non-reverting execution path to each method, including those overridden in the harness.
-A method has such an execution path if it violates this rule.
-How it works:
-    - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails.
-    - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously.
-*/
-	
-rule sanity(method f) {
-    env e;
-    calldataarg arg;
-    f(e, arg);
-    assert false;
-}

package-lock.json

@@ -39,6 +39,7 @@
         "lodash.zip": "^4.2.0",
         "merkletreejs": "^0.2.13",
         "micromatch": "^4.0.2",
+        "p-limit": "^3.1.0",
         "prettier": "^2.8.1",
         "prettier-plugin-solidity": "^1.1.0",
         "rimraf": "^3.0.2",
@@ -215,6 +216,21 @@
         "changeset": "bin.js"
       }
     },
+    "node_modules/@changesets/cli/node_modules/p-limit": {
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+      "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+      "dev": true,
+      "dependencies": {
+        "p-try": "^2.0.0"
+      },
+      "engines": {
+        "node": ">=6"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/sindresorhus"
+      }
+    },
     "node_modules/@changesets/cli/node_modules/semver": {
       "version": "5.7.1",
       "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.1.tgz",
@@ -5375,21 +5391,6 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
-    "node_modules/eslint/node_modules/p-limit": {
-      "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
-      "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
-      "dev": true,
-      "dependencies": {
-        "yocto-queue": "^0.1.0"
-      },
-      "engines": {
-        "node": ">=10"
-      },
-      "funding": {
-        "url": "https://github.com/sponsors/sindresorhus"
-      }
-    },
     "node_modules/eslint/node_modules/p-locate": {
       "version": "5.0.0",
       "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz",
@@ -5835,6 +5836,21 @@
         "node": ">= 0.4"
       }
     },
+    "node_modules/eth-gas-reporter/node_modules/p-limit": {
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+      "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+      "dev": true,
+      "dependencies": {
+        "p-try": "^2.0.0"
+      },
+      "engines": {
+        "node": ">=6"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/sindresorhus"
+      }
+    },
     "node_modules/eth-gas-reporter/node_modules/p-locate": {
       "version": "3.0.0",
       "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz",
@@ -9516,21 +9532,6 @@
       "integrity": "sha512-6FlzubTLZG3J2a/NVCAleEhjzq5oxgHyaCU9yYXvcLsvoVaHJq/s5xXI6/XXP6tz7R9xAOtHnSO/tXtF3WRTlA==",
       "dev": true
     },
-    "node_modules/mocha/node_modules/p-limit": {
-      "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
-      "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
-      "dev": true,
-      "dependencies": {
-        "yocto-queue": "^0.1.0"
-      },
-      "engines": {
-        "node": ">=10"
-      },
-      "funding": {
-        "url": "https://github.com/sponsors/sindresorhus"
-      }
-    },
     "node_modules/mocha/node_modules/p-locate": {
       "version": "5.0.0",
       "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz",
@@ -10108,15 +10109,15 @@
       }
     },
     "node_modules/p-limit": {
-      "version": "2.3.0",
-      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
-      "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+      "version": "3.1.0",
+      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
+      "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
       "dev": true,
       "dependencies": {
-        "p-try": "^2.0.0"
+        "yocto-queue": "^0.1.0"
       },
       "engines": {
-        "node": ">=6"
+        "node": ">=10"
       },
       "funding": {
         "url": "https://github.com/sponsors/sindresorhus"
@@ -10134,6 +10135,21 @@
         "node": ">=8"
       }
     },
+    "node_modules/p-locate/node_modules/p-limit": {
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+      "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+      "dev": true,
+      "dependencies": {
+        "p-try": "^2.0.0"
+      },
+      "engines": {
+        "node": ">=6"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/sindresorhus"
+      }
+    },
     "node_modules/p-map": {
       "version": "4.0.0",
       "resolved": "https://registry.npmjs.org/p-map/-/p-map-4.0.0.tgz",
@@ -10456,21 +10472,6 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
-    "node_modules/preferred-pm/node_modules/p-limit": {
-      "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
-      "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
-      "dev": true,
-      "dependencies": {
-        "yocto-queue": "^0.1.0"
-      },
-      "engines": {
-        "node": ">=10"
-      },
-      "funding": {
-        "url": "https://github.com/sponsors/sindresorhus"
-      }
-    },
     "node_modules/preferred-pm/node_modules/p-locate": {
       "version": "5.0.0",
       "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz",
@@ -12942,6 +12943,21 @@
         "node": ">= 0.4"
       }
     },
+    "node_modules/solidity-coverage/node_modules/p-limit": {
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+      "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+      "dev": true,
+      "dependencies": {
+        "p-try": "^2.0.0"
+      },
+      "engines": {
+        "node": ">=6"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/sindresorhus"
+      }
+    },
     "node_modules/solidity-coverage/node_modules/p-locate": {
       "version": "3.0.0",
       "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz",
@@ -15347,6 +15363,15 @@
         "tty-table": "^4.1.5"
       },
       "dependencies": {
+        "p-limit": {
+          "version": "2.3.0",
+          "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+          "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+          "dev": true,
+          "requires": {
+            "p-try": "^2.0.0"
+          }
+        },
         "semver": {
           "version": "5.7.1",
           "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.1.tgz",
@@ -19264,15 +19289,6 @@
             "p-locate": "^5.0.0"
           }
         },
-        "p-limit": {
-          "version": "3.1.0",
-          "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
-          "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
-          "dev": true,
-          "requires": {
-            "yocto-queue": "^0.1.0"
-          }
-        },
         "p-locate": {
           "version": "5.0.0",
           "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz",
@@ -19650,6 +19666,15 @@
             "object-keys": "^1.0.11"
           }
         },
+        "p-limit": {
+          "version": "2.3.0",
+          "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+          "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+          "dev": true,
+          "requires": {
+            "p-try": "^2.0.0"
+          }
+        },
         "p-locate": {
           "version": "3.0.0",
           "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz",
@@ -22564,15 +22589,6 @@
           "integrity": "sha512-6FlzubTLZG3J2a/NVCAleEhjzq5oxgHyaCU9yYXvcLsvoVaHJq/s5xXI6/XXP6tz7R9xAOtHnSO/tXtF3WRTlA==",
           "dev": true
         },
-        "p-limit": {
-          "version": "3.1.0",
-          "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
-          "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
-          "dev": true,
-          "requires": {
-            "yocto-queue": "^0.1.0"
-          }
-        },
         "p-locate": {
           "version": "5.0.0",
           "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz",
@@ -23028,12 +23044,12 @@
       }
     },
     "p-limit": {
-      "version": "2.3.0",
-      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
-      "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+      "version": "3.1.0",
+      "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
+      "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
       "dev": true,
       "requires": {
-        "p-try": "^2.0.0"
+        "yocto-queue": "^0.1.0"
       }
     },
     "p-locate": {
@@ -23043,6 +23059,17 @@
       "dev": true,
       "requires": {
         "p-limit": "^2.2.0"
+      },
+      "dependencies": {
+        "p-limit": {
+          "version": "2.3.0",
+          "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+          "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+          "dev": true,
+          "requires": {
+            "p-try": "^2.0.0"
+          }
+        }
       }
     },
     "p-map": {
@@ -23286,15 +23313,6 @@
             "p-locate": "^5.0.0"
           }
         },
-        "p-limit": {
-          "version": "3.1.0",
-          "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz",
-          "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==",
-          "dev": true,
-          "requires": {
-            "yocto-queue": "^0.1.0"
-          }
-        },
         "p-locate": {
           "version": "5.0.0",
           "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz",
@@ -25146,6 +25164,15 @@
             "object-keys": "^1.0.11"
           }
         },
+        "p-limit": {
+          "version": "2.3.0",
+          "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz",
+          "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==",
+          "dev": true,
+          "requires": {
+            "p-try": "^2.0.0"
+          }
+        },
         "p-locate": {
           "version": "3.0.0",
           "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz",

package.json

@@ -80,6 +80,7 @@
     "lodash.zip": "^4.2.0",
     "merkletreejs": "^0.2.13",
     "micromatch": "^4.0.2",
+    "p-limit": "^3.1.0",
     "prettier": "^2.8.1",
     "prettier-plugin-solidity": "^1.1.0",
     "rimraf": "^3.0.2",

requirements.txt

@@ -0,0 +1 @@
+certora-cli==3.6.3