moved contract modifications into munged directory

certora/munged/access/AccessControl.sol

@@ -0,0 +1,223 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (access/AccessControl.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IAccessControl.sol";
+import "../utils/Context.sol";
+import "../utils/Strings.sol";
+import "../utils/introspection/ERC165.sol";
+
+/**
+ * @dev Contract module that allows children to implement role-based access
+ * control mechanisms. This is a lightweight version that doesn't allow enumerating role
+ * members except through off-chain means by accessing the contract event logs. Some
+ * applications may benefit from on-chain enumerability, for those cases see
+ * {AccessControlEnumerable}.
+ *
+ * Roles are referred to by their `bytes32` identifier. These should be exposed
+ * in the external API and be unique. The best way to achieve this is by
+ * using `public constant` hash digests:
+ *
+ * ```
+ * bytes32 public constant MY_ROLE = keccak256("MY_ROLE");
+ * ```
+ *
+ * Roles can be used to represent a set of permissions. To restrict access to a
+ * function call, use {hasRole}:
+ *
+ * ```
+ * function foo() public {
+ *     require(hasRole(MY_ROLE, msg.sender));
+ *     ...
+ * }
+ * ```
+ *
+ * Roles can be granted and revoked dynamically via the {grantRole} and
+ * {revokeRole} functions. Each role has an associated admin role, and only
+ * accounts that have a role's admin role can call {grantRole} and {revokeRole}.
+ *
+ * By default, the admin role for all roles is `DEFAULT_ADMIN_ROLE`, which means
+ * that only accounts with this role will be able to grant or revoke other
+ * roles. More complex role relationships can be created by using
+ * {_setRoleAdmin}.
+ *
+ * WARNING: The `DEFAULT_ADMIN_ROLE` is also its own admin: it has permission to
+ * grant and revoke this role. Extra precautions should be taken to secure
+ * accounts that have been granted it.
+ */
+abstract contract AccessControl is Context, IAccessControl, ERC165 {
+    struct RoleData {
+        mapping(address => bool) members;
+        bytes32 adminRole;
+    }
+
+    mapping(bytes32 => RoleData) private _roles;
+
+    bytes32 public constant DEFAULT_ADMIN_ROLE = 0x00;
+
+    /**
+     * @dev Modifier that checks that an account has a specific role. Reverts
+     * with a standardized message including the required role.
+     *
+     * The format of the revert reason is given by the following regular expression:
+     *
+     *  /^AccessControl: account (0x[0-9a-f]{40}) is missing role (0x[0-9a-f]{64})$/
+     *
+     * _Available since v4.1._
+     */
+    modifier onlyRole(bytes32 role) {
+        _checkRole(role, _msgSender());
+        _;
+    }
+
+    /**
+     * @dev See {IERC165-supportsInterface}.
+     */
+    function supportsInterface(bytes4 interfaceId) public view virtual override returns (bool) {
+        return interfaceId == type(IAccessControl).interfaceId || super.supportsInterface(interfaceId);
+    }
+
+    /**
+     * @dev Returns `true` if `account` has been granted `role`.
+     */
+    function hasRole(bytes32 role, address account) public view override returns (bool) {
+        return _roles[role].members[account];
+    }
+
+    /**
+     * @dev Revert with a standard message if `account` is missing `role`.
+     *
+     * The format of the revert reason is given by the following regular expression:
+     *
+     *  /^AccessControl: account (0x[0-9a-f]{40}) is missing role (0x[0-9a-f]{64})$/
+     */
+    function _checkRole(bytes32 role, address account) internal view {
+        if (!hasRole(role, account)) {
+            revert(
+                string(
+                    abi.encodePacked(
+                        "AccessControl: account ",
+                        Strings.toHexString(uint160(account), 20),
+                        " is missing role ",
+                        Strings.toHexString(uint256(role), 32)
+                    )
+                )
+            );
+        }
+    }
+
+    /**
+     * @dev Returns the admin role that controls `role`. See {grantRole} and
+     * {revokeRole}.
+     *
+     * To change a role's admin, use {_setRoleAdmin}.
+     */
+    function getRoleAdmin(bytes32 role) public view override returns (bytes32) {
+        return _roles[role].adminRole;
+    }
+
+    /**
+     * @dev Grants `role` to `account`.
+     *
+     * If `account` had not been already granted `role`, emits a {RoleGranted}
+     * event.
+     *
+     * Requirements:
+     *
+     * - the caller must have ``role``'s admin role.
+     */
+    function grantRole(bytes32 role, address account) public virtual override onlyRole(getRoleAdmin(role)) {
+        _grantRole(role, account);
+    }
+
+    /**
+     * @dev Revokes `role` from `account`.
+     *
+     * If `account` had been granted `role`, emits a {RoleRevoked} event.
+     *
+     * Requirements:
+     *
+     * - the caller must have ``role``'s admin role.
+     */
+    function revokeRole(bytes32 role, address account) public virtual override onlyRole(getRoleAdmin(role)) {
+        _revokeRole(role, account);
+    }
+
+    /**
+     * @dev Revokes `role` from the calling account.
+     *
+     * Roles are often managed via {grantRole} and {revokeRole}: this function's
+     * purpose is to provide a mechanism for accounts to lose their privileges
+     * if they are compromised (such as when a trusted device is misplaced).
+     *
+     * If the calling account had been revoked `role`, emits a {RoleRevoked}
+     * event.
+     *
+     * Requirements:
+     *
+     * - the caller must be `account`.
+     */
+    function renounceRole(bytes32 role, address account) public virtual override {
+        require(account == _msgSender(), "AccessControl: can only renounce roles for self");
+
+        _revokeRole(role, account);
+    }
+
+    /**
+     * @dev Grants `role` to `account`.
+     *
+     * If `account` had not been already granted `role`, emits a {RoleGranted}
+     * event. Note that unlike {grantRole}, this function doesn't perform any
+     * checks on the calling account.
+     *
+     * [WARNING]
+     * ====
+     * This function should only be called from the constructor when setting
+     * up the initial roles for the system.
+     *
+     * Using this function in any other way is effectively circumventing the admin
+     * system imposed by {AccessControl}.
+     * ====
+     *
+     * NOTE: This function is deprecated in favor of {_grantRole}.
+     */
+    function _setupRole(bytes32 role, address account) internal virtual {
+        _grantRole(role, account);
+    }
+
+    /**
+     * @dev Sets `adminRole` as ``role``'s admin role.
+     *
+     * Emits a {RoleAdminChanged} event.
+     */
+    function _setRoleAdmin(bytes32 role, bytes32 adminRole) internal virtual {
+        bytes32 previousAdminRole = getRoleAdmin(role);
+        _roles[role].adminRole = adminRole;
+        emit RoleAdminChanged(role, previousAdminRole, adminRole);
+    }
+
+    /**
+     * @dev Grants `role` to `account`.
+     *
+     * Internal function without access restriction.
+     */
+    function _grantRole(bytes32 role, address account) internal virtual {
+        if (!hasRole(role, account)) {
+            _roles[role].members[account] = true;
+            emit RoleGranted(role, account, _msgSender());
+        }
+    }
+
+    /**
+     * @dev Revokes `role` from `account`.
+     *
+     * Internal function without access restriction.
+     */
+    function _revokeRole(bytes32 role, address account) internal virtual {
+        if (hasRole(role, account)) {
+            _roles[role].members[account] = false;
+            emit RoleRevoked(role, account, _msgSender());
+        }
+    }
+}

certora/munged/access/AccessControlEnumerable.sol

@@ -0,0 +1,64 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (access/AccessControlEnumerable.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IAccessControlEnumerable.sol";
+import "./AccessControl.sol";
+import "../utils/structs/EnumerableSet.sol";
+
+/**
+ * @dev Extension of {AccessControl} that allows enumerating the members of each role.
+ */
+abstract contract AccessControlEnumerable is IAccessControlEnumerable, AccessControl {
+    using EnumerableSet for EnumerableSet.AddressSet;
+
+    mapping(bytes32 => EnumerableSet.AddressSet) private _roleMembers;
+
+    /**
+     * @dev See {IERC165-supportsInterface}.
+     */
+    function supportsInterface(bytes4 interfaceId) public view virtual override returns (bool) {
+        return interfaceId == type(IAccessControlEnumerable).interfaceId || super.supportsInterface(interfaceId);
+    }
+
+    /**
+     * @dev Returns one of the accounts that have `role`. `index` must be a
+     * value between 0 and {getRoleMemberCount}, non-inclusive.
+     *
+     * Role bearers are not sorted in any particular way, and their ordering may
+     * change at any point.
+     *
+     * WARNING: When using {getRoleMember} and {getRoleMemberCount}, make sure
+     * you perform all queries on the same block. See the following
+     * https://forum.openzeppelin.com/t/iterating-over-elements-on-enumerableset-in-openzeppelin-contracts/2296[forum post]
+     * for more information.
+     */
+    function getRoleMember(bytes32 role, uint256 index) public view override returns (address) {
+        return _roleMembers[role].at(index);
+    }
+
+    /**
+     * @dev Returns the number of accounts that have `role`. Can be used
+     * together with {getRoleMember} to enumerate all bearers of a role.
+     */
+    function getRoleMemberCount(bytes32 role) public view override returns (uint256) {
+        return _roleMembers[role].length();
+    }
+
+    /**
+     * @dev Overload {_grantRole} to track enumerable memberships
+     */
+    function _grantRole(bytes32 role, address account) internal virtual override {
+        super._grantRole(role, account);
+        _roleMembers[role].add(account);
+    }
+
+    /**
+     * @dev Overload {_revokeRole} to track enumerable memberships
+     */
+    function _revokeRole(bytes32 role, address account) internal virtual override {
+        super._revokeRole(role, account);
+        _roleMembers[role].remove(account);
+    }
+}

certora/munged/access/IAccessControl.sol

@@ -0,0 +1,88 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (access/IAccessControl.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev External interface of AccessControl declared to support ERC165 detection.
+ */
+interface IAccessControl {
+    /**
+     * @dev Emitted when `newAdminRole` is set as ``role``'s admin role, replacing `previousAdminRole`
+     *
+     * `DEFAULT_ADMIN_ROLE` is the starting admin for all roles, despite
+     * {RoleAdminChanged} not being emitted signaling this.
+     *
+     * _Available since v3.1._
+     */
+    event RoleAdminChanged(bytes32 indexed role, bytes32 indexed previousAdminRole, bytes32 indexed newAdminRole);
+
+    /**
+     * @dev Emitted when `account` is granted `role`.
+     *
+     * `sender` is the account that originated the contract call, an admin role
+     * bearer except when using {AccessControl-_setupRole}.
+     */
+    event RoleGranted(bytes32 indexed role, address indexed account, address indexed sender);
+
+    /**
+     * @dev Emitted when `account` is revoked `role`.
+     *
+     * `sender` is the account that originated the contract call:
+     *   - if using `revokeRole`, it is the admin role bearer
+     *   - if using `renounceRole`, it is the role bearer (i.e. `account`)
+     */
+    event RoleRevoked(bytes32 indexed role, address indexed account, address indexed sender);
+
+    /**
+     * @dev Returns `true` if `account` has been granted `role`.
+     */
+    function hasRole(bytes32 role, address account) external view returns (bool);
+
+    /**
+     * @dev Returns the admin role that controls `role`. See {grantRole} and
+     * {revokeRole}.
+     *
+     * To change a role's admin, use {AccessControl-_setRoleAdmin}.
+     */
+    function getRoleAdmin(bytes32 role) external view returns (bytes32);
+
+    /**
+     * @dev Grants `role` to `account`.
+     *
+     * If `account` had not been already granted `role`, emits a {RoleGranted}
+     * event.
+     *
+     * Requirements:
+     *
+     * - the caller must have ``role``'s admin role.
+     */
+    function grantRole(bytes32 role, address account) external;
+
+    /**
+     * @dev Revokes `role` from `account`.
+     *
+     * If `account` had been granted `role`, emits a {RoleRevoked} event.
+     *
+     * Requirements:
+     *
+     * - the caller must have ``role``'s admin role.
+     */
+    function revokeRole(bytes32 role, address account) external;
+
+    /**
+     * @dev Revokes `role` from the calling account.
+     *
+     * Roles are often managed via {grantRole} and {revokeRole}: this function's
+     * purpose is to provide a mechanism for accounts to lose their privileges
+     * if they are compromised (such as when a trusted device is misplaced).
+     *
+     * If the calling account had been granted `role`, emits a {RoleRevoked}
+     * event.
+     *
+     * Requirements:
+     *
+     * - the caller must be `account`.
+     */
+    function renounceRole(bytes32 role, address account) external;
+}

certora/munged/access/IAccessControlEnumerable.sol

@@ -0,0 +1,31 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (access/IAccessControlEnumerable.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IAccessControl.sol";
+
+/**
+ * @dev External interface of AccessControlEnumerable declared to support ERC165 detection.
+ */
+interface IAccessControlEnumerable is IAccessControl {
+    /**
+     * @dev Returns one of the accounts that have `role`. `index` must be a
+     * value between 0 and {getRoleMemberCount}, non-inclusive.
+     *
+     * Role bearers are not sorted in any particular way, and their ordering may
+     * change at any point.
+     *
+     * WARNING: When using {getRoleMember} and {getRoleMemberCount}, make sure
+     * you perform all queries on the same block. See the following
+     * https://forum.openzeppelin.com/t/iterating-over-elements-on-enumerableset-in-openzeppelin-contracts/2296[forum post]
+     * for more information.
+     */
+    function getRoleMember(bytes32 role, uint256 index) external view returns (address);
+
+    /**
+     * @dev Returns the number of accounts that have `role`. Can be used
+     * together with {getRoleMember} to enumerate all bearers of a role.
+     */
+    function getRoleMemberCount(bytes32 role) external view returns (uint256);
+}

certora/munged/access/Ownable.sol

@@ -0,0 +1,76 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (access/Ownable.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/Context.sol";
+
+/**
+ * @dev Contract module which provides a basic access control mechanism, where
+ * there is an account (an owner) that can be granted exclusive access to
+ * specific functions.
+ *
+ * By default, the owner account will be the one that deploys the contract. This
+ * can later be changed with {transferOwnership}.
+ *
+ * This module is used through inheritance. It will make available the modifier
+ * `onlyOwner`, which can be applied to your functions to restrict their use to
+ * the owner.
+ */
+abstract contract Ownable is Context {
+    address private _owner;
+
+    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);
+
+    /**
+     * @dev Initializes the contract setting the deployer as the initial owner.
+     */
+    constructor() {
+        _transferOwnership(_msgSender());
+    }
+
+    /**
+     * @dev Returns the address of the current owner.
+     */
+    function owner() public view virtual returns (address) {
+        return _owner;
+    }
+
+    /**
+     * @dev Throws if called by any account other than the owner.
+     */
+    modifier onlyOwner() {
+        require(owner() == _msgSender(), "Ownable: caller is not the owner");
+        _;
+    }
+
+    /**
+     * @dev Leaves the contract without owner. It will not be possible to call
+     * `onlyOwner` functions anymore. Can only be called by the current owner.
+     *
+     * NOTE: Renouncing ownership will leave the contract without an owner,
+     * thereby removing any functionality that is only available to the owner.
+     */
+    function renounceOwnership() public virtual onlyOwner {
+        _transferOwnership(address(0));
+    }
+
+    /**
+     * @dev Transfers ownership of the contract to a new account (`newOwner`).
+     * Can only be called by the current owner.
+     */
+    function transferOwnership(address newOwner) public virtual onlyOwner {
+        require(newOwner != address(0), "Ownable: new owner is the zero address");
+        _transferOwnership(newOwner);
+    }
+
+    /**
+     * @dev Transfers ownership of the contract to a new account (`newOwner`).
+     * Internal function without access restriction.
+     */
+    function _transferOwnership(address newOwner) internal virtual {
+        address oldOwner = _owner;
+        _owner = newOwner;
+        emit OwnershipTransferred(oldOwner, newOwner);
+    }
+}

certora/munged/access/README.adoc

@@ -0,0 +1,21 @@
+= Access Control
+
+[.readme-notice]
+NOTE: This document is better viewed at https://docs.openzeppelin.com/contracts/api/access
+
+This directory provides ways to restrict who can access the functions of a contract or when they can do it.
+
+- {AccessControl} provides a general role based access control mechanism. Multiple hierarchical roles can be created and assigned each to multiple accounts.
+- {Ownable} is a simpler mechanism with a single owner "role" that can be assigned to a single account. This simpler mechanism can be useful for quick tests but projects with production concerns are likely to outgrow it.
+
+== Authorization
+
+{{Ownable}}
+
+{{IAccessControl}}
+
+{{AccessControl}}
+
+{{IAccessControlEnumerable}}
+
+{{AccessControlEnumerable}}

certora/munged/finance/PaymentSplitter.sol

@@ -0,0 +1,189 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (finance/PaymentSplitter.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/utils/SafeERC20.sol";
+import "../utils/Address.sol";
+import "../utils/Context.sol";
+
+/**
+ * @title PaymentSplitter
+ * @dev This contract allows to split Ether payments among a group of accounts. The sender does not need to be aware
+ * that the Ether will be split in this way, since it is handled transparently by the contract.
+ *
+ * The split can be in equal parts or in any other arbitrary proportion. The way this is specified is by assigning each
+ * account to a number of shares. Of all the Ether that this contract receives, each account will then be able to claim
+ * an amount proportional to the percentage of total shares they were assigned.
+ *
+ * `PaymentSplitter` follows a _pull payment_ model. This means that payments are not automatically forwarded to the
+ * accounts but kept in this contract, and the actual transfer is triggered as a separate step by calling the {release}
+ * function.
+ *
+ * NOTE: This contract assumes that ERC20 tokens will behave similarly to native tokens (Ether). Rebasing tokens, and
+ * tokens that apply fees during transfers, are likely to not be supported as expected. If in doubt, we encourage you
+ * to run tests before sending real value to this contract.
+ */
+contract PaymentSplitter is Context {
+    event PayeeAdded(address account, uint256 shares);
+    event PaymentReleased(address to, uint256 amount);
+    event ERC20PaymentReleased(IERC20 indexed token, address to, uint256 amount);
+    event PaymentReceived(address from, uint256 amount);
+
+    uint256 private _totalShares;
+    uint256 private _totalReleased;
+
+    mapping(address => uint256) private _shares;
+    mapping(address => uint256) private _released;
+    address[] private _payees;
+
+    mapping(IERC20 => uint256) private _erc20TotalReleased;
+    mapping(IERC20 => mapping(address => uint256)) private _erc20Released;
+
+    /**
+     * @dev Creates an instance of `PaymentSplitter` where each account in `payees` is assigned the number of shares at
+     * the matching position in the `shares` array.
+     *
+     * All addresses in `payees` must be non-zero. Both arrays must have the same non-zero length, and there must be no
+     * duplicates in `payees`.
+     */
+    constructor(address[] memory payees, uint256[] memory shares_) payable {
+        require(payees.length == shares_.length, "PaymentSplitter: payees and shares length mismatch");
+        require(payees.length > 0, "PaymentSplitter: no payees");
+
+        for (uint256 i = 0; i < payees.length; i++) {
+            _addPayee(payees[i], shares_[i]);
+        }
+    }
+
+    /**
+     * @dev The Ether received will be logged with {PaymentReceived} events. Note that these events are not fully
+     * reliable: it's possible for a contract to receive Ether without triggering this function. This only affects the
+     * reliability of the events, and not the actual splitting of Ether.
+     *
+     * To learn more about this see the Solidity documentation for
+     * https://solidity.readthedocs.io/en/latest/contracts.html#fallback-function[fallback
+     * functions].
+     */
+    receive() external payable virtual {
+        emit PaymentReceived(_msgSender(), msg.value);
+    }
+
+    /**
+     * @dev Getter for the total shares held by payees.
+     */
+    function totalShares() public view returns (uint256) {
+        return _totalShares;
+    }
+
+    /**
+     * @dev Getter for the total amount of Ether already released.
+     */
+    function totalReleased() public view returns (uint256) {
+        return _totalReleased;
+    }
+
+    /**
+     * @dev Getter for the total amount of `token` already released. `token` should be the address of an IERC20
+     * contract.
+     */
+    function totalReleased(IERC20 token) public view returns (uint256) {
+        return _erc20TotalReleased[token];
+    }
+
+    /**
+     * @dev Getter for the amount of shares held by an account.
+     */
+    function shares(address account) public view returns (uint256) {
+        return _shares[account];
+    }
+
+    /**
+     * @dev Getter for the amount of Ether already released to a payee.
+     */
+    function released(address account) public view returns (uint256) {
+        return _released[account];
+    }
+
+    /**
+     * @dev Getter for the amount of `token` tokens already released to a payee. `token` should be the address of an
+     * IERC20 contract.
+     */
+    function released(IERC20 token, address account) public view returns (uint256) {
+        return _erc20Released[token][account];
+    }
+
+    /**
+     * @dev Getter for the address of the payee number `index`.
+     */
+    function payee(uint256 index) public view returns (address) {
+        return _payees[index];
+    }
+
+    /**
+     * @dev Triggers a transfer to `account` of the amount of Ether they are owed, according to their percentage of the
+     * total shares and their previous withdrawals.
+     */
+    function release(address payable account) public virtual {
+        require(_shares[account] > 0, "PaymentSplitter: account has no shares");
+
+        uint256 totalReceived = address(this).balance + totalReleased();
+        uint256 payment = _pendingPayment(account, totalReceived, released(account));
+
+        require(payment != 0, "PaymentSplitter: account is not due payment");
+
+        _released[account] += payment;
+        _totalReleased += payment;
+
+        Address.sendValue(account, payment);
+        emit PaymentReleased(account, payment);
+    }
+
+    /**
+     * @dev Triggers a transfer to `account` of the amount of `token` tokens they are owed, according to their
+     * percentage of the total shares and their previous withdrawals. `token` must be the address of an IERC20
+     * contract.
+     */
+    function release(IERC20 token, address account) public virtual {
+        require(_shares[account] > 0, "PaymentSplitter: account has no shares");
+
+        uint256 totalReceived = token.balanceOf(address(this)) + totalReleased(token);
+        uint256 payment = _pendingPayment(account, totalReceived, released(token, account));
+
+        require(payment != 0, "PaymentSplitter: account is not due payment");
+
+        _erc20Released[token][account] += payment;
+        _erc20TotalReleased[token] += payment;
+
+        SafeERC20.safeTransfer(token, account, payment);
+        emit ERC20PaymentReleased(token, account, payment);
+    }
+
+    /**
+     * @dev internal logic for computing the pending payment of an `account` given the token historical balances and
+     * already released amounts.
+     */
+    function _pendingPayment(
+        address account,
+        uint256 totalReceived,
+        uint256 alreadyReleased
+    ) private view returns (uint256) {
+        return (totalReceived * _shares[account]) / _totalShares - alreadyReleased;
+    }
+
+    /**
+     * @dev Add a new payee to the contract.
+     * @param account The address of the payee to add.
+     * @param shares_ The number of shares owned by the payee.
+     */
+    function _addPayee(address account, uint256 shares_) private {
+        require(account != address(0), "PaymentSplitter: account is the zero address");
+        require(shares_ > 0, "PaymentSplitter: shares are 0");
+        require(_shares[account] == 0, "PaymentSplitter: account already has shares");
+
+        _payees.push(account);
+        _shares[account] = shares_;
+        _totalShares = _totalShares + shares_;
+        emit PayeeAdded(account, shares_);
+    }
+}

certora/munged/finance/README.adoc

@@ -0,0 +1,20 @@
+= Finance
+
+[.readme-notice]
+NOTE: This document is better viewed at https://docs.openzeppelin.com/contracts/api/finance
+
+This directory includes primitives for financial systems:
+
+- {PaymentSplitter} allows to split Ether and ERC20 payments among a group of accounts. The sender does not need to be
+  aware that the assets will be split in this way, since it is handled transparently by the contract. The split can be
+  in equal parts or in any other arbitrary proportion.
+
+- {VestingWallet} handles the vesting of Ether and ERC20 tokens for a given beneficiary. Custody of multiple tokens can
+  be given to this contract, which will release the token to the beneficiary following a given, customizable, vesting
+  schedule.
+
+== Contracts
+
+{{PaymentSplitter}}
+
+{{VestingWallet}}

certora/munged/finance/VestingWallet.sol

@@ -0,0 +1,135 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (finance/VestingWallet.sol)
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/utils/SafeERC20.sol";
+import "../utils/Address.sol";
+import "../utils/Context.sol";
+import "../utils/math/Math.sol";
+
+/**
+ * @title VestingWallet
+ * @dev This contract handles the vesting of Eth and ERC20 tokens for a given beneficiary. Custody of multiple tokens
+ * can be given to this contract, which will release the token to the beneficiary following a given vesting schedule.
+ * The vesting schedule is customizable through the {vestedAmount} function.
+ *
+ * Any token transferred to this contract will follow the vesting schedule as if they were locked from the beginning.
+ * Consequently, if the vesting has already started, any amount of tokens sent to this contract will (at least partly)
+ * be immediately releasable.
+ */
+contract VestingWallet is Context {
+    event EtherReleased(uint256 amount);
+    event ERC20Released(address token, uint256 amount);
+
+    uint256 private _released;
+    mapping(address => uint256) private _erc20Released;
+    address private immutable _beneficiary;
+    uint64 private immutable _start;
+    uint64 private immutable _duration;
+
+    /**
+     * @dev Set the beneficiary, start timestamp and vesting duration of the vesting wallet.
+     */
+    constructor(
+        address beneficiaryAddress,
+        uint64 startTimestamp,
+        uint64 durationSeconds
+    ) {
+        require(beneficiaryAddress != address(0), "VestingWallet: beneficiary is zero address");
+        _beneficiary = beneficiaryAddress;
+        _start = startTimestamp;
+        _duration = durationSeconds;
+    }
+
+    /**
+     * @dev The contract should be able to receive Eth.
+     */
+    receive() external payable virtual {}
+
+    /**
+     * @dev Getter for the beneficiary address.
+     */
+    function beneficiary() public view virtual returns (address) {
+        return _beneficiary;
+    }
+
+    /**
+     * @dev Getter for the start timestamp.
+     */
+    function start() public view virtual returns (uint256) {
+        return _start;
+    }
+
+    /**
+     * @dev Getter for the vesting duration.
+     */
+    function duration() public view virtual returns (uint256) {
+        return _duration;
+    }
+
+    /**
+     * @dev Amount of eth already released
+     */
+    function released() public view virtual returns (uint256) {
+        return _released;
+    }
+
+    /**
+     * @dev Amount of token already released
+     */
+    function released(address token) public view virtual returns (uint256) {
+        return _erc20Released[token];
+    }
+
+    /**
+     * @dev Release the native token (ether) that have already vested.
+     *
+     * Emits a {TokensReleased} event.
+     */
+    function release() public virtual {
+        uint256 releasable = vestedAmount(uint64(block.timestamp)) - released();
+        _released += releasable;
+        emit EtherReleased(releasable);
+        Address.sendValue(payable(beneficiary()), releasable);
+    }
+
+    /**
+     * @dev Release the tokens that have already vested.
+     *
+     * Emits a {TokensReleased} event.
+     */
+    function release(address token) public virtual {
+        uint256 releasable = vestedAmount(token, uint64(block.timestamp)) - released(token);
+        _erc20Released[token] += releasable;
+        emit ERC20Released(token, releasable);
+        SafeERC20.safeTransfer(IERC20(token), beneficiary(), releasable);
+    }
+
+    /**
+     * @dev Calculates the amount of ether that has already vested. Default implementation is a linear vesting curve.
+     */
+    function vestedAmount(uint64 timestamp) public view virtual returns (uint256) {
+        return _vestingSchedule(address(this).balance + released(), timestamp);
+    }
+
+    /**
+     * @dev Calculates the amount of tokens that has already vested. Default implementation is a linear vesting curve.
+     */
+    function vestedAmount(address token, uint64 timestamp) public view virtual returns (uint256) {
+        return _vestingSchedule(IERC20(token).balanceOf(address(this)) + released(token), timestamp);
+    }
+
+    /**
+     * @dev Virtual implementation of the vesting formula. This returns the amout vested, as a function of time, for
+     * an asset given its total historical allocation.
+     */
+    function _vestingSchedule(uint256 totalAllocation, uint64 timestamp) internal view virtual returns (uint256) {
+        if (timestamp < start()) {
+            return 0;
+        } else if (timestamp > start() + duration()) {
+            return totalAllocation;
+        } else {
+            return (totalAllocation * (timestamp - start())) / duration();
+        }
+    }
+}

certora/munged/governance/Governor.sol

@@ -0,0 +1,357 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/Governor.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/cryptography/ECDSA.sol";
+import "../utils/cryptography/draft-EIP712.sol";
+import "../utils/introspection/ERC165.sol";
+import "../utils/math/SafeCast.sol";
+import "../utils/Address.sol";
+import "../utils/Context.sol";
+import "../utils/Timers.sol";
+import "./IGovernor.sol";
+
+/**
+ * @dev Core of the governance system, designed to be extended though various modules.
+ *
+ * This contract is abstract and requires several function to be implemented in various modules:
+ *
+ * - A counting module must implement {quorum}, {_quorumReached}, {_voteSucceeded} and {_countVote}
+ * - A voting module must implement {getVotes}
+ * - Additionanly, the {votingPeriod} must also be implemented
+ *
+ * _Available since v4.3._
+ */
+abstract contract Governor is Context, ERC165, EIP712, IGovernor {
+    using SafeCast for uint256;
+    using Timers for Timers.BlockNumber;
+
+    bytes32 public constant BALLOT_TYPEHASH = keccak256("Ballot(uint256 proposalId,uint8 support)");
+
+    struct ProposalCore {
+        Timers.BlockNumber voteStart;
+        Timers.BlockNumber voteEnd;
+        bool executed;
+        bool canceled;
+    }
+
+    string private _name;
+
+    mapping(uint256 => ProposalCore) public _proposals;
+ 
+    /**
+     * @dev Restrict access to governor executing address. Some module might override the _executor function to make
+     * sure this modifier is consistant with the execution model.
+     */
+    modifier onlyGovernance() {
+        require(_msgSender() == _executor(), "Governor: onlyGovernance");
+        _;
+    }
+
+    /**
+     * @dev Sets the value for {name} and {version}
+     */
+    constructor(string memory name_) EIP712(name_, version()) {
+        _name = name_;
+    }
+
+    /**
+     * @dev Function to receive ETH that will be handled by the governor (disabled if executor is a third party contract)
+     */
+    receive() external payable virtual {
+        require(_executor() == address(this));
+    }
+
+    /**
+     * @dev See {IERC165-supportsInterface}.
+     */
+    function supportsInterface(bytes4 interfaceId) public view virtual override(IERC165, ERC165) returns (bool) {
+        return interfaceId == type(IGovernor).interfaceId || super.supportsInterface(interfaceId);
+    }
+
+    /**
+     * @dev See {IGovernor-name}.
+     */
+    function name() public view virtual override returns (string memory) {
+        return _name;
+    }
+
+    /**
+     * @dev See {IGovernor-version}.
+     */
+    function version() public view virtual override returns (string memory) {
+        return "1";
+    }
+
+    /**
+     * @dev See {IGovernor-hashProposal}.
+     *
+     * The proposal id is produced by hashing the RLC encoded `targets` array, the `values` array, the `calldatas` array
+     * and the descriptionHash (bytes32 which itself is the keccak256 hash of the description string). This proposal id
+     * can be produced from the proposal data which is part of the {ProposalCreated} event. It can even be computed in
+     * advance, before the proposal is submitted.
+     *
+     * Note that the chainId and the governor address are not part of the proposal id computation. Consequently, the
+     * same proposal (with same operation and same description) will have the same id if submitted on multiple governors
+     * accross multiple networks. This also means that in order to execute the same operation twice (on the same
+     * governor) the proposer will have to change the description in order to avoid proposal id conflicts.
+     */
+    function hashProposal(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) public pure virtual override returns (uint256) {
+        return uint256(keccak256(abi.encode(targets, values, calldatas, descriptionHash)));
+    }
+
+    /**
+     * @dev See {IGovernor-state}.
+     */
+    function state(uint256 proposalId) public view virtual override returns (ProposalState) {
+        ProposalCore memory proposal = _proposals[proposalId];
+
+        if (proposal.executed) {
+            return ProposalState.Executed;
+        } else if (proposal.canceled) {
+            return ProposalState.Canceled;
+        } else if (proposal.voteStart.getDeadline() >= block.number) {
+            return ProposalState.Pending;
+        } else if (proposal.voteEnd.getDeadline() >= block.number) {
+            return ProposalState.Active;
+        } else if (proposal.voteEnd.isExpired()) {
+            return
+                _quorumReached(proposalId) && _voteSucceeded(proposalId)
+                    ? ProposalState.Succeeded
+                    : ProposalState.Defeated;
+        } else {
+            revert("Governor: unknown proposal id");
+        }
+    }
+
+    /**
+     * @dev See {IGovernor-proposalSnapshot}.
+     */
+    function proposalSnapshot(uint256 proposalId) public view virtual override returns (uint256) {
+        return _proposals[proposalId].voteStart.getDeadline();
+    }
+
+    /**
+     * @dev See {IGovernor-proposalDeadline}.
+     */
+    function proposalDeadline(uint256 proposalId) public view virtual override returns (uint256) {
+        return _proposals[proposalId].voteEnd.getDeadline();
+    }
+
+    /**
+     * @dev Part of the Governor Bravo's interface: _"The number of votes required in order for a voter to become a proposer"_.
+     */
+    function proposalThreshold() public view virtual returns (uint256) {
+        return 0;
+    }
+
+    /**
+     * @dev Amount of votes already cast passes the threshold limit.
+     */
+    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+
+    /**
+     * @dev Is the proposal successful or not.
+     */
+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+
+    /**
+     * @dev Register a vote with a given support and voting weight.
+     *
+     * Note: Support is generic and can represent various things depending on the voting system used.
+     */
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal virtual;
+
+    /**
+     * @dev See {IGovernor-propose}.
+     */
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public virtual override returns (uint256) {
+        require(
+            getVotes(msg.sender, block.number - 1) >= proposalThreshold(),
+            "GovernorCompatibilityBravo: proposer votes below proposal threshold"
+        );
+
+        uint256 proposalId = hashProposal(targets, values, calldatas, keccak256(bytes(description)));
+
+        require(targets.length == values.length, "Governor: invalid proposal length");
+        require(targets.length == calldatas.length, "Governor: invalid proposal length");
+        require(targets.length > 0, "Governor: empty proposal");
+
+        ProposalCore storage proposal = _proposals[proposalId];
+        require(proposal.voteStart.isUnset(), "Governor: proposal already exists");
+
+        uint64 snapshot = block.number.toUint64() + votingDelay().toUint64();
+        uint64 deadline = snapshot + votingPeriod().toUint64();
+
+        proposal.voteStart.setDeadline(snapshot);
+        proposal.voteEnd.setDeadline(deadline);
+
+        emit ProposalCreated(
+            proposalId,
+            _msgSender(),
+            targets,
+            values,
+            new string[](targets.length),
+            calldatas,
+            snapshot,
+            deadline,
+            description
+        );
+
+        return proposalId;
+    }
+
+    /**
+     * @dev See {IGovernor-execute}.
+     */
+    function execute(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) public payable virtual override returns (uint256) {
+        uint256 proposalId = hashProposal(targets, values, calldatas, descriptionHash);
+
+        ProposalState status = state(proposalId);
+        require(
+            status == ProposalState.Succeeded || status == ProposalState.Queued,
+            "Governor: proposal not successful"
+        );
+        _proposals[proposalId].executed = true;
+
+        emit ProposalExecuted(proposalId);
+
+        _execute(proposalId, targets, values, calldatas, descriptionHash);
+
+        return proposalId;
+    }
+
+    /**
+     * @dev Internal execution mechanism. Can be overriden to implement different execution mechanism
+     */
+    function _execute(
+        uint256, /* proposalId */
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 /*descriptionHash*/
+    ) internal virtual {
+        string memory errorMessage = "Governor: call reverted without message";
+        for (uint256 i = 0; i < targets.length; ++i) {
+            (bool success, bytes memory returndata) = targets[i].call{value: values[i]}(calldatas[i]);
+            Address.verifyCallResult(success, returndata, errorMessage);
+        }
+    }
+
+    /**
+     * @dev Internal cancel mechanism: locks up the proposal timer, preventing it from being re-submitted. Marks it as
+     * canceled to allow distinguishing it from executed proposals.
+     *
+     * Emits a {IGovernor-ProposalCanceled} event.
+     */
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal virtual returns (uint256) {
+        uint256 proposalId = hashProposal(targets, values, calldatas, descriptionHash);
+        ProposalState status = state(proposalId);
+
+        require(
+            status != ProposalState.Canceled && status != ProposalState.Expired && status != ProposalState.Executed,
+            "Governor: proposal not active"
+        );
+        _proposals[proposalId].canceled = true;
+
+        emit ProposalCanceled(proposalId);
+
+        return proposalId;
+    }
+
+    /**
+     * @dev See {IGovernor-castVote}.
+     */
+    function castVote(uint256 proposalId, uint8 support) public virtual override returns (uint256) {
+        address voter = _msgSender();
+        return _castVote(proposalId, voter, support, "");
+    }
+
+    /**
+     * @dev See {IGovernor-castVoteWithReason}.
+     */
+    function castVoteWithReason(
+        uint256 proposalId,
+        uint8 support,
+        string calldata reason
+    ) public virtual override returns (uint256) {
+        address voter = _msgSender();
+        return _castVote(proposalId, voter, support, reason);
+    }
+
+    /**
+     * @dev See {IGovernor-castVoteBySig}.
+     */
+    function castVoteBySig(
+        uint256 proposalId,
+        uint8 support,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public virtual override returns (uint256) {
+        address voter = ECDSA.recover(
+            _hashTypedDataV4(keccak256(abi.encode(BALLOT_TYPEHASH, proposalId, support))),
+            v,
+            r,
+            s
+        ); // mention that we assume that hashing works correctly
+        return _castVote(proposalId, voter, support, "");
+    }
+
+    /**
+     * @dev Internal vote casting mechanism: Check that the vote is pending, that it has not been cast yet, retrieve
+     * voting weight using {IGovernor-getVotes} and call the {_countVote} internal function.
+     *
+     * Emits a {IGovernor-VoteCast} event.
+     */
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason
+    ) internal virtual returns (uint256) {
+        ProposalCore storage proposal = _proposals[proposalId];
+        require(state(proposalId) == ProposalState.Active, "Governor: vote not currently active");
+
+        uint256 weight = getVotes(account, proposal.voteStart.getDeadline());
+        _countVote(proposalId, account, support, weight);
+
+        emit VoteCast(account, proposalId, support, weight, reason);
+
+        return weight;
+    }
+
+    /**
+     * @dev Address through which the governor executes action. Will be overloaded by module that execute actions
+     * through another contract such as a timelock.
+     */
+    function _executor() internal view virtual returns (address) {
+        return address(this);
+    }
+}

certora/munged/governance/IGovernor.sol

@@ -0,0 +1,218 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/IGovernor.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/ERC165.sol";
+
+/**
+ * @dev Interface of the {Governor} core.
+ *
+ * _Available since v4.3._
+ */
+abstract contract IGovernor is IERC165 {
+    enum ProposalState {
+        Pending,
+        Active,
+        Canceled,
+        Defeated,
+        Succeeded,
+        Queued,
+        Expired,
+        Executed
+    }
+
+    /**
+     * @dev Emitted when a proposal is created.
+     */
+    event ProposalCreated(
+        uint256 proposalId,
+        address proposer,
+        address[] targets,
+        uint256[] values,
+        string[] signatures,
+        bytes[] calldatas,
+        uint256 startBlock,
+        uint256 endBlock,
+        string description
+    );
+
+    /**
+     * @dev Emitted when a proposal is canceled.
+     */
+    event ProposalCanceled(uint256 proposalId);
+
+    /**
+     * @dev Emitted when a proposal is executed.
+     */
+    event ProposalExecuted(uint256 proposalId);
+
+    /**
+     * @dev Emitted when a vote is cast.
+     *
+     * Note: `support` values should be seen as buckets. There interpretation depends on the voting module used.
+     */
+    event VoteCast(address indexed voter, uint256 proposalId, uint8 support, uint256 weight, string reason);
+
+    /**
+     * @notice module:core
+     * @dev Name of the governor instance (used in building the ERC712 domain separator).
+     */
+    function name() public view virtual returns (string memory);
+
+    /**
+     * @notice module:core
+     * @dev Version of the governor instance (used in building the ERC712 domain separator). Default: "1"
+     */
+    function version() public view virtual returns (string memory);
+
+    /**
+     * @notice module:voting
+     * @dev A description of the possible `support` values for {castVote} and the way these votes are counted, meant to
+     * be consumed by UIs to show correct vote options and interpret the results. The string is a URL-encoded sequence of
+     * key-value pairs that each describe one aspect, for example `support=bravo&quorum=for,abstain`.
+     *
+     * There are 2 standard keys: `support` and `quorum`.
+     *
+     * - `support=bravo` refers to the vote options 0 = Against, 1 = For, 2 = Abstain, as in `GovernorBravo`.
+     * - `quorum=bravo` means that only For votes are counted towards quorum.
+     * - `quorum=for,abstain` means that both For and Abstain votes are counted towards quorum.
+     *
+     * NOTE: The string can be decoded by the standard
+     * https://developer.mozilla.org/en-US/docs/Web/API/URLSearchParams[`URLSearchParams`]
+     * JavaScript class.
+     */
+    // solhint-disable-next-line func-name-mixedcase
+    function COUNTING_MODE() public pure virtual returns (string memory);
+
+    /**
+     * @notice module:core
+     * @dev Hashing function used to (re)build the proposal id from the proposal details..
+     */
+    function hashProposal(
+        address[] calldata targets,
+        uint256[] calldata values,
+        bytes[] calldata calldatas,
+        bytes32 descriptionHash
+    ) public pure virtual returns (uint256);
+
+    /**
+     * @notice module:core
+     * @dev Current state of a proposal, following Compound's convention
+     */
+    function state(uint256 proposalId) public view virtual returns (ProposalState);
+
+    /**
+     * @notice module:core
+     * @dev Block number used to retrieve user's votes and quorum. As per Compound's Comp and OpenZeppelin's
+     * ERC20Votes, the snapshot is performed at the end of this block. Hence, voting for this proposal starts at the
+     * beginning of the following block.
+     */
+    function proposalSnapshot(uint256 proposalId) public view virtual returns (uint256);
+
+    /**
+     * @notice module:core
+     * @dev Block number at which votes close. Votes close at the end of this block, so it is possible to cast a vote
+     * during this block.
+     */
+    function proposalDeadline(uint256 proposalId) public view virtual returns (uint256);
+
+    /**
+     * @notice module:user-config
+     * @dev Delay, in number of block, between the proposal is created and the vote starts. This can be increassed to
+     * leave time for users to buy voting power, of delegate it, before the voting of a proposal starts.
+     */
+    function votingDelay() public view virtual returns (uint256);
+
+    /**
+     * @notice module:user-config
+     * @dev Delay, in number of blocks, between the vote start and vote ends.
+     *
+     * NOTE: The {votingDelay} can delay the start of the vote. This must be considered when setting the voting
+     * duration compared to the voting delay.
+     */
+    function votingPeriod() public view virtual returns (uint256);
+
+    /**
+     * @notice module:user-config
+     * @dev Minimum number of cast voted required for a proposal to be successful.
+     *
+     * Note: The `blockNumber` parameter corresponds to the snaphot used for counting vote. This allows to scale the
+     * quroum depending on values such as the totalSupply of a token at this block (see {ERC20Votes}).
+     */
+    function quorum(uint256 blockNumber) public view virtual returns (uint256);
+
+    /**
+     * @notice module:reputation
+     * @dev Voting power of an `account` at a specific `blockNumber`.
+     *
+     * Note: this can be implemented in a number of ways, for example by reading the delegated balance from one (or
+     * multiple), {ERC20Votes} tokens.
+     */
+    function getVotes(address account, uint256 blockNumber) public view virtual returns (uint256);
+
+    /**
+     * @notice module:voting
+     * @dev Returns weither `account` has cast a vote on `proposalId`.
+     */
+    function hasVoted(uint256 proposalId, address account) public view virtual returns (bool);
+
+    /**
+     * @dev Create a new proposal. Vote start {IGovernor-votingDelay} blocks after the proposal is created and ends
+     * {IGovernor-votingPeriod} blocks after the voting starts.
+     *
+     * Emits a {ProposalCreated} event.
+     */
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public virtual returns (uint256 proposalId);
+
+    /**
+     * @dev Execute a successful proposal. This requires the quorum to be reached, the vote to be successful, and the
+     * deadline to be reached.
+     *
+     * Emits a {ProposalExecuted} event.
+     *
+     * Note: some module can modify the requirements for execution, for example by adding an additional timelock.
+     */
+    function execute(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) public payable virtual returns (uint256 proposalId);
+
+    /**
+     * @dev Cast a vote
+     *
+     * Emits a {VoteCast} event.
+     */
+    function castVote(uint256 proposalId, uint8 support) public virtual returns (uint256 balance);
+
+    /**
+     * @dev Cast a with a reason
+     *
+     * Emits a {VoteCast} event.
+     */
+    function castVoteWithReason(
+        uint256 proposalId,
+        uint8 support,
+        string calldata reason
+    ) public virtual returns (uint256 balance);
+
+    /**
+     * @dev Cast a vote using the user cryptographic signature.
+     *
+     * Emits a {VoteCast} event.
+     */
+    function castVoteBySig(
+        uint256 proposalId,
+        uint8 support,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public virtual returns (uint256 balance);
+}

certora/munged/governance/README.adoc

@@ -0,0 +1,168 @@
+= Governance
+
+[.readme-notice]
+NOTE: This document is better viewed at https://docs.openzeppelin.com/contracts/api/governance
+
+This directory includes primitives for on-chain governance.
+
+== Governor
+
+This modular system of Governor contracts allows the deployment on-chain voting protocols similar to https://compound.finance/docs/governance[Compound's Governor Alpha & Bravo] and beyond, through the ability to easily customize multiple aspects of the protocol.
+
+[TIP]
+====
+For a guided experience, set up your Governor contract using https://wizard.openzeppelin.com/#governor[Contracts Wizard].
+
+For a written walkthrough, check out our guide on xref:ROOT:governance.adoc[How to set up on-chain governance].
+====
+
+* {Governor}: The core contract that contains all the logic and primitives. It is abstract and requires choosing one of each of the modules below, or custom ones.
+
+Votes modules determine the source of voting power, and sometimes quorum number.
+
+* {GovernorVotes}: Extracts voting weight from an {ERC20Votes} token.
+
+* {GovernorVotesComp}: Extracts voting weight from a COMP-like or {ERC20VotesComp} token.
+
+* {GovernorVotesQuorumFraction}: Combines with `GovernorVotes` to set the quorum as a fraction of the total token supply.
+
+Counting modules determine valid voting options.
+
+* {GovernorCountingSimple}: Simple voting mechanism with 3 voting options: Against, For and Abstain.
+
+Timelock extensions add a delay for governance decisions to be executed. The workflow is extended to require a `queue` step before execution. With these modules, proposals are executed by the external timelock contract, thus it is the timelock that has to hold the assets that are being governed.
+
+* {GovernorTimelockControl}: Connects with an instance of {TimelockController}. Allows multiple proposers and executors, in addition to the Governor itself.
+
+* {GovernorTimelockCompound}: Connects with an instance of Compound's https://github.com/compound-finance/compound-protocol/blob/master/contracts/Timelock.sol[`Timelock`] contract.
+
+Other extensions can customize the behavior or interface in multiple ways.
+
+* {GovernorCompatibilityBravo}: Extends the interface to be fully `GovernorBravo`-compatible. Note that events are compatible regardless of whether this extension is included or not.
+
+* {GovernorSettings}: Manages some of the settings (voting delay, voting period duration, and proposal threshold) in a way that can be updated through a governance proposal, without requiering an upgrade.
+
+In addition to modules and extensions, the core contract requires a few virtual functions to be implemented to your particular specifications:
+
+* <<Governor-votingDelay-,`votingDelay()`>>: Delay (in number of blocks) since the proposal is submitted until voting power is fixed and voting starts. This can be used to enforce a delay after a proposal is published for users to buy tokens, or delegate their votes.
+* <<Governor-votingPeriod-,`votingPeriod()`>>: Delay (in number of blocks) since the proposal starts until voting ends.
+* <<Governor-quorum-uint256-,`quorum(uint256 blockNumber)`>>: Quorum required for a proposal to be successful. This function includes a `blockNumber` argument so the quorum can adapt through time, for example, to follow a token's `totalSupply`.
+
+NOTE: Functions of the `Governor` contract do not include access control. If you want to restrict access, you should add these checks by overloading the particular functions. Among these, {Governor-_cancel} is internal by default, and you will have to expose it (which the right access control mechanism) yourself if this function is needed.
+
+=== Core
+
+{{IGovernor}}
+
+{{Governor}}
+
+=== Modules
+
+{{GovernorCountingSimple}}
+
+{{GovernorVotes}}
+
+{{GovernorVotesQuorumFraction}}
+
+{{GovernorVotesComp}}
+
+=== Extensions
+
+{{GovernorTimelockControl}}
+
+{{GovernorTimelockCompound}}
+
+{{GovernorSettings}}
+
+{{GovernorCompatibilityBravo}}
+
+=== Deprecated
+
+{{GovernorProposalThreshold}}
+
+== Timelock
+
+In a governance system, the {TimelockController} contract is in carge of introducing a delay between a proposal and its execution. It can be used with or without a {Governor}.
+
+{{TimelockController}}
+
+[[timelock-terminology]]
+==== Terminology
+
+* *Operation:* A transaction (or a set of transactions) that is the subject of the timelock. It has to be scheduled by a proposer and executed by an executor. The timelock enforces a minimum delay between the proposition and the execution (see xref:access-control.adoc#operation_lifecycle[operation lifecycle]). If the operation contains multiple transactions (batch mode), they are executed atomically. Operations are identified by the hash of their content.
+* *Operation status:*
+** *Unset:* An operation that is not part of the timelock mechanism.
+** *Pending:* An operation that has been scheduled, before the timer expires.
+** *Ready:* An operation that has been scheduled, after the timer expires.
+** *Done:* An operation that has been executed.
+* *Predecessor*: An (optional) dependency between operations. An operation can depend on another operation (its predecessor), forcing the execution order of these two operations.
+* *Role*:
+** *Admin:* An address (smart contract or EOA) that is in charge of granting the roles of Proposer and Executor.
+** *Proposer:* An address (smart contract or EOA) that is in charge of scheduling (and cancelling) operations.
+** *Executor:* An address (smart contract or EOA) that is in charge of executing operations once the timelock has expired. This role can be given to the zero address to allow anyone to execute operations.
+
+[[timelock-operation]]
+==== Operation structure
+
+Operation executed by the xref:api:governance.adoc#TimelockController[`TimelockController`] can contain one or multiple subsequent calls. Depending on whether you need to multiple calls to be executed atomically, you can either use simple or batched operations.
+
+Both operations contain:
+
+* *Target*, the address of the smart contract that the timelock should operate on.
+* *Value*, in wei, that should be sent with the transaction. Most of the time this will be 0. Ether can be deposited before-end or passed along when executing the transaction.
+* *Data*, containing the encoded function selector and parameters of the call. This can be produced using a number of tools. For example, a maintenance operation granting role `ROLE` to `ACCOUNT` can be encode using web3js as follows:
+
+```javascript
+const data = timelock.contract.methods.grantRole(ROLE, ACCOUNT).encodeABI()
+```
+
+* *Predecessor*, that specifies a dependency between operations. This dependency is optional. Use `bytes32(0)` if the operation does not have any dependency.
+* *Salt*, used to disambiguate two otherwise identical operations. This can be any random value.
+
+In the case of batched operations, `target`, `value` and `data` are specified as arrays, which must be of the same length.
+
+[[timelock-operation-lifecycle]]
+==== Operation lifecycle
+
+Timelocked operations are identified by a unique id (their hash) and follow a specific lifecycle:
+
+`Unset` -> `Pending` -> `Pending` + `Ready` -> `Done`
+
+* By calling xref:api:governance.adoc#TimelockController-schedule-address-uint256-bytes-bytes32-bytes32-uint256-[`schedule`] (or xref:api:governance.adoc#TimelockController-scheduleBatch-address---uint256---bytes---bytes32-bytes32-uint256-[`scheduleBatch`]), a proposer moves the operation from the `Unset` to the `Pending` state. This starts a timer that must be longer than the minimum delay. The timer expires at a timestamp accessible through the xref:api:governance.adoc#TimelockController-getTimestamp-bytes32-[`getTimestamp`] method.
+* Once the timer expires, the operation automatically gets the `Ready` state. At this point, it can be executed.
+* By calling xref:api:governance.adoc#TimelockController-TimelockController-execute-address-uint256-bytes-bytes32-bytes32-[`execute`] (or xref:api:governance.adoc#TimelockController-executeBatch-address---uint256---bytes---bytes32-bytes32-[`executeBatch`]), an executor triggers the operation's underlying transactions and moves it to the `Done` state. If the operation has a predecessor, it has to be in the `Done` state for this transition to succeed.
+* xref:api:governance.adoc#TimelockController-TimelockController-cancel-bytes32-[`cancel`] allows proposers to cancel any `Pending` operation. This resets the operation to the `Unset` state. It is thus possible for a proposer to re-schedule an operation that has been cancelled. In this case, the timer restarts when the operation is re-scheduled.
+
+Operations status can be queried using the functions:
+
+* xref:api:governance.adoc#TimelockController-isOperationPending-bytes32-[`isOperationPending(bytes32)`]
+* xref:api:governance.adoc#TimelockController-isOperationReady-bytes32-[`isOperationReady(bytes32)`]
+* xref:api:governance.adoc#TimelockController-isOperationDone-bytes32-[`isOperationDone(bytes32)`]
+
+[[timelock-roles]]
+==== Roles
+
+[[timelock-admin]]
+===== Admin
+
+The admins are in charge of managing proposers and executors. For the timelock to be self-governed, this role should only be given to the timelock itself. Upon deployment, both the timelock and the deployer have this role. After further configuration and testing, the deployer can renounce this role such that all further maintenance operations have to go through the timelock process.
+
+This role is identified by the *TIMELOCK_ADMIN_ROLE* value: `0x5f58e3a2316349923ce3780f8d587db2d72378aed66a8261c916544fa6846ca5`
+
+[[timelock-proposer]]
+===== Proposer
+
+The proposers are in charge of scheduling (and cancelling) operations. This is a critical role, that should be given to governing entities. This could be an EOA, a multisig, or a DAO.
+
+WARNING: *Proposer fight:* Having multiple proposers, while providing redundancy in case one becomes unavailable, can be dangerous. As proposer have their say on all operations, they could cancel operations they disagree with, including operations to remove them for the proposers.
+
+This role is identified by the *PROPOSER_ROLE* value: `0xb09aa5aeb3702cfd50b6b62bc4532604938f21248a27a1d5ca736082b6819cc1`
+
+[[timelock-executor]]
+===== Executor
+
+The executors are in charge of executing the operations scheduled by the proposers once the timelock expires. Logic dictates that multisig or DAO that are proposers should also be executors in order to guarantee operations that have been scheduled will eventually be executed. However, having additional executors can reduce the cost (the executing transaction does not require validation by the multisig or DAO that proposed it), while ensuring whoever is in charge of execution cannot trigger actions that have not been scheduled by the proposers. Alternatively, it is possible to allow _any_ address to execute a proposal once the timelock has expired by granting the executor role to the zero address.
+
+This role is identified by the *EXECUTOR_ROLE* value: `0xd8aa0f3194971a2a116679f7c2090f6939c8d4e01a2a8d7e41d55e5351469e63`
+
+WARNING: A live contract without at least one proposer and one executor is locked. Make sure these roles are filled by reliable entities before the deployer renounces its administrative rights in favour of the timelock contract itself. See the {AccessControl} documentation to learn more about role management.

certora/munged/governance/TimelockController.sol

@@ -0,0 +1,354 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/TimelockController.sol)
+
+pragma solidity ^0.8.0;
+
+import "../access/AccessControl.sol";
+
+/**
+ * @dev Contract module which acts as a timelocked controller. When set as the
+ * owner of an `Ownable` smart contract, it enforces a timelock on all
+ * `onlyOwner` maintenance operations. This gives time for users of the
+ * controlled contract to exit before a potentially dangerous maintenance
+ * operation is applied.
+ *
+ * By default, this contract is self administered, meaning administration tasks
+ * have to go through the timelock process. The proposer (resp executor) role
+ * is in charge of proposing (resp executing) operations. A common use case is
+ * to position this {TimelockController} as the owner of a smart contract, with
+ * a multisig or a DAO as the sole proposer.
+ *
+ * _Available since v3.3._
+ */
+contract TimelockController is AccessControl {
+    bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE");
+    bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
+    bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
+    uint256 internal constant _DONE_TIMESTAMP = uint256(1);
+
+    mapping(bytes32 => uint256) private _timestamps;
+    uint256 private _minDelay;
+
+    /**
+     * @dev Emitted when a call is scheduled as part of operation `id`.
+     */
+    event CallScheduled(
+        bytes32 indexed id,
+        uint256 indexed index,
+        address target,
+        uint256 value,
+        bytes data,
+        bytes32 predecessor,
+        uint256 delay
+    );
+
+    /**
+     * @dev Emitted when a call is performed as part of operation `id`.
+     */
+    event CallExecuted(bytes32 indexed id, uint256 indexed index, address target, uint256 value, bytes data);
+
+    /**
+     * @dev Emitted when operation `id` is cancelled.
+     */
+    event Cancelled(bytes32 indexed id);
+
+    /**
+     * @dev Emitted when the minimum delay for future operations is modified.
+     */
+    event MinDelayChange(uint256 oldDuration, uint256 newDuration);
+
+    /**
+     * @dev Initializes the contract with a given `minDelay`.
+     */
+    constructor(
+        uint256 minDelay,
+        address[] memory proposers,
+        address[] memory executors
+    ) {
+        _setRoleAdmin(TIMELOCK_ADMIN_ROLE, TIMELOCK_ADMIN_ROLE);
+        _setRoleAdmin(PROPOSER_ROLE, TIMELOCK_ADMIN_ROLE);
+        _setRoleAdmin(EXECUTOR_ROLE, TIMELOCK_ADMIN_ROLE);
+
+        // deployer + self administration
+        _setupRole(TIMELOCK_ADMIN_ROLE, _msgSender());
+        _setupRole(TIMELOCK_ADMIN_ROLE, address(this));
+
+        // register proposers
+        for (uint256 i = 0; i < proposers.length; ++i) {
+            _setupRole(PROPOSER_ROLE, proposers[i]);
+        }
+
+        // register executors
+        for (uint256 i = 0; i < executors.length; ++i) {
+            _setupRole(EXECUTOR_ROLE, executors[i]);
+        }
+
+        _minDelay = minDelay;
+        emit MinDelayChange(0, minDelay);
+    }
+
+    /**
+     * @dev Modifier to make a function callable only by a certain role. In
+     * addition to checking the sender's role, `address(0)` 's role is also
+     * considered. Granting a role to `address(0)` is equivalent to enabling
+     * this role for everyone.
+     */
+    modifier onlyRoleOrOpenRole(bytes32 role) {
+        if (!hasRole(role, address(0))) {
+            _checkRole(role, _msgSender());
+        }
+        _;
+    }
+
+    /**
+     * @dev Contract might receive/hold ETH as part of the maintenance process.
+     */
+    receive() external payable {}
+
+    /**
+     * @dev Returns whether an id correspond to a registered operation. This
+     * includes both Pending, Ready and Done operations.
+     */
+    function isOperation(bytes32 id) public view virtual returns (bool pending) {
+        return getTimestamp(id) > 0;
+    }
+
+    /**
+     * @dev Returns whether an operation is pending or not.
+     */
+    function isOperationPending(bytes32 id) public view virtual returns (bool pending) {
+        return getTimestamp(id) > _DONE_TIMESTAMP;
+    }
+
+    /**
+     * @dev Returns whether an operation is ready or not.
+     */
+    function isOperationReady(bytes32 id) public view virtual returns (bool ready) {
+        uint256 timestamp = getTimestamp(id);
+        return timestamp > _DONE_TIMESTAMP && timestamp <= block.timestamp;
+    }
+
+    /**
+     * @dev Returns whether an operation is done or not.
+     */
+    function isOperationDone(bytes32 id) public view virtual returns (bool done) {
+        return getTimestamp(id) == _DONE_TIMESTAMP;
+    }
+
+    /**
+     * @dev Returns the timestamp at with an operation becomes ready (0 for
+     * unset operations, 1 for done operations).
+     */
+    function getTimestamp(bytes32 id) public view virtual returns (uint256 timestamp) {
+        return _timestamps[id];
+    }
+
+    /**
+     * @dev Returns the minimum delay for an operation to become valid.
+     *
+     * This value can be changed by executing an operation that calls `updateDelay`.
+     */
+    function getMinDelay() public view virtual returns (uint256 duration) {
+        return _minDelay;
+    }
+
+    /**
+     * @dev Returns the identifier of an operation containing a single
+     * transaction.
+     */
+    function hashOperation(
+        address target,
+        uint256 value,
+        bytes calldata data,
+        bytes32 predecessor,
+        bytes32 salt
+    ) public pure virtual returns (bytes32 hash) {
+        return keccak256(abi.encode(target, value, data, predecessor, salt));
+    }
+
+    /**
+     * @dev Returns the identifier of an operation containing a batch of
+     * transactions.
+     */
+    function hashOperationBatch(
+        address[] calldata targets,
+        uint256[] calldata values,
+        bytes[] calldata datas,
+        bytes32 predecessor,
+        bytes32 salt
+    ) public pure virtual returns (bytes32 hash) {
+        return keccak256(abi.encode(targets, values, datas, predecessor, salt));
+    }
+
+    /**
+     * @dev Schedule an operation containing a single transaction.
+     *
+     * Emits a {CallScheduled} event.
+     *
+     * Requirements:
+     *
+     * - the caller must have the 'proposer' role.
+     */
+    function schedule(
+        address target,
+        uint256 value,
+        bytes calldata data,
+        bytes32 predecessor,
+        bytes32 salt,
+        uint256 delay
+    ) public virtual onlyRole(PROPOSER_ROLE) {
+        bytes32 id = hashOperation(target, value, data, predecessor, salt);
+        _schedule(id, delay);
+        emit CallScheduled(id, 0, target, value, data, predecessor, delay);
+    }
+
+    /**
+     * @dev Schedule an operation containing a batch of transactions.
+     *
+     * Emits one {CallScheduled} event per transaction in the batch.
+     *
+     * Requirements:
+     *
+     * - the caller must have the 'proposer' role.
+     */
+    function scheduleBatch(
+        address[] calldata targets,
+        uint256[] calldata values,
+        bytes[] calldata datas,
+        bytes32 predecessor,
+        bytes32 salt,
+        uint256 delay
+    ) public virtual onlyRole(PROPOSER_ROLE) {
+        require(targets.length == values.length, "TimelockController: length mismatch");
+        require(targets.length == datas.length, "TimelockController: length mismatch");
+
+        bytes32 id = hashOperationBatch(targets, values, datas, predecessor, salt);
+        _schedule(id, delay);
+        for (uint256 i = 0; i < targets.length; ++i) {
+            emit CallScheduled(id, i, targets[i], values[i], datas[i], predecessor, delay);
+        }
+    }
+
+    /**
+     * @dev Schedule an operation that is to becomes valid after a given delay.
+     */
+    function _schedule(bytes32 id, uint256 delay) private {
+        require(!isOperation(id), "TimelockController: operation already scheduled");
+        require(delay >= getMinDelay(), "TimelockController: insufficient delay");
+        _timestamps[id] = block.timestamp + delay;
+    }
+
+    /**
+     * @dev Cancel an operation.
+     *
+     * Requirements:
+     *
+     * - the caller must have the 'proposer' role.
+     */
+    function cancel(bytes32 id) public virtual onlyRole(PROPOSER_ROLE) {
+        require(isOperationPending(id), "TimelockController: operation cannot be cancelled");
+        delete _timestamps[id];
+
+        emit Cancelled(id);
+    }
+
+    /**
+     * @dev Execute an (ready) operation containing a single transaction.
+     *
+     * Emits a {CallExecuted} event.
+     *
+     * Requirements:
+     *
+     * - the caller must have the 'executor' role.
+     */
+    function execute(
+        address target,
+        uint256 value,
+        bytes calldata data,
+        bytes32 predecessor,
+        bytes32 salt
+    ) public payable virtual onlyRoleOrOpenRole(EXECUTOR_ROLE) {
+        bytes32 id = hashOperation(target, value, data, predecessor, salt);
+        _beforeCall(id, predecessor);
+        _call(id, 0, target, value, data);
+        _afterCall(id);
+    }
+
+    /**
+     * @dev Execute an (ready) operation containing a batch of transactions.
+     *
+     * Emits one {CallExecuted} event per transaction in the batch.
+     *
+     * Requirements:
+     *
+     * - the caller must have the 'executor' role.
+     */
+    function executeBatch(
+        address[] calldata targets,
+        uint256[] calldata values,
+        bytes[] calldata datas,
+        bytes32 predecessor,
+        bytes32 salt
+    ) public payable virtual onlyRoleOrOpenRole(EXECUTOR_ROLE) {
+        require(targets.length == values.length, "TimelockController: length mismatch");
+        require(targets.length == datas.length, "TimelockController: length mismatch");
+
+        bytes32 id = hashOperationBatch(targets, values, datas, predecessor, salt);
+        _beforeCall(id, predecessor);
+        for (uint256 i = 0; i < targets.length; ++i) {
+            _call(id, i, targets[i], values[i], datas[i]);
+        }
+        _afterCall(id);
+        // ASSUME THAT THERE IS NO REENTRANCY IN WIZARDHARNESS1
+    }
+
+    /**
+     * @dev Checks before execution of an operation's calls.
+     */
+    function _beforeCall(bytes32 id, bytes32 predecessor) private view {
+        require(isOperationReady(id), "TimelockController: operation is not ready");
+        require(predecessor == bytes32(0) || isOperationDone(predecessor), "TimelockController: missing dependency");
+    }
+
+    /**
+     * @dev Checks after execution of an operation's calls.
+     */
+    function _afterCall(bytes32 id) private {
+        require(isOperationReady(id), "TimelockController: operation is not ready");
+        _timestamps[id] = _DONE_TIMESTAMP;
+    }
+
+    /**
+     * @dev Execute an operation's call.
+     *
+     * Emits a {CallExecuted} event.
+     */
+    function _call(
+        bytes32 id,
+        uint256 index,
+        address target,
+        uint256 value,
+        bytes calldata data
+    ) private {
+        (bool success, ) = target.call{value: value}(data);
+        require(success, "TimelockController: underlying transaction reverted");
+
+        emit CallExecuted(id, index, target, value, data);
+    }
+
+    /**
+     * @dev Changes the minimum timelock duration for future operations.
+     *
+     * Emits a {MinDelayChange} event.
+     *
+     * Requirements:
+     *
+     * - the caller must be the timelock itself. This can only be achieved by scheduling and later executing
+     * an operation where the timelock is the target and the data is the ABI-encoded call to this function.
+     */
+    function updateDelay(uint256 newDelay) external virtual {
+        require(msg.sender == address(this), "TimelockController: caller must be timelock");
+        emit MinDelayChange(_minDelay, newDelay);
+        _minDelay = newDelay;
+    }
+}

certora/munged/governance/compatibility/GovernorCompatibilityBravo.sol

@@ -0,0 +1,288 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/compatibility/GovernorCompatibilityBravo.sol)
+
+pragma solidity ^0.8.0;
+
+import "../../utils/Counters.sol";
+import "../../utils/math/SafeCast.sol";
+import "../extensions/IGovernorTimelock.sol";
+import "../Governor.sol";
+import "./IGovernorCompatibilityBravo.sol";
+
+/**
+ * @dev Compatibility layer that implements GovernorBravo compatibility on to of {Governor}.
+ *
+ * This compatibility layer includes a voting system and requires a {IGovernorTimelock} compatible module to be added
+ * through inheritance. It does not include token bindings, not does it include any variable upgrade patterns.
+ *
+ * NOTE: When using this module, you may need to enable the Solidity optimizer to avoid hitting the contract size limit.
+ *
+ * _Available since v4.3._
+ */
+abstract contract GovernorCompatibilityBravo is IGovernorTimelock, IGovernorCompatibilityBravo, Governor {
+    using Counters for Counters.Counter;
+    using Timers for Timers.BlockNumber;
+
+    enum VoteType {
+        Against,
+        For,
+        Abstain
+    }
+
+    struct ProposalDetails {
+        address proposer;
+        address[] targets;
+        uint256[] values;
+        string[] signatures;
+        bytes[] calldatas;
+        uint256 forVotes;
+        uint256 againstVotes;
+        uint256 abstainVotes;
+        mapping(address => Receipt) receipts;
+        bytes32 descriptionHash;
+    }
+
+    mapping(uint256 => ProposalDetails) private _proposalDetails;
+
+    // solhint-disable-next-line func-name-mixedcase
+    function COUNTING_MODE() public pure virtual override returns (string memory) {
+        return "support=bravo&quorum=bravo";
+    }
+
+    // ============================================== Proposal lifecycle ==============================================
+    /**
+     * @dev See {IGovernor-propose}.
+     */
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public virtual override(IGovernor, Governor) returns (uint256) {
+        _storeProposal(_msgSender(), targets, values, new string[](calldatas.length), calldatas, description);
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    /**
+     * @dev See {IGovernorCompatibilityBravo-propose}.
+     */
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        string[] memory signatures,
+        bytes[] memory calldatas,
+        string memory description
+    ) public virtual override returns (uint256) {
+        _storeProposal(_msgSender(), targets, values, signatures, calldatas, description);
+        return propose(targets, values, _encodeCalldata(signatures, calldatas), description);
+    }
+
+    /**
+     * @dev See {IGovernorCompatibilityBravo-queue}.
+     */
+    function queue(uint256 proposalId) public virtual override {
+        ProposalDetails storage details = _proposalDetails[proposalId];
+        queue(
+            details.targets,
+            details.values,
+            _encodeCalldata(details.signatures, details.calldatas),
+            details.descriptionHash
+        );
+    }
+
+    /**
+     * @dev See {IGovernorCompatibilityBravo-execute}.
+     */
+    function execute(uint256 proposalId) public payable virtual override {
+        ProposalDetails storage details = _proposalDetails[proposalId];
+        execute(
+            details.targets,
+            details.values,
+            _encodeCalldata(details.signatures, details.calldatas),
+            details.descriptionHash
+        );
+    }
+
+    function cancel(uint256 proposalId) public virtual override {
+        ProposalDetails storage details = _proposalDetails[proposalId];
+
+        require(
+            _msgSender() == details.proposer || getVotes(details.proposer, block.number - 1) < proposalThreshold(),
+            "GovernorBravo: proposer above threshold"
+        );
+
+        _cancel(
+            details.targets,
+            details.values,
+            _encodeCalldata(details.signatures, details.calldatas),
+            details.descriptionHash
+        );
+    }
+
+    /**
+     * @dev Encodes calldatas with optional function signature.
+     */
+    function _encodeCalldata(string[] memory signatures, bytes[] memory calldatas)
+        private
+        pure
+        returns (bytes[] memory)
+    {
+        bytes[] memory fullcalldatas = new bytes[](calldatas.length);
+
+        for (uint256 i = 0; i < signatures.length; ++i) {
+            fullcalldatas[i] = bytes(signatures[i]).length == 0
+                ? calldatas[i]
+                : abi.encodeWithSignature(signatures[i], calldatas[i]);
+        }
+
+        return fullcalldatas;
+    }
+
+    /**
+     * @dev Store proposal metadata for later lookup
+     */
+    function _storeProposal(
+        address proposer,
+        address[] memory targets,
+        uint256[] memory values,
+        string[] memory signatures,
+        bytes[] memory calldatas,
+        string memory description
+    ) private {
+        bytes32 descriptionHash = keccak256(bytes(description));
+        uint256 proposalId = hashProposal(targets, values, _encodeCalldata(signatures, calldatas), descriptionHash);
+
+        ProposalDetails storage details = _proposalDetails[proposalId];
+        if (details.descriptionHash == bytes32(0)) {
+            details.proposer = proposer;
+            details.targets = targets;
+            details.values = values;
+            details.signatures = signatures;
+            details.calldatas = calldatas;
+            details.descriptionHash = descriptionHash;
+        }
+    }
+
+    // ==================================================== Views =====================================================
+    /**
+     * @dev See {IGovernorCompatibilityBravo-proposals}.
+     */
+    function proposals(uint256 proposalId)
+        public
+        view
+        virtual
+        override
+        returns (
+            uint256 id,
+            address proposer,
+            uint256 eta,
+            uint256 startBlock,
+            uint256 endBlock,
+            uint256 forVotes,
+            uint256 againstVotes,
+            uint256 abstainVotes,
+            bool canceled,
+            bool executed
+        )
+    {
+        id = proposalId;
+        eta = proposalEta(proposalId);
+        startBlock = proposalSnapshot(proposalId);
+        endBlock = proposalDeadline(proposalId);
+
+        ProposalDetails storage details = _proposalDetails[proposalId];
+        proposer = details.proposer;
+        forVotes = details.forVotes;
+        againstVotes = details.againstVotes;
+        abstainVotes = details.abstainVotes;
+
+        ProposalState status = state(proposalId);
+        canceled = status == ProposalState.Canceled;
+        executed = status == ProposalState.Executed;
+    }
+
+    /**
+     * @dev See {IGovernorCompatibilityBravo-getActions}.
+     */
+    function getActions(uint256 proposalId)
+        public
+        view
+        virtual
+        override
+        returns (
+            address[] memory targets,
+            uint256[] memory values,
+            string[] memory signatures,
+            bytes[] memory calldatas
+        )
+    {
+        ProposalDetails storage details = _proposalDetails[proposalId];
+        return (details.targets, details.values, details.signatures, details.calldatas);
+    }
+
+    /**
+     * @dev See {IGovernorCompatibilityBravo-getReceipt}.
+     */
+    function getReceipt(uint256 proposalId, address voter) public view virtual override returns (Receipt memory) {
+        return _proposalDetails[proposalId].receipts[voter];
+    }
+
+    /**
+     * @dev See {IGovernorCompatibilityBravo-quorumVotes}.
+     */
+    function quorumVotes() public view virtual override returns (uint256) {
+        return quorum(block.number - 1);
+    }
+
+    // ==================================================== Voting ====================================================
+    /**
+     * @dev See {IGovernor-hasVoted}.
+     */
+    function hasVoted(uint256 proposalId, address account) public view virtual override returns (bool) {
+        return _proposalDetails[proposalId].receipts[account].hasVoted;
+    }
+
+    /**
+     * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
+     */
+    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;
+    }
+
+    /**
+     * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
+     */
+    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;
+    }
+
+    /**
+     * @dev See {Governor-_countVote}. In this module, the support follows Governor Bravo.
+     */
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal virtual override {
+        ProposalDetails storage details = _proposalDetails[proposalId];
+        Receipt storage receipt = details.receipts[account];
+
+        require(!receipt.hasVoted, "GovernorCompatibilityBravo: vote already cast");
+        receipt.hasVoted = true;
+        receipt.support = support;
+        receipt.votes = SafeCast.toUint96(weight);
+
+        if (support == uint8(VoteType.Against)) {
+            details.againstVotes += weight;
+        } else if (support == uint8(VoteType.For)) {
+            details.forVotes += weight;
+        } else if (support == uint8(VoteType.Abstain)) {
+            details.abstainVotes += weight;
+        } else {
+            revert("GovernorCompatibilityBravo: invalid vote type");
+        }
+    }
+}

certora/munged/governance/compatibility/IGovernorCompatibilityBravo.sol

@@ -0,0 +1,114 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/compatibility/IGovernorCompatibilityBravo.sol)
+
+pragma solidity ^0.8.0;
+
+import "../IGovernor.sol";
+
+/**
+ * @dev Interface extension that adds missing functions to the {Governor} core to provide `GovernorBravo` compatibility.
+ *
+ * _Available since v4.3._
+ */
+abstract contract IGovernorCompatibilityBravo is IGovernor {
+    /**
+     * @dev Proposal structure from Compound Governor Bravo. Not actually used by the compatibility layer, as
+     * {{proposal}} returns a very different structure.
+     */
+    struct Proposal {
+        uint256 id;
+        address proposer;
+        uint256 eta;
+        address[] targets;
+        uint256[] values;
+        string[] signatures;
+        bytes[] calldatas;
+        uint256 startBlock;
+        uint256 endBlock;
+        uint256 forVotes;
+        uint256 againstVotes;
+        uint256 abstainVotes;
+        bool canceled;
+        bool executed;
+        mapping(address => Receipt) receipts;
+    }
+
+    /**
+     * @dev Receipt structure from Compound Governor Bravo
+     */
+    struct Receipt {
+        bool hasVoted;
+        uint8 support;
+        uint96 votes;
+    }
+
+    /**
+     * @dev Part of the Governor Bravo's interface.
+     */
+    function quorumVotes() public view virtual returns (uint256);
+
+    /**
+     * @dev Part of the Governor Bravo's interface: _"The official record of all proposals ever proposed"_.
+     */
+    function proposals(uint256)
+        public
+        view
+        virtual
+        returns (
+            uint256 id,
+            address proposer,
+            uint256 eta,
+            uint256 startBlock,
+            uint256 endBlock,
+            uint256 forVotes,
+            uint256 againstVotes,
+            uint256 abstainVotes,
+            bool canceled,
+            bool executed
+        );
+
+    /**
+     * @dev Part of the Governor Bravo's interface: _"Function used to propose a new proposal"_.
+     */
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        string[] memory signatures,
+        bytes[] memory calldatas,
+        string memory description
+    ) public virtual returns (uint256);
+
+    /**
+     * @dev Part of the Governor Bravo's interface: _"Queues a proposal of state succeeded"_.
+     */
+    function queue(uint256 proposalId) public virtual;
+
+    /**
+     * @dev Part of the Governor Bravo's interface: _"Executes a queued proposal if eta has passed"_.
+     */
+    function execute(uint256 proposalId) public payable virtual;
+
+    /**
+     * @dev Cancels a proposal only if sender is the proposer, or proposer delegates dropped below proposal threshold.
+     */
+    function cancel(uint256 proposalId) public virtual;
+
+    /**
+     * @dev Part of the Governor Bravo's interface: _"Gets actions of a proposal"_.
+     */
+    function getActions(uint256 proposalId)
+        public
+        view
+        virtual
+        returns (
+            address[] memory targets,
+            uint256[] memory values,
+            string[] memory signatures,
+            bytes[] memory calldatas
+        );
+
+    /**
+     * @dev Part of the Governor Bravo's interface: _"Gets the receipt for a voter on a given proposal"_.
+     */
+    function getReceipt(uint256 proposalId, address voter) public view virtual returns (Receipt memory);
+}

certora/munged/governance/extensions/GovernorCountingSimple.sol

@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorCountingSimple.sol)
+
+pragma solidity ^0.8.0;
+
+import "../Governor.sol";
+
+/**
+ * @dev Extension of {Governor} for simple, 3 options, vote counting.
+ *
+ * _Available since v4.3._
+ */
+abstract contract GovernorCountingSimple is Governor {
+    /**
+     * @dev Supported vote types. Matches Governor Bravo ordering.
+     */
+    enum VoteType {
+        Against,
+        For,
+        Abstain
+    }
+
+    struct ProposalVote {
+        uint256 againstVotes;
+        uint256 forVotes;
+        uint256 abstainVotes;
+        mapping(address => bool) hasVoted;
+    }
+
+    mapping(uint256 => ProposalVote) private _proposalVotes;
+
+    /**
+     * @dev See {IGovernor-COUNTING_MODE}.
+     */
+    // solhint-disable-next-line func-name-mixedcase
+    function COUNTING_MODE() public pure virtual override returns (string memory) {
+        return "support=bravo&quorum=for,abstain";
+    }
+
+    /**
+     * @dev See {IGovernor-hasVoted}.
+     */
+    function hasVoted(uint256 proposalId, address account) public view virtual override returns (bool) {
+        return _proposalVotes[proposalId].hasVoted[account];
+    }
+
+    /**
+     * @dev Accessor to the internal vote counts.
+     */
+    function proposalVotes(uint256 proposalId)
+        public
+        view
+        virtual
+        returns (
+            uint256 againstVotes,
+            uint256 forVotes,
+            uint256 abstainVotes
+        )
+    {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return (proposalvote.againstVotes, proposalvote.forVotes, proposalvote.abstainVotes);
+    }
+
+    /**
+     * @dev See {Governor-_quorumReached}.
+     */
+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+
+        return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
+    }
+
+    /**
+     * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
+     */
+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+
+        return proposalvote.forVotes > proposalvote.againstVotes;
+    }
+
+    /**
+     * @dev See {Governor-_countVote}. In this module, the support follows the `VoteType` enum (from Governor Bravo).
+     */
+    function _countVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight
+    ) internal virtual override {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+
+        require(!proposalvote.hasVoted[account], "GovernorVotingSimple: vote already cast");
+        proposalvote.hasVoted[account] = true;
+
+        if (support == uint8(VoteType.Against)) {
+            proposalvote.againstVotes += weight;
+        } else if (support == uint8(VoteType.For)) {
+            proposalvote.forVotes += weight;
+        } else if (support == uint8(VoteType.Abstain)) {
+            proposalvote.abstainVotes += weight;
+        } else {
+            revert("GovernorVotingSimple: invalid value for enum VoteType");
+        }
+    }
+}

