Merge remote-tracking branch 'Certora/master' into formal-verification

.github/workflows/verify.yml

@@ -0,0 +1,65 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - master
+      - main
+      - certora/erc20
+      - certora/erc1155ext
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.6, 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.4/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.4
+
+      - name: Verify rule ${{ matrix.script }}
+        run: |
+          touch certora/applyHarness.patch
+          make -C certora munged
+          echo "key length" ${#CERTORAKEY}
+          sh certora/scripts/${{ matrix.script }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+
+      matrix:
+        script:
+#          - old/verifyTimelock.sh
+#          - old/verifyERC1155.sh
+#          - old/verifyERC20FlashMint.sh
+#          - old/verifyERC20Wrapper.sh
+#          - old/verifyAccessControl.sh
+#          - old/verifyERC20Votes.sh "checking ERC20Votes.spec on ERC20Votes.sol"
+#          - old/verifyERC721Votes.sh "checking ERC721Votes.spec on draft-ERC721Votes.sol and Votes.sol"
+          - Round3/verifyERC1155Burnable.sh
+          - Round3/verifyERC1155Supply.sh
+          - Round3/verifyERC1155Pausable.sh
+          - Round3/verifyInitializable.sh
+          - Round3/verifyGovernorPreventLateQuorum.sh
+
+
+
+

.gitignore

@@ -62,3 +62,4 @@ artifacts
 .certora*
 .last_confs
 certora_*
+resource_errors.json

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "solidity.compileUsingRemoteVersion": "v0.8.2+commit.661d1103"
+}

certora/applyHarness.patch

@@ -1,101 +1,1486 @@
 diff -ruN .gitignore .gitignore
---- .gitignore	1969-12-31 19:00:00.000000000 -0500
-+++ .gitignore	2021-12-09 14:46:33.923637220 -0500
+--- .gitignore	1969-12-31 16:00:00.000000000 -0800
++++ .gitignore	2022-08-11 21:28:36.000000000 -0700
 @@ -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 @@
+diff -ruN access/AccessControl.sol access/AccessControl.sol
+--- access/AccessControl.sol	2022-08-11 21:28:00.000000000 -0700
++++ access/AccessControl.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -93,7 +93,7 @@
+      *
+      * _Available since v4.6._
+      */
+-    function _checkRole(bytes32 role) internal view virtual {
++    function _checkRole(bytes32 role) public view virtual {         // HARNESS: internal -> public
+         _checkRole(role, _msgSender());
+     }
+ 
+diff -ruN access/Ownable.sol access/Ownable.sol
+--- access/Ownable.sol	2022-08-11 21:28:00.000000000 -0700
++++ access/Ownable.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -30,14 +30,6 @@
+     }
+ 
      /**
-      * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
+-     * @dev Throws if called by any account other than the owner.
+-     */
+-    modifier onlyOwner() {
+-        _checkOwner();
+-        _;
+-    }
+-
+-    /**
+      * @dev Returns the address of the current owner.
       */
--    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;
+     function owner() public view virtual returns (address) {
+@@ -45,10 +37,11 @@
      }
-@@ -253,7 +253,7 @@
+ 
      /**
-      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
+-     * @dev Throws if the sender is not the owner.
++     * @dev Throws if called by any account other than the owner.
       */
--    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;
+-    function _checkOwner() internal view virtual {
++    modifier onlyOwner() {
+         require(owner() == _msgSender(), "Ownable: caller is not the owner");
++        _;
      }
+ 
+     /**
+diff -ruN governance/Governor.sol governance/Governor.sol
+--- governance/Governor.sol	2022-08-11 21:28:00.000000000 -0700
++++ governance/Governor.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -44,7 +44,7 @@
+ 
+     string private _name;
+ 
+-    mapping(uint256 => ProposalCore) private _proposals;
++    mapping(uint256 => ProposalCore) internal _proposals;
+ 
+     // 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 -ruN governance/TimelockController.sol governance/TimelockController.sol
+--- governance/TimelockController.sol	2022-08-11 21:28:00.000000000 -0700
++++ governance/TimelockController.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -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);
+ 
+     mapping(bytes32 => uint256) private _timestamps;
+-    uint256 private _minDelay;
++    uint256 public _minDelay;
+ 
+     /**
+      * @dev Emitted when a call is scheduled as part of operation `id`.
 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 @@
+--- governance/extensions/GovernorCountingSimple.sol	2022-08-11 21:28:00.000000000 -0700
++++ governance/extensions/GovernorCountingSimple.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -27,7 +27,7 @@
+         mapping(address => bool) hasVoted;
+     }
+ 
+-    mapping(uint256 => ProposalVote) private _proposalVotes;
++    mapping(uint256 => ProposalVote) internal _proposalVotes;
+ 
      /**
-      * @dev See {Governor-_quorumReached}.
+      * @dev See {IGovernor-COUNTING_MODE}.
+diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
+--- governance/extensions/GovernorPreventLateQuorum.sol	2022-08-11 21:28:00.000000000 -0700
++++ governance/extensions/GovernorPreventLateQuorum.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -21,8 +21,8 @@
+     using SafeCast for uint256;
+     using Timers for Timers.BlockNumber;
+ 
+-    uint64 private _voteExtension;
+-    mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines;
++    uint64 internal _voteExtension;                                         // PRIVATE => INTERNAL
++    mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines;     // 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 -ruN governance/utils/Votes.sol governance/utils/Votes.sol
+--- governance/utils/Votes.sol	2022-08-11 21:28:00.000000000 -0700
++++ governance/utils/Votes.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -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]._blockNumber;
++    }
++    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
++        return _delegateCheckpoints[account]._checkpoints[pos]._value;
++    }
++
++    mapping(address => address) public _delegation;
+     mapping(address => Checkpoints.History) private _delegateCheckpoints;
+     Checkpoints.History private _totalCheckpoints;
+ 
+@@ -124,7 +142,7 @@
+      *
+      * Emits events {DelegateChanged} and {DelegateVotesChanged}.
       */
--    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];
+-    function _delegate(address account, address delegatee) internal virtual {
++    function _delegate(address account, address delegatee) public virtual {
+         address oldDelegate = delegates(account);
+         _delegation[account] = delegatee;
  
-         return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
-@@ -73,7 +73,7 @@
+@@ -142,10 +160,10 @@
+         uint256 amount
+     ) internal virtual {
+         if (from == address(0)) {
+-            _totalCheckpoints.push(_add, amount);
++            _totalCheckpoints.push(_totalCheckpoints.latest() + amount); // Harnessed to remove function pointers
+         }
+         if (to == address(0)) {
+-            _totalCheckpoints.push(_subtract, amount);
++            _totalCheckpoints.push(_totalCheckpoints.latest() - amount); // Harnessed to remove function pointers
+         }
+         _moveDelegateVotes(delegates(from), delegates(to), amount);
+     }
+@@ -160,11 +178,13 @@
+     ) private {
+         if (from != to && amount > 0) {
+             if (from != address(0)) {
+-                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_subtract, amount);
++                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_delegateCheckpoints[from].latest() - amount); // HARNESSED TO REMOVE FUNCTION POINTERS
++                _checkpoints[from] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS
+                 emit DelegateVotesChanged(from, oldValue, newValue);
+             }
+             if (to != address(0)) {
+-                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_add, amount);
++                (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_delegateCheckpoints[to].latest() + amount); // HARNESSED TO REMOVE FUNCTION POINTERS
++                _checkpoints[to] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS
+                 emit DelegateVotesChanged(to, oldValue, newValue);
+             }
+         }
+@@ -207,5 +227,5 @@
      /**
-      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
+      * @dev Must return the voting units held by an account.
       */
--    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];
+-    function _getVotingUnits(address) internal view virtual returns (uint256);
++    function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public
+ }
+diff -ruN metatx/MinimalForwarder.sol metatx/MinimalForwarder.sol
+--- metatx/MinimalForwarder.sol	2022-08-11 21:28:00.000000000 -0700
++++ metatx/MinimalForwarder.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -8,11 +8,6 @@
  
-         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);
+ /**
+  * @dev Simple minimal forwarder to be used together with an ERC2771 compatible contract. See {ERC2771Context}.
+- *
+- * MinimalForwarder is mainly meant for testing, as it is missing features to be a good production-ready forwarder. This
+- * contract does not intend to have all the properties that are needed for a sound forwarding system. A fully
+- * functioning forwarding system with good properties requires more complexity. We suggest you look at other projects
+- * such as the GSN which do have the goal of building a system like that.
+  */
+ contract MinimalForwarder is EIP712 {
+     using ECDSA for bytes32;
+diff -ruN mocks/ERC20TokenizedVaultMock.sol mocks/ERC20TokenizedVaultMock.sol
+--- mocks/ERC20TokenizedVaultMock.sol	1969-12-31 16:00:00.000000000 -0800
++++ mocks/ERC20TokenizedVaultMock.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -0,0 +1,22 @@
++// SPDX-License-Identifier: MIT
++
++pragma solidity ^0.8.0;
++
++import "../token/ERC20/extensions/ERC20TokenizedVault.sol";
++
++// mock class using ERC20
++contract ERC20TokenizedVaultMock is ERC20TokenizedVault {
++    constructor(
++        IERC20Metadata asset,
++        string memory name,
++        string memory symbol
++    ) ERC20(name, symbol) ERC20TokenizedVault(asset) {}
++
++    function mockMint(address account, uint256 amount) public {
++        _mint(account, amount);
++    }
++
++    function mockBurn(address account, uint256 amount) public {
++        _burn(account, amount);
++    }
++}
+diff -ruN mocks/ERC4626Mock.sol mocks/ERC4626Mock.sol
+--- mocks/ERC4626Mock.sol	2022-08-11 21:28:00.000000000 -0700
++++ mocks/ERC4626Mock.sol	1969-12-31 16:00:00.000000000 -0800
+@@ -1,22 +0,0 @@
+-// SPDX-License-Identifier: MIT
+-
+-pragma solidity ^0.8.0;
+-
+-import "../token/ERC20/extensions/ERC4626.sol";
+-
+-// mock class using ERC20
+-contract ERC4626Mock is ERC4626 {
+-    constructor(
+-        IERC20Metadata asset,
+-        string memory name,
+-        string memory symbol
+-    ) ERC20(name, symbol) ERC4626(asset) {}
+-
+-    function mockMint(address account, uint256 amount) public {
+-        _mint(account, amount);
+-    }
+-
+-    function mockBurn(address account, uint256 amount) public {
+-        _burn(account, amount);
+-    }
+-}
+diff -ruN mocks/MathMock.sol mocks/MathMock.sol
+--- mocks/MathMock.sol	2022-08-11 21:28:00.000000000 -0700
++++ mocks/MathMock.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -29,8 +29,4 @@
+     ) public pure returns (uint256) {
+         return Math.mulDiv(a, b, denominator, direction);
      }
+-
+-    function sqrt(uint256 a, Math.Rounding direction) public pure returns (uint256) {
+-        return Math.sqrt(a, direction);
+-    }
+ }
+diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol
+--- mocks/SafeERC20Helper.sol	2022-08-11 21:28:00.000000000 -0700
++++ mocks/SafeERC20Helper.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -4,7 +4,6 @@
  
