nightly

Co-authored-by: Michael George <michael@certora.com>
Co-authored-by: Nick Armstrong <nick@certora.com>
Co-authored-by: Michael George <mdgeorge@cs.cornell.edu>
Co-authored-by: Aleksander Kryukov <firealexkryukov@gmail.com>
Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>

.github/workflows/formal-verifiation.yml

@@ -0,0 +1,55 @@
+name: Formal verification
+
+on:
+  push:
+    branches:
+      - master
+      - release-v*
+      - formal-verification
+  pull_request: {}
+  workflow_dispatch: {}
+
+jobs:
+  list-scripts:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - uses: actions/checkout@v2
+      - id: set-matrix
+        run: echo ::set-output name=matrix::$(ls certora/scripts/{,**}/*.sh | grep -v '\WnoCI\W' | jq -Rsc 'split("\n")[:-1]')
+
+  verify:
+    runs-on: ubuntu-latest
+    needs: list-scripts
+    steps:
+      - uses: actions/checkout@v2
+      - name: Install python
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.10'
+          cache: 'pip'
+      - name: Install java
+        uses: actions/setup-java@v1
+        with:
+          java-version: '11'
+          java-package: 'jre'
+      - name: Install certora
+        run: pip install certora-cli
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+          chmod +x /usr/local/bin/solc
+      - name: Verify rule ${{ matrix.params }}
+        run: |
+          touch certora/applyHarness.patch
+          make -C certora munged
+          bash ${{ matrix.params }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        params: ${{ fromJson(needs.list-scripts.outputs.matrix) }}

.gitignore

@@ -68,3 +68,4 @@ contracts-exposed
 .certora*
 .last_confs
 certora_*
+resource_errors.json

certora/.gitignore

@@ -0,0 +1 @@
+munged

certora/Makefile

@@ -16,9 +16,10 @@ munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
 	patch -p0 -d $@ < $(PATCH)
 
 record:
-	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
+	diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
+
+refresh: munged record
 
 clean:
 	git clean -fdX
 	touch $(PATCH)
-

certora/applyHarness.patch

@@ -1,101 +1,408 @@
-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 -druN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
+--- governance/extensions/GovernorCountingSimple.sol	2023-02-27 10:59:32.652558153 +0100
++++ governance/extensions/GovernorCountingSimple.sol	2023-02-28 16:49:10.417726143 +0100
+@@ -27,7 +27,7 @@
+         mapping(address => bool) hasVoted;
      }
  
-     /**
-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 @@
+-    mapping(uint256 => ProposalVote) private _proposalVotes;
++    mapping(uint256 => ProposalVote) internal _proposalVotes; // HARNESS: private -> internal
  
+     /**
+      * @dev See {IGovernor-COUNTING_MODE}.
+diff -druN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
+--- governance/extensions/GovernorPreventLateQuorum.sol	2023-02-27 10:59:32.652558153 +0100
++++ governance/extensions/GovernorPreventLateQuorum.sol	2023-02-28 16:49:10.417726143 +0100
+@@ -20,10 +20,10 @@
+ abstract contract GovernorPreventLateQuorum is Governor {
+     using SafeCast for uint256;
+ 
+-    uint64 private _voteExtension;
++    uint64 internal _voteExtension; // HARNESS: private -> internal
+ 
+     /// @custom:oz-retyped-from mapping(uint256 => Timers.BlockNumber)
+-    mapping(uint256 => uint64) private _extendedDeadlines;
++    mapping(uint256 => uint64) internal _extendedDeadlines; // HARNESS: private -> internal
+ 
+     /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
+     event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
+diff -druN governance/extensions/GovernorVotesQuorumFraction.sol governance/extensions/GovernorVotesQuorumFraction.sol
+--- governance/extensions/GovernorVotesQuorumFraction.sol	2023-02-27 10:59:32.655891529 +0100
++++ governance/extensions/GovernorVotesQuorumFraction.sol	2023-02-28 16:49:10.417726143 +0100
+@@ -17,10 +17,10 @@
+     using SafeCast for *;
+     using Checkpoints for Checkpoints.Trace224;
+ 
+-    uint256 private _quorumNumerator; // DEPRECATED in favor of _quorumNumeratorHistory
++    uint256 internal _quorumNumerator; // DEPRECATED // MUNGED private => internal
+ 
+     /// @custom:oz-retyped-from Checkpoints.History
+-    Checkpoints.Trace224 private _quorumNumeratorHistory;
++    Checkpoints.Trace224 internal _quorumNumeratorHistory; // MUNGED private => internal
+ 
+     event QuorumNumeratorUpdated(uint256 oldQuorumNumerator, uint256 newQuorumNumerator);
+ 
+diff -druN governance/Governor.sol governance/Governor.sol
+--- governance/Governor.sol	2023-02-27 10:59:32.652558153 +0100
++++ governance/Governor.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -51,7 +51,7 @@
      string private _name;
  
+     /// @custom:oz-retyped-from mapping(uint256 => Governor.ProposalCore)
 -    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
++    mapping(uint256 => ProposalCore) internal _proposals; // HARNESS: private -> internal
+ 
+     // This queue keeps track of the governor operating on itself. Calls to functions protected by the
+     // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
+diff -druN governance/TimelockController.sol governance/TimelockController.sol
+--- governance/TimelockController.sol	2023-02-27 10:59:32.652558153 +0100
++++ governance/TimelockController.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -28,10 +28,10 @@
+     bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
+     bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
+     bytes32 public constant CANCELLER_ROLE = keccak256("CANCELLER_ROLE");
+-    uint256 internal constant _DONE_TIMESTAMP = uint256(1);
++    uint256 public constant _DONE_TIMESTAMP = uint256(1); // HARNESS: internal -> public
+ 
+     mapping(bytes32 => uint256) private _timestamps;
+-    uint256 private _minDelay;
++    uint256 public _minDelay; // HARNESS: private -> public
  
      /**
-      * @dev Is the proposal successful or not.
+      * @dev Emitted when a call is scheduled as part of operation `id`.
+diff -druN governance/utils/Votes.sol governance/utils/Votes.sol
+--- governance/utils/Votes.sol	2023-02-27 10:59:32.655891529 +0100
++++ governance/utils/Votes.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -35,7 +35,25 @@
+     bytes32 private constant _DELEGATION_TYPEHASH =
+         keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
+ 
+-    mapping(address => address) private _delegation;
++    // HARNESS : Hooks cannot access any information from Checkpoints yet, so I am also updating votes and fromBlock in this struct
++    struct Ckpt {
++        uint32 fromBlock;
++        uint224 votes;
++    }
++    mapping(address => Ckpt) public _checkpoints;
++
++    // HARNESSED getters
++    function numCheckpoints(address account) public view returns (uint32) {
++        return SafeCast.toUint32(_delegateCheckpoints[account]._checkpoints.length);
++    }
++    function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
++        return _delegateCheckpoints[account]._checkpoints[pos]._key;
++    }
++    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
++        return _delegateCheckpoints[account]._checkpoints[pos]._value;
++    }
++
++    mapping(address => address) public _delegation; // HARNESS: private -> public
+ 
+     /// @custom:oz-retyped-from mapping(address => Checkpoints.History)
+     mapping(address => Checkpoints.Trace224) private _delegateCheckpoints;
+@@ -240,5 +258,5 @@
+     /**
+      * @dev Must return the voting units held by an account.
       */
--    function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
-+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+-    function _getVotingUnits(address) internal view virtual returns (uint256);
++    function _getVotingUnits(address) public view virtual returns (uint256); // HARNESS: internal -> public
+ }
+diff -druN proxy/utils/Initializable.sol proxy/utils/Initializable.sol
+--- proxy/utils/Initializable.sol	2023-02-27 10:59:32.655891529 +0100
++++ proxy/utils/Initializable.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -60,12 +60,12 @@
+      * @dev Indicates that the contract has been initialized.
+      * @custom:oz-retyped-from bool
+      */
+-    uint8 private _initialized;
++    uint8 internal _initialized; // HARNESS: private -> 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 @@
+      * @dev Indicates that the contract is in the process of being initialized.
+      */
+-    bool private _initializing;
++    bool internal _initializing; // HARNESS: private -> internal
+ 
+     /**
+      * @dev Triggered when the contract has been initialized or reinitialized.
+diff -druN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
+--- token/ERC1155/ERC1155.sol	2023-02-27 10:59:32.655891529 +0100
++++ token/ERC1155/ERC1155.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -21,7 +21,7 @@
+     using Address for address;
+ 
+     // Mapping from token ID to account balances
+-    mapping(uint256 => mapping(address => uint256)) private _balances;
++    mapping(uint256 => mapping(address => uint256)) internal _balances; // HARNESS: private -> internal
+ 
+     // Mapping from account to operator approvals
+     mapping(address => mapping(address => bool)) private _operatorApprovals;
+@@ -451,7 +451,7 @@
+         uint256 id,
+         uint256 amount,
+         bytes memory data
+-    ) private {
++    ) public { // HARNESS: private -> public
+         if (to.isContract()) {
+             try IERC1155Receiver(to).onERC1155Received(operator, from, id, amount, data) returns (bytes4 response) {
+                 if (response != IERC1155Receiver.onERC1155Received.selector) {
+@@ -472,7 +472,7 @@
+         uint256[] memory ids,
+         uint256[] memory amounts,
+         bytes memory data
+-    ) private {
++    ) public { // HARNESS: private -> public
+         if (to.isContract()) {
+             try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns (
+                 bytes4 response
+diff -druN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
+--- token/ERC20/ERC20.sol	2023-02-27 10:59:32.655891529 +0100
++++ token/ERC20/ERC20.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -248,7 +248,7 @@
       *
-      * - `blockNumber` must have been already mined
+      * - `account` cannot be the zero address.
       */