certora/munged/governance/extensions/GovernorProposalThreshold.sol

@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorProposalThreshold.sol)
+
+pragma solidity ^0.8.0;
+
+import "../Governor.sol";
+
+/**
+ * @dev Extension of {Governor} for proposal restriction to token holders with a minimum balance.
+ *
+ * _Available since v4.3._
+ * _Deprecated since v4.4._
+ */
+abstract contract GovernorProposalThreshold is Governor {
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public virtual override returns (uint256) {
+        return super.propose(targets, values, calldatas, description);
+    }
+}

certora/munged/governance/extensions/GovernorSettings.sol

@@ -0,0 +1,114 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorSettings.sol)
+
+pragma solidity ^0.8.0;
+
+import "../Governor.sol";
+
+/**
+ * @dev Extension of {Governor} for settings updatable through governance.
+ *
+ * _Available since v4.4._
+ */
+abstract contract GovernorSettings is Governor {
+    uint256 private _votingDelay;
+    uint256 private _votingPeriod;
+    uint256 private _proposalThreshold;
+
+    event VotingDelaySet(uint256 oldVotingDelay, uint256 newVotingDelay);
+    event VotingPeriodSet(uint256 oldVotingPeriod, uint256 newVotingPeriod);
+    event ProposalThresholdSet(uint256 oldProposalThreshold, uint256 newProposalThreshold);
+
+    /**
+     * @dev Initialize the governance parameters.
+     */
+    constructor(
+        uint256 initialVotingDelay,
+        uint256 initialVotingPeriod,
+        uint256 initialProposalThreshold
+    ) {
+        _setVotingDelay(initialVotingDelay);
+        _setVotingPeriod(initialVotingPeriod);
+        _setProposalThreshold(initialProposalThreshold);
+    }
+
+    /**
+     * @dev See {IGovernor-votingDelay}.
+     */
+    function votingDelay() public view virtual override returns (uint256) {
+        return _votingDelay;
+    }
+
+    /**
+     * @dev See {IGovernor-votingPeriod}.
+     */
+    function votingPeriod() public view virtual override returns (uint256) {
+        return _votingPeriod;
+    }
+
+    /**
+     * @dev See {Governor-proposalThreshold}.
+     */
+    function proposalThreshold() public view virtual override returns (uint256) {
+        return _proposalThreshold;
+    }
+
+    /**
+     * @dev Update the voting delay. This operation can only be performed through a governance proposal.
+     *
+     * Emits a {VotingDelaySet} event.
+     */
+    function setVotingDelay(uint256 newVotingDelay) public onlyGovernance {
+        _setVotingDelay(newVotingDelay);
+    }
+
+    /**
+     * @dev Update the voting period. This operation can only be performed through a governance proposal.
+     *
+     * Emits a {VotingPeriodSet} event.
+     */
+    function setVotingPeriod(uint256 newVotingPeriod) public onlyGovernance {
+        _setVotingPeriod(newVotingPeriod);
+    }
+
+    /**
+     * @dev Update the proposal threshold. This operation can only be performed through a governance proposal.
+     *
+     * Emits a {ProposalThresholdSet} event.
+     */
+    function setProposalThreshold(uint256 newProposalThreshold) public onlyGovernance {
+        _setProposalThreshold(newProposalThreshold);
+    }
+
+    /**
+     * @dev Internal setter for the voting delay.
+     *
+     * Emits a {VotingDelaySet} event.
+     */
+    function _setVotingDelay(uint256 newVotingDelay) internal virtual {
+        emit VotingDelaySet(_votingDelay, newVotingDelay);
+        _votingDelay = newVotingDelay;
+    }
+
+    /**
+     * @dev Internal setter for the voting period.
+     *
+     * Emits a {VotingPeriodSet} event.
+     */
+    function _setVotingPeriod(uint256 newVotingPeriod) internal virtual {
+        // voting period must be at least one block long
+        require(newVotingPeriod > 0, "GovernorSettings: voting period too low");
+        emit VotingPeriodSet(_votingPeriod, newVotingPeriod);
+        _votingPeriod = newVotingPeriod;
+    }
+
+    /**
+     * @dev Internal setter for the proposal threshold.
+     *
+     * Emits a {ProposalThresholdSet} event.
+     */
+    function _setProposalThreshold(uint256 newProposalThreshold) internal virtual {
+        emit ProposalThresholdSet(_proposalThreshold, newProposalThreshold);
+        _proposalThreshold = newProposalThreshold;
+    }
+}