-     /**
-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 @@
+ import "../utils/Context.sol";
+ import "../token/ERC20/IERC20.sol";
+-import "../token/ERC20/extensions/draft-ERC20Permit.sol";
+ import "../token/ERC20/utils/SafeERC20.sol";
  
-     string private _name;
+ contract ERC20ReturnFalseMock is Context {
+@@ -106,43 +105,6 @@
+     }
+ }
  
--    mapping(uint256 => ProposalCore) private _proposals;
+-contract ERC20PermitNoRevertMock is
+-    ERC20("ERC20PermitNoRevertMock", "ERC20PermitNoRevertMock"),
+-    ERC20Permit("ERC20PermitNoRevertMock")
+-{
+-    function getChainId() external view returns (uint256) {
+-        return block.chainid;
+-    }
+-
+-    function permitThatMayRevert(
+-        address owner,
+-        address spender,
+-        uint256 value,
+-        uint256 deadline,
+-        uint8 v,
+-        bytes32 r,
+-        bytes32 s
+-    ) public virtual {
+-        super.permit(owner, spender, value, deadline, v, r, s);
+-    }
+-
+-    function permit(
+-        address owner,
+-        address spender,
+-        uint256 value,
+-        uint256 deadline,
+-        uint8 v,
+-        bytes32 r,
+-        bytes32 s
+-    ) public virtual override {
+-        try this.permitThatMayRevert(owner, spender, value, deadline, v, r, s) {
+-            // do nothing
+-        } catch {
+-            // do nothing
+-        }
+-    }
+-}
+-
+ contract SafeERC20Wrapper is Context {
+     using SafeERC20 for IERC20;
+ 
+@@ -172,18 +134,6 @@
+         _token.safeDecreaseAllowance(address(0), amount);
+     }
+ 
+-    function permit(
+-        address owner,
+-        address spender,
+-        uint256 value,
+-        uint256 deadline,
+-        uint8 v,
+-        bytes32 r,
+-        bytes32 s
+-    ) public {
+-        SafeERC20.safePermit(IERC20Permit(address(_token)), owner, spender, value, deadline, v, r, s);
+-    }
 -
-+    mapping(uint256 => ProposalCore) public _proposals;
-+ 
+     function setAllowance(uint256 allowance_) public {
+         ERC20ReturnTrueMock(address(_token)).setAllowance(allowance_);
+     }
+diff -ruN proxy/Clones.sol proxy/Clones.sol
+--- proxy/Clones.sol	2022-08-11 21:28:00.000000000 -0700
++++ proxy/Clones.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -26,10 +26,10 @@
+         /// @solidity memory-safe-assembly
+         assembly {
+             let ptr := mload(0x40)
+-            mstore(ptr, 0x3d602d80600a3d3981f3363d3d373d3d3d363d73000000000000000000000000)
+-            mstore(add(ptr, 0x14), shl(0x60, implementation))
+-            mstore(add(ptr, 0x28), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000)
+-            instance := create(0, ptr, 0x37)
++            mstore(ptr, 0x602d8060093d393df3363d3d373d3d3d363d7300000000000000000000000000)
++            mstore(add(ptr, 0x13), shl(0x60, implementation))
++            mstore(add(ptr, 0x27), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000)
++            instance := create(0, ptr, 0x36)
+         }
+         require(instance != address(0), "ERC1167: create failed");
+     }
+@@ -45,10 +45,10 @@
+         /// @solidity memory-safe-assembly
+         assembly {
+             let ptr := mload(0x40)
+-            mstore(ptr, 0x3d602d80600a3d3981f3363d3d373d3d3d363d73000000000000000000000000)
+-            mstore(add(ptr, 0x14), shl(0x60, implementation))
+-            mstore(add(ptr, 0x28), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000)
+-            instance := create2(0, ptr, 0x37, salt)
++            mstore(ptr, 0x602d8060093d393df3363d3d373d3d3d363d7300000000000000000000000000)
++            mstore(add(ptr, 0x13), shl(0x60, implementation))
++            mstore(add(ptr, 0x27), 0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000)
++            instance := create2(0, ptr, 0x36, salt)
+         }
+         require(instance != address(0), "ERC1167: create2 failed");
+     }
+@@ -64,13 +64,13 @@
+         /// @solidity memory-safe-assembly
+         assembly {
+             let ptr := mload(0x40)
+-            mstore(ptr, 0x3d602d80600a3d3981f3363d3d373d3d3d363d73000000000000000000000000)
+-            mstore(add(ptr, 0x14), shl(0x60, implementation))
+-            mstore(add(ptr, 0x28), 0x5af43d82803e903d91602b57fd5bf3ff00000000000000000000000000000000)
+-            mstore(add(ptr, 0x38), shl(0x60, deployer))
+-            mstore(add(ptr, 0x4c), salt)
+-            mstore(add(ptr, 0x6c), keccak256(ptr, 0x37))
+-            predicted := keccak256(add(ptr, 0x37), 0x55)
++            mstore(ptr, 0x602d8060093d393df3363d3d373d3d3d363d7300000000000000000000000000)
++            mstore(add(ptr, 0x13), shl(0x60, implementation))
++            mstore(add(ptr, 0x27), 0x5af43d82803e903d91602b57fd5bf3ff00000000000000000000000000000000)
++            mstore(add(ptr, 0x37), shl(0x60, deployer))
++            mstore(add(ptr, 0x4b), salt)
++            mstore(add(ptr, 0x6b), keccak256(ptr, 0x36))
++            predicted := keccak256(add(ptr, 0x36), 0x55)
+         }
+     }
+ 
+diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol
+--- proxy/ERC1967/ERC1967Proxy.sol	2022-08-11 21:28:00.000000000 -0700
++++ proxy/ERC1967/ERC1967Proxy.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -20,6 +20,7 @@
+      * function call, and allows initializing the storage of the proxy like a Solidity constructor.
+      */
+     constructor(address _logic, bytes memory _data) payable {
++        assert(_IMPLEMENTATION_SLOT == bytes32(uint256(keccak256("eip1967.proxy.implementation")) - 1));
+         _upgradeToAndCall(_logic, _data, false);
+     }
+ 
+diff -ruN proxy/beacon/BeaconProxy.sol proxy/beacon/BeaconProxy.sol
+--- proxy/beacon/BeaconProxy.sol	2022-08-11 21:28:00.000000000 -0700
++++ proxy/beacon/BeaconProxy.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -28,6 +28,7 @@
+      * - `beacon` must be a contract with the interface {IBeacon}.
+      */
+     constructor(address beacon, bytes memory data) payable {
++        assert(_BEACON_SLOT == bytes32(uint256(keccak256("eip1967.proxy.beacon")) - 1));
+         _upgradeBeaconToAndCall(beacon, data, false);
+     }
+ 
+diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/TransparentUpgradeableProxy.sol
+--- proxy/transparent/TransparentUpgradeableProxy.sol	2022-08-11 21:28:00.000000000 -0700
++++ proxy/transparent/TransparentUpgradeableProxy.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -36,6 +36,7 @@
+         address admin_,
+         bytes memory _data
+     ) payable ERC1967Proxy(_logic, _data) {
++        assert(_ADMIN_SLOT == bytes32(uint256(keccak256("eip1967.proxy.admin")) - 1));
+         _changeAdmin(admin_);
+     }
+ 
+diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol
+--- proxy/utils/Initializable.sol	2022-08-11 21:28:00.000000000 -0700
++++ proxy/utils/Initializable.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -59,12 +59,12 @@
+      * @dev Indicates that the contract has been initialized.
+      * @custom:oz-retyped-from bool
+      */
+-    uint8 private _initialized;
++    uint8 internal _initialized;
+ 
      /**
-      * @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 Indicates that the contract is in the process of being initialized.
+      */
+-    bool private _initializing;
++    bool internal _initializing;
+ 
      /**
-      * @dev Amount of votes already cast passes the threshold limit.
+      * @dev Triggered when the contract has been initialized or reinitialized.
+diff -ruN proxy/utils/Initializable.sol.orig proxy/utils/Initializable.sol.orig
+--- proxy/utils/Initializable.sol.orig	1969-12-31 16:00:00.000000000 -0800
++++ proxy/utils/Initializable.sol.orig	2022-08-11 21:28:36.000000000 -0700
+@@ -0,0 +1,138 @@
++// SPDX-License-Identifier: MIT
++// OpenZeppelin Contracts (last updated v4.6.0) (proxy/utils/Initializable.sol)
++
++pragma solidity ^0.8.2;
++
++import "../../utils/Address.sol";
++
++/**
++ * @dev This is a base contract to aid in writing upgradeable contracts, or any kind of contract that will be deployed
++ * behind a proxy. Since proxied contracts do not make use of a constructor, it's common to move constructor logic to an
++ * external initializer function, usually called `initialize`. It then becomes necessary to protect this initializer
++ * function so it can only be called once. The {initializer} modifier provided by this contract will have this effect.
++ *
++ * The initialization functions use a version number. Once a version number is used, it is consumed and cannot be
++ * reused. This mechanism prevents re-execution of each "step" but allows the creation of new initialization steps in
++ * case an upgrade adds a module that needs to be initialized.
++ *
++ * For example:
++ *
++ * [.hljs-theme-light.nopadding]
++ * ```
++ * contract MyToken is ERC20Upgradeable {
++ *     function initialize() initializer public {
++ *         __ERC20_init("MyToken", "MTK");
++ *     }
++ * }
++ * contract MyTokenV2 is MyToken, ERC20PermitUpgradeable {
++ *     function initializeV2() reinitializer(2) public {
++ *         __ERC20Permit_init("MyToken");
++ *     }
++ * }
++ * ```
++ *
++ * TIP: To avoid leaving the proxy in an uninitialized state, the initializer function should be called as early as
++ * possible by providing the encoded function call as the `_data` argument to {ERC1967Proxy-constructor}.
++ *
++ * CAUTION: When used with inheritance, manual care must be taken to not invoke a parent initializer twice, or to ensure
++ * that all initializers are idempotent. This is not verified automatically as constructors are by Solidity.
++ *
++ * [CAUTION]
++ * ====
++ * Avoid leaving a contract uninitialized.
++ *
++ * An uninitialized contract can be taken over by an attacker. This applies to both a proxy and its implementation
++ * contract, which may impact the proxy. To prevent the implementation contract from being used, you should invoke
++ * the {_disableInitializers} function in the constructor to automatically lock it when it is deployed:
++ *
++ * [.hljs-theme-light.nopadding]
++ * ```
++ * /// @custom:oz-upgrades-unsafe-allow constructor
++ * constructor() {
++ *     _disableInitializers();
++ * }
++ * ```
++ * ====
++ */
++abstract contract Initializable {
++    /**
++     * @dev Indicates that the contract has been initialized.
++     * @custom:oz-retyped-from bool
++     */
++    uint8 private _initialized;
++
++    /**
++     * @dev Indicates that the contract is in the process of being initialized.
++     */
++    bool private _initializing;
++
++    /**
++     * @dev Triggered when the contract has been initialized or reinitialized.
++     */
++    event Initialized(uint8 version);
++
++    /**
++     * @dev A modifier that defines a protected initializer function that can be invoked at most once. In its scope,
++     * `onlyInitializing` functions can be used to initialize parent contracts. Equivalent to `reinitializer(1)`.
++     */
++    modifier initializer() {
++        bool isTopLevelCall = !_initializing;
++        require(
++            (isTopLevelCall && _initialized < 1) || (!Address.isContract(address(this)) && _initialized == 1),
++            "Initializable: contract is already initialized"
++        );
++        _initialized = 1;
++        if (isTopLevelCall) {
++            _initializing = true;
++        }
++        _;
++        if (isTopLevelCall) {
++            _initializing = false;
++            emit Initialized(1);
++        }
++    }
++
++    /**
++     * @dev A modifier that defines a protected reinitializer function that can be invoked at most once, and only if the
++     * contract hasn't been initialized to a greater version before. In its scope, `onlyInitializing` functions can be
++     * used to initialize parent contracts.
++     *
++     * `initializer` is equivalent to `reinitializer(1)`, so a reinitializer may be used after the original
++     * initialization step. This is essential to configure modules that are added through upgrades and that require
++     * initialization.
++     *
++     * Note that versions can jump in increments greater than 1; this implies that if multiple reinitializers coexist in
++     * a contract, executing them in the right order is up to the developer or operator.
++     */
++    modifier reinitializer(uint8 version) {
++        require(!_initializing && _initialized < version, "Initializable: contract is already initialized");
++        _initialized = version;
++        _initializing = true;
++        _;
++        _initializing = false;
++        emit Initialized(version);
++    }
++
++    /**
++     * @dev Modifier to protect an initialization function so that it can only be invoked by functions with the
++     * {initializer} and {reinitializer} modifiers, directly or indirectly.
++     */
++    modifier onlyInitializing() {
++        require(_initializing, "Initializable: contract is not initializing");
++        _;
++    }
++
++    /**
++     * @dev Locks the contract, preventing any future reinitialization. This cannot be part of an initializer call.
++     * Calling this in the constructor of a contract will prevent that contract from being initialized or reinitialized
++     * to any version. It is recommended to use this to lock implementation contracts that are designed to be called
++     * through proxies.
++     */
++    function _disableInitializers() internal virtual {
++        require(!_initializing, "Initializable: contract is initializing");
++        if (_initialized < type(uint8).max) {
++            _initialized = type(uint8).max;
++            emit Initialized(type(uint8).max);
++        }
++    }
++}
+diff -ruN proxy/utils/Initializable.sol.rej proxy/utils/Initializable.sol.rej
+--- proxy/utils/Initializable.sol.rej	1969-12-31 16:00:00.000000000 -0800
++++ proxy/utils/Initializable.sol.rej	2022-08-11 21:28:36.000000000 -0700
+@@ -0,0 +1,17 @@
++***************
++*** 130,136 ****
++          _setInitializedVersion(type(uint8).max);
++      }
++  
++-     function _setInitializedVersion(uint8 version) private returns (bool) {
++          // If the contract is initializing we ignore whether _initialized is set in order to support multiple
++          // inheritance patterns, but we only do this in the context of a constructor, and for the lowest level
++          // of initializers, because in other contexts the contract may have been reentered.
++--- 130,136 ----
++          _setInitializedVersion(type(uint8).max);
++      }
++  
+++     function _setInitializedVersion(uint8 version) internal returns (bool) {
++          // If the contract is initializing we ignore whether _initialized is set in order to support multiple
++          // inheritance patterns, but we only do this in the context of a constructor, and for the lowest level
++          // of initializers, because in other contexts the contract may have been reentered.
+diff -ruN security/Pausable.sol security/Pausable.sol
+--- security/Pausable.sol	2022-08-11 21:28:00.000000000 -0700
++++ security/Pausable.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -35,6 +35,13 @@
+     }
+ 
+     /**
++     * @dev Returns true if the contract is paused, and false otherwise.
++     */
++    function paused() public view virtual returns (bool) {
++        return _paused;
++    }
++
++    /**
+      * @dev Modifier to make a function callable only when the contract is not paused.
+      *
+      * Requirements:
+@@ -42,7 +49,7 @@
+      * - The contract must not be paused.
       */