--    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);
+-    function _mint(address account, uint256 amount) internal virtual {
++    function _mint(address account, uint256 amount) public virtual { // HARNESS: internal -> public
+         require(account != address(0), "ERC20: mint to the zero address");
+ 
+         _beforeTokenTransfer(address(0), account, amount);
+@@ -274,7 +274,7 @@
+      * - `account` cannot be the zero address.
+      * - `account` must have at least `amount` tokens.
+      */
+-    function _burn(address account, uint256 amount) internal virtual {
++    function _burn(address account, uint256 amount) public virtual { // HARNESS: internal -> public
+         require(account != address(0), "ERC20: burn from the zero address");
+ 
+         _beforeTokenTransfer(account, address(0), amount);
+diff -druN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Capped.sol
+--- token/ERC20/extensions/ERC20Capped.sol	2023-02-22 15:43:36.624717708 +0100
++++ token/ERC20/extensions/ERC20Capped.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -30,7 +30,7 @@
+     /**
+      * @dev See {ERC20-_mint}.
+      */
+-    function _mint(address account, uint256 amount) internal virtual override {
++    function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public
+         require(ERC20.totalSupply() + amount <= cap(), "ERC20Capped: cap exceeded");
+         super._mint(account, amount);
      }
+diff -druN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
+--- token/ERC20/extensions/ERC20FlashMint.sol	2023-02-27 10:59:32.655891529 +0100
++++ token/ERC20/extensions/ERC20FlashMint.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -53,9 +53,11 @@
+         // silence warning about unused variable without the addition of bytecode.
+         token;
+         amount;
+-        return 0;
++        return fee; // HARNESS: made "return" nonzero
+     }
+ 
++    uint256 public fee; // HARNESS: added it to simulate random fee amount
++
+     /**
+      * @dev Returns the receiver address of the flash fee. By default this
+      * implementation returns the address(0) which means the fee amount will be burnt.
+diff -druN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
+--- token/ERC20/extensions/ERC20Votes.sol	2023-02-27 10:59:32.655891529 +0100
++++ token/ERC20/extensions/ERC20Votes.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -33,8 +33,8 @@
+     bytes32 private constant _DELEGATION_TYPEHASH =
+         keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
+ 
+-    mapping(address => address) private _delegates;
+-    mapping(address => Checkpoint[]) private _checkpoints;
++    mapping(address => address) public _delegates; // HARNESS: private -> public
++    mapping(address => Checkpoint[]) public _checkpoints;  // HARNESS: private -> public
+     Checkpoint[] private _totalSupplyCheckpoints;
+ 
+     /**
+@@ -186,27 +186,27 @@
+     /**
+      * @dev Maximum token supply. Defaults to `type(uint224).max` (2^224^ - 1).
+      */
+-    function _maxSupply() internal view virtual returns (uint224) {
++    function _maxSupply() public view virtual returns (uint224) {  // HARNESS: internal -> public
+         return type(uint224).max;
+     }
+ 
+     /**
+      * @dev Snapshots the totalSupply after it has been increased.
+      */
+-    function _mint(address account, uint256 amount) internal virtual override {
++    function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public
+         super._mint(account, amount);
+         require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes");
+ 
+-        _writeCheckpoint(_totalSupplyCheckpoints, _add, amount);
++        _writeCheckpointAdd(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer
+     }
+ 
+     /**
+      * @dev Snapshots the totalSupply after it has been decreased.
+      */
+-    function _burn(address account, uint256 amount) internal virtual override {
++    function _burn(address account, uint256 amount) public virtual override { // HARNESS: internal -> public (to comply with the ERC20 harness)
+         super._burn(account, amount);
+ 
+-        _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount);
++        _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer
+     }
+ 
+     /**
+@@ -225,7 +225,7 @@
+      *
+      * Emits events {IVotes-DelegateChanged} and {IVotes-DelegateVotesChanged}.
+      */
+-    function _delegate(address delegator, address delegatee) internal virtual {
++    function _delegate(address delegator, address delegatee) public virtual { // HARNESS: internal -> public
+         address currentDelegate = delegates(delegator);
+         uint256 delegatorBalance = balanceOf(delegator);
+         _delegates[delegator] = delegatee;
+@@ -238,35 +238,60 @@
+     function _moveVotingPower(address src, address dst, uint256 amount) private {
+         if (src != dst && amount > 0) {
+             if (src != address(0)) {
+-                (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[src], _subtract, amount);
++                (uint256 oldWeight, uint256 newWeight) = _writeCheckpointSub(_checkpoints[src], amount); // HARNESS: new version without pointer
+                 emit DelegateVotesChanged(src, oldWeight, newWeight);
+             }
+ 
+             if (dst != address(0)) {
+-                (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount);
++                (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount); // HARNESS: new version without pointer
+                 emit DelegateVotesChanged(dst, oldWeight, newWeight);
+             }
+         }
+     }
+ 
+-    function _writeCheckpoint(
+-        Checkpoint[] storage ckpts,
+-        function(uint256, uint256) view returns (uint256) op,
+-        uint256 delta
+-    ) private returns (uint256 oldWeight, uint256 newWeight) {
++    // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool
++    // function _writeCheckpoint(
++    //     Checkpoint[] storage ckpts,
++    //     function(uint256, uint256) view returns (uint256) op,
++    //     uint256 delta
++    // ) private returns (uint256 oldWeight, uint256 newWeight) {
++    //     uint256 pos = ckpts.length;
++
++    //     unchecked {
++    //         Checkpoint memory oldCkpt = pos == 0 ? Checkpoint(0, 0) : _unsafeAccess(ckpts, pos - 1);
++
++    //         oldWeight = oldCkpt.votes;
++    //         newWeight = op(oldWeight, delta);
++
++    //         if (pos > 0 && oldCkpt.fromBlock == clock()) {
++    //             _unsafeAccess(ckpts, pos - 1).votes = SafeCast.toUint224(newWeight);
++    //         } else {
++    //             ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
++    //         }
++    //     }
++    // }
++
++    function _writeCheckpointAdd(Checkpoint[] storage ckpts, uint256 delta) private returns (uint256 oldWeight, uint256 newWeight) {
+         uint256 pos = ckpts.length;
++        oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
++        newWeight = _add(oldWeight, delta);
+ 
+-        unchecked {
+-            Checkpoint memory oldCkpt = pos == 0 ? Checkpoint(0, 0) : _unsafeAccess(ckpts, pos - 1);
++        if (pos > 0 && ckpts[pos - 1].fromBlock == clock()) {
++            ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
++        } else {
++            ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
++        }
++    }
+ 
+-            oldWeight = oldCkpt.votes;
+-            newWeight = op(oldWeight, delta);
++    function _writeCheckpointSub(Checkpoint[] storage ckpts, uint256 delta) private returns (uint256 oldWeight, uint256 newWeight) {
++        uint256 pos = ckpts.length;
++        oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
++        newWeight = _subtract(oldWeight, delta);
+ 
+-            if (pos > 0 && oldCkpt.fromBlock == clock()) {
+-                _unsafeAccess(ckpts, pos - 1).votes = SafeCast.toUint224(newWeight);
+-            } else {
+-                ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
+-            }
++        if (pos > 0 && ckpts[pos - 1].fromBlock == clock()) {
++            ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
++        } else {
++            ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(clock()), votes: SafeCast.toUint224(newWeight)}));
+         }
+     }
+ 
+diff -druN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
+--- token/ERC20/extensions/ERC20Wrapper.sol	2023-02-27 10:59:32.655891529 +0100
++++ token/ERC20/extensions/ERC20Wrapper.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -62,7 +62,7 @@
+      * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
+      * function that can be exposed with access control if desired.
+      */
+-    function _recover(address account) internal virtual returns (uint256) {
++    function _recover(address account) public virtual returns (uint256) { // HARNESS: internal -> public
+         uint256 value = _underlying.balanceOf(address(this)) - totalSupply();
+         _mint(account, value);
+         return value;
+diff -druN token/ERC721/extensions/ERC721Votes.sol token/ERC721/extensions/ERC721Votes.sol
+--- token/ERC721/extensions/ERC721Votes.sol	2023-02-27 10:59:32.655891529 +0100
++++ token/ERC721/extensions/ERC721Votes.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -35,7 +35,7 @@
+     /**
+      * @dev Returns the balance of `account`.
+      */
+-    function _getVotingUnits(address account) internal view virtual override returns (uint256) {
++    function _getVotingUnits(address account) public view virtual override returns (uint256) { // HARNESS: internal -> public
+         return balanceOf(account);
+     }
+ }
+diff -druN utils/Address.sol utils/Address.sol
+--- utils/Address.sol	2023-02-27 10:59:32.659224903 +0100
++++ utils/Address.sol	2023-02-28 16:49:10.421059488 +0100
+@@ -197,7 +197,7 @@
+         bool success,
+         bytes memory returndata,
+         string memory errorMessage
+-    ) internal view returns (bytes memory) {
++    ) internal view returns (bytes memory val) { // MUNGED undeterministic return causes error for Prover
+         if (success) {
+             if (returndata.length == 0) {
+                 // only check isContract if the call was successful and the return data is empty
+@@ -220,7 +220,7 @@
+         bool success,
+         bytes memory returndata,
+         string memory errorMessage
+-    ) internal pure returns (bytes memory) {
++    ) internal pure returns (bytes memory val) { // MUNGED undeterministic return causes error for Prover
+         if (success) {
+             return returndata;
+         } else {
+diff -druN utils/Checkpoints.sol utils/Checkpoints.sol
+--- utils/Checkpoints.sol	2023-02-27 10:59:32.659224903 +0100
++++ utils/Checkpoints.sol	2023-02-28 16:49:10.424392833 +0100
+@@ -84,13 +84,13 @@
+      *
+      * Returns previous value and new value.
+      */
+-    function push(
+-        History storage self,
+-        function(uint256, uint256) view returns (uint256) op,
+-        uint256 delta
+-    ) internal returns (uint256, uint256) {
+-        return push(self, op(latest(self), delta));
+-    }
++    // function push(
++    //     History storage self,
++    //     function(uint256, uint256) view returns (uint256) op,
++    //     uint256 delta
++    // ) internal returns (uint256, uint256) {
++    //     return push(self, op(latest(self), delta));
++    // }
+ 
+     /**
+      * @dev Returns the value in the most recent checkpoint, or zero if there are no checkpoints.

certora/harnesses/AccessControlHarness.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts (last updated v4.5.0) (access/AccessControl.sol)
+
+pragma solidity ^0.8.0;
+
+import "../munged/access/AccessControl.sol";
+
+contract AccessControlHarness is AccessControl {}

certora/harnesses/ERC1155/ERC1155BurnableHarness.sol

@@ -0,0 +1,5 @@
+import "../../munged/token/ERC1155/extensions/ERC1155Burnable.sol";
+
+contract ERC1155BurnableHarness is ERC1155Burnable {
+    constructor(string memory uri_) ERC1155(uri_) {}
+}

certora/harnesses/ERC1155/ERC1155Harness.sol

@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+import "../../munged/token/ERC1155/ERC1155.sol";
+
+contract ERC1155Harness is ERC1155 {
+    constructor(string memory uri_) ERC1155(uri_) {}
+
+    function burn(
+        address from,
+        uint256 id,
+        uint256 amount
+    ) public virtual {
+        _burn(from, id, amount);
+    }
+
+    function burnBatch(
+        address from,
+        uint256[] memory ids,
+        uint256[] memory amounts
+    ) public virtual {
+        _burnBatch(from, ids, amounts);
+    }
+
+    function mint(
+        address to,
+        uint256 id,
+        uint256 amount,
+        bytes memory data
+    ) public virtual {
+        _mint(to, id, amount, data);
+    }
+
+    function mintBatch(
+        address to,
+        uint256[] memory ids,
+        uint256[] memory amounts,
+        bytes memory data
+    ) public virtual {
+        _mintBatch(to, ids, amounts, data);
+    }
+}

certora/harnesses/ERC1155/ERC1155PausableHarness.sol

@@ -0,0 +1,17 @@
+import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol";
+
+contract ERC1155PausableHarness is ERC1155Pausable {
+    constructor(string memory uri_) ERC1155(uri_) {}
+
+    function pause() public {
+        _pause();
+    }
+
+    function unpause() public {
+        _unpause();
+    }
+
+    function onlyWhenPausedMethod() public whenPaused {}
+
+    function onlyWhenNotPausedMethod() public whenNotPaused {}
+}

certora/harnesses/ERC1155/ERC1155SupplyHarness.sol

@@ -0,0 +1,65 @@
+import "../../munged/token/ERC1155/extensions/ERC1155Supply.sol";
+
+contract ERC1155SupplyHarness is ERC1155Supply {
+    address public owner;
+
+    constructor(string memory uri_) ERC1155(uri_) {
+        owner = msg.sender;
+    }
+
+    // workaround for problem caused by `exists` being a CVL keyword
+    function exists_wrapper(uint256 id) public view virtual returns (bool) {
+        return exists(id);
+    }
+
+    // These rules were not implemented in the base but there are changes in supply
+    // that are affected by the internal contracts so we implemented them. We assume
+    // only the owner can call any of these functions to be able to test them but also
+    // limit false positives.
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function burn(
+        address from,
+        uint256 id,
+        uint256 amount
+    ) public virtual onlyOwner {
+        _burn(from, id, amount);
+    }
+
+    function burnBatch(
+        address from,
+        uint256[] memory ids,
+        uint256[] memory amounts
+    ) public virtual onlyOwner {
+        _burnBatch(from, ids, amounts);
+    }
+
+    function mint(
+        address to,
+        uint256 id,
+        uint256 amount,
+        bytes memory data
+    ) public virtual onlyOwner {
+        _mint(to, id, amount, data);
+    }
+
+    function mintBatch(
+        address to,
+        uint256[] memory ids,
+        uint256[] memory amounts,
+        bytes memory data
+    ) public virtual onlyOwner {
+        _mintBatch(to, ids, amounts, data);
+    }
+
+    // In order to check the invariant that zero address never holds any tokens, we need to remove the require
+    // from this function.
+    function balanceOf(address account, uint256 id) public view virtual override returns (uint256) {
+        // require(account != address(0), "ERC1155: address zero is not a valid owner");
+        return _balances[id][account];
+    }
+}

certora/harnesses/ERC20FlashMintHarness.sol

@@ -0,0 +1,5 @@
+import "../munged/token/ERC20/extensions/ERC20FlashMint.sol";
+
+contract ERC20FlashMintHarness is ERC20FlashMint {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) {}
+}

certora/harnesses/ERC20PermitHarness.sol

@@ -0,0 +1,5 @@
+import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol";
+
+contract ERC20PermitHarness is ERC20, ERC20Permit {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
+}

certora/harnesses/ERC20VotesHarness.sol

@@ -1,28 +1,26 @@
 import "../munged/token/ERC20/extensions/ERC20Votes.sol";
 
 contract ERC20VotesHarness is ERC20Votes {
-    constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
 
-    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;
+    function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
+        return _checkpoints[account][pos].fromBlock;
     }
 
-    /**
-     * @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);
+    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
+        return _checkpoints[account][pos].fromBlock;
     }
+
+    function unsafeNumCheckpoints(address account) public view returns (uint256) {
+        return _checkpoints[account].length;
+    }
+
+    function delegateBySig(
+        address delegatee,
+        uint256 nonce,
+        uint256 expiry,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public virtual override {}
 }

certora/harnesses/ERC20WrapperHarness.sol

@@ -0,0 +1,17 @@
+import "../munged/token/ERC20/extensions/ERC20Wrapper.sol";
+
+contract ERC20WrapperHarness is ERC20Wrapper {
+    constructor(
+        IERC20 _underlying,
+        string memory _name,
+        string memory _symbol
+    ) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {}
+
+    function underlyingTotalSupply() public view returns (uint256) {
+        return underlying().totalSupply();
+    }
+
+    function underlyingBalanceOf(address account) public view returns (uint256) {
+        return underlying().balanceOf(account);
+    }
+}

certora/harnesses/ERC721VotesHarness.sol

@@ -0,0 +1,26 @@
+pragma solidity ^0.8.0;
+
+import "../munged/token/ERC721/extensions/draft-ERC721Votes.sol";
+
+contract ERC721VotesHarness is ERC721Votes {
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, symbol) {}
+
+    function delegateBySig(
+        address delegatee,
+        uint256 nonce,
+        uint256 expiry,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public virtual override {
+        assert(true);
+    }
+
+    function mint(address account, uint256 tokenID) public {
+        _mint(account, tokenID);
+    }
+
+    function burn(uint256 tokenID) public {
+        _burn(tokenID);
+    }
+}

certora/harnesses/GovernorFullHarness.sol

@@ -0,0 +1,206 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorPreventLateQuorum.sol";
+import "../munged/governance/extensions/GovernorTimelockControl.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/token/ERC20/extensions/ERC20Votes.sol";
+
+contract GovernorFullHarness is
+    Governor,
+    GovernorCountingSimple,
+    GovernorTimelockControl,
+    GovernorPreventLateQuorum,
+    GovernorVotes,
+    GovernorVotesQuorumFraction
+{
+    using Checkpoints for Checkpoints.Trace224;
+
+    constructor(
+        IVotes _token,
+        TimelockController _timelock,
+        uint64 initialVoteExtension,
+        uint256 quorumNumeratorValue
+    )
+        Governor("Harness")
+        GovernorPreventLateQuorum(initialVoteExtension)
+        GovernorTimelockControl(_timelock)
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumNumeratorValue)
+    {}
+
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
+    // Harness from Votes //
+
+    function getPastTotalSupply(uint256 blockNumber) public view returns(uint256) {
+        return token.getPastTotalSupply(blockNumber);
+    }
+    // Harness from GovernorVotesQuorumFraction //
+
+    function getQuorumNumeratorLength() public view returns(uint256) {
+        return _quorumNumeratorHistory._checkpoints.length;
+    }
+
+    function getQuorumNumeratorLatest() public view returns(uint256) {
+        return _quorumNumeratorHistory.latest();
+    }
+
+    function getDeprecatedQuorumNumerator() public view returns(uint256) {
+        return _quorumNumerator;
+    }
+
+    // Harness from GovernorPreventLateQuorum //
+
+    function getVoteExtension() public view returns (uint64) {
+        return _voteExtension;
+    }
+
+    function getExtendedDeadline(uint256 proposalId) public view returns (uint64) {
+        return _extendedDeadlines[proposalId];
+    }
+
+    // Harness from GovernorCountingSimple //
+
+    function getAgainstVotes(uint256 proposalId) public view returns (uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.againstVotes;
+    }
+
+    function getAbstainVotes(uint256 proposalId) public view returns (uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.abstainVotes;
+    }
+
+    function getForVotes(uint256 proposalId) public view returns (uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.forVotes;
+    }
+
+    function quorumReached(uint256 proposalId) public view returns (bool) {
+        return _quorumReached(proposalId);
+    }
+
+    function voteSucceeded(uint256 proposalId) public view returns (bool) {
+        return _voteSucceeded(proposalId);
+    }
+
+    // Harness from Governor //
+
+    function getExecutor() public view returns (address) {
+        return _executor();
+    }
+
+    function proposalProposer(uint256 proposalId) public view returns (address) {
+        return _proposalProposer(proposalId);
+    }
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    // The following functions are overrides required by Solidity added by Certora. //
+
+    function proposalDeadline(uint256 proposalId)
+        public
+        view
+        virtual
+        override(Governor, GovernorPreventLateQuorum, IGovernor)
+        returns (uint256)
+    {
+        return super.proposalDeadline(proposalId);
+    }
+
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason,
+        bytes memory params
+    ) internal virtual override(Governor, GovernorPreventLateQuorum) returns (uint256) {
+        // added to run GovernorCountingSimple.spec
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params);
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+
+        return deltaWeight;
+    }
+
+    function lateQuorumVoteExtension() public view virtual override returns (uint64) {
+        return super.lateQuorumVoteExtension();
+    }
+
+    function setLateQuorumVoteExtension(uint64 newVoteExtension) public virtual override onlyGovernance {
+        super.setLateQuorumVoteExtension(newVoteExtension);
+    }
+
+    // The following functions are overrides required by Solidity added by OZ Wizard. //
+
+    function votingDelay() public pure override returns (uint256) {
+        return 1; // 1 block
+    }
+
+    function votingPeriod() public pure override returns (uint256) {
+        return 45818; // 1 week
+    }
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(blockNumber);
+    }
+
+    function state(uint256 proposalId) public view override(Governor, GovernorTimelockControl) returns (ProposalState) {
+        return super.state(proposalId);
+    }
+
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public override(Governor, IGovernor) returns (uint256) {
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    function _execute(
+        uint256 proposalId,
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) returns (uint256) {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/harnesses/GovernorHarness.sol

@@ -0,0 +1,154 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorTimelockControl.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/token/ERC20/extensions/ERC20Votes.sol";
+
+contract GovernorHarness is
+    Governor,
+    GovernorCountingSimple,
+    GovernorVotes,
+    GovernorVotesQuorumFraction,
+    GovernorTimelockControl
+{
+    constructor(
+        IVotes _token,
+        TimelockController _timelock,
+        uint64 initialVoteExtension,
+        uint256 quorumNumeratorValue
+    )
+        Governor("Harness")
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumNumeratorValue)
+        GovernorTimelockControl(_timelock)
+    {}
+
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
+    // Harness from GovernorCountingSimple //
+
+    function getAgainstVotes(uint256 proposalId) public view returns (uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.againstVotes;
+    }
+
+    function getAbstainVotes(uint256 proposalId) public view returns (uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.abstainVotes;
+    }
+
+    function getForVotes(uint256 proposalId) public view returns (uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.forVotes;
+    }
+
+    function quorumReached(uint256 proposalId) public view returns (bool) {
+        return _quorumReached(proposalId);
+    }
+
+    function voteSucceeded(uint256 proposalId) public view returns (bool) {
+        return _voteSucceeded(proposalId);
+    }
+
+    // Harness from Governor //
+
+    function getExecutor() public view returns (address) {
+        return _executor();
+    }
+
+    function proposalProposer(uint256 proposalId) public view returns (address) {
+        return _proposalProposer(proposalId);
+    }
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    // The following functions are overrides required by Solidity added by Certora. //
+
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason,
+        bytes memory params
+    ) internal virtual override returns (uint256) {
+        // added to run GovernorCountingSimple.spec
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params);
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+
+        return deltaWeight;
+    }
+
+    // The following functions are overrides required by Solidity added by OZ Wizard. //
+
+    function votingDelay() public pure override returns (uint256) {
+        return 1; // 1 block
+    }
+
+    function votingPeriod() public pure override returns (uint256) {
+        return 45818; // 1 week
+    }
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(blockNumber);
+    }
+
+    function state(uint256 proposalId) public view override(Governor, GovernorTimelockControl) returns (ProposalState) {
+        return super.state(proposalId);
+    }
+
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public override(Governor, IGovernor) returns (uint256) {
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    function _execute(
+        uint256 proposalId,
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) returns (uint256) {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/harnesses/IERC3156FlashBorrowerHarness.sol

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.4.1 (interfaces/IERC3156FlashBorrower.sol)
+
+import "../munged/interfaces/IERC3156FlashBorrower.sol";
+
+pragma solidity ^0.8.0;
+
+contract IERC3156FlashBorrowerHarness is IERC3156FlashBorrower {
+    bytes32 somethingToReturn;
+
+    function onFlashLoan(
+        address initiator,
+        address token,
+        uint256 amount,
+        uint256 fee,
+        bytes calldata data
+    ) external override returns (bytes32) {
+        return somethingToReturn;
+    }
+}

certora/harnesses/InitializableBasicHarness.sol

@@ -0,0 +1,80 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/proxy/utils/Initializable.sol";
+
+contract InitializableBasicHarness is Initializable {
+    uint256 public val;
+    uint256 public a;
+    uint256 public b;
+
+    modifier version1() {
+        require(_initialized == 1);
+        _;
+    }
+
+    modifier versionN(uint8 n) {
+        require(_initialized == n);
+        _;
+    }
+
+    function initialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b
+    ) public initializer {
+        a = _a;
+        b = _b;
+        val = _val;
+    }
+
+    function reinitialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b,
+        uint8 n
+    ) public reinitializer(n) {
+        a = _a;
+        b = _b;
+        val = _val;
+    }
+
+    // Versioned return functions for testing
+
+    function returnsV1() public view version1 returns (uint256) {
+        return val;
+    }
+
+    function returnsVN(uint8 n) public view versionN(n) returns (uint256) {
+        return val;
+    }
+
+    function returnsAV1() public view version1 returns (uint256) {
+        return a;
+    }
+
+    function returnsAVN(uint8 n) public view versionN(n) returns (uint256) {
+        return a;
+    }
+
+    function returnsBV1() public view version1 returns (uint256) {
+        return b;
+    }
+
+    function returnsBVN(uint8 n) public view versionN(n) returns (uint256) {
+        return b;
+    }
+
+    // Harness //
+    function initialized() public view returns (uint8) {
+        return _initialized;
+    }
+
+    function initializing() public view returns (bool) {
+        return _initializing;
+    }
+
+    function thisIsContract() public view returns (bool) {
+        return !Address.isContract(address(this));
+    }
+}

certora/harnesses/InitializableComplexHarness.sol

@@ -0,0 +1,92 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/proxy/utils/Initializable.sol";
+
+contract InitializableA is Initializable {
+    uint256 public a;
+
+    modifier version1() {
+        require(_initialized == 1);
+        _;
+    }
+
+    modifier versionN(uint8 n) {
+        require(_initialized == n);
+        _;
+    }
+
+    function __InitializableA_init(uint256 _a) internal onlyInitializing {
+        a = _a;
+    }
+
+    function returnsAV1() public view version1 returns (uint256) {
+        return a;
+    }
+
+    function returnsAVN(uint8 n) public view versionN(n) returns (uint256) {
+        return a;
+    }
+}
+
+contract InitializableB is Initializable, InitializableA {
+    uint256 public b;
+
+    function __InitializableB_init(uint256 _b) internal onlyInitializing {
+        b = _b;
+    }
+
+    function returnsBV1() public view version1 returns (uint256) {
+        return b;
+    }
+
+    function returnsBVN(uint8 n) public view versionN(n) returns (uint256) {
+        return b;
+    }
+}
+
+contract InitializableComplexHarness is Initializable, InitializableB {
+    uint256 public val;
+
+    function initialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b
+    ) public initializer {
+        val = _val;
+        __InitializableA_init(_a);
+        __InitializableB_init(_b);
+    }
+
+    function reinitialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b,
+        uint8 n
+    ) public reinitializer(n) {
+        val = _val;
+        __InitializableA_init(_a);
+        __InitializableB_init(_b);
+    }
+
+    function returnsV1() public view version1 returns (uint256) {
+        return val;
+    }
+
+    function returnsVN(uint8 n) public view versionN(n) returns (uint256) {
+        return val;
+    }
+
+    // Harness //
+    function initialized() public view returns (uint8) {
+        return _initialized;
+    }
+
+    function initializing() public view returns (bool) {
+        return _initializing;
+    }
+
+    function thisIsContract() public view returns (bool) {
+        return !Address.isContract(address(this));
+    }
+}

certora/harnesses/TimelockControllerHarness.sol

@@ -0,0 +1,12 @@
+pragma solidity ^0.8.0;
+
+import "../munged/governance/TimelockController.sol";
+
+contract TimelockControllerHarness is TimelockController {
+    constructor(
+        uint256 minDelay,
+        address[] memory proposers,
+        address[] memory executors,
+        address admin
+    ) TimelockController(minDelay, proposers, executors, admin) {}
+}

certora/harnesses/WizardControlFirstPriority.sol

@@ -7,16 +7,29 @@ import "../munged/governance/extensions/GovernorVotes.sol";
 import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
 import "../munged/governance/extensions/GovernorTimelockControl.sol";
 import "../munged/governance/extensions/GovernorProposalThreshold.sol";
+import "../munged/token/ERC20/extensions/ERC20Votes.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)
+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)
@@ -28,7 +41,7 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove
     function isExecuted(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].executed;
     }
-    
+
     function isCanceled(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].canceled;
     }
@@ -46,35 +59,36 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove
         address account,
         uint8 support,
         string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+    ) internal virtual override returns (uint256) {
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS
         ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
 
-        return deltaWeight;        
+        return deltaWeight;
     }
-    
+
     function snapshot(uint256 proposalId) public view returns (uint64) {
         return _proposals[proposalId].voteStart._deadline;
     }
 
-
-    function getExecutor() public view returns (address){
+    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 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 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
+    function proposalThreshold() public view override returns (uint256) {
+        // HARNESS: pure -> view
+        return _proposalThreshold; // HARNESS: parametric
     }
 
     // original code, not harnessed
@@ -92,50 +106,45 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove
     function getVotes(address account, uint256 blockNumber)
         public
         view
-        override(IGovernor, GovernorVotes)
+        override(IGovernor, Governor)
         returns (uint256)
     {
         return super.getVotes(account, blockNumber);
     }
 
-    function state(uint256 proposalId)
-        public
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (ProposalState)
-    {
+    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)
-    {
+    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)
-    {
+    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)
-    {
+    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)
-    {
+    function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) {
         return super._executor();
     }
 

certora/harnesses/WizardFirstTry.sol

@@ -6,15 +6,27 @@ import "../munged/governance/extensions/GovernorCountingSimple.sol";
 import "../munged/governance/extensions/GovernorVotes.sol";
 import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
 import "../munged/governance/extensions/GovernorTimelockCompound.sol";
+import "../munged/token/ERC20/extensions/ERC20Votes.sol";
 
-/* 
+/*
 Wizard options:
 ERC20Votes
 TimelockCompound
 */
 
-contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
-    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
+contract WizardFirstTry is
+    Governor,
+    GovernorCountingSimple,
+    GovernorVotes,
+    GovernorVotesQuorumFraction,
+    GovernorTimelockCompound
+{
+    constructor(
+        ERC20Votes _token,
+        ICompoundTimelock _timelock,
+        string memory name,
+        uint256 quorumFraction
+    )
         Governor(name)
         GovernorVotes(_token)
         GovernorVotesQuorumFraction(quorumFraction)
@@ -26,7 +38,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
     function isExecuted(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].executed;
     }
-    
+
     function isCanceled(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].canceled;
     }
@@ -35,7 +47,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
         return _proposals[proposalId].voteStart._deadline;
     }
 
-    function getExecutor() public view returns (address){
+    function getExecutor() public view returns (address) {
         return _executor();
     }
 
@@ -50,22 +62,23 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
         address account,
         uint8 support,
         string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+    ) internal virtual override returns (uint256) {
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS
         ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
 
-        return deltaWeight;        
+        return deltaWeight;
     }
 
     // original code, harnessed
 
-    function votingDelay() public view override virtual returns (uint256) {     // HARNESS: pure -> view
-        return _votingDelay;                                                    // HARNESS: parametric
+    function votingDelay() public view virtual override returns (uint256) {
+        // HARNESS: pure -> view
+        return _votingDelay; // HARNESS: parametric
     }
 
-    function votingPeriod() public view override virtual returns (uint256) {    // HARNESS: pure -> view
-        return _votingPeriod;                                                   // HARNESS: parametric
+    function votingPeriod() public view virtual override returns (uint256) {
+        // HARNESS: pure -> view
+        return _votingPeriod; // HARNESS: parametric
     }
 
     // original code, not harnessed
@@ -83,7 +96,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
     function getVotes(address account, uint256 blockNumber)
         public
         view
-        override(IGovernor, GovernorVotes)
+        override(IGovernor, Governor)
         returns (uint256)
     {
         return super.getVotes(account, blockNumber);
@@ -98,35 +111,35 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
         return super.state(proposalId);
     }
 
-    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
-        public
-        override(Governor, IGovernor)
-        returns (uint256)
-    {
+    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)
-    {
+    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)
-    {
+    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)
-    {
+    function _executor() internal view override(Governor, GovernorTimelockCompound) returns (address) {
         return super._executor();
     }
 

certora/munged/.gitignore

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

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/noCI/Round1/WizardControlFirstPriority.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
+    --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
+    --link WizardControlFirstPriority:token=ERC20VotesHarness \
+    --solc solc \
+    --optimistic_loop \
+    --disableLocalTypeChecking \
+    --settings -copyLoopUnroll=4 \
+    $@

certora/scripts/noCI/Round1/WizardFirstTry.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
+    --verify WizardFirstTry:certora/specs/GovernorBase.spec \
+    --link WizardFirstTry:token=ERC20VotesHarness \
+    --solc solc \
+    --optimistic_loop \
+    --disableLocalTypeChecking \
+    --settings -copyLoopUnroll=4 \
+    $@

certora/scripts/noCI/Round1/verifyGovernor.sh

@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+for contract in certora/harnesses/Wizard*.sol;
+do
+    for spec in certora/specs/Governor*.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 solc \
+                    --optimistic_loop \
+                    --disableLocalTypeChecking \
+                    --settings -copyLoopUnroll=4 \
+                    --msg "checking $specFile on ${contractFile%.*}"
+            else
+                certoraRun \
+                    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                    --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                    --solc solc \
+                    --optimistic_loop \
+                    --disableLocalTypeChecking \
+                    --settings -copyLoopUnroll=4 \
+                    --msg "checking $specFile on ${contractFile%.*}"
+            fi
+        fi
+    done
+done

certora/scripts/noCI/sanity/sanity.sh

@@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+# 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 solc \
+#         --optimistic_loop \
+#         --settings -copyLoopUnroll=4 \
+#         --msg "checking sanity on ${file%.*}"
+# done
+
+# TimelockController
+certoraRun \
+    certora/harnesses/TimelockControllerHarness.sol \
+    --verify TimelockControllerHarness:certora/specs/sanity.spec \
+    --solc solc \
+    --optimistic_loop \
+    --msg "sanity and keccak check"
+
+# Votes
+# certoraRun \
+#     certora/harnesses/VotesHarness.sol \
+#     --verify VotesHarness:certora/specs/sanity.spec \
+#     --solc solc \
+#     --optimistic_loop \
+#     --settings -strictDecompiler=false,-assumeUnwindCond \
+#     --msg "sanityVotes"

certora/scripts/noCI/sanity/sanityGovernor.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+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 solc \
+        --optimistic_loop \
+        --settings -copyLoopUnroll=4 \
+        --msg "checking sanity on ${file%.*}"
+done

certora/scripts/noCI/sanity/sanityTokens.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+for f in certora/harnesses/ERC20{Votes,Permit,Wrapper}Harness.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+        --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+        --solc solc \
+        --optimistic_loop \
+        --settings -copyLoopUnroll=4,-strictDecompiler=false \
+        --msg "checking sanity on ${file%.*}"
+done

certora/scripts/passes/verifyAccessControl.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/AccessControlHarness.sol \
+    --verify AccessControlHarness:certora/specs/AccessControl.spec \
+    --optimistic_loop \
+    $@

certora/scripts/passes/verifyERC1155.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155Harness.sol \
+    --verify ERC1155Harness:certora/specs/ERC1155.spec \
+    --optimistic_loop \
+    --loop_iter 3 \
+    $@

certora/scripts/passes/verifyERC1155Burnable.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
+    --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
+    --optimistic_loop \
+    --loop_iter 3 \
+    $@

certora/scripts/passes/verifyERC1155Pausable.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
+    --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
+    --optimistic_loop \
+    --loop_iter 3 \
+    $@

certora/scripts/passes/verifyERC1155Supply.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
+    --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
+    --optimistic_loop \
+    --loop_iter 3 \
+    $@

certora/scripts/passes/verifyERC20FlashMint.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20FlashMintHarness.sol \
+    certora/harnesses/IERC3156FlashBorrowerHarness.sol \
+    --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
+    --optimistic_loop \
+    $@

certora/scripts/passes/verifyERC20Votes.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol \
+    --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    $@

certora/scripts/passes/verifyERC20Wrapper.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20WrapperHarness.sol certora/harnesses/ERC20PermitHarness.sol \
+    --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
+    --optimistic_loop \
+    $@

certora/scripts/passes/verifyERC721Votes.sh

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC721VotesHarness.sol certora/munged/utils/Checkpoints.sol \
+    --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \
+    --optimistic_loop \
+    --disableLocalTypeChecking \
+    --settings -copyLoopUnroll=4 \
+    $@

certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \
+    --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    --link GovernorFullHarness:token=ERC20VotesHarness \
+    --optimistic_loop \
+    --optimistic_hashing \
+    --rule deadlineCantBeUnextended \
+    --loop_iter 1 \
+    $@

certora/scripts/passes/verifyGPLQ_proposalInOneState.sh

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \
+    --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    --link GovernorFullHarness:token=ERC20VotesHarness \
+    --optimistic_loop \
+    --optimistic_hashing \
+    --rule proposalInOneState \
+    --loop_iter 1 \
+    --settings -t=1000 \
+    $@

certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \
+    --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    --link GovernorFullHarness:token=ERC20VotesHarness \
+    --optimistic_loop \
+    --optimistic_hashing \
+    --rule quorumReachedEffect \
+    --loop_iter 1 \
+    $@

certora/scripts/passes/verifyGovernor.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+# Changed: GovernorHarness missing
+#
+# Note: rule `immutableFieldsAfterProposalCreation` fails with
+# GovernorFullHarness because of late quorum changing the vote's end.
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
+    --verify GovernorHarness:certora/specs/GovernorBase.spec \
+    --link GovernorHarness:token=ERC20VotesHarness \
+    --optimistic_loop \
+    --optimistic_hashing \
+    --settings -copyLoopUnroll=4 \
+    $@

certora/scripts/passes/verifyGovernorCountingSimple.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+# Changed: GovernorBasicHarness missing
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
+    --verify GovernorHarness:certora/specs/GovernorCountingSimple.spec \
+    --link GovernorHarness:token=ERC20VotesHarness \
+    --optimistic_loop \
+    --optimistic_hashing \
+    --settings -copyLoopUnroll=4 \
+    $@

certora/scripts/passes/verifyGovernorPreventLateQuorum.sh

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol certora/munged/governance/TimelockController.sol \
+    --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    --link GovernorFullHarness:token=ERC20VotesHarness \
+    --optimistic_loop \
+    --optimistic_hashing \
+    $@

certora/scripts/passes/verifyInitializable.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/InitializableComplexHarness.sol \
+    --verify InitializableComplexHarness:certora/specs/Initializable.spec \
+    --optimistic_loop \
+    --loop_iter 3 \
+    $@

certora/scripts/passes/verifyTimelock.sh

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \
+    --verify TimelockControllerHarness:certora/specs/TimelockController.spec \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --optimistic_hashing \
+    $@

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/scripts/verifyERC20.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20PermitHarness.sol \
+    --verify ERC20PermitHarness:certora/specs/ERC20.spec \
+    --solc solc \
+    --optimistic_loop \
+    $@

certora/specs/AccessControl.spec

@@ -0,0 +1,133 @@
+methods {
+    hasRole(bytes32, address) returns(bool) envfree
+    getRoleAdmin(bytes32) returns(bytes32) envfree
+
+    grantRole(bytes32, address)
+    revokeRole(bytes32, address)
+    renounceRole(bytes32, address)
+}
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only grantRole can grant a role                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyGrantCanGrant(env e, bytes32 role, address account) {
+    require !hasRole(role, account);
+
+    method f; calldataarg args;
+    f(e, args);
+
+    assert hasRole(role, account) => f.selector == grantRole(bytes32, address).selector;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only revokeRole and renounceRole can grant a role                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyRevokeAndRenounceCanRevoke(env e, bytes32 role, address account) {
+    require hasRole(role, account);
+
+    method f; calldataarg args;
+    f(e, args);
+
+    assert !hasRole(role, account) => (f.selector == revokeRole(bytes32, address).selector || f.selector == renounceRole(bytes32, address).selector);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only an account with admin role can call grantRole                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAdminCanGrant(env e, bytes32 role, address account) {
+    bool isAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+
+    grantRole@withrevert(e, role, account);
+
+    assert !lastReverted => isAdmin;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only an account with admin role can call revokeRole                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAdminCanRevoke(env e, bytes32 role, address account) {
+    bool isAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+
+    revokeRole@withrevert(e, role, account);
+
+    assert !lastReverted => isAdmin;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only the affected account can revoke                                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyUserCanRenounce(env e, bytes32 role, address account) {
+    renounceRole@withrevert(e, role, account);
+    assert !lastReverted => account == e.msg.sender;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: grantRole only affects the specified user/role combo                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule grantRoleEffect(env e) {
+    bytes32 role1; bytes32 role2;
+    address account1; address account2;
+
+    bool hasRoleBefore = hasRole(role1, account1);
+    grantRole(e, role2, account2);
+    bool hasRoleAfter = hasRole(role1, account1);
+
+    assert (
+        hasRoleBefore != hasRoleAfter
+    ) => (
+        hasRoleAfter == true && role1 == role2 && account1 == account2
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: revokeRole only affects the specified user/role combo                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule revokeRoleEffect(env e) {
+    bytes32 role1; bytes32 role2;
+    address account1; address account2;
+
+    bool hasRoleBefore = hasRole(role1, account1);
+    revokeRole(e, role2, account2);
+    bool hasRoleAfter = hasRole(role1, account1);
+
+    assert (
+        hasRoleBefore != hasRoleAfter
+    ) => (
+        hasRoleAfter == false && role1 == role2 && account1 == account2
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: renounceRole only affects the specified user/role combo                                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceRoleEffect(env e) {
+    bytes32 role1; bytes32 role2;
+    address account1; address account2;
+
+    bool hasRoleBefore = hasRole(role1, account1);
+    renounceRole(e, role2, account2);
+    bool hasRoleAfter = hasRole(role1, account1);
+
+    assert (
+        hasRoleBefore != hasRoleAfter
+    ) => (
+        hasRoleAfter == false && role1 == role2 && account1 == account2
+    );
+}

certora/specs/ERC1155.spec

@@ -0,0 +1,877 @@
+methods {
+    isApprovedForAll(address, address) returns(bool) envfree
+    balanceOf(address, uint256) returns(uint256) envfree
+    balanceOfBatch(address[], uint256[]) returns(uint256[]) envfree
+    _doSafeBatchTransferAcceptanceCheck(address, address, address, uint256[], uint256[], bytes) envfree
+    _doSafeTransferAcceptanceCheck(address, address, address, uint256, uint256, bytes) envfree
+
+    setApprovalForAll(address, bool)
+    safeTransferFrom(address, address, uint256, uint256, bytes)
+    safeBatchTransferFrom(address, address, uint256[], uint256[], bytes)
+    mint(address, uint256, uint256, bytes)
+    mintBatch(address, uint256[], uint256[], bytes)
+    burn(address, uint256, uint256)
+    burnBatch(address, uint256[], uint256[])
+}
+
+
+/////////////////////////////////////////////////
+// Approval (4/4)
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// Function $f, which is not setApprovalForAll, should not change approval
+rule unexpectedAllowanceChange(method f, env e) filtered { f -> f.selector != setApprovalForAll(address, bool).selector } {
+    address account; address operator;
+    bool approveBefore = isApprovedForAll(account, operator);
+
+    calldataarg args;
+    f(e, args);
+
+    bool approveAfter = isApprovedForAll(account, operator);
+
+    assert approveBefore == approveAfter, "You couldn't get king's approval this way!";
+}
+
+
+// STATUS - verified
+// approval can be changed only by owner
+rule onlyOwnerCanApprove(env e){
+    address owner; address operator; bool approved;
+
+    bool aprovalBefore = isApprovedForAll(owner, operator);
+
+    setApprovalForAll(e, operator, approved);
+
+    bool aprovalAfter = isApprovedForAll(owner, operator);
+
+    assert aprovalBefore != aprovalAfter => owner == e.msg.sender, "There should be only one owner";
+}
+
+
+// STATUS - verified
+// Check that isApprovedForAll() revertes in planned scenarios and no more.
+rule approvalRevertCases(env e){
+    address account; address operator;
+    isApprovedForAll@withrevert(account, operator);
+    assert !lastReverted, "Houston, we have a problem";
+}
+
+
+// STATUS - verified
+// setApproval changes only one approval
+rule onlyOneAllowanceChange(method f, env e) {
+    address owner; address operator; address user;
+    bool approved;
+
+    bool userApproveBefore = isApprovedForAll(owner, user);
+
+    setApprovalForAll(e, operator, approved);
+
+    bool userApproveAfter = isApprovedForAll(owner, user);
+
+    assert userApproveBefore != userApproveAfter => (e.msg.sender == owner && operator == user), "Imposter!";
+}
+
+
+
+/////////////////////////////////////////////////
+// Balance (3/3)
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// Function $f, which is not one of transfers, mints and burns, should not change balanceOf of a user
+rule unexpectedBalanceChange(method f, env e)
+    filtered { f -> f.selector != safeTransferFrom(address, address, uint256, uint256, bytes).selector
+                        && f.selector != safeBatchTransferFrom(address, address, uint256[], uint256[], bytes).selector
+                        && f.selector != mint(address, uint256, uint256, bytes).selector
+                        && f.selector != mintBatch(address, uint256[], uint256[], bytes).selector
+                        && f.selector != burn(address, uint256, uint256).selector
+                        && f.selector != burnBatch(address, uint256[], uint256[]).selector } {
+    address from; uint256 id;
+    uint256 balanceBefore = balanceOf(from, id);
+
+    calldataarg args;
+    f(e, args);
+
+    uint256 balanceAfter = balanceOf(from, id);
+
+    assert balanceBefore == balanceAfter, "How you dare to take my money?";
+}
+
+
+// STATUS - verified
+// Check that `balanceOf()` revertes in planned scenarios and no more (only if `account` is 0)
+rule balanceOfRevertCases(env e){
+    address account; uint256 id;
+    balanceOf@withrevert(account, id);
+    assert lastReverted => account == 0, "Houston, we have a problem";
+}
+
+
+// STATUS - verified
+// Check that `balanceOfBatch()` revertes in planned scenarios and no more (only if at least one of `account`s is 0)
+rule balanceOfBatchRevertCases(env e){
+    address[] accounts; uint256[] ids;
+    address account1; address account2; address account3;
+    uint256 id1; uint256 id2; uint256 id3;
+
+    require accounts.length == 3;
+    require ids.length == 3;
+
+    require accounts[0] == account1; require accounts[1] == account2; require accounts[2] == account3;
+
+    balanceOfBatch@withrevert(accounts, ids);
+    assert lastReverted => (account1 == 0 || account2 == 0 || account3 == 0), "Houston, we have a problem";
+}
+
+
+
+/////////////////////////////////////////////////
+// Transfer (13/13)
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// transfer additivity
+rule transferAdditivity(env e){
+    address from; address to; uint256 id; bytes data;
+    uint256 amount; uint256 amount1; uint256 amount2;
+    require amount == amount1 + amount2;
+
+    storage initialStorage = lastStorage;
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 balanceAfterSingleTransaction = balanceOf(to, id);
+
+    safeTransferFrom(e, from, to, id, amount1, data) at initialStorage;
+    safeTransferFrom(e, from, to, id, amount2, data);
+
+    uint256 balanceAfterDoubleTransaction = balanceOf(to, id);
+
+    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
+}
+
+
+// STATUS - verified
+// safeTransferFrom updates `from` and `to` balances
+rule transferCorrectness(env e){
+    address from; address to; uint256 id; uint256 amount; bytes data;
+
+    require to != from;
+
+    uint256 fromBalanceBefore = balanceOf(from, id);
+    uint256 toBalanceBefore = balanceOf(to, id);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 fromBalanceAfter = balanceOf(from, id);
+    uint256 toBalanceAfter = balanceOf(to, id);
+
+    assert fromBalanceBefore == fromBalanceAfter + amount, "Something wet wrong";
+    assert toBalanceBefore == toBalanceAfter - amount, "Something wet wrong";
+}
+
+
+// STATUS - verified
+// safeBatchTransferFrom updates `from` and `to` balances)
+rule transferBatchCorrectness(env e){
+    address from; address to; uint256[] ids; uint256[] amounts; bytes data;
+    uint256 idToCheck1; uint256 amountToCheck1;
+    uint256 idToCheck2; uint256 amountToCheck2;
+    uint256 idToCheck3; uint256 amountToCheck3;
+
+    require to != from;
+    require idToCheck1 != idToCheck2 && idToCheck3 != idToCheck2 && idToCheck1 != idToCheck3;
+
+    require ids.length == 3;
+    require amounts.length == 3;
+    require ids[0] == idToCheck1; require amounts[0] == amountToCheck1;
+    require ids[1] == idToCheck2; require amounts[1] == amountToCheck2;
+    require ids[2] == idToCheck3; require amounts[2] == amountToCheck3;
+
+    uint256 fromBalanceBefore1 = balanceOf(from, idToCheck1);
+    uint256 fromBalanceBefore2 = balanceOf(from, idToCheck2);
+    uint256 fromBalanceBefore3 = balanceOf(from, idToCheck3);
+
+    uint256 toBalanceBefore1 = balanceOf(to, idToCheck1);
+    uint256 toBalanceBefore2 = balanceOf(to, idToCheck2);
+    uint256 toBalanceBefore3 = balanceOf(to, idToCheck3);
+
+    safeBatchTransferFrom(e, from, to, ids, amounts, data);
+
+    uint256 fromBalanceAfter1 = balanceOf(from, idToCheck1);
+    uint256 fromBalanceAfter2 = balanceOf(from, idToCheck2);
+    uint256 fromBalanceAfter3 = balanceOf(from, idToCheck3);
+
+    uint256 toBalanceAfter1 = balanceOf(to, idToCheck1);
+    uint256 toBalanceAfter2 = balanceOf(to, idToCheck2);
+    uint256 toBalanceAfter3 = balanceOf(to, idToCheck3);
+
+    assert (fromBalanceBefore1 == fromBalanceAfter1 + amountToCheck1)
+                && (fromBalanceBefore2 == fromBalanceAfter2 + amountToCheck2)
+                && (fromBalanceBefore3 == fromBalanceAfter3 + amountToCheck3), "Something wet wrong";
+    assert (toBalanceBefore1 == toBalanceAfter1 - amountToCheck1)
+                && (toBalanceBefore2 == toBalanceAfter2 - amountToCheck2)
+                && (toBalanceBefore3 == toBalanceAfter3 - amountToCheck3), "Something wet wrong";
+}
+
+
+// STATUS - verified
+// cannot transfer more than `from` balance (safeTransferFrom version)
+rule cannotTransferMoreSingle(env e){
+    address from; address to; uint256 id; uint256 amount; bytes data;
+    uint256 balanceBefore = balanceOf(from, id);
+
+    safeTransferFrom@withrevert(e, from, to, id, amount, data);
+
+    assert amount > balanceBefore => lastReverted, "Achtung! Scammer!";
+}
+
+
+// STATUS - verified
+// cannot transfer more than allowed (safeBatchTransferFrom version)
+rule cannotTransferMoreBatch(env e){
+    address from; address to; uint256[] ids; uint256[] amounts; bytes data;
+    uint256 idToCheck1; uint256 amountToCheck1;
+    uint256 idToCheck2; uint256 amountToCheck2;
+    uint256 idToCheck3; uint256 amountToCheck3;
+
+    uint256 balanceBefore1 = balanceOf(from, idToCheck1);
+    uint256 balanceBefore2 = balanceOf(from, idToCheck2);
+    uint256 balanceBefore3 = balanceOf(from, idToCheck3);
+
+    require ids.length == 3;
+    require amounts.length == 3;
+    require ids[0] == idToCheck1; require amounts[0] == amountToCheck1;
+    require ids[1] == idToCheck2; require amounts[1] == amountToCheck2;
+    require ids[2] == idToCheck3; require amounts[2] == amountToCheck3;
+
+    safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);
+
+    assert (amountToCheck1 > balanceBefore1 || amountToCheck2 > balanceBefore2 || amountToCheck3 > balanceBefore3) => lastReverted, "Achtung! Scammer!";
+}
+
+
+// STATUS - verified
+// Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0
+rule transferBalanceReduceEffect(env e){
+    address from; address to; address other;
+    uint256 id; uint256 amount;
+    bytes data;
+
+    require other != to;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 otherBalanceAfter = balanceOf(other, id);
+
+    assert from != other => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!";
+}
+
+
+// STATUS - verified
+// Sender calling safeTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0
+rule transferBalanceIncreaseEffect(env e){
+    address from; address to; address other;
+    uint256 id; uint256 amount;
+    bytes data;
+
+    require from != other;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 otherBalanceAfter = balanceOf(other, id);
+
+    assert other != to => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!";
+}
+
+
+// STATUS - verified
+// Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0
+rule transferBatchBalanceFromEffect(env e){
+    address from; address to; address other;
+    uint256[] ids; uint256[] amounts;
+    uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3;
+    bytes data;
+
+    require other != to;
+
+    uint256 otherBalanceBefore1 = balanceOf(other, id1);
+    uint256 otherBalanceBefore2 = balanceOf(other, id2);
+    uint256 otherBalanceBefore3 = balanceOf(other, id3);
+
+    safeBatchTransferFrom(e, from, to, ids, amounts, data);
+
+    uint256 otherBalanceAfter1 = balanceOf(other, id1);
+    uint256 otherBalanceAfter2 = balanceOf(other, id2);
+    uint256 otherBalanceAfter3 = balanceOf(other, id3);
+
+    assert from != other => (otherBalanceBefore1 == otherBalanceAfter1
+                                && otherBalanceBefore2 == otherBalanceAfter2
+                                && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!";
+}
+
+
+// STATUS - verified
+// Sender calling safeBatchTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0
+rule transferBatchBalanceToEffect(env e){
+    address from; address to; address other;
+    uint256[] ids; uint256[] amounts;
+    uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3;
+    bytes data;
+
+    require other != from;
+
+    uint256 otherBalanceBefore1 = balanceOf(other, id1);
+    uint256 otherBalanceBefore2 = balanceOf(other, id2);
+    uint256 otherBalanceBefore3 = balanceOf(other, id3);
+
+    safeBatchTransferFrom(e, from, to, ids, amounts, data);
+
+    uint256 otherBalanceAfter1 = balanceOf(other, id1);
+    uint256 otherBalanceAfter2 = balanceOf(other, id2);
+    uint256 otherBalanceAfter3 = balanceOf(other, id3);
+
+    assert other != to => (otherBalanceBefore1 == otherBalanceAfter1
+                                && otherBalanceBefore2 == otherBalanceAfter2
+                                && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!";
+}
+
+
+// STATUS - verified
+// cannot transfer without approval (safeTransferFrom version)
+rule noTransferForNotApproved(env e) {
+    address from; address operator;
+    address to; uint256 id; uint256 amount; bytes data;
+
+    require from != e.msg.sender;
+
+    bool approve = isApprovedForAll(from, e.msg.sender);
+
+    safeTransferFrom@withrevert(e, from, to, id, amount, data);
+
+    assert !approve => lastReverted, "You don't have king's approval!";
+}
+
+
+// STATUS - verified
+// cannot transfer without approval (safeBatchTransferFrom version)
+rule noTransferBatchForNotApproved(env e) {
+    address from; address operator; address to;
+    bytes data;
+    uint256[] ids; uint256[] amounts;
+
+    require from != e.msg.sender;
+
+    bool approve = isApprovedForAll(from, e.msg.sender);
+
+    safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);
+
+    assert !approve => lastReverted, "You don't have king's approval!";
+}
+
+
+// STATUS - verified
+// safeTransferFrom doesn't affect any approval
+rule noTransferEffectOnApproval(env e){
+    address from; address to;
+    address owner; address operator;
+    uint256 id; uint256 amount;
+    bytes data;
+
+    bool approveBefore = isApprovedForAll(owner, operator);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    bool approveAfter = isApprovedForAll(owner, operator);
+
+    assert approveBefore == approveAfter, "Something was effected";
+}
+
+
+// STATUS - verified
+// safeTransferFrom doesn't affect any approval
+rule noTransferBatchEffectOnApproval(env e){
+    address from; address to;
+    address owner; address operator;
+    uint256[] ids; uint256[] amounts;
+    bytes data;
+
+    bool approveBefore = isApprovedForAll(owner, operator);
+
+    safeBatchTransferFrom(e, from, to, ids, amounts, data);
+
+    bool approveAfter = isApprovedForAll(owner, operator);
+
+    assert approveBefore == approveAfter, "Something was effected";
+}
+
+
+
+/////////////////////////////////////////////////
+// Mint (7/9)
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// Additivity of mint: mint(a); mint(b) has same effect as mint(a+b)
+rule mintAdditivity(env e){
+    address to; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; bytes data;
+    require amount == amount1 + amount2;
+
+    storage initialStorage = lastStorage;
+
+    mint(e, to, id, amount, data);
+
+    uint256 balanceAfterSingleTransaction = balanceOf(to, id);
+
+    mint(e, to, id, amount1, data) at initialStorage;
+    mint(e, to, id, amount2, data);
+
+    uint256 balanceAfterDoubleTransaction = balanceOf(to, id);
+
+    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
+}
+
+
+// STATUS - verified
+// Check that `mint()` revertes in planned scenario(s) (only if `to` is 0)
+rule mintRevertCases(env e){
+    address to; uint256 id; uint256 amount; bytes data;
+
+    mint@withrevert(e, to, id, amount, data);
+
+    assert to == 0 => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
+// Check that `mintBatch()` revertes in planned scenario(s) (only if `to` is 0 or arrays have different length)
+rule mintBatchRevertCases(env e){
+    address to; uint256[] ids; uint256[] amounts; bytes data;
+
+    require ids.length < 1000000000;
+    require amounts.length < 1000000000;
+
+    mintBatch@withrevert(e, to, ids, amounts, data);
+
+    assert (ids.length != amounts.length || to == 0) => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
+// Check that mint updates `to` balance correctly
+rule mintCorrectWork(env e){
+    address to; uint256 id; uint256 amount; bytes data;
+
+    uint256 otherBalanceBefore = balanceOf(to, id);
+
+    mint(e, to, id, amount, data);
+
+    uint256 otherBalanceAfter = balanceOf(to, id);
+
+    assert otherBalanceBefore == otherBalanceAfter - amount, "Something is wrong";
+}
+
+
+// STATUS - verified
+// check that mintBatch updates `bootcamp participantsfrom` balance correctly
+rule mintBatchCorrectWork(env e){
+    address to;
+    uint256 id1; uint256 id2; uint256 id3;
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+    bytes data;
+
+    require ids.length == 3;
+    require amounts.length == 3;
+
+    require id1 != id2 && id2 != id3 && id3 != id1;
+    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
+    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
+
+    uint256 otherBalanceBefore1 = balanceOf(to, id1);
+    uint256 otherBalanceBefore2 = balanceOf(to, id2);
+    uint256 otherBalanceBefore3 = balanceOf(to, id3);
+
+    mintBatch(e, to, ids, amounts, data);
+
+    uint256 otherBalanceAfter1 = balanceOf(to, id1);
+    uint256 otherBalanceAfter2 = balanceOf(to, id2);
+    uint256 otherBalanceAfter3 = balanceOf(to, id3);
+
+    assert otherBalanceBefore1 == otherBalanceAfter1 - amount1
+            && otherBalanceBefore2 == otherBalanceAfter2 - amount2
+            && otherBalanceBefore3 == otherBalanceAfter3 - amount3
+            , "Something is wrong";
+}
+
+
+// STATUS - verified
+// The user cannot mint more than max_uint256
+rule cantMintMoreSingle(env e){
+    address to; uint256 id; uint256 amount; bytes data;
+
+    require to_mathint(balanceOf(to, id) + amount) > max_uint256;
+
+    mint@withrevert(e, to, id, amount, data);
+
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// STATUS - verified
+// the user cannot mint more than max_uint256 (batch version)
+rule cantMintMoreBatch(env e){
+    address to; bytes data;
+    uint256 id1; uint256 id2; uint256 id3;
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+
+    require ids.length == 3;
+    require amounts.length == 3;
+
+    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
+    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
+
+    require to_mathint(balanceOf(to, id1) + amount1) > max_uint256
+                || to_mathint(balanceOf(to, id2) + amount2) > max_uint256
+                || to_mathint(balanceOf(to, id3) + amount3) > max_uint256;
+
+    mintBatch@withrevert(e, to, ids, amounts, data);
+
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// STATUS - verified
+// `mint()` changes only `to` balance
+rule cantMintOtherBalances(env e){
+    address to; uint256 id; uint256 amount; bytes data;
+    address other;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    mint(e, to, id, amount, data);
+
+    uint256 otherBalanceAfter = balanceOf(other, id);
+
+    assert other != to => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing";
+}
+
+
+// STATUS - verified
+// mintBatch changes only `to` balance
+rule cantMintBatchOtherBalances(env e){
+    address to;
+    uint256 id1; uint256 id2; uint256 id3;
+    uint256[] ids; uint256[] amounts;
+    address other;
+    bytes data;
+
+    uint256 otherBalanceBefore1 = balanceOf(other, id1);
+    uint256 otherBalanceBefore2 = balanceOf(other, id2);
+    uint256 otherBalanceBefore3 = balanceOf(other, id3);
+
+    mintBatch(e, to, ids, amounts, data);
+
+    uint256 otherBalanceAfter1 = balanceOf(other, id1);
+    uint256 otherBalanceAfter2 = balanceOf(other, id2);
+    uint256 otherBalanceAfter3 = balanceOf(other, id3);
+
+    assert other != to => (otherBalanceBefore1 == otherBalanceAfter1
+                                && otherBalanceBefore2 == otherBalanceAfter2
+                                && otherBalanceBefore3 == otherBalanceAfter3)
+                                , "I like to see your money disappearing";
+}
+
+
+/////////////////////////////////////////////////
+// Burn (9/9)
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// Additivity of burn: burn(a); burn(b) has same effect as burn(a+b)
+rule burnAdditivity(env e){
+    address from; uint256 id; uint256 amount; uint256 amount1; uint256 amount2;
+    require amount == amount1 + amount2;
+
+    storage initialStorage = lastStorage;
+
+    burn(e, from, id, amount);
+
+    uint256 balanceAfterSingleTransaction = balanceOf(from, id);
+
+    burn(e, from, id, amount1) at initialStorage;
+    burn(e, from, id, amount2);
+
+    uint256 balanceAfterDoubleTransaction = balanceOf(from, id);
+
+    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
+}
+
+
+// STATUS - verified
+// Check that `burn()` revertes in planned scenario(s) (if `from` is 0)
+rule burnRevertCases(env e){
+    address from; uint256 id; uint256 amount;
+
+    burn@withrevert(e, from, id, amount);
+
+    assert from == 0 => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
+// Check that `balanceOf()` revertes in planned scenario(s) (if `from` is 0 or arrays have different length)
+rule burnBatchRevertCases(env e){
+    address from; uint256[] ids; uint256[] amounts;
+
+    require ids.length < 1000000000;
+    require amounts.length < 1000000000;
+
+    burnBatch@withrevert(e, from, ids, amounts);
+
+    assert (from == 0 || ids.length != amounts.length) => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
+// check that burn updates `from` balance correctly
+rule burnCorrectWork(env e){
+    address from; uint256 id; uint256 amount;
+
+    uint256 otherBalanceBefore = balanceOf(from, id);
+
+    burn(e, from, id, amount);
+
+    uint256 otherBalanceAfter = balanceOf(from, id);
+
+    assert otherBalanceBefore == otherBalanceAfter + amount, "Something is wrong";
+}
+
+
+// STATUS - verified
+// check that burnBatch updates `from` balance correctly
+rule burnBatchCorrectWork(env e){
+    address from;
+    uint256 id1; uint256 id2; uint256 id3;
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+
+    require ids.length == 3;
+
+    require id1 != id2 && id2 != id3 && id3 != id1;
+    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
+    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
+
+    uint256 otherBalanceBefore1 = balanceOf(from, id1);
+    uint256 otherBalanceBefore2 = balanceOf(from, id2);
+    uint256 otherBalanceBefore3 = balanceOf(from, id3);
+
+    burnBatch(e, from, ids, amounts);
+
+    uint256 otherBalanceAfter1 = balanceOf(from, id1);
+    uint256 otherBalanceAfter2 = balanceOf(from, id2);
+    uint256 otherBalanceAfter3 = balanceOf(from, id3);
+
+    assert otherBalanceBefore1 == otherBalanceAfter1 + amount1
+            && otherBalanceBefore2 == otherBalanceAfter2 + amount2
+            && otherBalanceBefore3 == otherBalanceAfter3 + amount3
+            , "Something is wrong";
+}
+
+
+// STATUS - verified
+// the user cannot burn more than they have
+rule cantBurnMoreSingle(env e){
+    address from; uint256 id; uint256 amount;
+
+    require to_mathint(balanceOf(from, id) - amount) < 0;
+
+    burn@withrevert(e, from, id, amount);
+
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// STATUS - verified
+// the user cannot burn more than they have (batch version)
+rule cantBurnMoreBatch(env e){
+    address from;
+    uint256 id1; uint256 id2; uint256 id3;
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+
+    require ids.length == 3;
+
+    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
+    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
+
+    require to_mathint(balanceOf(from, id1) - amount1) < 0
+                || to_mathint(balanceOf(from, id2) - amount2) < 0
+                || to_mathint(balanceOf(from, id3) - amount3) < 0 ;
+
+    burnBatch@withrevert(e, from, ids, amounts);
+
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// STATUS - verified
+// burn changes only `from` balance
+rule cantBurnOtherBalances(env e){
+    address from; uint256 id; uint256 amount;
+    address other;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    burn(e, from, id, amount);
+
+    uint256 otherBalanceAfter = balanceOf(other, id);
+
+    assert other != from => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing";
+}
+
+
+// STATUS - verified
+// burnBatch changes only `from` balance
+rule cantBurnBatchOtherBalances(env e){
+    address from;
+    uint256 id1; uint256 id2; uint256 id3;
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+    address other;
+
+    uint256 otherBalanceBefore1 = balanceOf(other, id1);
+    uint256 otherBalanceBefore2 = balanceOf(other, id2);
+    uint256 otherBalanceBefore3 = balanceOf(other, id3);
+
+    burnBatch(e, from, ids, amounts);
+
+    uint256 otherBalanceAfter1 = balanceOf(other, id1);
+    uint256 otherBalanceAfter2 = balanceOf(other, id2);
+    uint256 otherBalanceAfter3 = balanceOf(other, id3);
+
+    assert other != from => (otherBalanceBefore1 == otherBalanceAfter1
+                                && otherBalanceBefore2 == otherBalanceAfter2
+                                && otherBalanceBefore3 == otherBalanceAfter3)
+                                , "I like to see your money disappearing";
+}
+
+/////////////////////////////////////////////////
+// The rules below were added to this base ERC1155 spec as part of a later
+// project with OpenZeppelin covering various ERC1155 extensions.
+/////////////////////////////////////////////////
+
+/// The result of transferring a single token must be equivalent whether done
+/// via safeTransferFrom or safeBatchTransferFrom.
+rule singleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
+    storage beforeTransfer = lastStorage;
+    env e;
+
+    address holder; address recipient;
+    uint256 token; uint256 transferAmount; bytes data;
+    uint256[] tokens; uint256[] transferAmounts;
+
+    mathint holderStartingBalance = balanceOf(holder, token);
+    mathint recipientStartingBalance = balanceOf(recipient, token);
+
+    require tokens.length == 1; require transferAmounts.length == 1;
+    require tokens[0] == token; require transferAmounts[0] == transferAmount;
+
+    // transferring via safeTransferFrom
+    safeTransferFrom(e, holder, recipient, token, transferAmount, data) at beforeTransfer;
+    mathint holderSafeTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
+    mathint recipientSafeTransferFromBalanceChange = balanceOf(recipient, token) - recipientStartingBalance;
+
+    // transferring via safeBatchTransferFrom
+    safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfer;
+    mathint holderSafeBatchTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
+    mathint recipientSafeBatchTransferFromBalanceChange = balanceOf(recipient, token) - recipientStartingBalance;
+
+    assert holderSafeTransferFromBalanceChange == holderSafeBatchTransferFromBalanceChange
+        && recipientSafeTransferFromBalanceChange == recipientSafeBatchTransferFromBalanceChange,
+        "Transferring a single token via safeTransferFrom or safeBatchTransferFrom must be equivalent";
+}
+
+/// The results of transferring multiple tokens must be equivalent whether done
+/// separately via safeTransferFrom or together via safeBatchTransferFrom.
+rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
+    storage beforeTransfers = lastStorage;
+    env e;
+
+    address holder; address recipient; bytes data;
+    uint256 tokenA; uint256 tokenB; uint256 tokenC;
+    uint256 transferAmountA; uint256 transferAmountB; uint256 transferAmountC;
+    uint256[] tokens; uint256[] transferAmounts;
+
+    mathint holderStartingBalanceA = balanceOf(holder, tokenA);
+    mathint holderStartingBalanceB = balanceOf(holder, tokenB);
+    mathint holderStartingBalanceC = balanceOf(holder, tokenC);
+    mathint recipientStartingBalanceA = balanceOf(recipient, tokenA);
+    mathint recipientStartingBalanceB = balanceOf(recipient, tokenB);
+    mathint recipientStartingBalanceC = balanceOf(recipient, tokenC);
+
+    require tokens.length == 3; require transferAmounts.length == 3;
+    require tokens[0] == tokenA; require transferAmounts[0] == transferAmountA;
+    require tokens[1] == tokenB; require transferAmounts[1] == transferAmountB;
+    require tokens[2] == tokenC; require transferAmounts[2] == transferAmountC;
+
+    // transferring via safeTransferFrom
+    safeTransferFrom(e, holder, recipient, tokenA, transferAmountA, data) at beforeTransfers;
+    safeTransferFrom(e, holder, recipient, tokenB, transferAmountB, data);
+    safeTransferFrom(e, holder, recipient, tokenC, transferAmountC, data);
+    mathint holderSafeTransferFromBalanceChangeA = holderStartingBalanceA - balanceOf(holder, tokenA);
+    mathint holderSafeTransferFromBalanceChangeB = holderStartingBalanceB - balanceOf(holder, tokenB);
+    mathint holderSafeTransferFromBalanceChangeC = holderStartingBalanceC - balanceOf(holder, tokenC);
+    mathint recipientSafeTransferFromBalanceChangeA = balanceOf(recipient, tokenA) - recipientStartingBalanceA;
+    mathint recipientSafeTransferFromBalanceChangeB = balanceOf(recipient, tokenB) - recipientStartingBalanceB;
+    mathint recipientSafeTransferFromBalanceChangeC = balanceOf(recipient, tokenC) - recipientStartingBalanceC;
+
+    // transferring via safeBatchTransferFrom
+    safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfers;
+    mathint holderSafeBatchTransferFromBalanceChangeA = holderStartingBalanceA - balanceOf(holder, tokenA);
+    mathint holderSafeBatchTransferFromBalanceChangeB = holderStartingBalanceB - balanceOf(holder, tokenB);
+    mathint holderSafeBatchTransferFromBalanceChangeC = holderStartingBalanceC - balanceOf(holder, tokenC);
+    mathint recipientSafeBatchTransferFromBalanceChangeA = balanceOf(recipient, tokenA) - recipientStartingBalanceA;
+    mathint recipientSafeBatchTransferFromBalanceChangeB = balanceOf(recipient, tokenB) - recipientStartingBalanceB;
+    mathint recipientSafeBatchTransferFromBalanceChangeC = balanceOf(recipient, tokenC) - recipientStartingBalanceC;
+
+    assert holderSafeTransferFromBalanceChangeA == holderSafeBatchTransferFromBalanceChangeA
+        && holderSafeTransferFromBalanceChangeB == holderSafeBatchTransferFromBalanceChangeB
+        && holderSafeTransferFromBalanceChangeC == holderSafeBatchTransferFromBalanceChangeC
+        && recipientSafeTransferFromBalanceChangeA == recipientSafeBatchTransferFromBalanceChangeA
+        && recipientSafeTransferFromBalanceChangeB == recipientSafeBatchTransferFromBalanceChangeB
+        && recipientSafeTransferFromBalanceChangeC == recipientSafeBatchTransferFromBalanceChangeC,
+        "Transferring multiple tokens via safeTransferFrom or safeBatchTransferFrom must be equivalent";
+}
+
+/// If transfer methods do not revert, the input arrays must be the same length.
+rule transfersHaveSameLengthInputArrays {
+    env e;
+
+    address recipient; bytes data;
+    uint256[] tokens; uint256[] transferAmounts;
+    uint max_int = 0xffffffffffffffffffffffffffffffff;
+
+    require tokens.length >= 0 && tokens.length <= max_int;
+    require transferAmounts.length >= 0 && transferAmounts.length <= max_int;
+
+    safeBatchTransferFrom(e, _, recipient, tokens, transferAmounts, data);
+
+    uint256 tokensLength = tokens.length;
+    uint256 transferAmountsLength = transferAmounts.length;
+
+    assert tokens.length == transferAmounts.length,
+        "If transfer methods do not revert, the input arrays must be the same length";
+}

certora/specs/ERC1155Burnable.spec

@@ -0,0 +1,187 @@
+//// ## Verification of `ERC1155Burnable`
+//// 
+//// `ERC1155Burnable` extends the `ERC1155` functionality by wrapping the internal
+//// methods `_burn` and `_burnBatch` in the public methods `burn` and `burnBatch`,
+//// adding a requirement that the caller of either method be the account holding
+//// the tokens or approved to act on that account's behalf.
+//// 
+//// ### Assumptions and Simplifications
+//// 
+//// - No changes made using the harness
+//// 
+//// ### Properties
+
+methods {
+    balanceOf(address, uint256) returns uint256 envfree
+    isApprovedForAll(address,address) returns bool envfree
+}
+
+/// If a method call reduces account balances, the caller must be either the 
+/// holder of the account or approved to act on the holder's behalf.
+rule onlyHolderOrApprovedCanReduceBalance(method f) 
+{
+    address holder; uint256 token; uint256 amount;
+    uint256 balanceBefore = balanceOf(holder, token);
+
+    env e; calldataarg args;
+    f(e, args);
+
+    uint256 balanceAfter = balanceOf(holder, token);
+
+    assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender), 
+        "An account balance may only be reduced by the holder or a holder-approved agent";
+}
+
+/// Burning a larger amount of a token must reduce that token's balance more 
+/// than burning a smaller amount.
+/// n.b. This rule holds for `burnBatch` as well due to rules establishing 
+/// appropriate equivalence between `burn` and `burnBatch` methods.
+rule burnAmountProportionalToBalanceReduction {
+    storage beforeBurn = lastStorage;
+    env e;
+    
+    address holder; uint256 token;
+    mathint startingBalance = balanceOf(holder, token);
+    uint256 smallBurn; uint256 largeBurn;
+    require smallBurn < largeBurn;
+
+    // smaller burn amount
+    burn(e, holder, token, smallBurn) at beforeBurn;
+    mathint smallBurnBalanceChange = startingBalance - balanceOf(holder, token);
+
+    // larger burn amount
+    burn(e, holder, token, largeBurn) at beforeBurn;
+    mathint largeBurnBalanceChange = startingBalance - balanceOf(holder, token);
+
+    assert smallBurnBalanceChange < largeBurnBalanceChange, 
+        "A larger burn must lead to a larger decrease in balance";
+}
+
+/// Two sequential burns must be equivalent to a single burn of the sum of their
+/// amounts.
+/// This rule holds for `burnBatch` as well due to rules establishing 
+/// appropriate equivalence between `burn` and `burnBatch` methods.
+rule sequentialBurnsEquivalentToSingleBurnOfSum {
+    storage beforeBurns = lastStorage;
+    env e;
+
+    address holder; uint256 token;
+    mathint startingBalance = balanceOf(holder, token);
+    uint256 firstBurn; uint256 secondBurn; uint256 sumBurn;
+    require sumBurn == firstBurn + secondBurn;
+
+    // sequential burns
+    burn(e, holder, token, firstBurn) at beforeBurns;
+    burn(e, holder, token, secondBurn);
+    mathint sequentialBurnsBalanceChange = startingBalance - balanceOf(holder, token);
+
+    // burn of sum of sequential burns
+    burn(e, holder, token, sumBurn) at beforeBurns;
+    mathint sumBurnBalanceChange = startingBalance - balanceOf(holder, token);
+
+    assert sequentialBurnsBalanceChange == sumBurnBalanceChange, 
+        "Sequential burns must be equivalent to a burn of their sum";
+}
+
+/// The result of burning a single token must be equivalent whether done via
+/// burn or burnBatch.
+/// @title Single token `burn` / `burnBatch` equivalence
+rule singleTokenBurnBurnBatchEquivalence {
+    storage beforeBurn = lastStorage;
+    env e;
+
+    address holder;
+    uint256 token; uint256 burnAmount;
+    uint256[] tokens; uint256[] burnAmounts;
+
+    mathint startingBalance = balanceOf(holder, token);
+
+    require tokens.length == 1; require burnAmounts.length == 1;
+    require tokens[0] == token; require burnAmounts[0] == burnAmount;
+
+    // burning via burn
+    burn(e, holder, token, burnAmount) at beforeBurn;
+    mathint burnBalanceChange = startingBalance - balanceOf(holder, token);
+
+    // burning via burnBatch
+    burnBatch(e, holder, tokens, burnAmounts) at beforeBurn;
+    mathint burnBatchBalanceChange = startingBalance - balanceOf(holder, token);
+
+    assert burnBalanceChange == burnBatchBalanceChange, 
+        "Burning a single token via burn or burnBatch must be equivalent";
+}   
+
+/// The results of burning multiple tokens must be equivalent whether done 
+/// separately via `burn` or together via `burnBatch`.
+/// @title Multiple token `burn` / `burnBatch` equivalence
+rule multipleTokenBurnBurnBatchEquivalence {
+    storage beforeBurns = lastStorage;
+    env e;
+
+    address holder;
+    uint256 tokenA; uint256 tokenB; uint256 tokenC;
+    uint256 burnAmountA; uint256 burnAmountB; uint256 burnAmountC;
+    uint256[] tokens; uint256[] burnAmounts;
+
+    mathint startingBalanceA = balanceOf(holder, tokenA);
+    mathint startingBalanceB = balanceOf(holder, tokenB);
+    mathint startingBalanceC = balanceOf(holder, tokenC);
+
+    require tokens.length == 3; require burnAmounts.length == 3;
+    require tokens[0] == tokenA; require burnAmounts[0] == burnAmountA;
+    require tokens[1] == tokenB; require burnAmounts[1] == burnAmountB;
+    require tokens[2] == tokenC; require burnAmounts[2] == burnAmountC;
+
+    // burning via burn
+    burn(e, holder, tokenA, burnAmountA) at beforeBurns;
+    burn(e, holder, tokenB, burnAmountB);
+    burn(e, holder, tokenC, burnAmountC);
+    mathint burnBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA);
+    mathint burnBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB);
+    mathint burnBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC);
+
+    // burning via burnBatch
+    burnBatch(e, holder, tokens, burnAmounts) at beforeBurns;
+    mathint burnBatchBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA);
+    mathint burnBatchBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB);
+    mathint burnBatchBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC);
+
+    assert burnBalanceChangeA == burnBatchBalanceChangeA
+        && burnBalanceChangeB == burnBatchBalanceChangeB
+        && burnBalanceChangeC == burnBatchBalanceChangeC, 
+        "Burning multiple tokens via burn or burnBatch must be equivalent";
+}
+
+/// If passed empty token and burn amount arrays, `burnBatch` must not change 
+/// token balances or address permissions.
+rule burnBatchOnEmptyArraysChangesNothing {
+    uint256 token; address nonHolderA; address nonHolderB;
+
+    uint256 startingBalance = balanceOf(nonHolderA, token);
+    bool startingPermission = isApprovedForAll(nonHolderA, nonHolderB);
+
+    env e; address holder; uint256[] noTokens; uint256[] noBurnAmounts;
+    require noTokens.length == 0; require noBurnAmounts.length == 0;
+
+    burnBatch(e, holder, noTokens, noBurnAmounts);
+    
+    uint256 endingBalance = balanceOf(nonHolderA, token);
+    bool endingPermission = isApprovedForAll(nonHolderA, nonHolderB);
+
+    assert startingBalance == endingBalance, 
+        "burnBatch must not change token balances if passed empty arrays";
+    assert startingPermission == endingPermission, 
+        "burnBatch must not change account permissions if passed empty arrays";
+}
+
+/*
+/// This rule should always fail.
+rule sanity {
+    method f; env e; calldataarg args;
+
+    f(e, args);
+
+    assert false, 
+        "This rule should always fail";
+}
+*/

certora/specs/ERC1155Pausable.spec

@@ -0,0 +1,130 @@
+//// ## Verification of `ERC1155Pausable`
+//// 
+//// `ERC1155Pausable` extends existing `Pausable` functionality by requiring that a
+//// contract not be in a `paused` state prior to a token transfer.
+//// 
+//// ### Assumptions and Simplifications
+//// - Internal methods `_pause` and `_unpause` wrapped by functions callable from CVL
+//// - Dummy functions created to verify `whenPaused` and `whenNotPaused` modifiers
+//// 
+//// 
+//// ### Properties
+
+methods {
+    balanceOf(address, uint256) returns uint256 envfree
+    paused() returns bool envfree
+}
+
+/// When a contract is in a paused state, the token balance for a given user and
+/// token must not change.
+rule balancesUnchangedWhenPaused() {
+    address user; uint256 token;
+    uint256 balanceBefore = balanceOf(user, token);
+
+    require paused();
+
+    method f; calldataarg arg; env e;
+    f(e, arg);
+
+    uint256 balanceAfter = balanceOf(user, token);
+
+    assert balanceBefore == balanceAfter, 
+        "Token balance for a user must not change in a paused contract";
+}
+
+/// When a contract is in a paused state, transfer methods must revert.
+rule transferMethodsRevertWhenPaused (method f)
+filtered {
+    f -> f.selector == safeTransferFrom(address,address,uint256,uint256,bytes).selector
+      || f.selector == safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector
+}
+{
+    require paused();
+
+    env e; calldataarg args;
+    f@withrevert(e, args);
+
+    assert lastReverted, 
+        "Transfer methods must revert in a paused contract";
+}
+
+/// When a contract is in an unpaused state, calling `pause()` must pause.
+rule pauseMethodPausesContract {
+    require !paused();
+
+    env e;
+    pause(e);
+
+    assert paused(), 
+        "Calling pause must pause an unpaused contract";
+}
+
+/// When a contract is in a paused state, calling unpause() must unpause.
+rule unpauseMethodUnpausesContract {
+    require paused();
+
+    env e;
+    unpause(e);
+
+    assert !paused(), 
+        "Calling unpause must unpause a paused contract";
+}
+
+/// When a contract is in a paused state, calling pause() must revert.
+rule cannotPauseWhilePaused {
+    require paused();
+
+    env e;
+    pause@withrevert(e);
+
+    assert lastReverted, 
+        "A call to pause when already paused must revert";
+}
+
+/// When a contract is in an unpaused state, calling unpause() must revert.
+rule cannotUnpauseWhileUnpaused {
+    require !paused();
+
+    env e;
+    unpause@withrevert(e);
+
+    assert lastReverted, 
+        "A call to unpause when already unpaused must revert";
+}
+
+/// When a contract is in a paused state, functions with the `whenNotPaused`
+/// modifier must revert.
+/// @title `whenNotPaused` modifier causes revert if paused
+rule whenNotPausedModifierCausesRevertIfPaused {
+    require paused();
+
+    env e; calldataarg args;
+    onlyWhenNotPausedMethod@withrevert(e, args);
+
+    assert lastReverted, 
+        "Functions with the whenNotPaused modifier must revert if the contract is paused";
+}
+
+/// When a contract is in an unpaused state, functions with the `whenPaused`
+/// modifier must revert.
+/// @title `whenPaused` modifier causes revert if unpaused
+rule whenPausedModifierCausesRevertIfUnpaused {
+    require !paused();
+
+    env e; calldataarg args;
+    onlyWhenPausedMethod@withrevert(e, args);
+
+    assert lastReverted, 
+        "Functions with the whenPaused modifier must revert if the contract is not paused";
+}
+/*
+/// This rule should always fail.
+rule sanity {
+    method f; env e; calldataarg args;
+
+    f(e, args);
+
+    assert false, 
+        "This rule should always fail";
+}
+*/

certora/specs/ERC1155Supply.spec

@@ -0,0 +1,93 @@
+//// ## Verification of `ERC1155Supply`
+//// 
+//// `ERC1155Supply` extends the `ERC1155` functionality. The contract creates a publicly callable `totalSupply` wrapper for the private `_totalSupply` method, a public `exists` method to check for a positive balance of a given token, and updates `_beforeTokenTransfer` to appropriately change the mapping `_totalSupply` in the context of minting and burning tokens.
+//// 
+//// ### Assumptions and Simplifications
+//// - The `exists` method was wrapped in the `exists_wrapper` method because `exists` is a keyword in CVL.
+//// - The public functions `burn`, `burnBatch`, `mint`, and `mintBatch` were implemented in the harnessing contract make their respective internal functions callable by the CVL. This was used to test the increase and decrease of `totalSupply` when tokens are minted and burned. 
+//// - We created the `onlyOwner` modifier to be used in the above functions so that they are not called in unrelated rules.
+//// 
+//// ### Properties
+
+
+methods {
+    totalSupply(uint256) returns uint256 envfree
+    balanceOf(address, uint256) returns uint256 envfree
+    exists_wrapper(uint256) returns bool envfree
+    owner() returns address envfree
+}
+ 
+/// Given two different token ids, if total supply for one changes, then
+/// total supply for other must not.
+rule token_totalSupply_independence(method f)
+filtered {
+    f -> f.selector != safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector
+}
+{
+    uint256 token1; uint256 token2;
+    require token1 != token2;
+
+    uint256 token1_before = totalSupply(token1);
+    uint256 token2_before = totalSupply(token2);
+
+    env e; calldataarg args;
+    require e.msg.sender != owner(); // owner can call mintBatch and burnBatch in our harness
+    f(e, args);
+
+    uint256 token1_after = totalSupply(token1);
+    uint256 token2_after = totalSupply(token2);
+
+    assert token1_after != token1_before => token2_after == token2_before,
+        "methods must not change the total supply of more than one token";
+}
+
+/******************************************************************************/
+
+ghost mapping(uint256 => mathint) sumOfBalances {
+    init_state axiom forall uint256 token . sumOfBalances[token] == 0;
+}
+
+hook Sstore _balances[KEY uint256 token][KEY address user] uint256 newValue (uint256 oldValue) STORAGE {
+    sumOfBalances[token] = sumOfBalances[token] + newValue - oldValue;
+}
+
+/// The sum of the balances over all users must equal the total supply for a 
+/// given token.
+invariant total_supply_is_sum_of_balances(uint256 token)
+    sumOfBalances[token] == totalSupply(token)
+    {
+        preserved {
+            requireInvariant balanceOfZeroAddressIsZero(token);
+        }
+    }
+
+/******************************************************************************/
+
+/// The balance of a token for the zero address must be zero.
+invariant balanceOfZeroAddressIsZero(uint256 token)
+    balanceOf(0, token) == 0
+
+/// If a user has a token, then the token should exist.
+rule held_tokens_should_exist {
+    address user; uint256 token;
+
+    requireInvariant balanceOfZeroAddressIsZero(token);
+
+    // This assumption is safe because of total_supply_is_sum_of_balances
+    require balanceOf(user, token) <= totalSupply(token);
+
+    // note: `exists_wrapper` just calls `exists`
+    assert balanceOf(user, token) > 0 => exists_wrapper(token),
+        "if a user's balance for a token is positive, the token must exist";
+}
+
+/******************************************************************************/
+/*
+rule sanity {
+    method f; env e; calldataarg args;
+
+    f(e, args);
+
+    assert false;
+}
+*/

certora/specs/ERC20.spec

@@ -0,0 +1,385 @@
+import "erc20methods.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    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 == approve(address,uint256).selector              && e.msg.sender == holder ) ||
+        (f.selector == decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
+        (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
+        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: mint behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mint() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address to;
+    address other;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // 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 > to_uint256(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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address from;
+    address other;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // 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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address recipient;
+    address other;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // 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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder;
+    address recipient;
+    address other;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
+    uint256 allowanceBefore        = allowance(holder, e.msg.sender);
+    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 || amount > holderBalanceBefore || amount > allowanceBefore;
+    } else {
+        // allowance is valid & updated
+        assert allowanceBefore                 >= amount;
+        assert allowance(holder, e.msg.sender) == (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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    approve@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert 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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    increaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert 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() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    decreaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert 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);
+    }
+}

certora/specs/ERC20FlashMint.spec

@@ -0,0 +1,30 @@
+import "erc20methods.spec"
+
+methods {
+    maxFlashLoan(address) returns(uint256) envfree
+    _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount)
+}
+
+ghost mapping(address => uint256) trackedBurnAmount;
+
+// returns is needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'"
+function specBurn(address account, uint256 amount) returns bool {
+    trackedBurnAmount[account] = amount;
+    return true;
+}
+
+// Check that if flashLoan() call is successful, then proper amount of tokens was burnt(fee + flashLoan amount)
+rule letsWatchItBurns(env e) {
+    address receiver;
+    address token;
+    uint256 amount;
+    bytes data;
+
+    uint256 feeBefore = flashFee(e, token, amount);
+
+    flashLoan(e, receiver, token, amount, data);
+
+    uint256 burned = trackedBurnAmount[receiver];
+
+    assert to_mathint(amount + feeBefore) == burned, "cheater";
+}

certora/specs/ERC20Votes.spec

@@ -0,0 +1,299 @@
+import "erc20methods.spec"
+
+methods {
+    // IVotes
+    getVotes(address)                                                 returns (uint256) envfree
+    getPastVotes(address, uint256)                                    returns (uint256) // not envfree (reads block.number)
+    getPastTotalSupply(uint256)                                       returns (uint256) // not envfree (reads block.number)
+    delegates(address)                                                returns (address) envfree
+    delegate(address)                                                                   // not envfree (reads msg.sender)
+    delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32)                   // not envfree (reads msg.sender)
+
+    // ERC20Votes
+    checkpoints(address, uint32)                                                        envfree
+    numCheckpoints(address)                                           returns (uint32)  envfree
+    _maxSupply()                                                      returns (uint224) envfree
+    _delegate(address, address)                                                         // not envfree (reads block.number when creating checkpoint)
+
+    // harnesss functions
+    ckptFromBlock(address, uint32)                                    returns (uint32)  envfree
+    ckptVotes(address, uint32)                                        returns (uint224) envfree
+    unsafeNumCheckpoints(address)                                     returns (uint256) envfree
+
+    // solidity generated getters
+    _delegates(address)                                               returns (address) envfree
+}
+
+// gets the most recent votes for a user
+ghost userVotes(address) returns uint224 {
+    init_state axiom forall address a. userVotes(a) == 0;
+}
+
+// sums the total votes for all users
+ghost totalVotes() returns uint224 {
+    init_state axiom totalVotes() == 0;
+}
+
+ghost lastIndex(address) returns uint32;
+
+// helper
+hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
+    havoc userVotes assuming
+        userVotes@new(account) == newVotes;
+
+    havoc totalVotes assuming
+        totalVotes@new() == totalVotes@old() + newVotes - userVotes(account);
+
+    havoc lastIndex assuming
+        lastIndex@new(account) == index;
+}
+
+ghost lastFromBlock(address) returns uint32;
+
+ghost doubleFromBlock(address) returns bool {
+    init_state axiom forall address a. doubleFromBlock(a) == false;
+}
+
+hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE {
+    havoc lastFromBlock assuming
+        lastFromBlock@new(account) == newBlock;
+
+    havoc doubleFromBlock assuming
+        doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
+}
+
+// sum of user balances is >= total amount of delegated votes
+// fails on burn. This is because burn does not remove votes from the users
+invariant votes_solvency()
+    totalSupply() >= to_uint256(totalVotes())
+    filtered { f -> f.selector != _burn(address, uint256).selector }
+{
+    preserved with(env e) {
+        require forall address account. numCheckpoints(account) < 1000000;
+    }
+    preserved _burn(address a, uint256 amount) with(env e) {
+        require _delegates(0) == 0;
+        require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(_delegates(a)) + balanceOf(_delegates(a2)) <= totalVotes());
+        require balanceOf(_delegates(a)) < totalVotes();
+        require amount < 100000;
+    }
+}
+
+// for some checkpoint, the fromBlock is less than the current block number
+invariant blockNum_constrains_fromBlock(address account, uint32 index, env e)
+    ckptFromBlock(account, index) < e.block.number
+    filtered { f -> !f.isView }
+
+// numCheckpoints are less than maxInt
+// passes because numCheckpoints does a safeCast
+// invariant maxInt_constrains_numBlocks(address account)
+//     numCheckpoints(account) < 4294967295 // 2^32
+
+// can't have more checkpoints for a given account than the last from block
+// passes
+invariant fromBlock_constrains_numBlocks(address account)
+    numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1)
+    filtered { f -> !f.isView }
+{
+    preserved with(env e) {
+        require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
+    }
+}
+
+// for any given checkpoint, the fromBlock must be greater than the checkpoint
+// this proves the above invariant in combination with the below invariant
+// if checkpoint has a greater fromBlock than the last, and the FromBlock is always greater than the pos.
+// Then the number of positions must be less than the currentFromBlock
+// ^note that the tool is assuming it's possible for the starting fromBlock to be 0 or anything, and does not know the current starting block
+// passes + rule sanity
+invariant fromBlock_greaterThanEq_pos(address account, uint32 pos)
+    ckptFromBlock(account, pos) >= pos
+    filtered { f -> !f.isView }
+
+// a larger index must have a larger fromBlock
+// passes + rule sanity
+invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2)
+    pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2)
+    filtered { f -> !f.isView }
+
+
+// converted from an invariant to a rule to slightly change the logic
+// if the fromBlock is the same as before, then the number of checkpoints stays the same
+// however if the fromBlock is new than the number of checkpoints increases
+// passes, fails rule sanity because tautology check seems to be bugged
+rule unique_checkpoints_rule(method f) {
+    env e; calldataarg args;
+    address account;
+    uint32 num_ckpts_ = numCheckpoints(account);
+    uint32 fromBlock_ = num_ckpts_ == 0 ? 0 : ckptFromBlock(account, num_ckpts_ - 1);
+
+    f(e, args);
+
+    uint32 _num_ckpts = numCheckpoints(account);
+    uint32 _fromBlock = _num_ckpts == 0 ? 0 : ckptFromBlock(account, _num_ckpts - 1);
+
+    assert fromBlock_ == _fromBlock => num_ckpts_ == _num_ckpts || _num_ckpts == 1, "same fromBlock, new checkpoint";
+}
+
+// assumes neither account has delegated
+// currently fails due to this scenario. A has maxint number of checkpoints
+// an additional checkpoint is added which overflows and sets A's votes to 0
+// passes + rule sanity (- a bad tautology check)
+rule transfer_safe() {
+    env e;
+    uint256 amount;
+    address a; address b;
+    require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same
+    require numCheckpoints(delegates(a)) < 1000000;
+    require numCheckpoints(delegates(b)) < 1000000;
+    uint256 votesA_pre = getVotes(delegates(a));
+    uint256 votesB_pre = getVotes(delegates(b));
+    uint224 totalVotes_pre = totalVotes();
+    transferFrom(e, a, b, amount);
+
+    uint224 totalVotes_post = totalVotes();
+    uint256 votesA_post = getVotes(delegates(a));
+    uint256 votesB_post = getVotes(delegates(b));
+    // if an account that has not delegated transfers balance to an account that has, it will increase the total supply of votes
+    assert totalVotes_pre == totalVotes_post, "transfer changed total supply";
+    assert delegates(a) != 0 => votesA_pre - votesA_post == amount, "A lost the wrong amount of votes";
+    assert delegates(b) != 0 => votesB_post - votesB_pre == amount, "B lost the wrong amount of votes";
+}
+
+// for any given function f, if the delegate is changed the function must be delegate or delegateBySig
+// passes
+rule delegates_safe(method f)
+    filtered { f -> (
+        f.selector != delegate(address).selector &&
+        f.selector != _delegate(address, address).selector &&
+        f.selector != delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32).selector
+    ) }
+{
+    env e; calldataarg args;
+    address account;
+    address pre = delegates(account);
+    f(e, args);
+    address post = delegates(account);
+    assert pre == post, "invalid delegate change";
+}
+
+// delegates increases the delegatee's votes by the proper amount
+// passes + rule sanity
+rule delegatee_receives_votes() {
+    env e;
+    address delegator; address delegatee;
+
+    require delegates(delegator) != delegatee;
+    require delegatee != 0x0;
+
+    uint256 delegator_bal = balanceOf(delegator);
+    uint256 votes_= getVotes(delegatee);
+
+    _delegate(e, delegator, delegatee);
+
+    require lastIndex(delegatee) < 1000000;
+
+    uint256 _votes = getVotes(delegatee);
+
+    assert _votes == votes_ + delegator_bal, "delegatee did not receive votes";
+}
+
+// passes + rule sanity
+rule previous_delegatee_votes_removed() {
+    env e;
+    address delegator; address delegatee; address third;
+
+    require third != delegatee;
+    require delegates(delegator) == third;
+    require numCheckpoints(third) < 1000000;
+
+    uint256 delegator_bal = balanceOf(delegator);
+    uint256 votes_ = getVotes(third);
+
+    _delegate(e, delegator, delegatee);
+
+    uint256 _votes = getVotes(third);
+
+    assert third != 0x0 => _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee";
+}
+
+// passes with rule sanity
+rule delegate_contained() {
+    env e;
+    address delegator; address delegatee; address other;
+
+    require other != delegatee;
+    require other != delegates(delegator);
+
+    uint256 votes_ = getVotes(other);
+
+    _delegate(e, delegator, delegatee);
+
+    uint256 _votes = getVotes(other);
+
+    assert votes_ == _votes, "votes not contained";
+}
+
+rule delegate_no_frontrunning(method f) {
+    env e; calldataarg args;
+    address delegator; address delegatee; address third; address other;
+
+    require numCheckpoints(delegatee) < 1000000;
+    require numCheckpoints(third) < 1000000;
+
+    f(e, args);
+
+    uint256 delegator_bal = balanceOf(delegator);
+    uint256 delegatee_votes_ = getVotes(delegatee);
+    uint256 third_votes_ = getVotes(third);
+    uint256 other_votes_ = getVotes(other);
+    require delegates(delegator) == third;
+    require third != delegatee;
+    require other != third;
+    require other != delegatee;
+    require delegatee != 0x0;
+
+    _delegate(e, delegator, delegatee);
+
+    uint256 _delegatee_votes = getVotes(delegatee);
+    uint256 _third_votes = getVotes(third);
+    uint256 _other_votes = getVotes(other);
+
+
+    // previous delegatee loses all of their votes
+    // delegatee gains that many votes
+    // third loses any votes delegated to them
+    assert _delegatee_votes == delegatee_votes_ + delegator_bal, "delegatee did not receive votes";
+    assert third != 0 => _third_votes == third_votes_ - delegator_bal, "votes not removed from third";
+    assert other_votes_ == _other_votes, "delegate not contained";
+}
+
+rule onMint() {
+    env e;
+    uint256 amount;
+    address account;
+
+    uint256 fromBlock = e.block.number;
+    uint224 totalVotesBefore = totalVotes();
+    uint256 totalSupplyBefore = totalSupply();
+
+    _mint(e, account, amount);
+
+    assert totalVotes() == totalVotesBefore, "totalVotes changed";
+    assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore, "previous totalSupply not saved properly";
+}
+
+rule onBurn() {
+    env e;
+    uint256 amount;
+    address account;
+
+    uint256 fromBlock = e.block.number;
+    uint224 totalVotesBefore = totalVotes();
+    uint256 totalSupplyBefore = totalSupply();
+
+    _burn(e, account, amount);
+
+    assert totalVotes() == totalVotesBefore, "totalVotes changed";
+    assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore, "previous totalSupply not saved properly";
+}

certora/specs/ERC20Wrapper.spec

@@ -0,0 +1,255 @@
+import "ERC20.spec"
+
+methods {
+    underlying() returns(address) envfree
+    underlyingTotalSupply() returns(uint256) envfree
+    underlyingBalanceOf(address) returns(uint256) envfree
+
+    depositFor(address, uint256) returns(bool)
+    withdrawTo(address, uint256) returns(bool)
+    _recover(address) returns(uint256)
+}
+
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+//                                                    Invariants                                                     //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+
+use invariant totalSupplyIsSumOfBalances
+
+// totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency
+invariant whatAboutTotal(env e)
+    totalSupply() <= underlyingTotalSupply()
+    filtered { f -> f.selector != certorafallback_0().selector && !f.isView }
+    {
+        preserved with (env e2) {
+            require underlyingBalanceOf(currentContract) <= underlyingTotalSupply();
+            requireInvariant totalSupplyIsSumOfBalances;
+            require e.msg.sender == e2.msg.sender;
+        }
+        preserved depositFor(address account, uint256 amount) with (env e3){
+            require totalSupply() + amount <= underlyingTotalSupply();
+        }
+        preserved _mint(address account, uint256 amount) with (env e4){
+            require totalSupply() + amount <= underlyingTotalSupply();
+        }
+        preserved _burn(address account, uint256 amount) with (env e5){
+            require balanceOf(account) >= amount;
+            requireInvariant totalSupplyIsSumOfBalances;
+        }
+    }
+
+// totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency
+invariant underTotalAndContractBalanceOfCorrelation(env e)
+    totalSupply() <= underlyingBalanceOf(currentContract)
+    {
+        preserved with (env e2) {
+            require underlying() != currentContract;
+            require e.msg.sender != currentContract;
+            require e.msg.sender == e2.msg.sender;
+            requireInvariant totalSupplyIsSumOfBalances;
+        }
+        preserved _mint(address account, uint256 amount) with (env e4){
+            require totalSupply() + amount <= underlyingBalanceOf(currentContract);
+            require underlying() != currentContract;
+        }
+        preserved _burn(address account, uint256 amount) with (env e5){
+            require balanceOf(account) >= amount;
+            requireInvariant totalSupplyIsSumOfBalances;
+        }
+        preserved depositFor(address account, uint256 amount) with (env e3){
+            require totalSupply() + amount <= underlyingBalanceOf(currentContract);
+            require underlyingBalanceOf(currentContract) + amount < max_uint256;
+            require underlying() != currentContract;
+        }
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+//                                                       Rules                                                       //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// Check that values are updated correctly by `depositFor()`
+rule depositForSpecBasic(env e) {
+    address account;
+    uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 wrapperTotalBefore = totalSupply();
+    uint256 underlyingTotalBefore = underlyingTotalSupply();
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
+
+    depositFor(e, account, amount);
+
+    uint256 wrapperTotalAfter = totalSupply();
+    uint256 underlyingTotalAfter = underlyingTotalSupply();
+    uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract);
+
+    assert wrapperTotalBefore == to_uint256(wrapperTotalAfter - amount), "wrapper total wrong update";
+    assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated";
+    assert underlyingThisBalanceBefore == to_uint256(underlyingThisBalanceAfter - amount), "underlying this balance wrong update";
+}
+
+// Check that values are updated correctly by `depositFor()`
+rule depositForSpecWrapper(env e) {
+    address account;
+    uint256 amount;
+
+    require underlying() != currentContract;
+
+    uint256 wrapperUserBalanceBefore = balanceOf(account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e.msg.sender);
+
+    depositFor(e, account, amount);
+
+    uint256 wrapperUserBalanceAfter = balanceOf(account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e.msg.sender);
+
+    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+        && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+        && wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - amount)
+        , "wrapper balances wrong update";
+
+    assert account != e.msg.sender => wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - amount)
+        && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter
+        , "wrapper balances wrong update";
+}
+
+// Check that values are updated correctly by `depositFor()`
+rule depositForSpecUnderlying(env e) {
+    address account;
+    uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account);
+
+    depositFor(e, account, amount);
+
+    uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account);
+
+    assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore
+        && underlyingSenderBalanceAfter == underlyingUserBalanceAfter
+        && underlyingSenderBalanceBefore == to_uint256(underlyingSenderBalanceAfter + amount)
+        , "underlying balances wrong update";
+
+    assert account != e.msg.sender
+        && account == currentContract => underlyingSenderBalanceBefore == to_uint256(underlyingSenderBalanceAfter + amount)
+        && underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter - amount)
+        , "underlying balances wrong update";
+
+    assert account != e.msg.sender
+        && account != currentContract => underlyingSenderBalanceBefore == to_uint256(underlyingSenderBalanceAfter + amount)
+        && underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter)
+        , "underlying balances wrong update";
+}
+
+// Check that values are updated correctly by `withdrawTo()`
+rule withdrawToSpecBasic(env e) {
+    address account;
+    uint256 amount;
+
+    require underlying() != currentContract;
+
+    uint256 wrapperTotalBefore = totalSupply();
+    uint256 underlyingTotalBefore = underlyingTotalSupply();
+
+    withdrawTo(e, account, amount);
+
+    uint256 wrapperTotalAfter = totalSupply();
+    uint256 underlyingTotalAfter = underlyingTotalSupply();
+
+    assert wrapperTotalBefore == to_uint256(wrapperTotalAfter + amount), "wrapper total wrong update";
+    assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated";
+}
+
+// Check that values are updated correctly by `withdrawTo()`
+rule withdrawToSpecWrapper(env e) {
+    address account; uint256 amount;
+
+    require underlying() != currentContract;
+
+    uint256 wrapperUserBalanceBefore = balanceOf(account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e.msg.sender);
+
+    withdrawTo(e, account, amount);
+
+    uint256 wrapperUserBalanceAfter = balanceOf(account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e.msg.sender);
+
+    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+        && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+        && wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter + amount)
+        , "wrapper user balance wrong update";
+
+    assert account != e.msg.sender => wrapperSenderBalanceBefore == to_uint256(wrapperSenderBalanceAfter + amount)
+        && wrapperUserBalanceBefore == wrapperUserBalanceAfter
+        , "wrapper user balance wrong update";
+}
+
+
+// STATUS - verified
+// Check that values are updated correctly by `withdrawTo()`
+rule withdrawToSpecUnderlying(env e) {
+    address account; uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account);
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
+
+    withdrawTo(e, account, amount);
+
+    uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account);
+    uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract);
+
+    assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore
+        && underlyingSenderBalanceAfter == underlyingUserBalanceAfter
+        && underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter - amount)
+        , "underlying balances wrong update (acc == sender)";
+
+    assert account != e.msg.sender && account == currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter
+        && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter
+        , "underlying balances wrong update (acc == contract)";
+
+    assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter - amount)
+        && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter
+        && underlyingThisBalanceBefore == to_uint256(underlyingThisBalanceAfter + amount)
+        , "underlying balances wrong update (acc != contract)";
+}
+
+// Check that values are updated correctly by `_recover()`
+rule recoverSpec(env e) {
+    address account;
+    uint256 amount;
+
+    uint256 wrapperTotalBefore = totalSupply();
+    uint256 wrapperUserBalanceBefore = balanceOf(account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e.msg.sender);
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
+
+    mathint value = underlyingThisBalanceBefore - wrapperTotalBefore;
+
+    _recover(e, account);
+
+    uint256 wrapperTotalAfter = totalSupply();
+    uint256 wrapperUserBalanceAfter = balanceOf(account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e.msg.sender);
+
+    assert wrapperTotalBefore == to_uint256(wrapperTotalAfter - value), "wrapper total wrong update";
+
+    assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+        && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+        && wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - value)
+        , "wrapper balances wrong update";
+
+    assert e.msg.sender != account => wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - value)
+        && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter
+        , "wrapper balances wrong update";
+}