certora/munged/governance/extensions/GovernorTimelockCompound.sol

@@ -0,0 +1,244 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorTimelockCompound.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IGovernorTimelock.sol";
+import "../Governor.sol";
+import "../../utils/math/SafeCast.sol";
+
+/**
+ * https://github.com/compound-finance/compound-protocol/blob/master/contracts/Timelock.sol[Compound's timelock] interface
+ */
+interface ICompoundTimelock {
+    receive() external payable;
+
+    // solhint-disable-next-line func-name-mixedcase
+    function GRACE_PERIOD() external view returns (uint256);
+
+    // solhint-disable-next-line func-name-mixedcase
+    function MINIMUM_DELAY() external view returns (uint256);
+
+    // solhint-disable-next-line func-name-mixedcase
+    function MAXIMUM_DELAY() external view returns (uint256);
+
+    function admin() external view returns (address);
+
+    function pendingAdmin() external view returns (address);
+
+    function delay() external view returns (uint256);
+
+    function queuedTransactions(bytes32) external view returns (bool);
+
+    function setDelay(uint256) external;
+
+    function acceptAdmin() external;
+
+    function setPendingAdmin(address) external;
+
+    function queueTransaction(
+        address target,
+        uint256 value,
+        string memory signature,
+        bytes memory data,
+        uint256 eta
+    ) external returns (bytes32);
+
+    function cancelTransaction(
+        address target,
+        uint256 value,
+        string memory signature,
+        bytes memory data,
+        uint256 eta
+    ) external;
+
+    function executeTransaction(
+        address target,
+        uint256 value,
+        string memory signature,
+        bytes memory data,
+        uint256 eta
+    ) external payable returns (bytes memory);
+}
+
+/**
+ * @dev Extension of {Governor} that binds the execution process to a Compound Timelock. This adds a delay, enforced by
+ * the external timelock to all successful proposal (in addition to the voting duration). The {Governor} needs to be
+ * the admin of the timelock for any operation to be performed. A public, unrestricted,
+ * {GovernorTimelockCompound-__acceptAdmin} is available to accept ownership of the timelock.
+ *
+ * Using this model means the proposal will be operated by the {TimelockController} and not by the {Governor}. Thus,
+ * the assets and permissions must be attached to the {TimelockController}. Any asset sent to the {Governor} will be
+ * inaccessible.
+ *
+ * _Available since v4.3._
+ */
+abstract contract GovernorTimelockCompound is IGovernorTimelock, Governor {
+    using SafeCast for uint256;
+    using Timers for Timers.Timestamp;
+
+    struct ProposalTimelock {
+        Timers.Timestamp timer;
+    }
+
+    ICompoundTimelock private _timelock;
+
+    mapping(uint256 => ProposalTimelock) private _proposalTimelocks;
+
+    /**
+     * @dev Emitted when the timelock controller used for proposal execution is modified.
+     */
+    event TimelockChange(address oldTimelock, address newTimelock);
+
+    /**
+     * @dev Set the timelock.
+     */
+    constructor(ICompoundTimelock timelockAddress) {
+        _updateTimelock(timelockAddress);
+    }
+
+    /**
+     * @dev See {IERC165-supportsInterface}.
+     */
+    function supportsInterface(bytes4 interfaceId) public view virtual override(IERC165, Governor) returns (bool) {
+        return interfaceId == type(IGovernorTimelock).interfaceId || super.supportsInterface(interfaceId);
+    }
+
+    /**
+     * @dev Overriden version of the {Governor-state} function with added support for the `Queued` and `Expired` status.
+     */
+    function state(uint256 proposalId) public view virtual override(IGovernor, Governor) returns (ProposalState) {
+        ProposalState status = super.state(proposalId);
+
+        if (status != ProposalState.Succeeded) {
+            return status;
+        }
+
+        uint256 eta = proposalEta(proposalId);
+        if (eta == 0) {
+            return status;
+        } else if (block.timestamp >= eta + _timelock.GRACE_PERIOD()) {
+            return ProposalState.Expired;
+        } else {
+            return ProposalState.Queued;
+        }
+    }
+
+    /**
+     * @dev Public accessor to check the address of the timelock
+     */
+    function timelock() public view virtual override returns (address) {
+        return address(_timelock);
+    }
+
+    /**
+     * @dev Public accessor to check the eta of a queued proposal
+     */
+    function proposalEta(uint256 proposalId) public view virtual override returns (uint256) {
+        return _proposalTimelocks[proposalId].timer.getDeadline();
+    }
+
+    /**
+     * @dev Function to queue a proposal to the timelock.
+     */
+    function queue(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) public virtual override returns (uint256) {
+        uint256 proposalId = hashProposal(targets, values, calldatas, descriptionHash);
+
+        require(state(proposalId) == ProposalState.Succeeded, "Governor: proposal not successful");
+
+        uint256 eta = block.timestamp + _timelock.delay();
+        _proposalTimelocks[proposalId].timer.setDeadline(eta.toUint64());
+        for (uint256 i = 0; i < targets.length; ++i) {
+            require(
+                !_timelock.queuedTransactions(keccak256(abi.encode(targets[i], values[i], "", calldatas[i], eta))),
+                "GovernorTimelockCompound: identical proposal action already queued"
+            );
+            _timelock.queueTransaction(targets[i], values[i], "", calldatas[i], eta);
+        }
+
+        emit ProposalQueued(proposalId, eta);
+
+        return proposalId;
+    }
+
+    /**
+     * @dev Overriden execute function that run the already queued proposal through the timelock.
+     */
+    function _execute(
+        uint256 proposalId,
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 /*descriptionHash*/
+    ) internal virtual override {
+        uint256 eta = proposalEta(proposalId);
+        require(eta > 0, "GovernorTimelockCompound: proposal not yet queued");
+        Address.sendValue(payable(_timelock), msg.value);
+        for (uint256 i = 0; i < targets.length; ++i) {
+            _timelock.executeTransaction(targets[i], values[i], "", calldatas[i], eta);
+        }
+    }
+
+    /**
+     * @dev Overriden version of the {Governor-_cancel} function to cancel the timelocked proposal if it as already
+     * been queued.
+     */
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal virtual override returns (uint256) {
+        uint256 proposalId = super._cancel(targets, values, calldatas, descriptionHash);
+
+        uint256 eta = proposalEta(proposalId);
+        if (eta > 0) {
+            for (uint256 i = 0; i < targets.length; ++i) {
+                _timelock.cancelTransaction(targets[i], values[i], "", calldatas[i], eta);
+            }
+            _proposalTimelocks[proposalId].timer.reset();
+        }
+
+        return proposalId;
+    }
+
+    /**
+     * @dev Address through which the governor executes action. In this case, the timelock.
+     */
+    function _executor() internal view virtual override returns (address) {
+        return address(_timelock);
+    }
+
+    /**
+     * @dev Accept admin right over the timelock.
+     */
+    // solhint-disable-next-line private-vars-leading-underscore
+    function __acceptAdmin() public {
+        _timelock.acceptAdmin();
+    }
+
+    /**
+     * @dev Public endpoint to update the underlying timelock instance. Restricted to the timelock itself, so updates
+     * must be proposed, scheduled and executed using the {Governor} workflow.
+     *
+     * For security reason, the timelock must be handed over to another admin before setting up a new one. The two
+     * operations (hand over the timelock) and do the update can be batched in a single proposal.
+     *
+     * Note that if the timelock admin has been handed over in a previous operation, we refuse updates made through the
+     * timelock if admin of the timelock has already been accepted and the operation is executed outside the scope of
+     * governance.
+     */
+    function updateTimelock(ICompoundTimelock newTimelock) external virtual onlyGovernance {
+        _updateTimelock(newTimelock);
+    }
+
+    function _updateTimelock(ICompoundTimelock newTimelock) private {
+        emit TimelockChange(address(_timelock), address(newTimelock));
+        _timelock = newTimelock;
+    }
+}