--    function _quorumReached(uint256 proposalId) internal view virtual returns (bool);
-+    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+     modifier whenNotPaused() {
+-        _requireNotPaused();
++        require(!paused(), "Pausable: paused");
+         _;
+     }
+ 
+@@ -54,29 +61,8 @@
+      * - The contract must be paused.
+      */
+     modifier whenPaused() {
+-        _requirePaused();
+-        _;
+-    }
+-
+-    /**
+-     * @dev Returns true if the contract is paused, and false otherwise.
+-     */
+-    function paused() public view virtual returns (bool) {
+-        return _paused;
+-    }
+-
+-    /**
+-     * @dev Throws if the contract is paused.
+-     */
+-    function _requireNotPaused() internal view virtual {
+-        require(!paused(), "Pausable: paused");
+-    }
+-
+-    /**
+-     * @dev Throws if the contract is not paused.
+-     */
+-    function _requirePaused() internal view virtual {
+         require(paused(), "Pausable: not paused");
++        _;
+     }
  
      /**
-      * @dev Is the proposal successful or not.
+diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
+--- token/ERC1155/ERC1155.sol	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC1155/ERC1155.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -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; // MUNGED private => internal
+ 
+     // Mapping from account to operator approvals
+     mapping(address => mapping(address => bool)) private _operatorApprovals;
+@@ -471,7 +471,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) {
+@@ -492,7 +492,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 -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
+--- token/ERC20/ERC20.sol	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC20/ERC20.sol	2022-08-11 23:01:50.000000000 -0700
+@@ -277,7 +277,7 @@
+      * - `account` cannot be the zero address.
+      * - `account` must have at least `amount` tokens.
       */
--    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 _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 -ruN token/ERC20/README.adoc token/ERC20/README.adoc
+--- token/ERC20/README.adoc	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC20/README.adoc	2022-08-11 21:28:36.000000000 -0700
+@@ -24,7 +24,7 @@
+ * {ERC20Votes}: support for voting and vote delegation.
+ * {ERC20VotesComp}: support for voting and vote delegation (compatible with Compound's token, with uint96 restrictions).
+ * {ERC20Wrapper}: wrapper to create an ERC20 backed by another ERC20, with deposit and withdraw methods. Useful in conjunction with {ERC20Votes}.
+-* {ERC4626}: tokenized vault that manages shares (represented as ERC20) that are backed by assets (another ERC20).
++* {ERC20TokenizedVault}: tokenized vault that manages shares (represented as ERC20) that are backed by assets (another ERC20).
+ 
+ Finally, there are some utilities to interact with ERC20 contracts in various ways.
+ 
+@@ -63,7 +63,7 @@
+ 
+ {{ERC20FlashMint}}
+ 
+-{{ERC4626}}
++{{ERC20TokenizedVault}}
+ 
+ == Draft EIPs
+ 
+diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
+--- token/ERC20/extensions/ERC20FlashMint.sol	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC20/extensions/ERC20FlashMint.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -40,9 +40,11 @@
+         require(token == address(this), "ERC20FlashMint: wrong token");
+         // silence warning about unused variable without the addition of bytecode.
+         amount;
+-        return 0;
++        return fee;                 // HARNESS: made "return" nonzero
+     }
+ 
++    uint256 public fee;             // HARNESS: added it to simulate random fee amount
++
      /**
-      * @dev Register a vote with a given support and voting weight.
+      * @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 -ruN token/ERC20/extensions/ERC20TokenizedVault.sol token/ERC20/extensions/ERC20TokenizedVault.sol
+--- token/ERC20/extensions/ERC20TokenizedVault.sol	1969-12-31 16:00:00.000000000 -0800
++++ token/ERC20/extensions/ERC20TokenizedVault.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -0,0 +1,217 @@
++// SPDX-License-Identifier: MIT
++
++pragma solidity ^0.8.0;
++
++import "../ERC20.sol";
++import "../utils/SafeERC20.sol";
++import "../../../interfaces/IERC4626.sol";
++import "../../../utils/math/Math.sol";
++
++/**
++ * @dev Implementation of the ERC4626 "Tokenized Vault Standard" as defined in
++ * https://eips.ethereum.org/EIPS/eip-4626[EIP-4626].
++ *
++ * This extension allows the minting and burning of "shares" (represented using the ERC20 inheritance) in exchange for
++ * underlying "assets" through standardized {deposit}, {mint}, {redeem} and {burn} workflows. This contract extends
++ * the ERC20 standard. Any additional extensions included along it would affect the "shares" token represented by this
++ * contract and not the "assets" token which is an independent contract.
++ *
++ * _Available since v4.7._
++ */
++abstract contract ERC20TokenizedVault is ERC20, IERC4626 {
++    using Math for uint256;
++
++    IERC20Metadata private immutable _asset;
++
++    /**
++     * @dev Set the underlying asset contract. This must be an ERC20-compatible contract (ERC20 or ERC777).
++     */
++    constructor(IERC20Metadata asset_) {
++        _asset = asset_;
++    }
++
++    /** @dev See {IERC4262-asset} */
++    function asset() public view virtual override returns (address) {
++        return address(_asset);
++    }
++
++    /** @dev See {IERC4262-totalAssets} */
++    function totalAssets() public view virtual override returns (uint256) {
++        return _asset.balanceOf(address(this));
++    }
++
++    /** @dev See {IERC4262-convertToShares} */
++    function convertToShares(uint256 assets) public view virtual override returns (uint256 shares) {
++        return _convertToShares(assets, Math.Rounding.Down);
++    }
++
++    /** @dev See {IERC4262-convertToAssets} */
++    function convertToAssets(uint256 shares) public view virtual override returns (uint256 assets) {
++        return _convertToAssets(shares, Math.Rounding.Down);
++    }
++
++    /** @dev See {IERC4262-maxDeposit} */
++    function maxDeposit(address) public view virtual override returns (uint256) {
++        return _isVaultCollateralized() ? type(uint256).max : 0;
++    }
++
++    /** @dev See {IERC4262-maxMint} */
++    function maxMint(address) public view virtual override returns (uint256) {
++        return type(uint256).max;
++    }
++
++    /** @dev See {IERC4262-maxWithdraw} */
++    function maxWithdraw(address owner) public view virtual override returns (uint256) {
++        return _convertToAssets(balanceOf(owner), Math.Rounding.Down);
++    }
++
++    /** @dev See {IERC4262-maxRedeem} */
++    function maxRedeem(address owner) public view virtual override returns (uint256) {
++        return balanceOf(owner);
++    }
++
++    /** @dev See {IERC4262-previewDeposit} */
++    function previewDeposit(uint256 assets) public view virtual override returns (uint256) {
++        return _convertToShares(assets, Math.Rounding.Down);
++    }
++
++    /** @dev See {IERC4262-previewMint} */
++    function previewMint(uint256 shares) public view virtual override returns (uint256) {
++        return _convertToAssets(shares, Math.Rounding.Up);
++    }
++
++    /** @dev See {IERC4262-previewWithdraw} */
++    function previewWithdraw(uint256 assets) public view virtual override returns (uint256) {
++        return _convertToShares(assets, Math.Rounding.Up);
++    }
++
++    /** @dev See {IERC4262-previewRedeem} */
++    function previewRedeem(uint256 shares) public view virtual override returns (uint256) {
++        return _convertToAssets(shares, Math.Rounding.Down);
++    }
++
++    /** @dev See {IERC4262-deposit} */
++    function deposit(uint256 assets, address receiver) public virtual override returns (uint256) {
++        require(assets <= maxDeposit(receiver), "ERC20TokenizedVault: deposit more than max");
++
++        uint256 shares = previewDeposit(assets);
++        _deposit(_msgSender(), receiver, assets, shares);
++
++        return shares;
++    }
++
++    /** @dev See {IERC4262-mint} */
++    function mint(uint256 shares, address receiver) public virtual override returns (uint256) {
++        require(shares <= maxMint(receiver), "ERC20TokenizedVault: mint more than max");
++
++        uint256 assets = previewMint(shares);
++        _deposit(_msgSender(), receiver, assets, shares);
++
++        return assets;
++    }
++
++    /** @dev See {IERC4262-withdraw} */
++    function withdraw(
++        uint256 assets,
++        address receiver,
++        address owner
++    ) public virtual override returns (uint256) {
++        require(assets <= maxWithdraw(owner), "ERC20TokenizedVault: withdraw more than max");
++
++        uint256 shares = previewWithdraw(assets);
++        _withdraw(_msgSender(), receiver, owner, assets, shares);
++
++        return shares;
++    }
++
++    /** @dev See {IERC4262-redeem} */
++    function redeem(
++        uint256 shares,
++        address receiver,
++        address owner
++    ) public virtual override returns (uint256) {
++        require(shares <= maxRedeem(owner), "ERC20TokenizedVault: redeem more than max");
++
++        uint256 assets = previewRedeem(shares);
++        _withdraw(_msgSender(), receiver, owner, assets, shares);
++
++        return assets;
++    }
++
++    /**
++     * @dev Internal convertion function (from assets to shares) with support for rounding direction
++     *
++     * Will revert if assets > 0, totalSupply > 0 and totalAssets = 0. That corresponds to a case where any asset
++     * would represent an infinite amout of shares.
++     */
++    function _convertToShares(uint256 assets, Math.Rounding rounding) internal view virtual returns (uint256 shares) {
++        uint256 supply = totalSupply();
++        return
++            (assets == 0 || supply == 0)
++                ? assets.mulDiv(10**decimals(), 10**_asset.decimals(), rounding)
++                : assets.mulDiv(supply, totalAssets(), rounding);
++    }
++
++    /**
++     * @dev Internal convertion function (from shares to assets) with support for rounding direction
++     */
++    function _convertToAssets(uint256 shares, Math.Rounding rounding) internal view virtual returns (uint256 assets) {
++        uint256 supply = totalSupply();
++        return
++            (supply == 0)
++                ? shares.mulDiv(10**_asset.decimals(), 10**decimals(), rounding)
++                : shares.mulDiv(totalAssets(), supply, rounding);
++    }
++
++    /**
++     * @dev Deposit/mint common workflow
++     */
++    function _deposit(
++        address caller,
++        address receiver,
++        uint256 assets,
++        uint256 shares
++    ) private {
++        // If _asset is ERC777, `transferFrom` can trigger a reenterancy BEFORE the transfer happens through the
++        // `tokensToSend` hook. On the other hand, the `tokenReceived` hook, that is triggered after the transfer,
++        // calls the vault, which is assumed not malicious.
++        //
++        // Conclusion: we need to do the transfer before we mint so that any reentrancy would happen before the
++        // assets are transfered and before the shares are minted, which is a valid state.
++        // slither-disable-next-line reentrancy-no-eth
++        SafeERC20.safeTransferFrom(_asset, caller, address(this), assets);
++        _mint(receiver, shares);
++
++        emit Deposit(caller, receiver, assets, shares);
++    }
++
++    /**
++     * @dev Withdraw/redeem common workflow
++     */
++    function _withdraw(
++        address caller,
++        address receiver,
++        address owner,
++        uint256 assets,
++        uint256 shares
++    ) private {
++        if (caller != owner) {
++            _spendAllowance(owner, caller, shares);
++        }
++
++        // If _asset is ERC777, `transfer` can trigger trigger a reentrancy AFTER the transfer happens through the
++        // `tokensReceived` hook. On the other hand, the `tokensToSend` hook, that is triggered before the transfer,
++        // calls the vault, which is assumed not malicious.
++        //
++        // Conclusion: we need to do the transfer after the burn so that any reentrancy would happen after the
++        // shares are burned and after the assets are transfered, which is a valid state.
++        _burn(owner, shares);
++        SafeERC20.safeTransfer(_asset, receiver, assets);
++
++        emit Withdraw(caller, receiver, owner, assets, shares);
++    }
++
++    function _isVaultCollateralized() private view returns (bool) {
++        return totalAssets() > 0 || totalSupply() == 0;
++    }
++}
 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 @@