certora/specs/ERC721Votes.spec

@@ -0,0 +1,271 @@
+using Checkpoints as Checkpoints
+
+methods {
+    // functions
+    checkpoints(address, uint32) envfree
+    numCheckpoints(address) returns (uint32) envfree
+    getVotes(address) returns (uint256) envfree
+    getPastVotes(address, uint256) returns (uint256)
+    getPastTotalSupply(uint256) returns (uint256)
+    delegates(address) returns (address) envfree
+    delegate(address)
+    _delegate(address, address)
+    delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32)
+    nonces(address) returns (uint256)
+    totalSupply() returns (uint256) envfree
+    _maxSupply() returns (uint224) envfree
+
+    // harnesss functions
+    ckptFromBlock(address, uint32) returns (uint32) envfree
+    ckptVotes(address, uint32) returns (uint224) envfree
+    mint(address, uint256)
+    burn(uint256)
+    unsafeNumCheckpoints(address) returns (uint256) envfree
+
+    // solidity generated getters
+    _delegation(address) returns (address) envfree
+
+    // external functions
+
+
+}
+
+// gets the most recent votes for a user
+ghost userVotes(address) returns uint224{
+        init_state axiom forall address a. userVotes(a) == 0;
+}
+
+// sums the total votes for all users
+ghost totalVotes() returns mathint {
+    init_state axiom totalVotes() == 0;
+    axiom totalVotes() >= 0;
+}
+
+hook Sstore _checkpoints[KEY address account].votes uint224 newVotes (uint224 oldVotes) STORAGE {
+    havoc userVotes assuming
+        userVotes@new(account) == newVotes;
+
+    havoc totalVotes assuming
+        totalVotes@new() == totalVotes@old() + to_mathint(newVotes) - to_mathint(userVotes(account));
+}
+
+
+ghost lastFromBlock(address) returns uint32;
+
+ghost doubleFromBlock(address) returns bool {
+    init_state axiom forall address a. doubleFromBlock(a) == false;
+}
+
+
+
+
+hook Sstore _checkpoints[KEY address account].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE {
+    havoc lastFromBlock assuming
+        lastFromBlock@new(account) == newBlock;
+
+    havoc doubleFromBlock assuming
+        doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
+}
+
+// for some checkpoint, the fromBlock is less than the current block number
+// passes but fails rule sanity from hash on delegate by sig
+invariant timestamp_constrains_fromBlock(address account, uint32 index, env e)
+    ckptFromBlock(account, index) < e.block.number
+    filtered { f -> !f.isView }
+{
+    preserved {
+        require index < numCheckpoints(account);
+    }
+}
+
+// numCheckpoints are less than maxInt
+// passes because numCheckpoints does a safeCast
+// invariant maxInt_constrains_numBlocks(address account)
+//     numCheckpoints(account) < 4294967295 // 2^32
+
+// can't have more checkpoints for a given account than the last from block
+// passes
+invariant fromBlock_constrains_numBlocks(address account)
+    numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1)
+    filtered { f -> !f.isView }
+{ preserved with(env e) {
+    require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
+}}
+
+// for any given checkpoint, the fromBlock must be greater than the checkpoint
+// this proves the above invariant in combination with the below invariant
+// if checkpoint has a greater fromBlock than the last, and the FromBlock is always greater than the pos.
+// Then the number of positions must be less than the currentFromBlock
+// ^note that the tool is assuming it's possible for the starting fromBlock to be 0 or anything, and does not know the current starting block
+// passes + rule sanity
+invariant fromBlock_greaterThanEq_pos(address account, uint32 pos)
+    ckptFromBlock(account, pos) >= pos
+    filtered { f -> !f.isView }
+
+// a larger index must have a larger fromBlock
+// passes + rule sanity
+invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2)
+    pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2)
+    filtered { f -> !f.isView }
+
+
+// converted from an invariant to a rule to slightly change the logic
+// if the fromBlock is the same as before, then the number of checkpoints stays the same
+// however if the fromBlock is new than the number of checkpoints increases
+// passes, fails rule sanity because tautology check seems to be bugged
+rule unique_checkpoints_rule(method f) {
+    env e; calldataarg args;
+    address account;
+    uint32 num_ckpts_ = numCheckpoints(account);
+    uint32 fromBlock_ = num_ckpts_ == 0 ? 0 : ckptFromBlock(account, num_ckpts_ - 1);
+
+    f(e, args);
+
+    uint32 _num_ckpts = numCheckpoints(account);
+    uint32 _fromBlock = _num_ckpts == 0 ? 0 : ckptFromBlock(account, _num_ckpts - 1);
+
+
+    assert fromBlock_ == _fromBlock => num_ckpts_ == _num_ckpts || _num_ckpts == 1, "same fromBlock, new checkpoint";
+    // this assert fails consistently
+    // assert !doubleFromBlock(account) => ckpts_ != _ckpts, "new fromBlock but total checkpoints not being increased";
+}
+
+// assumes neither account has delegated
+// currently fails due to this scenario. A has maxint number of checkpoints
+// an additional checkpoint is added which overflows and sets A's votes to 0
+// passes + rule sanity (- a bad tautology check)
+rule transfer_safe() {
+    env e;
+    uint256 ID;
+    address a; address b;
+
+    require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same
+    require numCheckpoints(delegates(a)) < 1000000;
+    require numCheckpoints(delegates(b)) < 1000000;
+
+    uint256 votesA_pre = getVotes(delegates(a));
+    uint256 votesB_pre = getVotes(delegates(b));
+
+    mathint totalVotes_pre = totalVotes();
+
+    transferFrom(e, a, b, ID);
+
+    mathint totalVotes_post = totalVotes();
+    uint256 votesA_post = getVotes(delegates(a));
+    uint256 votesB_post = getVotes(delegates(b));
+
+    // if an account that has not delegated transfers balance to an account that has, it will increase the total supply of votes
+    assert totalVotes_pre == totalVotes_post, "transfer changed total supply";
+    assert delegates(a) != 0 => votesA_pre - 1 == votesA_post, "A lost the wrong amount of votes";
+    assert delegates(b) != 0 => votesB_pre + 1 == votesB_post, "B gained the wrong amount of votes";
+}
+
+// for any given function f, if the delegate is changed the function must be delegate or delegateBySig
+// passes
+rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).selector &&
+                                                f.selector != _delegate(address, address).selector &&
+                                                f.selector != delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32).selector) }
+{
+    env e; calldataarg args;
+    address account;
+    address pre = delegates(account);
+
+    f(e, args);
+
+    address post = delegates(account);
+
+    assert pre == post, "invalid delegate change";
+}
+
+// delegates increases the delegatee's votes by the proper amount
+// passes + rule sanity
+rule delegatee_receives_votes() {
+    env e;
+    address delegator; address delegatee;
+
+    require numCheckpoints(delegatee) < 1000000;
+    require delegates(delegator) != delegatee;
+    require delegatee != 0x0;
+
+
+    uint256 delegator_bal = balanceOf(e, delegator);
+    uint256 votes_= getVotes(delegatee);
+
+    _delegate(e, delegator, delegatee);
+
+    uint256 _votes = getVotes(delegatee);
+    assert _votes == votes_ + delegator_bal, "delegatee did not receive votes";
+}
+
+// passes + rule sanity
+rule previous_delegatee_votes_removed() {
+    env e;
+    address delegator; address delegatee; address third;
+
+    require third != delegatee;
+    require delegates(delegator) == third;
+    require numCheckpoints(third) < 1000000;
+
+    uint256 delegator_bal = balanceOf(e, delegator);
+    uint256 votes_ = getVotes(third);
+
+    _delegate(e, delegator, delegatee);
+
+    uint256 _votes = getVotes(third);
+
+    assert third != 0x0 => _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee";
+}
+
+// passes with rule sanity
+rule delegate_contained() {
+    env e;
+    address delegator; address delegatee; address other;
+
+    require other != delegatee;
+    require other != delegates(delegator);
+
+    uint256 votes_ = getVotes(other);
+
+    _delegate(e, delegator, delegatee);
+
+    uint256 _votes = getVotes(other);
+
+    assert votes_ == _votes, "votes not contained";
+}
+
+rule delegate_no_frontrunning(method f) {
+    env e; calldataarg args;
+    address delegator; address delegatee; address third; address other;
+
+
+
+    require numCheckpoints(delegatee) < 1000000;
+    require numCheckpoints(third) < 1000000;
+
+
+    f(e, args);
+
+    uint256 delegator_bal = balanceOf(e, delegator);
+    uint256 delegatee_votes_ = getVotes(delegatee);
+    uint256 third_votes_ = getVotes(third);
+    uint256 other_votes_ = getVotes(other);
+    require delegates(delegator) == third;
+    require third != delegatee;
+    require other != third;
+    require other != delegatee;
+    require delegatee != 0x0;
+
+    _delegate(e, delegator, delegatee);
+
+    uint256 _delegatee_votes = getVotes(delegatee);
+    uint256 _third_votes = getVotes(third);
+    uint256 _other_votes = getVotes(other);
+
+
+    // previous delegatee loses all of their votes
+    // delegatee gains that many votes
+    // third loses any votes delegated to them
+    assert _delegatee_votes == delegatee_votes_ + delegator_bal, "delegatee did not receive votes";
+    assert third != 0 => _third_votes == third_votes_ - delegator_bal, "votes not removed from third";
+    assert other_votes_ == _other_votes, "delegate not contained";
+}