certora/munged/governance/extensions/GovernorTimelockControl.sol

@@ -0,0 +1,154 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorTimelockControl.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IGovernorTimelock.sol";
+import "../Governor.sol";
+import "../TimelockController.sol";
+
+/**
+ * @dev Extension of {Governor} that binds the execution process to an instance of {TimelockController}. This adds a
+ * delay, enforced by the {TimelockController} to all successful proposal (in addition to the voting duration). The
+ * {Governor} needs the proposer (an ideally the executor) roles for the {Governor} to work properly.
+ *
+ * Using this model means the proposal will be operated by the {TimelockController} and not by the {Governor}. Thus,
+ * the assets and permissions must be attached to the {TimelockController}. Any asset sent to the {Governor} will be
+ * inaccessible.
+ *
+ * _Available since v4.3._
+ */
+abstract contract GovernorTimelockControl is IGovernorTimelock, Governor {
+    TimelockController private _timelock;
+    mapping(uint256 => bytes32) private _timelockIds;
+
+    /**
+     * @dev Emitted when the timelock controller used for proposal execution is modified.
+     */
+    event TimelockChange(address oldTimelock, address newTimelock);
+
+    /**
+     * @dev Set the timelock.
+     */
+    constructor(TimelockController timelockAddress) {
+        _updateTimelock(timelockAddress);
+    }
+
+    /**
+     * @dev See {IERC165-supportsInterface}.
+     */
+    function supportsInterface(bytes4 interfaceId) public view virtual override(IERC165, Governor) returns (bool) {
+        return interfaceId == type(IGovernorTimelock).interfaceId || super.supportsInterface(interfaceId);
+    }
+
+    /**
+     * @dev Overriden version of the {Governor-state} function with added support for the `Queued` status.
+     */
+    function state(uint256 proposalId) public view virtual override(IGovernor, Governor) returns (ProposalState) {
+        ProposalState status = super.state(proposalId);
+
+        if (status != ProposalState.Succeeded) {
+            return status;
+        }
+
+        // core tracks execution, so we just have to check if successful proposal have been queued.
+        bytes32 queueid = _timelockIds[proposalId];
+        if (queueid == bytes32(0)) {
+            return status;
+        } else if (_timelock.isOperationDone(queueid)) {
+            return ProposalState.Executed;
+        } else {
+            return ProposalState.Queued;
+        }
+    }
+
+    /**
+     * @dev Public accessor to check the address of the timelock
+     */
+    function timelock() public view virtual override returns (address) {
+        return address(_timelock);
+    }
+
+    /**
+     * @dev Public accessor to check the eta of a queued proposal
+     */
+    function proposalEta(uint256 proposalId) public view virtual override returns (uint256) {
+        uint256 eta = _timelock.getTimestamp(_timelockIds[proposalId]);
+        return eta == 1 ? 0 : eta; // _DONE_TIMESTAMP (1) should be replaced with a 0 value
+    }
+
+    /**
+     * @dev Function to queue a proposal to the timelock.
+     */
+    function queue(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) public virtual override returns (uint256) {
+        uint256 proposalId = hashProposal(targets, values, calldatas, descriptionHash);
+
+        require(state(proposalId) == ProposalState.Succeeded, "Governor: proposal not successful");
+
+        uint256 delay = _timelock.getMinDelay();
+        _timelockIds[proposalId] = _timelock.hashOperationBatch(targets, values, calldatas, 0, descriptionHash);
+        _timelock.scheduleBatch(targets, values, calldatas, 0, descriptionHash, delay);
+
+        emit ProposalQueued(proposalId, block.timestamp + delay);
+
+        return proposalId;
+    }
+
+    /**
+     * @dev Overriden execute function that run the already queued proposal through the timelock.
+     */
+    function _execute(
+        uint256, /* proposalId */
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal virtual override {
+         _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
+    }
+
+    /**
+     * @dev Overriden version of the {Governor-_cancel} function to cancel the timelocked proposal if it as already
+     * been queued.
+     */
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal virtual override returns (uint256) {
+        uint256 proposalId = super._cancel(targets, values, calldatas, descriptionHash);
+
+        if (_timelockIds[proposalId] != 0) {
+            _timelock.cancel(_timelockIds[proposalId]);
+            delete _timelockIds[proposalId];
+        }
+
+        return proposalId;
+    }
+
+    /**
+     * @dev Address through which the governor executes action. In this case, the timelock.
+     */
+    function _executor() internal view virtual override returns (address) {
+        return address(_timelock);
+    }
+
+    /**
+     * @dev Public endpoint to update the underlying timelock instance. Restricted to the timelock itself, so updates
+     * must be proposed, scheduled and executed using the {Governor} workflow.
+     */
+    function updateTimelock(TimelockController newTimelock) external virtual onlyGovernance {
+        _updateTimelock(newTimelock);
+    }
+
+    function _updateTimelock(TimelockController newTimelock) private {
+        emit TimelockChange(address(_timelock), address(newTimelock));
+        _timelock = newTimelock;
+    }
+}

certora/munged/governance/extensions/GovernorVotes.sol

@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorVotes.sol)
+
+pragma solidity ^0.8.0;
+
+import "../Governor.sol";
+import "../../token/ERC20/extensions/ERC20Votes.sol";
+import "../../utils/math/Math.sol";
+
+/**
+ * @dev Extension of {Governor} for voting weight extraction from an {ERC20Votes} token.
+ *
+ * _Available since v4.3._
+ */
+abstract contract GovernorVotes is Governor {
+    ERC20Votes public immutable token;
+
+    constructor(ERC20Votes tokenAddress) {
+        token = tokenAddress;
+    }
+
+    /**
+     * Read the voting weight from the token's built in snapshot mechanism (see {IGovernor-getVotes}).
+     */
+    function getVotes(address account, uint256 blockNumber) public view virtual override returns (uint256) {
+        return token.getPastVotes(account, blockNumber);
+    }
+}