+--- token/ERC20/extensions/ERC20Votes.sol	2022-08-11 21:16:57.000000000 -0700
++++ token/ERC20/extensions/ERC20Votes.sol	2022-08-11 22:47:30.000000000 -0700
+@@ -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;
++    mapping(address => Checkpoint[]) public _checkpoints;
+     Checkpoint[] private _totalSupplyCheckpoints;
+ 
+     /**
+@@ -152,7 +152,7 @@
+     /**
+      * @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) { //harnessed to public
+         return type(uint224).max;
+     }
+ 
+@@ -163,16 +163,16 @@
+         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
+     }
+ 
+     /**
+@@ -187,7 +187,7 @@
+     ) internal virtual override {
+         super._afterTokenTransfer(from, to, amount);
+ 
+-        _moveVotingPower(delegates(from), delegates(to), amount);
++        _moveVotingPower(delegates(from), delegates(to), amount);       
+     }
+ 
+     /**
+@@ -195,7 +195,7 @@
       *
-      * - `blockNumber` must have been already mined
+      * Emits events {DelegateChanged} and {DelegateVotesChanged}.
       */
--    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 _delegate(address delegator, address delegatee) internal virtual {
++    function _delegate(address delegator, address delegatee) public virtual { // HARNESSED TO MAKE PUBLIC
+         address currentDelegate = delegates(delegator);
+         uint256 delegatorBalance = balanceOf(delegator);
+         _delegates[delegator] = delegatee;
+@@ -212,25 +212,25 @@
+     ) 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(
++    // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool
++    function _writeCheckpointAdd(
+         Checkpoint[] storage ckpts,
+-        function(uint256, uint256) view returns (uint256) op,
+         uint256 delta
+     ) private returns (uint256 oldWeight, uint256 newWeight) {
+         uint256 pos = ckpts.length;
+         oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
+-        newWeight = op(oldWeight, delta);
++        newWeight = _add(oldWeight, delta);
+ 
+         if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) {
+             ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
+@@ -239,6 +239,39 @@
+         }
+     }
+ 
++    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 && ckpts[pos - 1].fromBlock == block.number) {
++            ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
++        } else {
++            ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)}));
++        }
++    }
++
++    // backup of original function
++    //
++    // function _writeCheckpoint(
++    //     Checkpoint[] storage ckpts,
++    //     function(uint256, uint256) view returns (uint256) op,
++    //     uint256 delta
++    // ) private returns (uint256 oldWeight, uint256 newWeight) {
++    //     uint256 pos = ckpts.length;
++    //     oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
++    //     newWeight = op(oldWeight, delta);
++    //
++    //     if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) {
++    //         ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
++    //     } else {
++    //         ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)}));
++    //     }
++    // }
++
+     function _add(uint256 a, uint256 b) private pure returns (uint256) {
+         return a + b;
+     }
+diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
+--- token/ERC20/extensions/ERC20Wrapper.sol	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC20/extensions/ERC20Wrapper.sol	2022-08-11 21:29:19.000000000 -0700
+@@ -1,5 +1,5 @@
+ // SPDX-License-Identifier: MIT
+-// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/extensions/ERC20Wrapper.sol)
++// OpenZeppelin Contracts v4.4.1 (token/ERC20/extensions/ERC20Wrapper.sol)
+ 
+ pragma solidity ^0.8.0;
+ 
+@@ -23,17 +23,6 @@
+     }
+ 
+     /**
+-     * @dev See {ERC20-decimals}.
+-     */
+-    function decimals() public view virtual override returns (uint8) {
+-        try IERC20Metadata(address(underlying)).decimals() returns (uint8 value) {
+-            return value;
+-        } catch {
+-            return super.decimals();
+-        }
+-    }
+-
+-    /**
+      * @dev Allow a user to deposit underlying tokens and mint the corresponding number of wrapped tokens.
+      */
+     function depositFor(address account, uint256 amount) public virtual returns (bool) {
+@@ -55,7 +44,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 -ruN token/ERC20/extensions/ERC4626.sol token/ERC20/extensions/ERC4626.sol
+--- token/ERC20/extensions/ERC4626.sol	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC20/extensions/ERC4626.sol	1969-12-31 16:00:00.000000000 -0800
+@@ -1,217 +0,0 @@
+-// SPDX-License-Identifier: MIT
+-
+-pragma solidity ^0.8.0;
+-
+-import "../ERC20.sol";
+-import "../utils/SafeERC20.sol";
+-import "../../../interfaces/IERC4626.sol";
+-import "../../../utils/math/Math.sol";
+-
+-/**
+- * @dev Implementation of the ERC4626 "Tokenized Vault Standard" as defined in
+- * https://eips.ethereum.org/EIPS/eip-4626[EIP-4626].
+- *
+- * This extension allows the minting and burning of "shares" (represented using the ERC20 inheritance) in exchange for
+- * underlying "assets" through standardized {deposit}, {mint}, {redeem} and {burn} workflows. This contract extends
+- * the ERC20 standard. Any additional extensions included along it would affect the "shares" token represented by this
+- * contract and not the "assets" token which is an independent contract.
+- *
+- * _Available since v4.7._
+- */
+-abstract contract ERC4626 is ERC20, IERC4626 {
+-    using Math for uint256;
+-
+-    IERC20Metadata private immutable _asset;
+-
+-    /**
+-     * @dev Set the underlying asset contract. This must be an ERC20-compatible contract (ERC20 or ERC777).
+-     */
+-    constructor(IERC20Metadata asset_) {
+-        _asset = asset_;
+-    }
+-
+-    /** @dev See {IERC4262-asset} */
+-    function asset() public view virtual override returns (address) {
+-        return address(_asset);
+-    }
+-
+-    /** @dev See {IERC4262-totalAssets} */
+-    function totalAssets() public view virtual override returns (uint256) {
+-        return _asset.balanceOf(address(this));
+-    }
+-
+-    /** @dev See {IERC4262-convertToShares} */
+-    function convertToShares(uint256 assets) public view virtual override returns (uint256 shares) {
+-        return _convertToShares(assets, Math.Rounding.Down);
+-    }
+-
+-    /** @dev See {IERC4262-convertToAssets} */
+-    function convertToAssets(uint256 shares) public view virtual override returns (uint256 assets) {
+-        return _convertToAssets(shares, Math.Rounding.Down);
+-    }
+-
+-    /** @dev See {IERC4262-maxDeposit} */
+-    function maxDeposit(address) public view virtual override returns (uint256) {
+-        return _isVaultCollateralized() ? type(uint256).max : 0;
+-    }
+-
+-    /** @dev See {IERC4262-maxMint} */
+-    function maxMint(address) public view virtual override returns (uint256) {
+-        return type(uint256).max;
+-    }
+-
+-    /** @dev See {IERC4262-maxWithdraw} */
+-    function maxWithdraw(address owner) public view virtual override returns (uint256) {
+-        return _convertToAssets(balanceOf(owner), Math.Rounding.Down);
+-    }
+-
+-    /** @dev See {IERC4262-maxRedeem} */
+-    function maxRedeem(address owner) public view virtual override returns (uint256) {
+-        return balanceOf(owner);
+-    }
+-
+-    /** @dev See {IERC4262-previewDeposit} */
+-    function previewDeposit(uint256 assets) public view virtual override returns (uint256) {
+-        return _convertToShares(assets, Math.Rounding.Down);
+-    }
+-
+-    /** @dev See {IERC4262-previewMint} */
+-    function previewMint(uint256 shares) public view virtual override returns (uint256) {
+-        return _convertToAssets(shares, Math.Rounding.Up);
+-    }
+-
+-    /** @dev See {IERC4262-previewWithdraw} */
+-    function previewWithdraw(uint256 assets) public view virtual override returns (uint256) {
+-        return _convertToShares(assets, Math.Rounding.Up);
+-    }
+-
+-    /** @dev See {IERC4262-previewRedeem} */
+-    function previewRedeem(uint256 shares) public view virtual override returns (uint256) {
+-        return _convertToAssets(shares, Math.Rounding.Down);
+-    }
+-
+-    /** @dev See {IERC4262-deposit} */
+-    function deposit(uint256 assets, address receiver) public virtual override returns (uint256) {
+-        require(assets <= maxDeposit(receiver), "ERC4626: deposit more than max");
+-
+-        uint256 shares = previewDeposit(assets);
+-        _deposit(_msgSender(), receiver, assets, shares);
+-
+-        return shares;
+-    }
+-
+-    /** @dev See {IERC4262-mint} */
+-    function mint(uint256 shares, address receiver) public virtual override returns (uint256) {
+-        require(shares <= maxMint(receiver), "ERC4626: mint more than max");
+-
+-        uint256 assets = previewMint(shares);
+-        _deposit(_msgSender(), receiver, assets, shares);
+-
+-        return assets;
+-    }
+-
+-    /** @dev See {IERC4262-withdraw} */
+-    function withdraw(
+-        uint256 assets,
+-        address receiver,
+-        address owner
+-    ) public virtual override returns (uint256) {
+-        require(assets <= maxWithdraw(owner), "ERC4626: withdraw more than max");
+-
+-        uint256 shares = previewWithdraw(assets);
+-        _withdraw(_msgSender(), receiver, owner, assets, shares);
+-
+-        return shares;
+-    }
+-
+-    /** @dev See {IERC4262-redeem} */
+-    function redeem(
+-        uint256 shares,
+-        address receiver,
+-        address owner
+-    ) public virtual override returns (uint256) {
+-        require(shares <= maxRedeem(owner), "ERC4626: redeem more than max");
+-
+-        uint256 assets = previewRedeem(shares);
+-        _withdraw(_msgSender(), receiver, owner, assets, shares);
+-
+-        return assets;
+-    }
+-
+-    /**
+-     * @dev Internal convertion function (from assets to shares) with support for rounding direction
+-     *
+-     * Will revert if assets > 0, totalSupply > 0 and totalAssets = 0. That corresponds to a case where any asset
+-     * would represent an infinite amout of shares.
+-     */
+-    function _convertToShares(uint256 assets, Math.Rounding rounding) internal view virtual returns (uint256 shares) {
+-        uint256 supply = totalSupply();
+-        return
+-            (assets == 0 || supply == 0)
+-                ? assets.mulDiv(10**decimals(), 10**_asset.decimals(), rounding)
+-                : assets.mulDiv(supply, totalAssets(), rounding);
+-    }
+-
+-    /**
+-     * @dev Internal convertion function (from shares to assets) with support for rounding direction
+-     */
+-    function _convertToAssets(uint256 shares, Math.Rounding rounding) internal view virtual returns (uint256 assets) {
+-        uint256 supply = totalSupply();
+-        return
+-            (supply == 0)
+-                ? shares.mulDiv(10**_asset.decimals(), 10**decimals(), rounding)
+-                : shares.mulDiv(totalAssets(), supply, rounding);
+-    }
+-
+-    /**
+-     * @dev Deposit/mint common workflow
+-     */
+-    function _deposit(
+-        address caller,
+-        address receiver,
+-        uint256 assets,
+-        uint256 shares
+-    ) private {
+-        // If _asset is ERC777, `transferFrom` can trigger a reenterancy BEFORE the transfer happens through the
+-        // `tokensToSend` hook. On the other hand, the `tokenReceived` hook, that is triggered after the transfer,
+-        // calls the vault, which is assumed not malicious.
+-        //
+-        // Conclusion: we need to do the transfer before we mint so that any reentrancy would happen before the
+-        // assets are transfered and before the shares are minted, which is a valid state.
+-        // slither-disable-next-line reentrancy-no-eth
+-        SafeERC20.safeTransferFrom(_asset, caller, address(this), assets);
+-        _mint(receiver, shares);
+-
+-        emit Deposit(caller, receiver, assets, shares);
+-    }
+-
+-    /**
+-     * @dev Withdraw/redeem common workflow
+-     */
+-    function _withdraw(
+-        address caller,
+-        address receiver,
+-        address owner,
+-        uint256 assets,
+-        uint256 shares
+-    ) private {
+-        if (caller != owner) {
+-            _spendAllowance(owner, caller, shares);
+-        }
+-
+-        // If _asset is ERC777, `transfer` can trigger trigger a reentrancy AFTER the transfer happens through the
+-        // `tokensReceived` hook. On the other hand, the `tokensToSend` hook, that is triggered before the transfer,
+-        // calls the vault, which is assumed not malicious.
+-        //
+-        // Conclusion: we need to do the transfer after the burn so that any reentrancy would happen after the
+-        // shares are burned and after the assets are transfered, which is a valid state.
+-        _burn(owner, shares);
+-        SafeERC20.safeTransfer(_asset, receiver, assets);
+-
+-        emit Withdraw(caller, receiver, owner, assets, shares);
+-    }
+-
+-    function _isVaultCollateralized() private view returns (bool) {
+-        return totalAssets() > 0 || totalSupply() == 0;
+-    }
+-}
+diff -ruN token/ERC20/utils/SafeERC20.sol token/ERC20/utils/SafeERC20.sol
+--- token/ERC20/utils/SafeERC20.sol	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC20/utils/SafeERC20.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -4,7 +4,6 @@
+ pragma solidity ^0.8.0;
+ 
+ import "../IERC20.sol";
+-import "../extensions/draft-IERC20Permit.sol";
+ import "../../../utils/Address.sol";
+ 
+ /**
+@@ -80,22 +79,6 @@
+         }
+     }
+ 
+-    function safePermit(
+-        IERC20Permit token,
+-        address owner,
+-        address spender,
+-        uint256 value,
+-        uint256 deadline,
+-        uint8 v,
+-        bytes32 r,
+-        bytes32 s
+-    ) internal {
+-        uint256 nonceBefore = token.nonces(owner);
+-        token.permit(owner, spender, value, deadline, v, r, s);
+-        uint256 nonceAfter = token.nonces(owner);
+-        require(nonceAfter == nonceBefore + 1, "SafeERC20: permit did not succeed");
+-    }
+-
+     /**
+      * @dev Imitates a Solidity high-level call (i.e. a regular function call to a contract), relaxing the requirement
+      * on the return value: the return value is optional (but if data is returned, it must not be false).
+diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
+--- token/ERC721/extensions/draft-ERC721Votes.sol	2022-08-11 21:28:00.000000000 -0700
++++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -34,7 +34,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) {
+         return balanceOf(account);
+     }
+ }
+diff -ruN utils/Address.sol utils/Address.sol
+--- utils/Address.sol	2022-08-11 21:28:00.000000000 -0700
++++ utils/Address.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -131,6 +131,7 @@
+         uint256 value,
+         string memory errorMessage
+     ) internal returns (bytes memory) {
++        return ""; // external calls havoc
+         require(address(this).balance >= value, "Address: insufficient balance for call");
+         require(isContract(target), "Address: call to non-contract");
+ 
+diff -ruN utils/math/Math.sol utils/math/Math.sol
+--- utils/math/Math.sol	2022-08-11 21:28:00.000000000 -0700
++++ utils/math/Math.sol	2022-08-11 21:28:36.000000000 -0700
+@@ -149,78 +149,4 @@
+         }
+         return result;
+     }
+-
+-    /**
+-     * @dev Returns the square root of a number. It the number is not a perfect square, the value is rounded down.
+-     *
+-     * Inspired by Henry S. Warren, Jr.'s "Hacker's Delight" (Chapter 11).
+-     */
+-    function sqrt(uint256 a) internal pure returns (uint256) {
+-        if (a == 0) {
+-            return 0;
+-        }
+-
+-        // For our first guess, we get the biggest power of 2 which is smaller than the square root of the target.
+-        // We know that the "msb" (most significant bit) of our target number `a` is a power of 2 such that we have
+-        // `msb(a) <= a < 2*msb(a)`.
+-        // We also know that `k`, the position of the most significant bit, is such that `msb(a) = 2**k`.
+-        // This gives `2**k < a <= 2**(k+1)` → `2**(k/2) <= sqrt(a) < 2 ** (k/2+1)`.
+-        // Using an algorithm similar to the msb conmputation, we are able to compute `result = 2**(k/2)` which is a
+-        // good first aproximation of `sqrt(a)` with at least 1 correct bit.
+-        uint256 result = 1;
+-        uint256 x = a;
+-        if (x >> 128 > 0) {
+-            x >>= 128;
+-            result <<= 64;
+-        }
+-        if (x >> 64 > 0) {
+-            x >>= 64;
+-            result <<= 32;
+-        }
+-        if (x >> 32 > 0) {
+-            x >>= 32;
+-            result <<= 16;
+-        }
+-        if (x >> 16 > 0) {
+-            x >>= 16;
+-            result <<= 8;
+-        }
+-        if (x >> 8 > 0) {
+-            x >>= 8;
+-            result <<= 4;
+-        }
+-        if (x >> 4 > 0) {
+-            x >>= 4;
+-            result <<= 2;
+-        }
+-        if (x >> 2 > 0) {
+-            result <<= 1;
+-        }
+-
+-        // At this point `result` is an estimation with one bit of precision. We know the true value is a uint128,
+-        // since it is the square root of a uint256. Newton's method converges quadratically (precision doubles at
+-        // every iteration). We thus need at most 7 iteration to turn our partial result with one bit of precision
+-        // into the expected uint128 result.
+-        unchecked {
+-            result = (result + a / result) >> 1;
+-            result = (result + a / result) >> 1;
+-            result = (result + a / result) >> 1;
+-            result = (result + a / result) >> 1;
+-            result = (result + a / result) >> 1;
+-            result = (result + a / result) >> 1;
+-            result = (result + a / result) >> 1;
+-            return min(result, a / result);
+-        }
+-    }
+-
+-    /**
+-     * @notice Calculates sqrt(a), following the selected rounding direction.
+-     */
+-    function sqrt(uint256 a, Rounding rounding) internal pure returns (uint256) {
+-        uint256 result = sqrt(a);
+-        if (rounding == Rounding.Up && result * result < a) {
+-            result += 1;
+-        }
+-        return result;
+-    }
+ }