certora/specs/GovernorBase.spec

@@ -2,332 +2,348 @@
 ///////////////////// Governor.sol base definitions //////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
-using ERC20VotesHarness as erc20votes
-
 methods {
+    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
+    state(uint256) returns uint8
+    proposalThreshold() returns uint256 envfree
     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
+    proposalProposer(uint256) returns address envfree
+
+    propose(address[], uint256[], bytes[], string) returns uint256
     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
+    cancel(address[], uint256[], bytes[], bytes32) returns uint256
 
     getVotes(address, uint256) returns uint256 => DISPATCHER(true)
+    getVotesWithParams(address, uint256, bytes) returns uint256 => DISPATCHER(true)
+    castVote(uint256, uint8) returns uint256
+    castVoteWithReason(uint256, uint8, string) returns uint256
+    castVoteWithReasonAndParams(uint256, uint8, string, bytes) returns uint256
 
-    getPastTotalSupply(uint256 t) returns uint256      => PER_CALLEE_CONSTANT
-    getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT
+    // GovernorTimelockController
+    queue(address[], uint256[], bytes[], bytes32) returns uint256
 
-    //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
-    //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
+    // GovernorCountingSimple
+    hasVoted(uint256, address) returns bool envfree
+    updateQuorumNumerator(uint256)
+
+    // harness functions
+    getAgainstVotes(uint256) returns uint256 envfree
+    getAbstainVotes(uint256) returns uint256 envfree
+    getForVotes(uint256) returns uint256 envfree
+    getExecutor(uint256) returns bool envfree
+    isExecuted(uint256) returns bool envfree
+    isCanceled(uint256) returns bool envfree
+
+    // full harness functions
+    getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true)
+    /// getPastVotes(address, uint256) returns uint256 => DISPATCHER(true)
+
+    // internal functions made public in harness:
+    quorumReached(uint256) returns bool
+    voteSucceeded(uint256) returns bool envfree
 }
 