certora/munged/governance/extensions/GovernorVotesComp.sol

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorVotesComp.sol)
+
+pragma solidity ^0.8.0;
+
+import "../Governor.sol";
+import "../../token/ERC20/extensions/ERC20VotesComp.sol";
+
+/**
+ * @dev Extension of {Governor} for voting weight extraction from a Comp token.
+ *
+ * _Available since v4.3._
+ */
+abstract contract GovernorVotesComp is Governor {
+    ERC20VotesComp public immutable token;
+
+    constructor(ERC20VotesComp token_) {
+        token = token_;
+    }
+
+    /**
+     * Read the voting weight from the token's built in snapshot mechanism (see {IGovernor-getVotes}).
+     */
+    function getVotes(address account, uint256 blockNumber) public view virtual override returns (uint256) {
+        return token.getPriorVotes(account, blockNumber);
+    }
+}

certora/munged/governance/extensions/GovernorVotesQuorumFraction.sol

@@ -0,0 +1,50 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/GovernorVotesQuorumFraction.sol)
+
+pragma solidity ^0.8.0;
+
+import "./GovernorVotes.sol";
+
+/**
+ * @dev Extension of {Governor} for voting weight extraction from an {ERC20Votes} token and a quorum expressed as a
+ * fraction of the total supply.
+ *
+ * _Available since v4.3._
+ */
+abstract contract GovernorVotesQuorumFraction is GovernorVotes {
+    uint256 private _quorumNumerator;
+
+    event QuorumNumeratorUpdated(uint256 oldQuorumNumerator, uint256 newQuorumNumerator);
+
+    constructor(uint256 quorumNumeratorValue) {
+        _updateQuorumNumerator(quorumNumeratorValue);
+    }
+
+    function quorumNumerator() public view virtual returns (uint256) {
+        return _quorumNumerator;
+    }
+
+    function quorumDenominator() public view virtual returns (uint256) {
+        return 100;
+    }
+
+    function quorum(uint256 blockNumber) public view virtual override returns (uint256) {
+        return (token.getPastTotalSupply(blockNumber) * quorumNumerator()) / quorumDenominator();
+    }
+
+    function updateQuorumNumerator(uint256 newQuorumNumerator) external virtual onlyGovernance {
+        _updateQuorumNumerator(newQuorumNumerator);
+    }
+
+    function _updateQuorumNumerator(uint256 newQuorumNumerator) internal virtual {
+        require(
+            newQuorumNumerator <= quorumDenominator(),
+            "GovernorVotesQuorumFraction: quorumNumerator over quorumDenominator"
+        );
+
+        uint256 oldQuorumNumerator = _quorumNumerator;
+        _quorumNumerator = newQuorumNumerator;
+
+        emit QuorumNumeratorUpdated(oldQuorumNumerator, newQuorumNumerator);
+    }
+}