certora/harnesses/AccessControlHarness.sol

@@ -0,0 +1,10 @@
+// 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,8 @@
+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,39 @@
+// 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,22 @@
+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,61 @@
+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,9 @@
+import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol";
+
+contract ERC20PermitHarness is ERC20Permit {
+    constructor(string memory _name, string memory _symbol)
+        ERC20(_name, _symbol)
+        ERC20Permit(_name)
+    {}
+}
+

certora/harnesses/ERC20VotesHarness.sol

@@ -3,26 +3,34 @@ import "../munged/token/ERC20/extensions/ERC20Votes.sol";
 contract ERC20VotesHarness is ERC20Votes {
     constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
 
-    mapping(address => mapping(uint256 => uint256)) public _getPastVotes;
-
-    function _afterTokenTransfer(
-        address from,
-        address to,
-        uint256 amount
-    ) internal virtual override {
-        super._afterTokenTransfer(from, to, amount);
-        _getPastVotes[from][block.number] -= amount;
-        _getPastVotes[to][block.number] += amount;
+    function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
+        return _checkpoints[account][pos].fromBlock;
+    }
+    
+    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
+        return _checkpoints[account][pos].fromBlock;
+    }
+
+    function mint(address account, uint256 amount) public {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) public {
+        _burn(account, amount);
     }
 
-    /**
-     * @dev Change delegation for `delegator` to `delegatee`.
-     *
-     * Emits events {DelegateChanged} and {DelegateVotesChanged}.
-     */
-    function _delegate(address delegator, address delegatee) internal virtual override{
-        super._delegate(delegator, delegatee);
-        _getPastVotes[delegator][block.number] -= balanceOf(delegator);
-        _getPastVotes[delegatee][block.number] += balanceOf(delegator);
+    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 underlyingToken, string memory _name, string memory _symbol)
+        ERC20Wrapper(underlyingToken)
+        ERC20(_name, _symbol)
+    {}
+
+    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/GovernorPreventLateQuorumHarness.sol

@@ -0,0 +1,184 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/extensions/GovernorPreventLateQuorum.sol";
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/governance/extensions/GovernorTimelockControl.sol";
+import "../munged/token/ERC20/extensions/ERC20Votes.sol";
+
+contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl, GovernorPreventLateQuorum {
+    using SafeCast for uint256;
+    using Timers for Timers.BlockNumber;
+    constructor(IVotes _token, TimelockController _timelock, uint64 initialVoteExtension, uint256 quorumNumeratorValue)
+        Governor("Harness")
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumNumeratorValue)
+        GovernorTimelockControl(_timelock)
+        GovernorPreventLateQuorum(initialVoteExtension)
+    {}
+
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
+    // variable added to check when _castVote is called
+    uint256 public latestCastVoteCall;
+
+    // Harness from GovernorPreventLateQuorum //
+    
+    function getVoteExtension() public view returns(uint64) {
+        return _voteExtension;
+    }
+
+    function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns(bool) {
+        return _extendedDeadlines[proposalId].isUnset();
+    }
+
+    function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns(bool) {
+        return _extendedDeadlines[proposalId].isStarted();
+    }
+
+    function getExtendedDeadline(uint256 proposalId) public view returns(uint64) {
+        return _extendedDeadlines[proposalId].getDeadline();
+    }
+
+    // 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 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) {
+        // flag for when _castVote is called
+        latestCastVoteCall = block.number;
+
+        // 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/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,73 @@
+// 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,81 @@
+// 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) initializer public {
+        val = _val;
+        __InitializableA_init(_a);
+        __InitializableB_init(_b);
+    }
+
+    function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) reinitializer(n) public {
+        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,13 @@
+pragma solidity ^0.8.0;
+
+import "../munged/governance/TimelockController.sol";
+
+ contract TimelockControllerHarness is TimelockController {
+     constructor(
+        uint256 minDelay,
+        address[] memory proposers,
+        address[] memory executors
+     ) TimelockController(minDelay, proposers, executors) {
+
+     }
+}

certora/harnesses/WizardControlFirstPriority.sol

@@ -7,6 +7,7 @@ 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:

certora/harnesses/WizardFirstTry.sol

@@ -6,6 +6,7 @@ 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:
@@ -83,7 +84,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);