-//////////////////////////////////////////////////////////////////////////////
-//////////////////////////////// Definitions /////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
 
+definition proposalCreated(uint256 pId) returns bool =
+    proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0;
 
-// proposal was created - relation proved in noStartBeforeCreation
-definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////// Helper Functions ///////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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) {
+    uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params;
+
+    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 == queue(address[], uint256[], bytes[], bytes32).selector)
+    {
+        uint256 result = queue@withrevert(e, targets, values, calldatas, descriptionHash);
+        require result == proposalId;
+    }
+    else if (f.selector == cancel(address[], uint256[], bytes[], bytes32).selector)
+    {
+        uint256 result = cancel@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 {
+    }
+    else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector)
+    {
+        castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params);
+    }
+    else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector)
+    {
+        castVoteBySig@withrevert(e, proposalId, support, v, r, s);
+    }
+    else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector)
+    {
+        castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s);
+    }
+    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             //
- //                                                                                                                          //
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Votes start and end are either initialized (non zero) or uninitialized (zero) simultaneously             │
+│                                                                                                                     │
+│ This invariant assumes that the block number cannot be 0 at any stage of the contract cycle                         │
+│ This is very safe assumption as usually the 0 block is genesis block which is uploaded with data                    │
+│ by the developers and will not be valid to raise proposals (at the current way that block chain is functioning)     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-
-
-///////////////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// 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);
+invariant proposalStateConsistency(uint256 pId)
+    (proposalProposer(pId) != 0 <=> proposalSnapshot(pId) != 0) && (proposalProposer(pId) != 0 <=> proposalDeadline(pId) != 0)
+    {
+        preserved with (env e) {
             require e.block.number > 0;
-        }}
-
+        }
+    }
 
 /*
- * A proposal starting block number must be less or equal than the proposal end date
- */
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: cancel => created                                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant canceledImplyCreated(uint pId)
+    isCanceled(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            requireInvariant proposalStateConsistency(pId);
+            require e.block.number > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: executed => created                                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant executedImplyCreated(uint pId)
+    isExecuted(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            requireInvariant proposalStateConsistency(pId);
+            require e.block.number > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Votes start before it ends                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
 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);
-        }}
-
+    proposalSnapshot(pId) <= proposalDeadline(pId)
+    {
+        preserved {
+            requireInvariant proposalStateConsistency(pId);
+        }
+    }
 
 /*
- * A proposal cannot be both executed and canceled simultaneously.
- */
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A proposal cannot be both executed and canceled simultaneously                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
 invariant noBothExecutedAndCanceled(uint256 pId)