certora/munged/governance/extensions/IGovernorTimelock.sol

@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (governance/extensions/IGovernorTimelock.sol)
+
+pragma solidity ^0.8.0;
+
+import "../IGovernor.sol";
+
+/**
+ * @dev Extension of the {IGovernor} for timelock supporting modules.
+ *
+ * _Available since v4.3._
+ */
+abstract contract IGovernorTimelock is IGovernor {
+    event ProposalQueued(uint256 proposalId, uint256 eta);
+
+    function timelock() public view virtual returns (address);
+
+    function proposalEta(uint256 proposalId) public view virtual returns (uint256);
+
+    function queue(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) public virtual returns (uint256 proposalId);
+}

certora/munged/interfaces/IERC1155.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1155.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC1155/IERC1155.sol";

certora/munged/interfaces/IERC1155MetadataURI.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1155MetadataURI.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC1155/extensions/IERC1155MetadataURI.sol";

certora/munged/interfaces/IERC1155Receiver.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1155Receiver.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC1155/IERC1155Receiver.sol";

certora/munged/interfaces/IERC1271.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1271.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Interface of the ERC1271 standard signature validation method for
+ * contracts as defined in https://eips.ethereum.org/EIPS/eip-1271[ERC-1271].
+ *
+ * _Available since v4.1._
+ */
+interface IERC1271 {
+    /**
+     * @dev Should return whether the signature provided is valid for the provided data
+     * @param hash      Hash of the data to be signed
+     * @param signature Signature byte array associated with _data
+     */
+    function isValidSignature(bytes32 hash, bytes memory signature) external view returns (bytes4 magicValue);
+}

certora/munged/interfaces/IERC1363.sol

@@ -0,0 +1,95 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1363.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IERC20.sol";
+import "./IERC165.sol";
+
+interface IERC1363 is IERC165, IERC20 {
+    /*
+     * Note: the ERC-165 identifier for this interface is 0x4bbee2df.
+     * 0x4bbee2df ===
+     *   bytes4(keccak256('transferAndCall(address,uint256)')) ^
+     *   bytes4(keccak256('transferAndCall(address,uint256,bytes)')) ^
+     *   bytes4(keccak256('transferFromAndCall(address,address,uint256)')) ^
+     *   bytes4(keccak256('transferFromAndCall(address,address,uint256,bytes)'))
+     */
+
+    /*
+     * Note: the ERC-165 identifier for this interface is 0xfb9ec8ce.
+     * 0xfb9ec8ce ===
+     *   bytes4(keccak256('approveAndCall(address,uint256)')) ^
+     *   bytes4(keccak256('approveAndCall(address,uint256,bytes)'))
+     */
+
+    /**
+     * @dev Transfer tokens from `msg.sender` to another address and then call `onTransferReceived` on receiver
+     * @param to address The address which you want to transfer to
+     * @param value uint256 The amount of tokens to be transferred
+     * @return true unless throwing
+     */
+    function transferAndCall(address to, uint256 value) external returns (bool);
+
+    /**
+     * @dev Transfer tokens from `msg.sender` to another address and then call `onTransferReceived` on receiver
+     * @param to address The address which you want to transfer to
+     * @param value uint256 The amount of tokens to be transferred
+     * @param data bytes Additional data with no specified format, sent in call to `to`
+     * @return true unless throwing
+     */
+    function transferAndCall(
+        address to,
+        uint256 value,
+        bytes memory data
+    ) external returns (bool);
+
+    /**
+     * @dev Transfer tokens from one address to another and then call `onTransferReceived` on receiver
+     * @param from address The address which you want to send tokens from
+     * @param to address The address which you want to transfer to
+     * @param value uint256 The amount of tokens to be transferred
+     * @return true unless throwing
+     */
+    function transferFromAndCall(
+        address from,
+        address to,
+        uint256 value
+    ) external returns (bool);
+
+    /**
+     * @dev Transfer tokens from one address to another and then call `onTransferReceived` on receiver
+     * @param from address The address which you want to send tokens from
+     * @param to address The address which you want to transfer to
+     * @param value uint256 The amount of tokens to be transferred
+     * @param data bytes Additional data with no specified format, sent in call to `to`
+     * @return true unless throwing
+     */
+    function transferFromAndCall(
+        address from,
+        address to,
+        uint256 value,
+        bytes memory data
+    ) external returns (bool);
+
+    /**
+     * @dev Approve the passed address to spend the specified amount of tokens on behalf of msg.sender
+     * and then call `onApprovalReceived` on spender.
+     * @param spender address The address which will spend the funds
+     * @param value uint256 The amount of tokens to be spent
+     */
+    function approveAndCall(address spender, uint256 value) external returns (bool);
+
+    /**
+     * @dev Approve the passed address to spend the specified amount of tokens on behalf of msg.sender
+     * and then call `onApprovalReceived` on spender.
+     * @param spender address The address which will spend the funds
+     * @param value uint256 The amount of tokens to be spent
+     * @param data bytes Additional data with no specified format, sent in call to `spender`
+     */
+    function approveAndCall(
+        address spender,
+        uint256 value,
+        bytes memory data
+    ) external returns (bool);
+}

certora/munged/interfaces/IERC1363Receiver.sol

@@ -0,0 +1,32 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1363Receiver.sol)
+
+pragma solidity ^0.8.0;
+
+interface IERC1363Receiver {
+    /*
+     * Note: the ERC-165 identifier for this interface is 0x88a7ca5c.
+     * 0x88a7ca5c === bytes4(keccak256("onTransferReceived(address,address,uint256,bytes)"))
+     */
+
+    /**
+     * @notice Handle the receipt of ERC1363 tokens
+     * @dev Any ERC1363 smart contract calls this function on the recipient
+     * after a `transfer` or a `transferFrom`. This function MAY throw to revert and reject the
+     * transfer. Return of other than the magic value MUST result in the
+     * transaction being reverted.
+     * Note: the token contract address is always the message sender.
+     * @param operator address The address which called `transferAndCall` or `transferFromAndCall` function
+     * @param from address The address which are token transferred from
+     * @param value uint256 The amount of tokens transferred
+     * @param data bytes Additional data with no specified format
+     * @return `bytes4(keccak256("onTransferReceived(address,address,uint256,bytes)"))`
+     *  unless throwing
+     */
+    function onTransferReceived(
+        address operator,
+        address from,
+        uint256 value,
+        bytes memory data
+    ) external returns (bytes4);
+}

certora/munged/interfaces/IERC1363Spender.sol

@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1363Spender.sol)
+
+pragma solidity ^0.8.0;
+
+interface IERC1363Spender {
+    /*
+     * Note: the ERC-165 identifier for this interface is 0x7b04a2d0.
+     * 0x7b04a2d0 === bytes4(keccak256("onApprovalReceived(address,uint256,bytes)"))
+     */
+
+    /**
+     * @notice Handle the approval of ERC1363 tokens
+     * @dev Any ERC1363 smart contract calls this function on the recipient
+     * after an `approve`. This function MAY throw to revert and reject the
+     * approval. Return of other than the magic value MUST result in the
+     * transaction being reverted.
+     * Note: the token contract address is always the message sender.
+     * @param owner address The address which called `approveAndCall` function
+     * @param value uint256 The amount of tokens to be spent
+     * @param data bytes Additional data with no specified format
+     * @return `bytes4(keccak256("onApprovalReceived(address,uint256,bytes)"))`
+     *  unless throwing
+     */
+    function onApprovalReceived(
+        address owner,
+        uint256 value,
+        bytes memory data
+    ) external returns (bytes4);
+}

certora/munged/interfaces/IERC165.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC165.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/IERC165.sol";

certora/munged/interfaces/IERC1820Implementer.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1820Implementer.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/IERC1820Implementer.sol";

certora/munged/interfaces/IERC1820Registry.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC1820Registry.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/IERC1820Registry.sol";

certora/munged/interfaces/IERC20.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC20.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/IERC20.sol";

certora/munged/interfaces/IERC20Metadata.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC20Metadata.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/IERC20Metadata.sol";

certora/munged/interfaces/IERC2981.sol

@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC2981.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IERC165.sol";
+
+/**
+ * @dev Interface for the NFT Royalty Standard
+ */
+interface IERC2981 is IERC165 {
+    /**
+     * @dev Called with the sale price to determine how much royalty is owed and to whom.
+     * @param tokenId - the NFT asset queried for royalty information
+     * @param salePrice - the sale price of the NFT asset specified by `tokenId`
+     * @return receiver - address of who should be sent the royalty payment
+     * @return royaltyAmount - the royalty payment amount for `salePrice`
+     */
+    function royaltyInfo(uint256 tokenId, uint256 salePrice)
+        external
+        view
+        returns (address receiver, uint256 royaltyAmount);
+}

certora/munged/interfaces/IERC3156.sol

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC3156.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IERC3156FlashBorrower.sol";
+import "./IERC3156FlashLender.sol";

certora/munged/interfaces/IERC3156FlashBorrower.sol

@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC3156FlashBorrower.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Interface of the ERC3156 FlashBorrower, as defined in
+ * https://eips.ethereum.org/EIPS/eip-3156[ERC-3156].
+ *
+ * _Available since v4.1._
+ */
+interface IERC3156FlashBorrower {
+    /**
+     * @dev Receive a flash loan.
+     * @param initiator The initiator of the loan.
+     * @param token The loan currency.
+     * @param amount The amount of tokens lent.
+     * @param fee The additional amount of tokens to repay.
+     * @param data Arbitrary data structure, intended to contain user-defined parameters.
+     * @return The keccak256 hash of "ERC3156FlashBorrower.onFlashLoan"
+     */
+    function onFlashLoan(
+        address initiator,
+        address token,
+        uint256 amount,
+        uint256 fee,
+        bytes calldata data
+    ) external returns (bytes32);
+}

certora/munged/interfaces/IERC3156FlashLender.sol

@@ -0,0 +1,43 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC3156FlashLender.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IERC3156FlashBorrower.sol";
+
+/**
+ * @dev Interface of the ERC3156 FlashLender, as defined in
+ * https://eips.ethereum.org/EIPS/eip-3156[ERC-3156].
+ *
+ * _Available since v4.1._
+ */
+interface IERC3156FlashLender {
+    /**
+     * @dev The amount of currency available to be lended.
+     * @param token The loan currency.
+     * @return The amount of `token` that can be borrowed.
+     */
+    function maxFlashLoan(address token) external view returns (uint256);
+
+    /**
+     * @dev The fee to be charged for a given loan.
+     * @param token The loan currency.
+     * @param amount The amount of tokens lent.
+     * @return The amount of `token` to be charged for the loan, on top of the returned principal.
+     */
+    function flashFee(address token, uint256 amount) external view returns (uint256);
+
+    /**
+     * @dev Initiate a flash loan.
+     * @param receiver The receiver of the tokens in the loan, and the receiver of the callback.
+     * @param token The loan currency.
+     * @param amount The amount of tokens lent.
+     * @param data Arbitrary data structure, intended to contain user-defined parameters.
+     */
+    function flashLoan(
+        IERC3156FlashBorrower receiver,
+        address token,
+        uint256 amount,
+        bytes calldata data
+    ) external returns (bool);
+}

certora/munged/interfaces/IERC721.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC721.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/IERC721.sol";

certora/munged/interfaces/IERC721Enumerable.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC721Enumerable.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/extensions/IERC721Enumerable.sol";

certora/munged/interfaces/IERC721Metadata.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC721Metadata.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/extensions/IERC721Metadata.sol";

certora/munged/interfaces/IERC721Receiver.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC721Receiver.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/IERC721Receiver.sol";

certora/munged/interfaces/IERC777.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC777.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC777/IERC777.sol";

certora/munged/interfaces/IERC777Recipient.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC777Recipient.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC777/IERC777Recipient.sol";

certora/munged/interfaces/IERC777Sender.sol

@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/IERC777Sender.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC777/IERC777Sender.sol";

certora/munged/interfaces/README.adoc

@@ -0,0 +1,50 @@
+= Interfaces
+
+[.readme-notice]
+NOTE: This document is better viewed at https://docs.openzeppelin.com/contracts/api/interfaces
+
+== List of standardized interfaces
+These interfaces are available as `.sol` files, and also as compiler `.json` ABI files (through the npm package). These
+are usefull to interract with third party contracts that implement them.
+
+- {IERC20}
+- {IERC20Metadata}
+- {IERC165}
+- {IERC721}
+- {IERC721Receiver}
+- {IERC721Enumerable}
+- {IERC721Metadata}
+- {IERC777}
+- {IERC777Recipient}
+- {IERC777Sender}
+- {IERC1155}
+- {IERC1155Receiver}
+- {IERC1155MetadataURI}
+- {IERC1271}
+- {IERC1363}
+- {IERC1820Implementer}
+- {IERC1820Registry}
+- {IERC2612}
+- {IERC2981}
+- {IERC3156FlashLender}
+- {IERC3156FlashBorrower}
+
+== Detailed ABI
+
+{{IERC1271}}
+
+{{IERC1363}}
+
+{{IERC1363Receiver}}
+
+{{IERC1820Implementer}}
+
+{{IERC1820Registry}}
+
+{{IERC2612}}
+
+{{IERC2981}}
+
+{{IERC3156FlashLender}}
+
+{{IERC3156FlashBorrower}}

certora/munged/interfaces/draft-IERC2612.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (interfaces/draft-IERC2612.sol)
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/draft-IERC20Permit.sol";
+
+interface IERC2612 is IERC20Permit {}