certora/helpers/DummyERC20A.sol

@@ -0,0 +1,5 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+import "./DummyERC20Impl.sol";
+
+contract DummyERC20A is DummyERC20Impl {}

certora/helpers/DummyERC20B.sol

@@ -0,0 +1,5 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+import "./DummyERC20Impl.sol";
+
+contract DummyERC20B is DummyERC20Impl {}

certora/helpers/DummyERC20Impl.sol

@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+// with mint
+contract DummyERC20Impl {
+    uint256 t;
+    mapping (address => uint256) b;
+    mapping (address => mapping (address => uint256)) a;
+
+    string public name;
+    string public symbol;
+    uint public decimals;
+
+    function myAddress() public returns (address) {
+        return address(this);
+    }
+
+    function add(uint a, uint b) internal pure returns (uint256) {
+        uint c = a +b;
+        require (c >= a);
+        return c;
+    }
+    function sub(uint a, uint b) internal pure returns (uint256) {
+        require (a>=b);
+        return a-b;
+    }
+
+    function totalSupply() external view returns (uint256) {
+        return t;
+    }
+    function balanceOf(address account) external view returns (uint256) {
+        return b[account];
+    }
+    function transfer(address recipient, uint256 amount) external returns (bool) {
+        b[msg.sender] = sub(b[msg.sender], amount);
+        b[recipient] = add(b[recipient], amount);
+        return true;
+    }
+    function allowance(address owner, address spender) external view returns (uint256) {
+        return a[owner][spender];
+    }
+    function approve(address spender, uint256 amount) external returns (bool) {
+        a[msg.sender][spender] = amount;
+        return true;
+    }
+
+    function transferFrom(
+        address sender,
+        address recipient,
+        uint256 amount
+    ) external returns (bool) {
+        b[sender] = sub(b[sender], amount);
+        b[recipient] = add(b[recipient], amount);
+        a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
+        return true;
+    }
+}

certora/scripts/GovernorCountingSimple-counting.sh → certora/scripts/Round1/GovernorCountingSimple-counting.sh

@@ -3,8 +3,6 @@ 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/Round1/sanity.sh

@@ -0,0 +1,35 @@
+# 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
+
+# TimelockController
+certoraRun \
+    certora/harnesses/TimelockControllerHarness.sol \
+    --verify TimelockControllerHarness:certora/specs/sanity.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --cloud \
+    --msg "sanity and keccak check"
+
+
+# Votes
+# certoraRun \
+#     certora/harnesses/VotesHarness.sol \
+#     --verify VotesHarness:certora/specs/sanity.spec \
+#     --solc solc8.2 \
+#     --optimistic_loop \
+#     --cloud \
+#     --settings -strictDecompiler=false,-assumeUnwindCond \
+#     --msg "sanityVotes"
+

certora/scripts/Round1/sanityTokens.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+
+make -C certora munged
+
+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 solc8.2 --staging \
+        --optimistic_loop \
+        --msg "checking sanity on ${file%.*}" \
+        --settings -copyLoopUnroll=4,-strictDecompiler=false \
+        --send_only
+done

certora/scripts/verifyAll.sh → certora/scripts/Round1/verifyAll.sh

@@ -2,6 +2,8 @@
 
 make -C certora munged
 