-        !isExecuted(pId) || !isCanceled(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);
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: No double proposition                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDoublePropose(uint256 pId, env e) {
+    require proposalCreated(pId);
 
-    calldataarg args;
-    f(e, args);
+    address[] targets; uint256[] values; bytes[] calldatas; string reason;
+    uint256 result = propose(e, targets, values, calldatas, reason);
 
-    bool isExecutedAfter = isExecuted(pId);
-    assert (!isExecutedBefore && isExecutedAfter) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed";
+    assert result != pId, "double proposal";
 }
 
-///////////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////// In-State Rules /////////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg) {
+    require proposalCreated(pId);
 
-//==========================================
-//------------- Voting Period --------------
-//==========================================
+    uint256 voteStart = proposalSnapshot(pId);
+    uint256 voteEnd = proposalDeadline(pId);
+    address proposer = proposalProposer(pId);
+
+    f(e, arg);
+
+    assert voteStart == proposalSnapshot(pId), "Start date was changed";
+    assert voteEnd == proposalDeadline(pId), "End date was changed";
+    assert proposer == proposalProposer(pId), "Proposer was changed";
+}
 
 /*
- * 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);
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A user cannot vote twice                                                                                      │
+│                                                                                                                     │
+│ Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is      │
+│ counted on the fact that the 3 functions themselves makes no changes, but rather call an internal function to       │
+│ execute. That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it   │
+│ is quite trivial to understand why this is ok. For castVoteBySig we basically assume that the signature referendum  │
+│ is correct without checking it. We could check each function separately and pass the rule, but that would have      │
+│ uglyfied the code with no concrete benefit, as it is evident that nothing is happening in the first 2 functions     │
+│ (calling a view function), and we do not desire to check the signature verification.                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDoubleVoting(uint256 pId, env e, uint8 sup) {
+    bool votedCheck = hasVoted(pId, e.msg.sender);
 
     castVote@withrevert(e, pId, sup);
 
     assert votedCheck => lastReverted, "double voting occurred";
 }
 
-
-///////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////// 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);
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A proposal could be executed only if quorum was reached and vote succeeded                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, calldataarg args) {
+    require !isExecuted(pId);
 
-    require proposalCreated(pId); // startDate > 0
+    bool quorumReachedBefore = quorumReached(e, pId);
+    bool voteSucceededBefore = voteSucceeded(pId);
 
-    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");
+    assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed";
 }
 
 /*
- * All proposal specific (non-view) functions should revert if proposal is canceled
- */
-rule allFunctionsRevertIfCanceled(method f) filtered {
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Voting cannot start at a block number prior to proposal’s creation block number                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noStartBeforeCreation(uint256 pId, env e, method f, calldataarg args){
+    require !proposalCreated(pId);
+    f(e, args);
+    assert proposalCreated(pId) => proposalSnapshot(pId) >= e.block.number, "starts before proposal";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A proposal cannot be executed before it ends                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) {
+    require !isExecuted(pId);
+    f(e, args);
+    assert isExecuted(pId) => proposalDeadline(pId) <= e.block.number, "executed before deadline";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: All proposal specific (non-view) functions should revert if proposal is executed                              │
+│                                                                                                                     │
+│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, non of the       │
+│ proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc we connected the executed       │
+│ attribute to the execute() function, showing that only execute() can change it, and that it will always change it.  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args) filtered {
     f -> !f.isView && !f.isFallback
       && f.selector != updateTimelock(address).selector
       && f.selector != updateQuorumNumerator(uint256).selector
-      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
       && f.selector != relay(address,uint256,bytes).selector
       && f.selector != 0xb9a61961 // __acceptAdmin()
+      && f.selector != onERC721Received(address,address,uint256,bytes).selector
+      && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector
+      && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector
 } {
-    env e; calldataarg args;
-    uint256 pId;
-    require(isCanceled(pId));
+    require isExecuted(pId);
     requireInvariant noBothExecutedAndCanceled(pId);
-    requireInvariant canceledImplyStartAndEndDateNonZero(pId);
+    requireInvariant executedImplyCreated(pId);
 
     helperFunctionsWithRevert(pId, f, e);
 
-    assert(lastReverted, "Function was not reverted");
+    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);
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: All proposal specific (non-view) functions should revert if proposal is canceled                              │
+│                                                                                                                     │
+│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, non of the       │
+│ proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc we connected the executed       │
+│ attribute to the execute() function, showing that only execute() can change it, and that it will always change it.  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args) filtered {
+    f -> !f.isView && !f.isFallback
+      && f.selector != updateTimelock(address).selector
+      && f.selector != updateQuorumNumerator(uint256).selector
+      && f.selector != relay(address,uint256,bytes).selector
+      && f.selector != 0xb9a61961 // __acceptAdmin()
+      && f.selector != onERC721Received(address,address,uint256,bytes).selector
+      && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector
+      && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector
+} {
+    require isCanceled(pId);
+    requireInvariant noBothExecutedAndCanceled(pId);
+    requireInvariant canceledImplyCreated(pId);
 
     helperFunctionsWithRevert(pId, f, e);
 
-    bool executedAfter = isExecuted(pId);
-    assert(executedAfter != executedBefore => f.selector == execute(address[], uint256[], bytes[], bytes32).selector, "isExecuted only changes in the execute method");
+    assert lastReverted, "Function was not reverted";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Proposal can be switched state only by specific functions                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateOnlyAfterFunc(uint256 pId, env e, method f) {
+    bool createdBefore = proposalCreated(pId);
+    bool executedBefore = isExecuted(pId);
+    bool canceledBefore = isCanceled(pId);
+
+    helperFunctionsWithRevert(pId, f, e);
+
+    assert (proposalCreated(pId) != createdBefore)
+        => (createdBefore == false && f.selector == propose(address[], uint256[], bytes[], string).selector),
+        "proposalCreated only changes in the propose method";
+
+    assert (isExecuted(pId) != executedBefore)
+        => (executedBefore == false && f.selector == execute(address[], uint256[], bytes[], bytes32).selector),
+        "isExecuted only changes in the execute method";
+
+    assert (isCanceled(pId) != canceledBefore)
+        => (canceledBefore == false && f.selector == cancel(address[], uint256[], bytes[], bytes32).selector),
+        "isCanceled only changes in the cancel method";
 }

certora/specs/GovernorCountingSimple.spec

@@ -1,7 +1,5 @@
 import "GovernorBase.spec"
 
-using ERC20VotesHarness as erc20votes
-
 methods {
     ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
 
@@ -9,9 +7,6 @@ methods {
     proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
 
     quorumNumerator() returns uint256
-    _executor() returns address
-
-    erc20votes._getPastVotes(address, uint256) returns uint256
 
     getExecutor() returns address
 
@@ -102,21 +97,21 @@ hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256
 /*
  * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal
  */
-invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId) 
+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() 
+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) 
+invariant OneIsNotMoreThanAll(uint256 pId)
 	sum_all_votes_power() >= tracked_weight(pId)
 
 
@@ -132,7 +127,7 @@ invariant OneIsNotMoreThanAll(uint256 pId)
  // 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 
+ // 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;
@@ -140,24 +135,24 @@ rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) {
     address voter = e.msg.sender;
     address user;
 
-    bool hasVotedBefore_User = hasVoted(e, pId, user);
+    bool hasVotedBefore_User = hasVoted(pId, user);
 
     castVote@withrevert(e, pId, sup);
     require(!lastReverted);
 
-    bool hasVotedAfter_User = hasVoted(e, pId, user);
+    bool hasVotedAfter_User = hasVoted(pId, user);
 
     assert user != voter => hasVotedBefore_User == hasVotedAfter_User;
 }
 
 
 /*
-* Total voting tally is monotonically non-decreasing in every operation 
+* Total voting tally is monotonically non-decreasing in every operation
 */
 rule votingWeightMonotonicity(method f){
     uint256 votingWeightBefore = sum_tracked_weight();
 
-    env e; 
+    env e;
     calldataarg args;
     f(e, args);
 
@@ -172,12 +167,12 @@ rule votingWeightMonotonicity(method f){
 */
 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);
+    bool hasVotedBefore = hasVoted(pId, acc);
 
     helperFunctionsWithRevert(pId, f, e);
     require(!lastReverted);
@@ -185,10 +180,11 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
     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";
+    bool hasVotedAfter = hasVoted(pId, acc);
+
+    // want all vote categories to not decrease and at least one category to increase
+    assert (!hasVotedBefore && hasVotedAfter) => (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), "no correlation: some category decreased";
 }
 
 