certora/munged/metatx/ERC2771Context.sol

@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (metatx/ERC2771Context.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/Context.sol";
+
+/**
+ * @dev Context variant with ERC2771 support.
+ */
+abstract contract ERC2771Context is Context {
+    address private _trustedForwarder;
+
+    constructor(address trustedForwarder) {
+        _trustedForwarder = trustedForwarder;
+    }
+
+    function isTrustedForwarder(address forwarder) public view virtual returns (bool) {
+        return forwarder == _trustedForwarder;
+    }
+
+    function _msgSender() internal view virtual override returns (address sender) {
+        if (isTrustedForwarder(msg.sender)) {
+            // The assembly code is more direct than the Solidity version using `abi.decode`.
+            assembly {
+                sender := shr(96, calldataload(sub(calldatasize(), 20)))
+            }
+        } else {
+            return super._msgSender();
+        }
+    }
+
+    function _msgData() internal view virtual override returns (bytes calldata) {
+        if (isTrustedForwarder(msg.sender)) {
+            return msg.data[:msg.data.length - 20];
+        } else {
+            return super._msgData();
+        }
+    }
+}

certora/munged/metatx/MinimalForwarder.sol

@@ -0,0 +1,59 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.3.2 (metatx/MinimalForwarder.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/cryptography/ECDSA.sol";
+import "../utils/cryptography/draft-EIP712.sol";
+
+/**
+ * @dev Simple minimal forwarder to be used together with an ERC2771 compatible contract. See {ERC2771Context}.
+ */
+contract MinimalForwarder is EIP712 {
+    using ECDSA for bytes32;
+
+    struct ForwardRequest {
+        address from;
+        address to;
+        uint256 value;
+        uint256 gas;
+        uint256 nonce;
+        bytes data;
+    }
+
+    bytes32 private constant _TYPEHASH =
+        keccak256("ForwardRequest(address from,address to,uint256 value,uint256 gas,uint256 nonce,bytes data)");
+
+    mapping(address => uint256) private _nonces;
+
+    constructor() EIP712("MinimalForwarder", "0.0.1") {}
+
+    function getNonce(address from) public view returns (uint256) {
+        return _nonces[from];
+    }
+
+    function verify(ForwardRequest calldata req, bytes calldata signature) public view returns (bool) {
+        address signer = _hashTypedDataV4(
+            keccak256(abi.encode(_TYPEHASH, req.from, req.to, req.value, req.gas, req.nonce, keccak256(req.data)))
+        ).recover(signature);
+        return _nonces[req.from] == req.nonce && signer == req.from;
+    }
+
+    function execute(ForwardRequest calldata req, bytes calldata signature)
+        public
+        payable
+        returns (bool, bytes memory)
+    {
+        require(verify(req, signature), "MinimalForwarder: signature does not match request");
+        _nonces[req.from] = req.nonce + 1;
+
+        (bool success, bytes memory returndata) = req.to.call{gas: req.gas, value: req.value}(
+            abi.encodePacked(req.data, req.from)
+        );
+        // Validate that the relayer has sent enough gas for the call.
+        // See https://ronan.eth.link/blog/ethereum-gas-dangers/
+        assert(gasleft() > req.gas / 63);
+
+        return (success, returndata);
+    }
+}

certora/munged/metatx/README.adoc

@@ -0,0 +1,12 @@
+= Meta Transactions
+
+[.readme-notice]
+NOTE: This document is better viewed at https://docs.openzeppelin.com/contracts/api/metatx
+
+== Core
+
+{{ERC2771Context}}
+
+== Utils
+
+{{MinimalForwarder}}

certora/munged/mocks/AccessControlEnumerableMock.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../access/AccessControlEnumerable.sol";
+
+contract AccessControlEnumerableMock is AccessControlEnumerable {
+    constructor() {
+        _setupRole(DEFAULT_ADMIN_ROLE, _msgSender());
+    }
+
+    function setRoleAdmin(bytes32 roleId, bytes32 adminRoleId) public {
+        _setRoleAdmin(roleId, adminRoleId);
+    }
+
+    function senderProtected(bytes32 roleId) public onlyRole(roleId) {}
+}

certora/munged/mocks/AccessControlMock.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../access/AccessControl.sol";
+
+contract AccessControlMock is AccessControl {
+    constructor() {
+        _setupRole(DEFAULT_ADMIN_ROLE, _msgSender());
+    }
+
+    function setRoleAdmin(bytes32 roleId, bytes32 adminRoleId) public {
+        _setRoleAdmin(roleId, adminRoleId);
+    }
+
+    function senderProtected(bytes32 roleId) public onlyRole(roleId) {}
+}

certora/munged/mocks/AddressImpl.sol

@@ -0,0 +1,46 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/Address.sol";
+
+contract AddressImpl {
+    string public sharedAnswer;
+
+    event CallReturnValue(string data);
+
+    function isContract(address account) external view returns (bool) {
+        return Address.isContract(account);
+    }
+
+    function sendValue(address payable receiver, uint256 amount) external {
+        Address.sendValue(receiver, amount);
+    }
+
+    function functionCall(address target, bytes calldata data) external {
+        bytes memory returnData = Address.functionCall(target, data);
+        emit CallReturnValue(abi.decode(returnData, (string)));
+    }
+
+    function functionCallWithValue(
+        address target,
+        bytes calldata data,
+        uint256 value
+    ) external payable {
+        bytes memory returnData = Address.functionCallWithValue(target, data, value);
+        emit CallReturnValue(abi.decode(returnData, (string)));
+    }
+
+    function functionStaticCall(address target, bytes calldata data) external {
+        bytes memory returnData = Address.functionStaticCall(target, data);
+        emit CallReturnValue(abi.decode(returnData, (string)));
+    }
+
+    function functionDelegateCall(address target, bytes calldata data) external {
+        bytes memory returnData = Address.functionDelegateCall(target, data);
+        emit CallReturnValue(abi.decode(returnData, (string)));
+    }
+
+    // sendValue's tests require the contract to hold Ether
+    receive() external payable {}
+}

certora/munged/mocks/ArraysImpl.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/Arrays.sol";
+
+contract ArraysImpl {
+    using Arrays for uint256[];
+
+    uint256[] private _array;
+
+    constructor(uint256[] memory array) {
+        _array = array;
+    }
+
+    function findUpperBound(uint256 element) external view returns (uint256) {
+        return _array.findUpperBound(element);
+    }
+}

certora/munged/mocks/BadBeacon.sol

@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+contract BadBeaconNoImpl {}
+
+contract BadBeaconNotContract {
+    function implementation() external pure returns (address) {
+        return address(0x1);
+    }
+}

certora/munged/mocks/BitmapMock.sol

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/structs/BitMaps.sol";
+
+contract BitMapMock {
+    using BitMaps for BitMaps.BitMap;
+
+    BitMaps.BitMap private _bitmap;
+
+    function get(uint256 index) public view returns (bool) {
+        return _bitmap.get(index);
+    }
+
+    function setTo(uint256 index, bool value) public {
+        _bitmap.setTo(index, value);
+    }
+
+    function set(uint256 index) public {
+        _bitmap.set(index);
+    }
+
+    function unset(uint256 index) public {
+        _bitmap.unset(index);
+    }
+}

certora/munged/mocks/CallReceiverMock.sol

@@ -0,0 +1,50 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+contract CallReceiverMock {
+    string public sharedAnswer;
+
+    event MockFunctionCalled();
+
+    uint256[] private _array;
+
+    function mockFunction() public payable returns (string memory) {
+        emit MockFunctionCalled();
+
+        return "0x1234";
+    }
+
+    function mockFunctionNonPayable() public returns (string memory) {
+        emit MockFunctionCalled();
+
+        return "0x1234";
+    }
+
+    function mockStaticFunction() public pure returns (string memory) {
+        return "0x1234";
+    }
+
+    function mockFunctionRevertsNoReason() public payable {
+        revert();
+    }
+
+    function mockFunctionRevertsReason() public payable {
+        revert("CallReceiverMock: reverting");
+    }
+
+    function mockFunctionThrows() public payable {
+        assert(false);
+    }
+
+    function mockFunctionOutOfGas() public payable {
+        for (uint256 i = 0; ; ++i) {
+            _array.push(i);
+        }
+    }
+
+    function mockFunctionWritesStorage() public returns (string memory) {
+        sharedAnswer = "42";
+        return "0x1234";
+    }
+}

certora/munged/mocks/ClashingImplementation.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Implementation contract with an admin() function made to clash with
+ * @dev TransparentUpgradeableProxy's to test correct functioning of the
+ * @dev Transparent Proxy feature.
+ */
+contract ClashingImplementation {
+    function admin() external pure returns (address) {
+        return 0x0000000000000000000000000000000011111142;
+    }
+
+    function delegatedFunction() external pure returns (bool) {
+        return true;
+    }
+}

certora/munged/mocks/ClonesMock.sol

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../proxy/Clones.sol";
+import "../utils/Address.sol";
+
+contract ClonesMock {
+    using Address for address;
+    using Clones for address;
+
+    event NewInstance(address instance);
+
+    function clone(address implementation, bytes calldata initdata) public payable {
+        _initAndEmit(implementation.clone(), initdata);
+    }
+
+    function cloneDeterministic(
+        address implementation,
+        bytes32 salt,
+        bytes calldata initdata
+    ) public payable {
+        _initAndEmit(implementation.cloneDeterministic(salt), initdata);
+    }
+
+    function predictDeterministicAddress(address implementation, bytes32 salt) public view returns (address predicted) {
+        return implementation.predictDeterministicAddress(salt);
+    }
+
+    function _initAndEmit(address instance, bytes memory initdata) private {
+        if (initdata.length > 0) {
+            instance.functionCallWithValue(initdata, msg.value);
+        }
+        emit NewInstance(instance);
+    }
+}

certora/munged/mocks/ConditionalEscrowMock.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/escrow/ConditionalEscrow.sol";
+
+// mock class using ConditionalEscrow
+contract ConditionalEscrowMock is ConditionalEscrow {
+    mapping(address => bool) private _allowed;
+
+    function setAllowed(address payee, bool allowed) public {
+        _allowed[payee] = allowed;
+    }
+
+    function withdrawalAllowed(address payee) public view override returns (bool) {
+        return _allowed[payee];
+    }
+}

certora/munged/mocks/ContextMock.sol

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/Context.sol";
+
+contract ContextMock is Context {
+    event Sender(address sender);
+
+    function msgSender() public {
+        emit Sender(_msgSender());
+    }
+
+    event Data(bytes data, uint256 integerValue, string stringValue);
+
+    function msgData(uint256 integerValue, string memory stringValue) public {
+        emit Data(_msgData(), integerValue, stringValue);
+    }
+}
+
+contract ContextMockCaller {
+    function callSender(ContextMock context) public {
+        context.msgSender();
+    }
+
+    function callData(
+        ContextMock context,
+        uint256 integerValue,
+        string memory stringValue
+    ) public {
+        context.msgData(integerValue, stringValue);
+    }
+}

certora/munged/mocks/CountersImpl.sol

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/Counters.sol";
+
+contract CountersImpl {
+    using Counters for Counters.Counter;
+
+    Counters.Counter private _counter;
+
+    function current() public view returns (uint256) {
+        return _counter.current();
+    }
+
+    function increment() public {
+        _counter.increment();
+    }
+
+    function decrement() public {
+        _counter.decrement();
+    }
+
+    function reset() public {
+        _counter.reset();
+    }
+}

certora/munged/mocks/Create2Impl.sol

@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/Create2.sol";
+import "../utils/introspection/ERC1820Implementer.sol";
+
+contract Create2Impl {
+    function deploy(
+        uint256 value,
+        bytes32 salt,
+        bytes memory code
+    ) public {
+        Create2.deploy(value, salt, code);
+    }
+
+    function deployERC1820Implementer(uint256 value, bytes32 salt) public {
+        Create2.deploy(value, salt, type(ERC1820Implementer).creationCode);
+    }
+
+    function computeAddress(bytes32 salt, bytes32 codeHash) public view returns (address) {
+        return Create2.computeAddress(salt, codeHash);
+    }
+
+    function computeAddressWithDeployer(
+        bytes32 salt,
+        bytes32 codeHash,
+        address deployer
+    ) public pure returns (address) {
+        return Create2.computeAddress(salt, codeHash, deployer);
+    }
+
+    receive() external payable {}
+}

certora/munged/mocks/DummyImplementation.sol

@@ -0,0 +1,61 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+abstract contract Impl {
+    function version() public pure virtual returns (string memory);
+}
+
+contract DummyImplementation {
+    uint256 public value;
+    string public text;
+    uint256[] public values;
+
+    function initializeNonPayable() public {
+        value = 10;
+    }
+
+    function initializePayable() public payable {
+        value = 100;
+    }
+
+    function initializeNonPayableWithValue(uint256 _value) public {
+        value = _value;
+    }
+
+    function initializePayableWithValue(uint256 _value) public payable {
+        value = _value;
+    }
+
+    function initialize(
+        uint256 _value,
+        string memory _text,
+        uint256[] memory _values
+    ) public {
+        value = _value;
+        text = _text;
+        values = _values;
+    }
+
+    function get() public pure returns (bool) {
+        return true;
+    }
+
+    function version() public pure virtual returns (string memory) {
+        return "V1";
+    }
+
+    function reverts() public pure {
+        require(false, "DummyImplementation reverted");
+    }
+}
+
+contract DummyImplementationV2 is DummyImplementation {
+    function migrate(uint256 newVal) public payable {
+        value = newVal;
+    }
+
+    function version() public pure override returns (string memory) {
+        return "V2";
+    }
+}

certora/munged/mocks/ECDSAMock.sol

@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/cryptography/ECDSA.sol";
+
+contract ECDSAMock {
+    using ECDSA for bytes32;
+    using ECDSA for bytes;
+
+    function recover(bytes32 hash, bytes memory signature) public pure returns (address) {
+        return hash.recover(signature);
+    }
+
+    // solhint-disable-next-line func-name-mixedcase
+    function recover_v_r_s(
+        bytes32 hash,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public pure returns (address) {
+        return hash.recover(v, r, s);
+    }
+
+    // solhint-disable-next-line func-name-mixedcase
+    function recover_r_vs(
+        bytes32 hash,
+        bytes32 r,
+        bytes32 vs
+    ) public pure returns (address) {
+        return hash.recover(r, vs);
+    }
+
+    function toEthSignedMessageHash(bytes32 hash) public pure returns (bytes32) {
+        return hash.toEthSignedMessageHash();
+    }
+
+    function toEthSignedMessageHash(bytes memory s) public pure returns (bytes32) {
+        return s.toEthSignedMessageHash();
+    }
+}

certora/munged/mocks/EIP712External.sol

@@ -0,0 +1,31 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/cryptography/draft-EIP712.sol";
+import "../utils/cryptography/ECDSA.sol";
+
+contract EIP712External is EIP712 {
+    constructor(string memory name, string memory version) EIP712(name, version) {}
+
+    function domainSeparator() external view returns (bytes32) {
+        return _domainSeparatorV4();
+    }
+
+    function verify(
+        bytes memory signature,
+        address signer,
+        address mailTo,
+        string memory mailContents
+    ) external view {
+        bytes32 digest = _hashTypedDataV4(
+            keccak256(abi.encode(keccak256("Mail(address to,string contents)"), mailTo, keccak256(bytes(mailContents))))
+        );
+        address recoveredSigner = ECDSA.recover(digest, signature);
+        require(recoveredSigner == signer);
+    }
+
+    function getChainId() external view returns (uint256) {
+        return block.chainid;
+    }
+}

certora/munged/mocks/ERC1155BurnableMock.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC1155/extensions/ERC1155Burnable.sol";
+
+contract ERC1155BurnableMock is ERC1155Burnable {
+    constructor(string memory uri) ERC1155(uri) {}
+
+    function mint(
+        address to,
+        uint256 id,
+        uint256 value,
+        bytes memory data
+    ) public {
+        _mint(to, id, value, data);
+    }
+}

certora/munged/mocks/ERC1155Mock.sol

@@ -0,0 +1,51 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC1155/ERC1155.sol";
+
+/**
+ * @title ERC1155Mock
+ * This mock just publicizes internal functions for testing purposes
+ */
+contract ERC1155Mock is ERC1155 {
+    constructor(string memory uri) ERC1155(uri) {}
+
+    function setURI(string memory newuri) public {
+        _setURI(newuri);
+    }
+
+    function mint(
+        address to,
+        uint256 id,
+        uint256 value,
+        bytes memory data
+    ) public {
+        _mint(to, id, value, data);
+    }
+
+    function mintBatch(
+        address to,
+        uint256[] memory ids,
+        uint256[] memory values,
+        bytes memory data
+    ) public {
+        _mintBatch(to, ids, values, data);
+    }
+
+    function burn(
+        address owner,
+        uint256 id,
+        uint256 value
+    ) public {
+        _burn(owner, id, value);
+    }
+
+    function burnBatch(
+        address owner,
+        uint256[] memory ids,
+        uint256[] memory values
+    ) public {
+        _burnBatch(owner, ids, values);
+    }
+}

certora/munged/mocks/ERC1155PausableMock.sol

@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "./ERC1155Mock.sol";
+import "../token/ERC1155/extensions/ERC1155Pausable.sol";
+
+contract ERC1155PausableMock is ERC1155Mock, ERC1155Pausable {
+    constructor(string memory uri) ERC1155Mock(uri) {}
+
+    function pause() external {
+        _pause();
+    }
+
+    function unpause() external {
+        _unpause();
+    }
+
+    function _beforeTokenTransfer(
+        address operator,
+        address from,
+        address to,
+        uint256[] memory ids,
+        uint256[] memory amounts,
+        bytes memory data
+    ) internal virtual override(ERC1155, ERC1155Pausable) {
+        super._beforeTokenTransfer(operator, from, to, ids, amounts, data);
+    }
+}

certora/munged/mocks/ERC1155ReceiverMock.sol

@@ -0,0 +1,52 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC1155/IERC1155Receiver.sol";
+import "../utils/introspection/ERC165.sol";
+
+contract ERC1155ReceiverMock is ERC165, IERC1155Receiver {
+    bytes4 private _recRetval;
+    bool private _recReverts;
+    bytes4 private _batRetval;
+    bool private _batReverts;
+
+    event Received(address operator, address from, uint256 id, uint256 value, bytes data, uint256 gas);
+    event BatchReceived(address operator, address from, uint256[] ids, uint256[] values, bytes data, uint256 gas);
+
+    constructor(
+        bytes4 recRetval,
+        bool recReverts,
+        bytes4 batRetval,
+        bool batReverts
+    ) {
+        _recRetval = recRetval;
+        _recReverts = recReverts;
+        _batRetval = batRetval;
+        _batReverts = batReverts;
+    }
+
+    function onERC1155Received(
+        address operator,
+        address from,
+        uint256 id,
+        uint256 value,
+        bytes calldata data
+    ) external override returns (bytes4) {
+        require(!_recReverts, "ERC1155ReceiverMock: reverting on receive");
+        emit Received(operator, from, id, value, data, gasleft());
+        return _recRetval;
+    }
+
+    function onERC1155BatchReceived(
+        address operator,
+        address from,
+        uint256[] calldata ids,
+        uint256[] calldata values,
+        bytes calldata data
+    ) external override returns (bytes4) {
+        require(!_batReverts, "ERC1155ReceiverMock: reverting on batch receive");
+        emit BatchReceived(operator, from, ids, values, data, gasleft());
+        return _batRetval;
+    }
+}

certora/munged/mocks/ERC1155SupplyMock.sol

@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "./ERC1155Mock.sol";
+import "../token/ERC1155/extensions/ERC1155Supply.sol";
+
+contract ERC1155SupplyMock is ERC1155Mock, ERC1155Supply {
+    constructor(string memory uri) ERC1155Mock(uri) {}
+
+    function _beforeTokenTransfer(
+        address operator,
+        address from,
+        address to,
+        uint256[] memory ids,
+        uint256[] memory amounts,
+        bytes memory data
+    ) internal virtual override(ERC1155, ERC1155Supply) {
+        super._beforeTokenTransfer(operator, from, to, ids, amounts, data);
+    }
+}

certora/munged/mocks/ERC1271WalletMock.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../access/Ownable.sol";
+import "../interfaces/IERC1271.sol";
+import "../utils/cryptography/ECDSA.sol";
+
+contract ERC1271WalletMock is Ownable, IERC1271 {
+    constructor(address originalOwner) {
+        transferOwnership(originalOwner);
+    }
+
+    function isValidSignature(bytes32 hash, bytes memory signature) public view override returns (bytes4 magicValue) {
+        return ECDSA.recover(hash, signature) == owner() ? this.isValidSignature.selector : bytes4(0);
+    }
+}

certora/munged/mocks/ERC165/ERC165InterfacesSupported.sol

@@ -0,0 +1,58 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../../utils/introspection/IERC165.sol";
+
+/**
+ * https://eips.ethereum.org/EIPS/eip-214#specification
+ * From the specification:
+ * > Any attempts to make state-changing operations inside an execution instance with STATIC set to true will instead
+ * throw an exception.
+ * > These operations include [...], LOG0, LOG1, LOG2, [...]
+ *
+ * therefore, because this contract is staticcall'd we need to not emit events (which is how solidity-coverage works)
+ * solidity-coverage ignores the /mocks folder, so we duplicate its implementation here to avoid instrumenting it
+ */
+contract SupportsInterfaceWithLookupMock is IERC165 {
+    /*
+     * bytes4(keccak256('supportsInterface(bytes4)')) == 0x01ffc9a7
+     */
+    bytes4 public constant INTERFACE_ID_ERC165 = 0x01ffc9a7;
+
+    /**
+     * @dev A mapping of interface id to whether or not it's supported.
+     */
+    mapping(bytes4 => bool) private _supportedInterfaces;
+
+    /**
+     * @dev A contract implementing SupportsInterfaceWithLookup
+     * implement ERC165 itself.
+     */
+    constructor() {
+        _registerInterface(INTERFACE_ID_ERC165);
+    }
+
+    /**
+     * @dev Implement supportsInterface(bytes4) using a lookup table.
+     */
+    function supportsInterface(bytes4 interfaceId) public view override returns (bool) {
+        return _supportedInterfaces[interfaceId];
+    }
+
+    /**
+     * @dev Private method for registering an interface.
+     */
+    function _registerInterface(bytes4 interfaceId) internal {
+        require(interfaceId != 0xffffffff, "ERC165InterfacesSupported: invalid interface id");
+        _supportedInterfaces[interfaceId] = true;
+    }
+}
+
+contract ERC165InterfacesSupported is SupportsInterfaceWithLookupMock {
+    constructor(bytes4[] memory interfaceIds) {
+        for (uint256 i = 0; i < interfaceIds.length; i++) {
+            _registerInterface(interfaceIds[i]);
+        }
+    }
+}

certora/munged/mocks/ERC165/ERC165MissingData.sol

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+contract ERC165MissingData {
+    function supportsInterface(bytes4 interfaceId) public view {} // missing return
+}

certora/munged/mocks/ERC165/ERC165NotSupported.sol

@@ -0,0 +1,5 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+contract ERC165NotSupported {}

certora/munged/mocks/ERC165CheckerMock.sol

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/ERC165Checker.sol";
+
+contract ERC165CheckerMock {
+    using ERC165Checker for address;
+
+    function supportsERC165(address account) public view returns (bool) {
+        return account.supportsERC165();
+    }
+
+    function supportsInterface(address account, bytes4 interfaceId) public view returns (bool) {
+        return account.supportsInterface(interfaceId);
+    }
+
+    function supportsAllInterfaces(address account, bytes4[] memory interfaceIds) public view returns (bool) {
+        return account.supportsAllInterfaces(interfaceIds);
+    }
+
+    function getSupportedInterfaces(address account, bytes4[] memory interfaceIds) public view returns (bool[] memory) {
+        return account.getSupportedInterfaces(interfaceIds);
+    }
+}

certora/munged/mocks/ERC165Mock.sol

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/ERC165.sol";
+
+contract ERC165Mock is ERC165 {}

certora/munged/mocks/ERC165StorageMock.sol

@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/ERC165Storage.sol";
+
+contract ERC165StorageMock is ERC165Storage {
+    function registerInterface(bytes4 interfaceId) public {
+        _registerInterface(interfaceId);
+    }
+}

certora/munged/mocks/ERC1820ImplementerMock.sol

@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../utils/introspection/ERC1820Implementer.sol";
+
+contract ERC1820ImplementerMock is ERC1820Implementer {
+    function registerInterfaceForAddress(bytes32 interfaceHash, address account) public {
+        _registerInterfaceForAddress(interfaceHash, account);
+    }
+}

certora/munged/mocks/ERC20BurnableMock.sol

@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20Burnable.sol";
+
+contract ERC20BurnableMock is ERC20Burnable {
+    constructor(
+        string memory name,
+        string memory symbol,
+        address initialAccount,
+        uint256 initialBalance
+    ) ERC20(name, symbol) {
+        _mint(initialAccount, initialBalance);
+    }
+}

certora/munged/mocks/ERC20CappedMock.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20Capped.sol";
+
+contract ERC20CappedMock is ERC20Capped {
+    constructor(
+        string memory name,
+        string memory symbol,
+        uint256 cap
+    ) ERC20(name, symbol) ERC20Capped(cap) {}
+
+    function mint(address to, uint256 tokenId) public {
+        _mint(to, tokenId);
+    }
+}

certora/munged/mocks/ERC20DecimalsMock.sol

@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/ERC20.sol";
+
+contract ERC20DecimalsMock is ERC20 {
+    uint8 private immutable _decimals;
+
+    constructor(
+        string memory name_,
+        string memory symbol_,
+        uint8 decimals_
+    ) ERC20(name_, symbol_) {
+        _decimals = decimals_;
+    }
+
+    function decimals() public view virtual override returns (uint8) {
+        return _decimals;
+    }
+}

certora/munged/mocks/ERC20FlashMintMock.sol

@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20FlashMint.sol";
+
+contract ERC20FlashMintMock is ERC20FlashMint {
+    constructor(
+        string memory name,
+        string memory symbol,
+        address initialAccount,
+        uint256 initialBalance
+    ) ERC20(name, symbol) {
+        _mint(initialAccount, initialBalance);
+    }
+}

certora/munged/mocks/ERC20Mock.sol

@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/ERC20.sol";
+
+// mock class using ERC20
+contract ERC20Mock is ERC20 {
+    constructor(
+        string memory name,
+        string memory symbol,
+        address initialAccount,
+        uint256 initialBalance
+    ) payable ERC20(name, symbol) {
+        _mint(initialAccount, initialBalance);
+    }
+
+    function mint(address account, uint256 amount) public {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) public {
+        _burn(account, amount);
+    }
+
+    function transferInternal(
+        address from,
+        address to,
+        uint256 value
+    ) public {
+        _transfer(from, to, value);
+    }
+
+    function approveInternal(
+        address owner,
+        address spender,
+        uint256 value
+    ) public {
+        _approve(owner, spender, value);
+    }
+}

certora/munged/mocks/ERC20PausableMock.sol

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20Pausable.sol";
+
+// mock class using ERC20Pausable
+contract ERC20PausableMock is ERC20Pausable {
+    constructor(
+        string memory name,
+        string memory symbol,
+        address initialAccount,
+        uint256 initialBalance
+    ) ERC20(name, symbol) {
+        _mint(initialAccount, initialBalance);
+    }
+
+    function pause() external {
+        _pause();
+    }
+
+    function unpause() external {
+        _unpause();
+    }
+
+    function mint(address to, uint256 amount) public {
+        _mint(to, amount);
+    }
+
+    function burn(address from, uint256 amount) public {
+        _burn(from, amount);
+    }
+}

certora/munged/mocks/ERC20PermitMock.sol

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/draft-ERC20Permit.sol";
+
+contract ERC20PermitMock is ERC20Permit {
+    constructor(
+        string memory name,
+        string memory symbol,
+        address initialAccount,
+        uint256 initialBalance
+    ) payable ERC20(name, symbol) ERC20Permit(name) {
+        _mint(initialAccount, initialBalance);
+    }
+
+    function getChainId() external view returns (uint256) {
+        return block.chainid;
+    }
+}

certora/munged/mocks/ERC20SnapshotMock.sol

@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20Snapshot.sol";
+
+contract ERC20SnapshotMock is ERC20Snapshot {
+    constructor(
+        string memory name,
+        string memory symbol,
+        address initialAccount,
+        uint256 initialBalance
+    ) ERC20(name, symbol) {
+        _mint(initialAccount, initialBalance);
+    }
+
+    function snapshot() public {
+        _snapshot();
+    }
+
+    function mint(address account, uint256 amount) public {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) public {
+        _burn(account, amount);
+    }
+}

certora/munged/mocks/ERC20VotesCompMock.sol

@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20VotesComp.sol";
+
+contract ERC20VotesCompMock is ERC20VotesComp {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
+
+    function mint(address account, uint256 amount) public {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) public {
+        _burn(account, amount);
+    }
+
+    function getChainId() external view returns (uint256) {
+        return block.chainid;
+    }
+}

certora/munged/mocks/ERC20VotesMock.sol

@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20Votes.sol";
+
+contract ERC20VotesMock is ERC20Votes {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
+
+    function mint(address account, uint256 amount) public {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) public {
+        _burn(account, amount);
+    }
+
+    function getChainId() external view returns (uint256) {
+        return block.chainid;
+    }
+}

certora/munged/mocks/ERC20WrapperMock.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/extensions/ERC20Wrapper.sol";
+
+contract ERC20WrapperMock is ERC20Wrapper {
+    constructor(
+        IERC20 _underlyingToken,
+        string memory name,
+        string memory symbol
+    ) ERC20(name, symbol) ERC20Wrapper(_underlyingToken) {}
+
+    function recover(address account) public returns (uint256) {
+        return _recover(account);
+    }
+}

certora/munged/mocks/ERC2771ContextMock.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "./ContextMock.sol";
+import "../metatx/ERC2771Context.sol";
+
+// By inheriting from ERC2771Context, Context's internal functions are overridden automatically
+contract ERC2771ContextMock is ContextMock, ERC2771Context {
+    constructor(address trustedForwarder) ERC2771Context(trustedForwarder) {}
+
+    function _msgSender() internal view virtual override(Context, ERC2771Context) returns (address) {
+        return ERC2771Context._msgSender();
+    }
+
+    function _msgData() internal view virtual override(Context, ERC2771Context) returns (bytes calldata) {
+        return ERC2771Context._msgData();
+    }
+}

certora/munged/mocks/ERC3156FlashBorrowerMock.sol

@@ -0,0 +1,53 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC20/IERC20.sol";
+import "../interfaces/IERC3156.sol";
+import "../utils/Address.sol";
+
+/**
+ * @dev WARNING: this IERC3156FlashBorrower mock implementation is for testing purposes ONLY.
+ * Writing a secure flash lock borrower is not an easy task, and should be done with the utmost care.
+ * This is not an example of how it should be done, and no pattern present in this mock should be considered secure.
+ * Following best practices, always have your contract properly audited before using them to manipulate important funds on
+ * live networks.
+ */
+contract ERC3156FlashBorrowerMock is IERC3156FlashBorrower {
+    bytes32 internal constant _RETURN_VALUE = keccak256("ERC3156FlashBorrower.onFlashLoan");
+
+    bool immutable _enableApprove;
+    bool immutable _enableReturn;
+
+    event BalanceOf(address token, address account, uint256 value);
+    event TotalSupply(address token, uint256 value);
+
+    constructor(bool enableReturn, bool enableApprove) {
+        _enableApprove = enableApprove;
+        _enableReturn = enableReturn;
+    }
+
+    function onFlashLoan(
+        address, /*initiator*/
+        address token,
+        uint256 amount,
+        uint256 fee,
+        bytes calldata data
+    ) public override returns (bytes32) {
+        require(msg.sender == token);
+
+        emit BalanceOf(token, address(this), IERC20(token).balanceOf(address(this)));
+        emit TotalSupply(token, IERC20(token).totalSupply());
+
+        if (data.length > 0) {
+            // WARNING: This code is for testing purposes only! Do not use.
+            Address.functionCall(token, data);
+        }
+
+        if (_enableApprove) {
+            IERC20(token).approve(token, amount + fee);
+        }
+
+        return _enableReturn ? _RETURN_VALUE : bytes32(0);
+    }
+}

certora/munged/mocks/ERC721BurnableMock.sol

@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/extensions/ERC721Burnable.sol";
+
+contract ERC721BurnableMock is ERC721Burnable {
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
+
+    function exists(uint256 tokenId) public view returns (bool) {
+        return _exists(tokenId);
+    }
+
+    function mint(address to, uint256 tokenId) public {
+        _mint(to, tokenId);
+    }
+
+    function safeMint(address to, uint256 tokenId) public {
+        _safeMint(to, tokenId);
+    }
+
+    function safeMint(
+        address to,
+        uint256 tokenId,
+        bytes memory _data
+    ) public {
+        _safeMint(to, tokenId, _data);
+    }
+}

certora/munged/mocks/ERC721EnumerableMock.sol

@@ -0,0 +1,51 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/extensions/ERC721Enumerable.sol";
+
+/**
+ * @title ERC721Mock
+ * This mock just provides a public safeMint, mint, and burn functions for testing purposes
+ */
+contract ERC721EnumerableMock is ERC721Enumerable {
+    string private _baseTokenURI;
+
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
+
+    function _baseURI() internal view virtual override returns (string memory) {
+        return _baseTokenURI;
+    }
+
+    function setBaseURI(string calldata newBaseTokenURI) public {
+        _baseTokenURI = newBaseTokenURI;
+    }
+
+    function baseURI() public view returns (string memory) {
+        return _baseURI();
+    }
+
+    function exists(uint256 tokenId) public view returns (bool) {
+        return _exists(tokenId);
+    }
+
+    function mint(address to, uint256 tokenId) public {
+        _mint(to, tokenId);
+    }
+
+    function safeMint(address to, uint256 tokenId) public {
+        _safeMint(to, tokenId);
+    }
+
+    function safeMint(
+        address to,
+        uint256 tokenId,
+        bytes memory _data
+    ) public {
+        _safeMint(to, tokenId, _data);
+    }
+
+    function burn(uint256 tokenId) public {
+        _burn(tokenId);
+    }
+}

certora/munged/mocks/ERC721Mock.sol

@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/ERC721.sol";
+
+/**
+ * @title ERC721Mock
+ * This mock just provides a public safeMint, mint, and burn functions for testing purposes
+ */
+contract ERC721Mock is ERC721 {
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
+
+    function baseURI() public view returns (string memory) {
+        return _baseURI();
+    }
+
+    function exists(uint256 tokenId) public view returns (bool) {
+        return _exists(tokenId);
+    }
+
+    function mint(address to, uint256 tokenId) public {
+        _mint(to, tokenId);
+    }
+
+    function safeMint(address to, uint256 tokenId) public {
+        _safeMint(to, tokenId);
+    }
+
+    function safeMint(
+        address to,
+        uint256 tokenId,
+        bytes memory _data
+    ) public {
+        _safeMint(to, tokenId, _data);
+    }
+
+    function burn(uint256 tokenId) public {
+        _burn(tokenId);
+    }
+}

certora/munged/mocks/ERC721PausableMock.sol

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/extensions/ERC721Pausable.sol";
+
+/**
+ * @title ERC721PausableMock
+ * This mock just provides a public mint, burn and exists functions for testing purposes
+ */
+contract ERC721PausableMock is ERC721Pausable {
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
+
+    function pause() external {
+        _pause();
+    }
+
+    function unpause() external {
+        _unpause();
+    }
+
+    function exists(uint256 tokenId) public view returns (bool) {
+        return _exists(tokenId);
+    }
+
+    function mint(address to, uint256 tokenId) public {
+        _mint(to, tokenId);
+    }
+
+    function safeMint(address to, uint256 tokenId) public {
+        _safeMint(to, tokenId);
+    }
+
+    function safeMint(
+        address to,
+        uint256 tokenId,
+        bytes memory _data
+    ) public {
+        _safeMint(to, tokenId, _data);
+    }
+
+    function burn(uint256 tokenId) public {
+        _burn(tokenId);
+    }
+}

certora/munged/mocks/ERC721ReceiverMock.sol

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/IERC721Receiver.sol";
+
+contract ERC721ReceiverMock is IERC721Receiver {
+    enum Error {
+        None,
+        RevertWithMessage,
+        RevertWithoutMessage,
+        Panic
+    }
+
+    bytes4 private immutable _retval;
+    Error private immutable _error;
+
+    event Received(address operator, address from, uint256 tokenId, bytes data, uint256 gas);
+
+    constructor(bytes4 retval, Error error) {
+        _retval = retval;
+        _error = error;
+    }
+
+    function onERC721Received(
+        address operator,
+        address from,
+        uint256 tokenId,
+        bytes memory data
+    ) public override returns (bytes4) {
+        if (_error == Error.RevertWithMessage) {
+            revert("ERC721ReceiverMock: reverting");
+        } else if (_error == Error.RevertWithoutMessage) {
+            revert();
+        } else if (_error == Error.Panic) {
+            uint256 a = uint256(0) / uint256(0);
+            a;
+        }
+        emit Received(operator, from, tokenId, data, gasleft());
+        return _retval;
+    }
+}

certora/munged/mocks/ERC721URIStorageMock.sol

@@ -0,0 +1,55 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../token/ERC721/extensions/ERC721URIStorage.sol";
+
+/**
+ * @title ERC721Mock
+ * This mock just provides a public safeMint, mint, and burn functions for testing purposes
+ */
+contract ERC721URIStorageMock is ERC721URIStorage {
+    string private _baseTokenURI;
+
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
+
+    function _baseURI() internal view virtual override returns (string memory) {
+        return _baseTokenURI;
+    }
+
+    function setBaseURI(string calldata newBaseTokenURI) public {
+        _baseTokenURI = newBaseTokenURI;
+    }
+
+    function baseURI() public view returns (string memory) {
+        return _baseURI();
+    }
+
+    function setTokenURI(uint256 tokenId, string memory _tokenURI) public {
+        _setTokenURI(tokenId, _tokenURI);
+    }
+
+    function exists(uint256 tokenId) public view returns (bool) {
+        return _exists(tokenId);
+    }
+
+    function mint(address to, uint256 tokenId) public {
+        _mint(to, tokenId);
+    }
+
+    function safeMint(address to, uint256 tokenId) public {
+        _safeMint(to, tokenId);
+    }
+
+    function safeMint(
+        address to,
+        uint256 tokenId,
+        bytes memory _data
+    ) public {
+        _safeMint(to, tokenId, _data);
+    }
+
+    function burn(uint256 tokenId) public {
+        _burn(tokenId);
+    }
+}