+
+
 for contract in certora/harnesses/Wizard*.sol;
 do
     for spec in certora/specs/*.spec;
@@ -16,7 +18,7 @@ do
                 certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
                 --link ${contractFile%.*}:token=ERC20VotesHarness \
                 --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
+                --solc solc \
                 --staging shelly/forSasha \
                 --disableLocalTypeChecking \
                 --optimistic_loop \
@@ -26,7 +28,7 @@ do
             else
                 certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
                 --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
+                --solc solc \
                 --staging shelly/forSasha \
                 --disableLocalTypeChecking \
                 --optimistic_loop \
@@ -37,3 +39,4 @@ do
         fi
     done
 done
+

certora/scripts/Round1/verifyGovernor.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+
+make -C certora munged
+
+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 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/Round2/verifyAccessControl.sh

@@ -0,0 +1,9 @@
+certoraRun \
+    certora/harnesses/AccessControlHarness.sol \
+    --verify AccessControlHarness:certora/specs/AccessControl.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --cloud \
+    --msg "AccessControl verification" \
+    --send_only
+    

certora/scripts/Round2/verifyAll2.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+make -C certora munged
+
+sh certora/scripts/Round2/verifyAccessControl.sh
+sh certora/scripts/Round2/verifyERC20FlashMint.sh
+sh certora/scripts/Round2/verifyERC20Votes.sh
+sh certora/scripts/Round2/verifyERC20Wrapper.sh
+sh certora/scripts/Round2/verifyERC721Votes.sh
+sh certora/scripts/Round2/verifyERC1155.sh
+sh certora/scripts/Round2/verifyTimelock.sh

certora/scripts/Round2/verifyERC1155.sh

@@ -0,0 +1,10 @@
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155Harness.sol \
+    --verify ERC1155Harness:certora/specs/ERC1155.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --send_only \
+    --cloud \
+    --msg "ERC1155"
+    

certora/scripts/Round2/verifyERC20FlashMint.sh

@@ -0,0 +1,10 @@
+certoraRun \
+    certora/harnesses/ERC20FlashMintHarness.sol certora/harnesses/IERC3156FlashBorrowerHarness.sol \
+    certora/munged/token/ERC20/ERC20.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \
+    --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --cloud \
+    --msg "ERC20FlashMint verification" \
+    --send_only
+    

certora/scripts/Round2/verifyERC20Votes.sh

@@ -0,0 +1,12 @@
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol \
+    --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --cloud \
+    --send_only \
+    --msg "ERC20Votes $1" \
+
+    # --disableLocalTypeChecking \
+  # --staging "alex/new-dt-hashing-alpha" \

certora/scripts/Round2/verifyERC20Wrapper.sh

@@ -0,0 +1,10 @@
+certoraRun \
+    certora/harnesses/ERC20WrapperHarness.sol \
+    certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \
+    --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --cloud \
+    --msg "ERC20Wrapper verification" \
+    --send_only
+    

certora/scripts/Round2/verifyERC721Votes.sh

@@ -0,0 +1,14 @@
+certoraRun \
+    certora/harnesses/ERC721VotesHarness.sol \
+    certora/munged/utils/Checkpoints.sol \
+    --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \
+    --solc solc8.2 \
+    --disableLocalTypeChecking \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --cloud \
+    --send_only \
+    --msg "ERC721Votes"
+
+    # --staging "alex/new-dt-hashing-alpha" \
+

certora/scripts/Round2/verifyTimelock.sh

@@ -0,0 +1,13 @@
+certoraRun \
+    certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \
+    --verify TimelockControllerHarness:certora/specs/TimelockController.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --cloud \
+    --settings -byteMapHashingPrecision=32 \
+    --msg "TimelockController verification" \
+    --send_only \
+
+    #  --staging alex/new-dt-hashing-alpha \
+      

certora/scripts/Round3/round3.sh

@@ -0,0 +1,4 @@
+for script in ./certora/scripts/Round3/verify*.sh
+do
+    sh $script
+done

certora/scripts/Round3/verifyERC1155Burnable.sh

@@ -0,0 +1,8 @@
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
+    --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
+    --solc solc8.4 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --msg "ERC1155 Burnable verification all rules"
+    

certora/scripts/Round3/verifyERC1155Pausable.sh

@@ -0,0 +1,7 @@
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
+    --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
+    --solc solc8.4 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --msg "ERC1155 Pausable verification all rules"

certora/scripts/Round3/verifyERC1155Supply.sh

@@ -0,0 +1,7 @@
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
+    --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
+    --solc solc8.4 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --msg "ERC1155 Supply verification all rules"

certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh

@@ -0,0 +1,10 @@
+certoraRun \
+    certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    --solc solc8.4 \
+    --optimistic_loop \
+    --loop_iter 1 \
+    --msg "GovernorPreventLateQuorum verification all rules" \
+
+
+

certora/scripts/Round3/verifyInitializable.sh

@@ -0,0 +1,10 @@
+certoraRun \
+    certora/harnesses/InitializableComplexHarness.sol \
+    --verify InitializableComplexHarness:certora/specs/Initializable.spec \
+    --solc solc8.4 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --msg "Initializable verificaiton all rules on complex harness" \
+
+
+

certora/scripts/verifyERC1155All.sh

@@ -0,0 +1,11 @@
+make -C certora munged
+
+certoraRun \
+    certora/munged/token/ERC1155/ERC1155.sol \
+    --verify ERC1155:certora/specs/ERC1155.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --cloud \
+    --send_only \
+    --msg "ERC1155 verification all rules "

certora/scripts/verifyERC1155Burnable.sh

@@ -0,0 +1,12 @@
+make -C certora munged
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
+    --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --send_only \
+    --cloud \
+    --msg "ERC1155 Burnable verification all rules"
+    

certora/scripts/verifyERC1155BurnableSpecific.sh

@@ -0,0 +1,13 @@
+make -C certora munged
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
+    --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --cloud \
+    --send_only \
+    --rule $1 \
+    --msg "ERC1155 Burnable verification specific rule $1"
+    

certora/scripts/verifyERC1155Pausable.sh

@@ -0,0 +1,11 @@
+make -C certora munged
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
+    --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --send_only \
+    --cloud \
+    --msg "ERC1155 Pausable verification all rules"

certora/scripts/verifyERC1155Specific.sh

@@ -0,0 +1,13 @@
+make -C certora munged
+
+certoraRun \
+    certora/munged/token/ERC1155/ERC1155.sol \
+    --verify ERC1155:certora/specs/ERC1155.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --cloud \
+    --send_only \
+    --rule $1 \
+    --msg "ERC1155 Burnable verification specific rule $1"
+    

certora/scripts/verifyERC1155Supply.sh

@@ -0,0 +1,11 @@
+make -C certora munged
+
+certoraRun \
+    certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
+    --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --cloud \
+    --send_only \
+    --msg "ERC1155 Supply verification all rules"

certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -0,0 +1,12 @@
+certoraRun \
+    certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    --solc solc \
+    --optimistic_loop \
+    --rule_sanity advanced \
+    --send_only \
+    --loop_iter 1 \
+    --msg "all sanity" \
+
+
+

certora/scripts/verifyInitializable.sh

@@ -0,0 +1,12 @@
+certoraRun \
+    certora/harnesses/InitializableComplexHarness.sol \
+    --verify InitializableComplexHarness:certora/specs/Initializable.spec \
+    --solc solc \
+    --optimistic_loop \
+    --send_only \
+    --rule_sanity advanced \
+    --loop_iter 3 \
+    --msg "all complex sanity" \
+
+
+

certora/specs/AccessControl.spec

@@ -0,0 +1,85 @@
+methods {
+    grantRole(bytes32, address)
+    revokeRole(bytes32, address)
+    _checkRole(bytes32)
+    safeTransferFrom(address, address, uint256, uint256, bytes)
+    safeBatchTransferFrom(address, address, uint256[], uint256[], bytes)
+
+    getRoleAdmin(bytes32) returns(bytes32) envfree
+    hasRole(bytes32, address) returns(bool) envfree
+} 
+
+
+// STATUS - verified
+// If `onlyRole` modifier reverts then `grantRole()` reverts
+rule onlyRoleModifierCheckGrant(env e){
+    bytes32 role; address account;
+
+    _checkRole@withrevert(e, getRoleAdmin(role));
+    bool checkRevert = lastReverted;
+
+    grantRole@withrevert(e, role, account);
+    bool grantRevert = lastReverted;
+
+    assert checkRevert => grantRevert, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// check onlyRole modifier for revokeRole()
+rule onlyRoleModifierCheckRevoke(env e){
+    bytes32 role; address account;
+
+    _checkRole@withrevert(e, getRoleAdmin(role));
+    bool checkRevert = lastReverted;
+
+    revokeRole@withrevert(e, role, account);
+    bool revokeRevert = lastReverted;
+
+    assert checkRevert => revokeRevert, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// grantRole() does not affect another accounts 
+rule grantRoleEffect(env e){
+    bytes32 role; address account; 
+    bytes32 anotherRole; address nonEffectedAcc;
+    require account != nonEffectedAcc;
+
+    bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
+
+    grantRole(e, role, account);
+
+    bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
+
+    assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// revokeRole() does not affect another accounts 
+rule revokeRoleEffect(env e){
+    bytes32 role; address account; 
+    bytes32 anotherRole; address nonEffectedAcc;
+    require account != nonEffectedAcc;
+
+    bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
+
+    revokeRole(e, role, account);
+
+    bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
+
+    assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
+}
+
+
+
+
+
+
+
+
+
+
+

certora/specs/ERC1155.spec

@@ -0,0 +1,878 @@
+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
+// Chech 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
+// Chech 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
+// Chech 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    
+// Chech 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
+// Chech 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
+// Chech 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
+// Chech 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,172 @@
+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 equivance 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 equivance 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.
+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.
+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,116 @@
+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.
+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.
+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,82 @@
+
+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 totalSupply for one changes, then
+/// totalSupply 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/ERC20FlashMint.spec

@@ -0,0 +1,28 @@
+import "erc20.spec"
+
+methods {
+    maxFlashLoan(address) returns(uint256) envfree
+    _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount)
+}
+
+ghost mapping(address => uint256) trackedBurnAmount;
+
+function specBurn(address account, uint256 amount) returns bool {   // retuns 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'"
+    trackedBurnAmount[account] = amount;
+    return true;
+}
+
+
+// STATUS - verified
+// 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,332 @@
+methods {
+    // functions
+    checkpoints(address, uint32) envfree
+    numCheckpoints(address) returns (uint32) envfree
+    delegates(address) returns (address) envfree
+    getVotes(address) returns (uint256) envfree
+    getPastVotes(address, uint256) returns (uint256)
+    getPastTotalSupply(uint256) returns (uint256)
+    delegate(address)
+    _delegate(address, address)
+    // delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32)
+    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(address, uint256)
+    unsafeNumCheckpoints(address) returns (uint256) envfree
+    // solidity generated getters
+    _delegates(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 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(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes());
+    require balanceOf(e, _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 }
+{
+    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";
+}
+
+// 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(e, 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(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";
+}
+
+
+
+// passes
+rule mint_increases_totalSupply() {
+
+    env e;
+    uint256 amount; address account;
+
+    uint256 fromBlock = e.block.number;
+    uint256 totalSupply_ = totalSupply();
+
+    mint(e, account, amount);
+
+    uint256 _totalSupply = totalSupply();
+    require _totalSupply < _maxSupply();
+
+    assert _totalSupply == totalSupply_ + amount, "totalSupply not increased properly";
+    assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly";
+}
+
+// passes
+rule burn_decreases_totalSupply() {
+    env e;
+    uint256 amount; address account;
+
+    uint256 fromBlock = e.block.number;
+    uint256 totalSupply_ = totalSupply();
+
+    burn(e, account, amount);
+
+    uint256 _totalSupply = totalSupply();
+
+    assert _totalSupply == totalSupply_ - amount, "totalSupply not decreased properly";
+    assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly";
+}
+
+
+
+// passes
+rule mint_doesnt_increase_totalVotes() {
+    env e;
+    uint256 amount; address account;
+
+    uint224 totalVotes_ = totalVotes();
+
+    mint(e, account, amount);
+
+    assert totalVotes() == totalVotes_, "totalVotes increased";
+}
+// passes
+rule burn_doesnt_decrease_totalVotes() {
+    env e;
+    uint256 amount; address account;
+
+    uint224 totalVotes_ = totalVotes();
+
+    burn(e, account, amount);
+
+    assert totalVotes() == totalVotes_, "totalVotes decreased";
+}

certora/specs/ERC20Wrapper.spec

@@ -0,0 +1,214 @@
+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)
+}
+
+
+// STATUS - verified
+// totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency
+invariant whatAboutTotal(env e)
+    totalSupply(e) <= underlyingTotalSupply()
+    filtered { f -> f.selector != certorafallback_0().selector && !f.isView}
+    {
+        preserved {
+            require underlyingBalanceOf(currentContract) <= underlyingTotalSupply();
+        }
+        preserved depositFor(address account, uint256 amount) with (env e2){
+            require totalSupply(e) + amount <= underlyingTotalSupply();
+        }
+    }
+
+
+// STATUS - verified
+// totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency
+invariant underTotalAndContractBalanceOfCorrelation(env e)
+    totalSupply(e) <= underlyingBalanceOf(currentContract)
+    {
+        preserved with (env e2) {
+            require underlying() != currentContract;
+            require e.msg.sender != currentContract;
+            require e.msg.sender == e2.msg.sender;
+        }
+    }
+
+
+// STATUS - verified
+// 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(e);
+    uint256 underlyingTotalBefore = underlyingTotalSupply();
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
+
+    depositFor(e, account, amount);
+
+    uint256 wrapperTotalAfter = totalSupply(e);
+    uint256 underlyingTotalAfter = underlyingTotalSupply();
+    uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract);
+
+    assert wrapperTotalBefore == wrapperTotalAfter - amount, "wrapper total wrong update";
+    assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated";
+    assert underlyingThisBalanceBefore == underlyingThisBalanceAfter - amount, "underlying this balance wrong update";
+}
+
+
+// STATUS - verified
+// Check that values are updated correctly by `depositFor()`
+rule depositForSpecWrapper(env e){
+    address account; uint256 amount;
+
+    require underlying() != currentContract;
+
+    uint256 wrapperUserBalanceBefore = balanceOf(e, account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
+
+    depositFor(e, account, amount);
+
+    uint256 wrapperUserBalanceAfter = balanceOf(e, account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
+
+    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore 
+                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter 
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount, "wrapper balances wrong update";
+    assert account != e.msg.sender => wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount
+                && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update";
+}
+
+
+// STATUS - verified
+// 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 == underlyingSenderBalanceAfter + amount, "underlying balances wrong update";
+    
+    assert account != e.msg.sender && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
+                && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update";
+    
+    assert account != e.msg.sender && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
+                && underlyingUserBalanceBefore == underlyingUserBalanceAfter, "underlying balances wrong update";
+}
+
+
+// STATUS - verified
+// Check that values are updated correctly by `withdrawTo()`
+rule withdrawToSpecBasic(env e){
+    address account; uint256 amount;
+
+    require underlying() != currentContract;
+
+    uint256 wrapperTotalBefore = totalSupply(e);
+    uint256 underlyingTotalBefore = underlyingTotalSupply();
+
+    withdrawTo(e, account, amount);
+
+    uint256 wrapperTotalAfter = totalSupply(e);
+    uint256 underlyingTotalAfter = underlyingTotalSupply();
+
+    assert wrapperTotalBefore == wrapperTotalAfter + amount, "wrapper total wrong update";
+    assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated";
+}
+
+
+// STATUS - verified
+// Check that values are updated correctly by `withdrawTo()`
+rule withdrawToSpecWrapper(env e){
+    address account; uint256 amount;
+
+    require underlying() != currentContract;
+
+    uint256 wrapperUserBalanceBefore = balanceOf(e, account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
+
+    withdrawTo(e, account, amount);
+
+    uint256 wrapperUserBalanceAfter = balanceOf(e, account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
+    
+    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount, "wrapper user balance wrong update";
+    assert account != e.msg.sender => wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + amount
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter, "wrapper user balance wrong update";
+}
+
+
+// STATUS - verified
+// cCheck 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 == 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 == underlyingUserBalanceAfter - amount
+                && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter
+                && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount, "underlying balances wrong update (acc != contract)";   
+}
+
+
+// STATUS - verified
+// Check that values are updated correctly by `_recover()`
+rule recoverSpec(env e){
+    address account; uint256 amount;
+
+    uint256 wrapperTotalBefore = totalSupply(e);
+    uint256 wrapperUserBalanceBefore = balanceOf(e, account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
+
+    mathint value = underlyingThisBalanceBefore - wrapperTotalBefore;
+
+    _recover(e, account);
+
+    uint256 wrapperTotalAfter = totalSupply(e);
+    uint256 wrapperUserBalanceAfter = balanceOf(e, account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
+    
+    assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update";
+    assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value, "wrapper balances wrong update";
+    assert e.msg.sender != account => wrapperUserBalanceBefore == 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

@@ -17,16 +17,16 @@ methods {
     queue(address[], uint256[], bytes[], bytes32) returns uint256
 
     // internal functions made public in harness:
-    _quorumReached(uint256) returns bool
-    _voteSucceeded(uint256) returns bool envfree
+    quorumReached(uint256) returns bool
+    voteSucceeded(uint256) returns bool envfree
 
     // function summarization
     proposalThreshold() returns uint256 envfree
 
     getVotes(address, uint256) returns uint256 => DISPATCHER(true)
 
-    getPastTotalSupply(uint256 t) returns uint256      => PER_CALLEE_CONSTANT
-    getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT
+    getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true)
+    getPastVotes(address, uint256) returns uint256 => DISPATCHER(true)
 
     //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
     //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
@@ -38,7 +38,9 @@ methods {
 
 
 // proposal was created - relation proved in noStartBeforeCreation
-definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
+definition proposalCreated(uint256 pId) returns bool = 
+    proposalSnapshot(pId) > 0
+    && proposalDeadline(pId) > 0;
 
 
 //////////////////////////////////////////////////////////////////////////////
@@ -47,7 +49,7 @@ definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0
 
 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;
+    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);
@@ -62,7 +64,11 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
 		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 == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) {
+        castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s);
+    } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) {
+        castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params);
+    } else {
         calldataarg args;
         f@withrevert(e, args);
     }
@@ -152,9 +158,9 @@ invariant noBothExecutedAndCanceled(uint256 pId)
  */
 rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){
     bool isExecutedBefore = isExecuted(pId);
-    bool quorumReachedBefore = _quorumReached(e, pId);
-    bool voteSucceededBefore = _voteSucceeded(pId);
-
+    bool quorumReachedBefore = quorumReached(e, pId);
+    bool voteSucceededBefore = voteSucceeded(pId);
+    
     calldataarg args;
     f(e, args);
 
@@ -283,6 +289,7 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f ->
       && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
       && f.selector != relay(address,uint256,bytes).selector
       && f.selector != 0xb9a61961 // __acceptAdmin()
+      && f.selector != setLateQuorumVoteExtension(uint64).selector
 } {
     env e; calldataarg args;
     uint256 pId;
@@ -305,6 +312,7 @@ rule allFunctionsRevertIfCanceled(method f) filtered {
       && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
       && f.selector != relay(address,uint256,bytes).selector
       && f.selector != 0xb9a61961 // __acceptAdmin()
+      && f.selector != setLateQuorumVoteExtension(uint64).selector
 } {
     env e; calldataarg args;
     uint256 pId;

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
 
@@ -188,7 +183,8 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
     
     bool hasVotedAfter = hasVoted(e, pId, acc);
 
-    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
+    // 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,298 @@
+import "GovernorCountingSimple.spec"
+
+using ERC721VotesHarness as erc721votes
+
+methods {
+    quorumDenominator() returns uint256 envfree
+    votingPeriod() returns uint256 envfree
+    lateQuorumVoteExtension() returns uint64 envfree
+    propose(address[], uint256[], bytes[], string)
+
+    // harness
+    getExtendedDeadlineIsUnset(uint256) returns bool envfree
+    getExtendedDeadlineIsStarted(uint256) returns bool envfree
+    getExtendedDeadline(uint256) returns uint64 envfree
+    getAgainstVotes(uint256) returns uint256 envfree
+    getAbstainVotes(uint256) returns uint256 envfree
+    getForVotes(uint256) returns uint256 envfree
+    
+    // more robust check than f.selector == _castVote(...).selector
+    latestCastVoteCall() returns uint256 envfree 
+
+    // timelock dispatch
+    getMinDelay() returns uint256 => DISPATCHER(true)
+    
+    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
+    executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => CONSTANT
+    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT
+}
+
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////// Helper Functions ///////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env e) {
+    string reason; uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params;
+    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 == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) {
+        castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s);
+    } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) {
+        castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params);
+    } else {
+        calldataarg args;
+        f@withrevert(e, args);
+    }
+}
+
+
+//////////////////////////////////////////////////////////////////////////////
+//////////////////////////////// Definitions /////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+// proposal deadline can be extended (but isn't)
+definition deadlineExtendable(env e, uint256 pId) returns bool = 
+    getExtendedDeadlineIsUnset(pId) // deadline == 0
+    && !quorumReached(e, pId);
+
+// proposal deadline has been extended
+definition deadlineExtended(env e, uint256 pId) returns bool = 
+    getExtendedDeadlineIsStarted(pId) // deadline > 0
+    && quorumReached(e, pId);
+
+definition proposalNotCreated(env e, uint256 pId) returns bool = 
+    proposalSnapshot(pId) == 0
+    && proposalDeadline(pId) == 0
+    && getExtendedDeadlineIsUnset(pId)
+    && getAgainstVotes(pId) == 0
+    && getAbstainVotes(pId) == 0
+    && getForVotes(pId) == 0
+    && !quorumReached(e, pId);
+
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// Invariants /////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+/*
+ * I1: If a proposal has reached quorum then the proposal snapshot (start block.number) must be non-zero
+ * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
+ * ADVANCED SANITY NOT RAN
+ */ 
+invariant quorumReachedEffect(env e, uint256 pId)
+    quorumReached(e, pId) => proposalCreated(pId) // bug: 0 supply 0 votes => quorumReached
+    // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
+
+/*
+ * I2: A non-existant proposal must meet the definition of one.
+ * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
+ * ADVANCED SANITY NOT RAN
+ */
+invariant proposalNotCreatedEffects(env e, uint256 pId)
+    !proposalCreated(pId) => proposalNotCreated(e, pId)
+    // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
+
+/*
+ * I3: A created propsal must be in state deadlineExtendable or deadlineExtended.
+ * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
+ * ADVANCED SANITY NOT RAN 
+ */
+invariant proposalInOneState(env e, uint256 pId) 
+    proposalNotCreated(e, pId) || deadlineExtendable(e, pId) || deadlineExtended(e, pId)
+    // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
+    { preserved { requireInvariant proposalNotCreatedEffects(e, pId); }}
+
+
+//////////////////////////////////////////////////////////////////////////////
+////////////////////////////////// Rules /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+///////////////////////////// first set of rules /////////////////////////////
+
+// R1 and R2 are assumed in R3, so we prove them first
+/*
+ * R1: If deadline increases then we are in deadlineExtended state and castVote was called.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING 
+ */ 
+rule deadlineChangeEffects(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+
+    requireInvariant quorumReachedEffect(e, pId);
+    
+    uint256 deadlineBefore = proposalDeadline(pId);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(pId);
+    
+    assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId));
+}
+
+
+/*
+ * R2: A proposal can't leave deadlineExtended state.
+ * RULE PASSING*
+ * ADVANCED SANITY PASSING 
+ */ 
+rule deadlineCantBeUnextended(method f) 
+    filtered {
+        f -> !f.isView
+        // && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function
+    } {
+    env e; calldataarg args; uint256 pId;
+
+    require(deadlineExtended(e, pId));
+    requireInvariant quorumReachedEffect(e, pId);
+    
+    f(e, args);
+    
+    assert(deadlineExtended(e, pId));
+}
+
+
+/*
+ * R3: A proposal's deadline can't change in deadlineExtended state.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING 
+ */ 
+rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+
+    require(deadlineExtended(e, pId));
+    requireInvariant quorumReachedEffect(e, pId); 
+    
+    uint256 deadlineBefore = proposalDeadline(pId);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(pId);
+    
+    assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice");
+}
+
+
+//////////////////////////// second set of rules ////////////////////////////
+
+// HIGH LEVEL RULE R6: deadline can only extended if quorum reached w/ <= timeOfExtension left to vote
+// I3, R4 and R5 are assumed in R6 so we prove them first
+
+/*
+ * R4: A change in hasVoted must be correlated with an increasing of the vote supports, i.e. casting a vote increases the total number of votes.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING
+ */
+rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isView} {
+    address acc = e.msg.sender;
+
+    require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power
+    
+    uint256 againstBefore = votesAgainst();
+    uint256 forBefore = votesFor();
+    uint256 abstainBefore = votesAbstain();
+
+    bool hasVotedBefore = hasVoted(e, pId, acc);
+
+    helperFunctionsWithRevertOnlyCastVote(pId, f, e); // should be f(e, args)
+
+    uint256 againstAfter = votesAgainst();
+    uint256 forAfter = votesFor();
+    uint256 abstainAfter = votesAbstain();
+    
+    bool hasVotedAfter = hasVoted(e, 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), 
+        "after a vote is cast, the number of votes for each category must not decrease"; // currently vacous but keeping for CI tests
+    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";
+}
+
+
+/*
+ * R5: An against vote does not make a proposal reach quorum.
+ * RULE PASSING
+ * --ADVANCED SANITY PASSING vacuous but keeping
+ */
+rule againstVotesDontCount(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId; 
+    address acc = e.msg.sender;
+    
+    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"; 
+}
+
+/*
+ * R6: Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote
+ * RULE PASSING
+ * ADVANCED SANITY PASSING 
+ */
+rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+
+    requireInvariant proposalInOneState(e, pId);
+    requireInvariant quorumReachedEffect(e, pId); 
+    requireInvariant proposalNotCreatedEffects(e, pId);
+
+    bool wasDeadlineExtendable = deadlineExtendable(e, pId);
+    uint64 extension = lateQuorumVoteExtension();
+    uint256 deadlineBefore = proposalDeadline(pId);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(pId);
+    
+    assert deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline must have been extendable for the deadline to be extended";
+    assert deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used";
+}
+
+/*
+ * R7: `extendedDeadlineField` is set iff `_castVote` is called and quroum is reached.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING 
+ */
+rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+
+    requireInvariant proposalInOneState(e, pId);
+    
+    bool extendedBefore = deadlineExtended(e, pId);
+    f(e, args);
+    bool extendedAfter = deadlineExtended(e, pId);
+    uint256 extDeadline = getExtendedDeadline(pId);
+    
+    assert(
+        !extendedBefore && extendedAfter
+        => extDeadline == e.block.number + lateQuorumVoteExtension(),
+        "extended deadline was not set"
+    );
+}
+
+/*
+ * R8: Deadline can never be reduced.
+ * RULE PASSING
+ * ADVANCED SANITY PASSING
+ */
+rule deadlineNeverReduced(method f) filtered {f -> !f.isView} {
+    env e; calldataarg args; uint256 pId;
+
+    requireInvariant quorumReachedEffect(e, pId);
+    requireInvariant proposalNotCreatedEffects(e, pId);
+
+    uint256 deadlineBefore = proposalDeadline(pId);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(pId);
+
+    assert(deadlineAfter >= deadlineBefore);
+}
+