certora/specs/GovernorPreventLateQuorum.spec

@@ -0,0 +1,308 @@
+import "GovernorBase.spec"
+import "GovernorCountingSimple.spec"
+
+using ERC20VotesHarness as token
+
+methods {
+    // envfree
+    quorumNumerator(uint256) returns uint256
+    quorumDenominator() returns uint256 envfree
+
+    // harness
+    getDeprecatedQuorumNumerator() returns uint256 envfree
+    getQuorumNumeratorLength() returns uint256 envfree
+    getQuorumNumeratorLatest() returns uint256 envfree
+    getExtendedDeadline(uint256) returns uint64 envfree
+    getPastTotalSupply(uint256) returns (uint256) envfree
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+////////////////////////////////////////////////////////////////////////////////
+// Helper Functions                                                           //
+////////////////////////////////////////////////////////////////////////////////
+
+
+
+function sanity() {
+    require getQuorumNumeratorLength() + 1 < max_uint;
+}
+
+
+
+
+
+definition deadlineExtendable(env e, uint256 pId) returns bool = getExtendedDeadline(pId) == 0;
+definition deadlineExtended(env e, uint256 pId) returns bool = getExtendedDeadline(pId) > 0;
+
+
+
+
+
+invariant deadlineConsistency(env e, uint256 pId)
+    (!quorumReached(e, pId) => deadlineExtendable(pId))
+    &&
+    (deadlineExtended(pId) => quorumReached(e, pId))
+
+
+invariant proposalStateConsistencyExtended(uint256 pId)
+    !proposalCreated(pId) => (getAgainstVotes(pId) == 0  && getAbstainVotes(pId) == 0  && getForVotes(pId) == 0)
+    && (proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0)
+    && (proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0)
+    {
+        preserved with (env e) {
+            require e.block.number > 0;
+        }
+    }
+
+
+
+
+
+
+
+
+/**
+ * If a proposal has reached quorum then the proposal snapshot (start `block.number`) must be non-zero
+ */
+invariant quorumReachedEffect(env e, uint256 pId)
+    (quorumReached(e, pId) && getPastTotalSupply(proposalSnapshot(pId)) > 0) => proposalCreated(pId)
+
+/**
+ * The quorum numerator is always less than or equal to the quorum denominator.
+ */
+invariant quorumRatioLessThanOne(env e, uint256 blockNumber)
+    quorumNumerator(e, blockNumber) <= quorumDenominator()
+
+
+/**
+ * If a proposal's deadline has been extended, then the proposal must have been created and reached quorum.
+ */
+invariant cantExtendWhenQuorumUnreached(env e, uint256 pId)
+    getExtendedDeadline(pId) > 0 => (quorumReached(e, pId) && proposalCreated(pId))
+    //{
+    //    preserved with (env e1) {
+    //        require e1.block.number > proposalSnapshot(pId);
+    //        setup(e1, e);
+    //    }
+    //}
+
+
+
+
+
+
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: `updateQuorumNumerator` can only change quorum requirements for future proposals.                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule quorumReachedCantChange(uint256 pId, env e, method f) filtered { f ->
+    !f.isFallback
+    && !f.isView
+    && f.selector != relay(address,uint256,bytes).selector
+    && !castVoteSubset(f)
+} {
+    sanity(); // not overflowing checkpoint struct
+    require proposalSnapshot(pId) < e.block.number; // vote has started
+
+    bool quorumReachedBefore = quorumReached(e, pId);
+
+    uint256 newQuorumNumerator;
+    updateQuorumNumerator(e, newQuorumNumerator);
+
+    assert quorumReachedBefore == quorumReached(e, pId);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Casting a vote must not decrease any category's total number of votes and increase at least one category's    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule hasVotedCorrelationNonzero(uint256 pId, env e, method f, calldataarg args) filtered { f ->
+    !f.isFallback
+    && !f.isView
+    && f.selector != relay(address,uint256,bytes).selector
+    && !castVoteSubset(f)
+} {
+    require getVotes(e, e.msg.sender, proposalSnapshot(pId)) > 0; // assuming voter has non-zero voting power
+
+    uint256 againstBefore = votesAgainst();
+    uint256 forBefore = votesFor();
+    uint256 abstainBefore = votesAbstain();
+
+    bool hasVotedBefore = hasVoted(pId, e.msg.sender);
+
+    f(e, args);
+
+    uint256 againstAfter = votesAgainst();
+    uint256 forAfter = votesFor();
+    uint256 abstainAfter = votesAbstain();
+
+    bool hasVotedAfter = hasVoted(pId, e.msg.sender);
+
+    // want all vote categories to not decrease and at least one category to increase
+    assert
+        (!hasVotedBefore && hasVotedAfter) =>
+        (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter),
+        "after a vote is cast, the number of votes for each category must not decrease";
+    assert
+        (!hasVotedBefore && hasVotedAfter) =>
+        (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter),
+        "after a vote is cast, the number of votes of at least one category must increase";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Voting against a proposal does not count towards quorum.                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule againstVotesDontCount(uint256 pId, env e, method f, calldataarg args) filtered { f ->
+    !f.isFallback
+    && !f.isView
+    && f.selector != relay(address,uint256,bytes).selector
+    && !castVoteSubset(f)
+} {
+    bool quorumBefore = quorumReached(e, pId);
+    uint256 againstBefore = votesAgainst();
+
+    f(e, args);
+
+    bool quorumAfter = quorumReached(e, pId);
+    uint256 againstAfter = votesAgainst();
+
+    assert againstBefore < againstAfter => quorumBefore == quorumAfter, "quorum must not be reached with an against vote";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule:                                                                                                               │
+│  * Deadline can never be reduced                                                                                    │
+│  * If deadline increases then we are in `deadlineExtended` state and `castVote` was called.                         │
+│  * A proposal's deadline can't change in `deadlineExtended` state.                                                  │
+│  * A proposal's deadline can't be unextended.                                                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule deadlineChangeEffects(uint256 pId, env e, method f, calldataarg args) filtered { f ->
+    !f.isFallback
+    && !f.isView
+    && f.selector != relay(address,uint256,bytes).selector
+    && !castVoteSubset(f)
+} {
+    requireInvariant proposalStateConsistencyExtended(pId);
+
+    uint256 deadlineBefore = proposalDeadline(pId);
+    bool deadlineExtendedBefore = deadlineExtended(e, pId);
+
+    f(e, args);
+
+    uint256 deadlineAfter = proposalDeadline(pId);
+    bool deadlineExtendedAfter = deadlineExtended(e, pId);
+
+    // deadline can never be reduced
+    assert deadlineBefore <= proposalDeadline(pId);
+
+    // deadline can only be extended in proposal or on cast vote
+    assert (
+        deadlineAfter > deadlineBefore
+    ) => (
+        (!deadlineExtendedBefore && !deadlineExtendedAfter && f.selector == propose(address[], uint256[], bytes[], string).selector)
+        ||
+        (!deadlineExtendedBefore && deadlineExtendedAfter && f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector)
+    );
+
+    // a deadline can only be extended once
+    assert deadlineExtendedBefore => deadlineBefore == deadlineAfter;
+
+    // a deadline cannot be un-extended
+    assert deadlineExtendedBefore => deadlineExtendedAfter;
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+function setup(env e1, env e2) {
+    require getQuorumNumeratorLength() + 1 < max_uint;
+    require e2.block.number >= e1.block.number;
+}
+
+/// The proposal with proposal id `pId` has not been created.
+definition proposalNotCreated(env e, uint256 pId) returns bool =
+    proposalSnapshot(pId) == 0
+    && proposalDeadline(pId) == 0
+    && getAgainstVotes(pId) == 0
+    && getAbstainVotes(pId) == 0
+    && getForVotes(pId) == 0;
+
+/// Method f is a version of `castVote` whose state changing effects are covered by `castVoteBySig`.
+/// @dev castVoteBySig allows anyone to cast a vote for anyone else if they can supply the signature. Specifically,
+/// it covers the case where the msg.sender supplies a signature for themselves which is normally done using the normal
+/// `castVote`.
+definition castVoteSubset(method f) returns bool =
+    f.selector == castVote(uint256, uint8).selector ||
+    f.selector == castVoteWithReason(uint256, uint8, string).selector ||
+    f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector ||
+    f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector;
+
+/**
+ * A created proposal must be in state `deadlineExtendable` or `deadlineExtended`.
+ * @dev We assume the total supply of the voting token is non-zero
+ */
+invariant proposalInOneState(env e1, uint256 pId)
+    getPastTotalSupply(0) > 0 => (proposalNotCreated(e1, pId) || deadlineExtendable(e1, pId) || deadlineExtended(e1, pId))
+    filtered { f -> !f.isFallback && !f.isView && !castVoteSubset(f) && f.selector != relay(address,uint256,bytes).selector }
+    {
+        preserved with (env e2) {
+            setup(e1, e2);
+        }
+    }

certora/specs/Initializable.spec

@@ -0,0 +1,215 @@
+//// ## Verification of `Initializable`
+//// 
+//// `Initializable` is a contract used to make constructors for upgradable
+//// contracts. This is accomplished by applying the `initializer` modifier to any
+//// function that serves as a constructor, which makes this function only
+//// callable once. The secondary modifier `reinitializer` allows for upgrades
+//// that should run at most once after the contract is upgraded.
+////     
+//// 
+//// ### Assumptions and Simplifications
+//// We assume `initializer()` and `reinitializer(1)` are equivalent if they
+//// both guarantee `_initialized` to be set to 1 after a successful call. This
+//// allows us to use `reinitializer(n)` as a general version that also handles
+//// the regular `initialzer` case.
+////     
+//// #### Harnessing
+//// Two harness versions were implemented, a simple flat contract, and a
+//// Multi-inheriting contract. The two versions together help us ensure there are
+//// No unexpected results because of different implementations. `Initializable` can
+//// Be used in many different ways but we believe these 2 cases provide good
+//// Coverage for all cases. In both harnesses we use getter functions for
+//// `_initialized` and `_initializing` and implement  `initializer` and
+//// `reinitializer` functions that use their respective modifiers. We also
+//// Implement some versioned functions that are only callable in specific
+//// Versions of the contract to mimic upgrading contracts.
+////     
+//// #### Munging
+//// Variables `_initialized` and `_initializing` were changed to have internal
+//// visibility to be harnessable.
+    
+methods {
+    initialize(uint256, uint256, uint256) envfree
+    reinitialize(uint256, uint256, uint256, uint8) envfree
+    initialized() returns uint8 envfree
+    initializing() returns bool envfree
+    thisIsContract() returns bool envfree
+
+    returnsV1() returns uint256 envfree
+    returnsVN(uint8) returns uint256 envfree
+    returnsAV1() returns uint256 envfree
+    returnsAVN(uint8) returns uint256 envfree
+    returnsBV1() returns uint256 envfree
+    returnsBVN(uint8) returns uint256 envfree
+    a() returns uint256 envfree
+    b() returns uint256 envfree
+    val() returns uint256 envfree
+}
+
+
+////////////////////////////////////////////////////////////////////////////////
+//// #### Definitions                                                       ////
+////////////////////////////////////////////////////////////////////////////////
+
+//// ***`isUninitialized:`*** A contract's `_initialized` variable is equal to 0.
+definition isUninitialized() returns bool = initialized() == 0;
+
+//// ***`isInitialized:`*** A contract's `_initialized` variable is greater than 0.
+definition isInitialized() returns bool = initialized() > 0;
+
+//// ***`isInitializedOnce:`*** A contract's `_initialized` variable is equal to 1.
+definition isInitializedOnce() returns bool = initialized() == 1;
+
+//// ***`isReinitialized:`*** A contract's `_initialized` variable is greater than 1.    
+definition isReinitialized() returns bool = initialized() > 1;
+
+//// ***`isDisabled:`*** A contract's `_initialized` variable is equal to 255.
+definition isDisabled() returns bool = initialized() == 255;
+
+
+//////////////////////////////////////////////////////////////////////////////
+//// ### Properties                                ///////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+//////////////////////////////////////////////////////////////////////////////
+// Invariants                            /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+/// A contract must only ever be in an initializing state while in the middle
+/// of a transaction execution.
+invariant notInitializing()
+    !initializing()
+
+
+//////////////////////////////////////////////////////////////////////////////
+// Rules                                 /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+/// @title Only initialized once
+/// @notice An initializable contract with a function that inherits the
+///         initializer modifier must be initializable only once
+rule initOnce() {
+    uint256 val; uint256 a; uint256 b;
+
+    require isInitialized();
+    initialize@withrevert(val, a, b);
+    assert lastReverted, "contract must only be initialized once";
+}
+
+/// Successfully calling reinitialize() with a version value of 1 must result
+/// in `_initialized` being set to 1.
+rule reinitializeEffects {
+    uint256 val; uint256 a; uint256 b;
+
+    reinitialize(val, a, b, 1);
+
+    assert isInitializedOnce(), "reinitialize(1) must set _initialized to 1";
+}
+
+/// Successfully calling `initialize()` must result in `_initialized` being set to 1.
+/// @dev We assume `initialize()` and `reinitialize(1)` are equivalent if this rule
+///      and the [above rule][#reinitializeEffects] both pass.
+rule initializeEffects {
+    uint256 val; uint256 a; uint256 b;
+
+    initialize(val, a, b);
+
+    assert isInitializedOnce(), "initialize() must set _initialized to 1";
+}
+
+/// A disabled initializable contract must always stay disabled.
+rule disabledStaysDisabled(method f) {
+    env e; calldataarg args; 
+
+    bool disabledBefore = isDisabled();
+    f(e, args);
+    bool disabledAfter = isDisabled();
+
+    assert disabledBefore => disabledAfter, "a disabled initializer must stay disabled";
+}
+
+/// The variable `_initialized` must not decrease.
+rule increasingInitialized(method f) {
+    env e; calldataarg args;
+
+    uint8 initBefore = initialized();
+    f(e, args);
+    uint8 initAfter = initialized();
+    assert initBefore <= initAfter, "_initialized must only increase";
+}
+
+/// If `reinitialize(...)` was called successfully, then the variable
+/// `_initialized` must increase.
+/// @title Reinitialize increases `init`
+rule reinitializeIncreasesInit {
+    uint256 val; uint8 n; uint256 a; uint256 b;
+
+    uint8 initBefore = initialized();
+    reinitialize(val, a, b, n);
+    uint8 initAfter = initialized();
+
+    assert initAfter > initBefore, "calling reinitialize must increase _initialized";
+}
+
+/// `reinitialize(n)` must be callable if the contract is not in an
+/// `_initializing` state and `n` is greater than `_initialized` and less than
+/// 255
+rule reinitializeLiveness {
+    uint256 val; uint8 n; uint256 a; uint256 b;
+
+    requireInvariant notInitializing();
+    uint8 initVal = initialized();
+    reinitialize@withrevert(val, a, b, n);
+
+    assert n > initVal => !lastReverted, "reinitialize(n) call must succeed if n was greater than _initialized";
+}
+
+/// If `reinitialize(n)` was called successfully then `n` was greater than
+/// `_initialized`.
+rule reinitializeRule {
+    uint256 val; uint8 n; uint256 a; uint256 b;
+
+    uint8 initBefore = initialized();
+    reinitialize(val, a, b, n);
+
+    assert n > initBefore;
+}
+
+/// Functions implemented in the parent contract that require `_initialized` to
+/// be a certain value are only callable when it is that value. 
+/// @title Reinitialize version check parent
+rule reinitVersionCheckParent {
+    uint8 n;
+
+    returnsVN(n);
+    assert initialized() == n, "parent contract's version n functions must only be callable in version n";
+}
+
+/// Functions implemented in the child contract that require `_initialized` to
+/// be a certain value are only callable when it is that value.
+/// @title Reinitialize version check child
+rule reinitVersionCheckChild {
+    uint8 n;
+
+    returnsAVN(n);
+    assert initialized() == n, "child contract's version n functions must only be callable in version n";
+}
+
+/// Functions implemented in the grandchild contract that require `_initialized`
+/// to be a certain value are only callable when it is that value.
+/// @title Reinitialize version check grandchild
+rule reinitVersionCheckGrandchild {
+    uint8 n;
+
+    returnsBVN(n);
+    assert initialized() == n, "gransdchild contract's version n functions must only be callable in version n";
+}
+
+/// Calling parent initializer function must initialize all child contracts.
+rule inheritanceCheck {
+    uint256 val; uint8 n; uint256 a; uint256 b;
+
+    reinitialize(val, a, b, n);
+    assert val() == val && a() == a && b() == b, "all child contract values must be initialized";
+}
+

certora/specs/RulesInProgress.spec

@@ -136,4 +136,40 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
     uint256 ps = proposalSnapshot(pId);
 
     assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
-}
+}
+
+
+
+/////////////////// 2nd iteration with OZ //////////////////////////
+
+function executionsCall(method f, env e, address target, uint256 value, bytes data,
+                                    bytes32 predecessor, bytes32 salt, uint256 delay,
+                                    address[] targets, uint256[] values, bytes[] calldatas) {
+    if  (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) {
+        execute(e, target, value, data, predecessor, salt);
+	} else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
+        executeBatch(e, targets, values, calldatas, predecessor, salt);
+	} else {
+        calldataarg args;
+        f(e, args);
+    }
+}
+
+// STATUS - in progress
+// execute() is the only way to set timestamp to 1
+rule getTimestampOnlyChange(method f, env e){
+    bytes32 id;
+    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay;
+    address[] targets; uint256[] values; bytes[] calldatas;
+
+    require (targets[0] == target && values[0] == value && calldatas[0] == data)
+                || (targets[1] == target && values[1] == value && calldatas[1] == data)
+                || (targets[2] == target && values[2] == value && calldatas[2] == data);
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, calldatas);
+
+    assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector
+                                        || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?";
+}

certora/specs/TimelockController.spec

@@ -0,0 +1,326 @@
+methods {
+    PROPOSER_ROLE() returns(bytes32) envfree
+
+    _DONE_TIMESTAMP() returns(uint256) envfree
+    _minDelay() returns(uint256) envfree
+    _checkRole(bytes32) => DISPATCHER(true)
+
+    isOperation(bytes32) returns(bool) envfree
+    isOperationPending(bytes32) returns(bool) envfree
+    isOperationReady(bytes32) returns(bool)
+    isOperationDone(bytes32) returns(bool) envfree
+    getTimestamp(bytes32) returns(uint256) envfree
+    getMinDelay() returns(uint256) envfree
+
+    hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree
+    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree
+
+    schedule(address, uint256, bytes, bytes32, bytes32, uint256)
+    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256)
+    execute(address, uint256, bytes, bytes32, bytes32)
+    executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
+    cancel(bytes32)
+}
+
+
+////////////////////////////////////////////////////////////////////////////
+//                         Functions                                      //
+////////////////////////////////////////////////////////////////////////////
+
+
+function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){
+    require data.length < 32;
+    require hashOperation(target, value, data, predecessor, salt) == id;
+}
+
+
+////////////////////////////////////////////////////////////////////////////
+//                         Invariants                                     //
+////////////////////////////////////////////////////////////////////////////
+
+
+// STATUS - verified
+// `isOperation()` correctness check
+invariant operationCheck(bytes32 id)
+    getTimestamp(id) > 0 <=> isOperation(id)
+filtered { f -> !f.isView }
+
+// STATUS - verified
+// `isOperationPending()` correctness check
+invariant pendingCheck(bytes32 id)
+    getTimestamp(id) > _DONE_TIMESTAMP() <=> isOperationPending(id)
+filtered { f -> !f.isView }
+
+// STATUS - verified
+// `isOperationReady()` correctness check
+invariant readyCheck(env e, bytes32 id)
+    (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id)
+filtered { f -> !f.isView }
+
+// STATUS - verified
+// `isOperationDone()` correctness check
+invariant doneCheck(bytes32 id)
+    getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id)
+filtered { f -> !f.isView }
+
+
+////////////////////////////////////////////////////////////////////////////
+//                            Rules                                       //
+////////////////////////////////////////////////////////////////////////////
+
+
+/////////////////////////////////////////////////////////////
+// STATE TRANSITIONS
+/////////////////////////////////////////////////////////////
+
+
+// STATUS - verified
+// Possible transitions: form `!isOperation()` to `!isOperation()` or `isOperationPending()` only
+rule unsetPendingTransitionGeneral(method f, env e){
+    bytes32 id;
+
+    require !isOperation(id);
+    require e.block.timestamp > 1;
+
+    calldataarg args;
+    f(e, args);
+
+    assert isOperationPending(id) || !isOperation(id);
+}
+
+
+// STATUS - verified
+// Possible transitions: form `!isOperation()` to `isOperationPending()` via `schedule()` and `scheduleBatch()` only
+rule unsetPendingTransitionMethods(method f, env e){
+    bytes32 id;
+
+    require !isOperation(id);
+
+    calldataarg args;
+    f(e, args);
+
+    assert isOperationPending(id) => (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector
+                                || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector), "Why do we need to follow the schedule?";
+}
+
+
+// STATUS - verified
+// Possible transitions: form `ready()` to `isOperationDone()` via `execute()` and `executeBatch()` only
+rule readyDoneTransition(method f, env e){
+    bytes32 id;
+
+    require isOperationReady(e, id);
+
+    calldataarg args;
+    f(e, args);
+
+    assert isOperationDone(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector
+                                || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not isOperationDone yet!";
+}
+
+
+// STATUS - verified
+// isOperationPending() -> cancelled() via cancel() only
+rule pendingCancelledTransition(method f, env e){
+    bytes32 id;
+
+    require isOperationPending(id);
+
+    calldataarg args;
+    f(e, args);
+
+    assert !isOperation(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?";
+}
+
+
+// STATUS - verified
+// isOperationDone() -> nowhere
+rule doneToNothingTransition(method f, env e){
+    bytes32 id;
+
+    require isOperationDone(id);
+
+    calldataarg args;
+    f(e, args);
+
+    assert isOperationDone(id), "Did you find a way to escape? There is no way! HA-HA-HA";
+}
+
+
+
+/////////////////////////////////////////////////////////////
+// THE REST
+/////////////////////////////////////////////////////////////
+
+
+// STATUS - verified
+// only TimelockController contract can change minDelay
+rule minDelayOnlyChange(method f, env e){
+    uint256 delayBefore = _minDelay();
+
+    calldataarg args;
+    f(e, args);
+
+    uint256 delayAfter = _minDelay();
+
+    assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!";
+}
+
+
+// STATUS - verified
+// scheduled operation timestamp == block.timestamp + delay (kind of unit test)
+rule scheduleCheck(method f, env e){
+    bytes32 id;
+
+    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    schedule(e, target, value, data, predecessor, salt, delay);
+
+    assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls";
+}
+
+
+// STATUS - verified
+// Cannot call `execute()` on a isOperationPending (not ready) operation
+rule cannotCallExecute(method f, env e){
+    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
+    bytes32 id;
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+    require isOperationPending(id) && !isOperationReady(e, id);
+
+    execute@withrevert(e, target, value, data, predecessor, salt);
+
+    assert lastReverted, "you go against execution nature";
+}
+
+
+// STATUS - verified
+// Cannot call `execute()` on a !isOperation operation
+rule executeRevertsFromUnset(method f, env e, env e2){
+    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
+    bytes32 id;
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+    require !isOperation(id);
+
+    execute@withrevert(e, target, value, data, predecessor, salt);
+
+    assert lastReverted, "you go against execution nature";
+}
+
+
+// STATUS - verified
+// Execute reverts => state returns to isOperationPending
+rule executeRevertsEffectCheck(method f, env e){
+    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
+    bytes32 id;
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+    require isOperationPending(id) && !isOperationReady(e, id);
+
+    execute@withrevert(e, target, value, data, predecessor, salt);
+    bool reverted = lastReverted;
+
+    assert lastReverted => isOperationPending(id) && !isOperationReady(e, id), "you go against execution nature";
+}
+
+
+// STATUS - verified
+// Canceled operations cannot be executed → can’t move from canceled to isOperationDone
+rule cancelledNotExecuted(method f, env e){
+    bytes32 id;
+
+    require !isOperation(id);
+    require e.block.timestamp > 1;
+
+    calldataarg args;
+    f(e, args);
+
+    assert !isOperationDone(id), "The ship is not a creature of the air";
+}
+
+
+// STATUS - verified
+// Only proposers can schedule
+rule onlyProposer(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector
+                                                    || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector } {
+    bytes32 id;
+    bytes32 role;
+    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
+
+    _checkRole@withrevert(e, PROPOSER_ROLE());
+
+    bool isCheckRoleReverted = lastReverted;
+
+    calldataarg args;
+    f@withrevert(e, args);
+
+    bool isScheduleReverted = lastReverted;
+
+    assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected";
+}
+
+
+// STATUS - verified
+// if `ready` then has waited minimum period after isOperationPending()
+rule cooldown(method f, env e, env e2){
+    bytes32 id;
+    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
+    uint256 minDelay = getMinDelay();
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    schedule(e, target, value, data, predecessor, salt, delay);
+
+    calldataarg args;
+    f(e, args);
+
+    assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready";
+}
+
+
+// STATUS - verified
+// `schedule()` should change only one id's timestamp
+rule scheduleChange(env e){
+    bytes32 id;  bytes32 otherId;
+    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
+
+    uint256 otherIdTimestampBefore = getTimestamp(otherId);
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    schedule(e, target, value, data, predecessor, salt, delay);
+
+    assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
+}
+
+
+// STATUS - verified
+// `execute()` should change only one id's timestamp
+rule executeChange(env e){
+    bytes32 id;  bytes32 otherId;
+    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt;
+    uint256 otherIdTimestampBefore = getTimestamp(otherId);
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    execute(e, target, value, data, predecessor, salt);
+
+    assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
+}
+
+
+// STATUS - verified
+// `cancel()` should change only one id's timestamp
+rule cancelChange(env e){
+    bytes32 id;  bytes32 otherId;
+
+    uint256 otherIdTimestampBefore = getTimestamp(otherId);
+
+    cancel(e, id);
+
+    assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
+}

certora/specs/erc20methods.spec

@@ -0,0 +1,12 @@
+// erc20 methods
+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/sanity.spec

@@ -5,10 +5,8 @@ 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;
+
+rule sanity(env e, method f, calldataarg arg) {
     f(e, arg);
     assert false;
 }

requirements.txt

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