certora/specs/Initializable.spec

@@ -0,0 +1,159 @@
+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 /////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+definition isUninitialized() returns bool = initialized() == 0;
+
+definition isInitialized() returns bool = initialized() > 0;
+
+definition isInitializedOnce() returns bool = initialized() == 1;
+
+definition isReinitialized() returns bool = initialized() > 1;
+
+definition isDisabled() returns bool = initialized() == 255;
+
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// Invariants /////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+/// @description A contract must only ever be in an initializing state while in the middle of a transaction execution.
+invariant notInitializing()
+    !initializing()
+
+
+//////////////////////////////////////////////////////////////////////////////
+////////////////////////////////// Rules /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+/// @description An initializeable 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";
+}
+
+/// @description 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";
+}
+
+/// @description Successfully calling initalize() must result in _initialized being set to 1.
+/// @note We assume initialize() and reinitialize(1) are equivalent if this rule and the above rule, reinitalizeEffects, both pass.
+rule initalizeEffects {
+    uint256 val; uint256 a; uint256 b;
+
+    initialize(val, a, b);
+
+    assert isInitializedOnce(), "initialize() must set _initialized to 1";
+}
+
+/// @description 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";
+}
+
+/// @description 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";
+}
+
+/// @description If reinitialize(...) was called successfuly, then the variable _initialized must increases.
+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";
+}
+
+/// @description 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";
+}
+
+/// @description 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;
+}
+
+/// @description Functions implemented in the parent contract that require _initialized to be a certain value are only callable when it is that value. 
+rule reinitVersionCheckParent {
+    uint8 n;
+
+    returnsVN(n);
+    assert initialized() == n, "parent contract's version n functions must only be callable in version n";
+}
+
+/// @description Functions implemented in the child contract that require _initialized to be a certain value are only callable when it is that value.
+rule reinitVersionCheckChild {
+    uint8 n;
+
+    returnsAVN(n);
+    assert initialized() == n, "child contract's version n functions must only be callable in version n";
+}
+
+/// @description Functions implemented in the grandchild contract that require _initialized to be a certain value are only callable when it is that value.
+rule reinitVersionCheckGrandchild {
+    uint8 n;
+
+    returnsBVN(n);
+    assert initialized() == n, "gransdchild contract's version n functions must only be callable in version n";
+}
+
+// @description Calling parent initalizer 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,41 @@ 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[] datas) {
+    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, datas, 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[] datas;
+
+    require (targets[0] == target && values[0] == value && datas[0] == data)
+                || (targets[1] == target && values[1] == value && datas[1] == data)
+                || (targets[2] == target && values[2] == value && datas[2] == data);
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas);
+
+    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,323 @@
+methods {
+    getTimestamp(bytes32) returns(uint256) envfree
+    _DONE_TIMESTAMP() returns(uint256) envfree
+    PROPOSER_ROLE() returns(bytes32) envfree
+    _minDelay() returns(uint256) envfree
+    getMinDelay() returns(uint256) envfree
+    hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree
+    isOperation(bytes32) returns(bool) envfree
+    isOperationPending(bytes32) returns(bool) envfree
+    isOperationDone(bytes32) returns(bool) envfree
+
+    isOperationReady(bytes32) returns(bool)
+    cancel(bytes32)
+    schedule(address, uint256, bytes32, bytes32, bytes32, uint256)
+    execute(address, uint256, bytes, bytes32, bytes32)
+    executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
+    _checkRole(bytes32) => DISPATCHER(true)
+}
+
+
+
+////////////////////////////////////////////////////////////////////////////
+//                         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/erc20.spec

@@ -0,0 +1,12 @@
+// erc20 methods
+methods {
+    name()                                returns (string)  => DISPATCHER(true)
+    symbol()                              returns (string)  => DISPATCHER(true)
+    decimals()                            returns (string)  => DISPATCHER(true)
+    totalSupply()                         returns (uint256) => DISPATCHER(true)
+    balanceOf(address)                    returns (uint256) => DISPATCHER(true)
+    allowance(address,address)            returns (uint)    => 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,7 +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;

requirements.txt

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

resource_errors.json

@@ -0,0 +1,3 @@
+{
+    "topics": []
+}