Partial TimelockController

certora/diff/governance_TimelockController.sol.patch

@@ -0,0 +1,11 @@
+--- governance/TimelockController.sol	2023-08-11 20:33:54
++++ governance/TimelockController.sol	2023-08-13 10:07:34
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.9.0) (governance/TimelockController.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {AccessControl} from "../access/AccessControl.sol";
+ import {ERC721Holder} from "../token/ERC721/utils/ERC721Holder.sol";

certora/diff/token_ERC1155_IERC1155Receiver.sol.patch

@@ -0,0 +1,11 @@
+--- token/ERC1155/IERC1155Receiver.sol	2023-08-11 20:33:54
++++ token/ERC1155/IERC1155Receiver.sol	2023-08-13 10:09:15
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.5.0) (token/ERC1155/IERC1155Receiver.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {IERC165} from "../../utils/introspection/IERC165.sol";
+ 

certora/diff/token_ERC1155_utils_ERC1155Holder.sol.patch

@@ -0,0 +1,11 @@
+--- token/ERC1155/utils/ERC1155Holder.sol	2023-08-11 20:33:54
++++ token/ERC1155/utils/ERC1155Holder.sol	2023-08-13 10:09:12
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.5.0) (token/ERC1155/utils/ERC1155Holder.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {IERC165, ERC165} from "../../../utils/introspection/ERC165.sol";
+ import {IERC1155Receiver} from "../IERC1155Receiver.sol";

certora/diff/token_ERC721_ERC721.sol.orig.patch

@@ -0,0 +1,468 @@
+--- token/ERC721/ERC721.sol.orig	1969-12-31 18:00:00
++++ token/ERC721/ERC721.sol.orig	2023-08-13 09:56:16
+@@ -0,0 +1,465 @@
++// SPDX-License-Identifier: MIT
++// OpenZeppelin Contracts (last updated v4.9.0) (token/ERC721/ERC721.sol)
++
++pragma solidity ^0.8.20;
++
++import {IERC721} from "./IERC721.sol";
++import {IERC721Receiver} from "./IERC721Receiver.sol";
++import {IERC721Metadata} from "./extensions/IERC721Metadata.sol";
++import {Context} from "../../utils/Context.sol";
++import {Strings} from "../../utils/Strings.sol";
++import {IERC165, ERC165} from "../../utils/introspection/ERC165.sol";
++import {IERC721Errors} from "../../interfaces/draft-IERC6093.sol";
++
++/**
++ * @dev Implementation of https://eips.ethereum.org/EIPS/eip-721[ERC721] Non-Fungible Token Standard, including
++ * the Metadata extension, but not including the Enumerable extension, which is available separately as
++ * {ERC721Enumerable}.
++ */
++abstract contract ERC721 is Context, ERC165, IERC721, IERC721Metadata, IERC721Errors {
++    using Strings for uint256;
++
++    // Token name
++    string private _name;
++
++    // Token symbol
++    string private _symbol;
++
++    mapping(uint256 tokenId => address) private _owners;
++
++    mapping(address owner => uint256) private _balances;
++
++    mapping(uint256 tokenId => address) private _tokenApprovals;
++
++    mapping(address owner => mapping(address operator => bool)) private _operatorApprovals;
++
++    /**
++     * @dev Initializes the contract by setting a `name` and a `symbol` to the token collection.
++     */
++    constructor(string memory name_, string memory symbol_) {
++        _name = name_;
++        _symbol = symbol_;
++    }
++
++    /**
++     * @dev See {IERC165-supportsInterface}.
++     */
++    function supportsInterface(bytes4 interfaceId) public view virtual override(ERC165, IERC165) returns (bool) {
++        return
++            interfaceId == type(IERC721).interfaceId ||
++            interfaceId == type(IERC721Metadata).interfaceId ||
++            super.supportsInterface(interfaceId);
++    }
++
++    /**
++     * @dev See {IERC721-balanceOf}.
++     */
++    function balanceOf(address owner) public view virtual returns (uint256) {
++        if (owner == address(0)) {
++            revert ERC721InvalidOwner(address(0));
++        }
++        return _balances[owner];
++    }
++
++    /**
++     * @dev See {IERC721-ownerOf}.
++     */
++    function ownerOf(uint256 tokenId) public view virtual returns (address) {
++        address owner = _ownerOf(tokenId);
++        if (owner == address(0)) {
++            revert ERC721NonexistentToken(tokenId);
++        }
++        return owner;
++    }
++
++    /**
++     * @dev See {IERC721Metadata-name}.
++     */
++    function name() public view virtual returns (string memory) {
++        return _name;
++    }
++
++    /**
++     * @dev See {IERC721Metadata-symbol}.
++     */
++    function symbol() public view virtual returns (string memory) {
++        return _symbol;
++    }
++
++    /**
++     * @dev See {IERC721Metadata-tokenURI}.
++     */
++    function tokenURI(uint256 tokenId) public view virtual returns (string memory) {
++        _requireMinted(tokenId);
++
++        string memory baseURI = _baseURI();
++        return bytes(baseURI).length > 0 ? string.concat(baseURI, tokenId.toString()) : "";
++    }
++
++    /**
++     * @dev Base URI for computing {tokenURI}. If set, the resulting URI for each
++     * token will be the concatenation of the `baseURI` and the `tokenId`. Empty
++     * by default, can be overridden in child contracts.
++     */
++    function _baseURI() internal view virtual returns (string memory) {
++        return "";
++    }
++
++    /**
++     * @dev See {IERC721-approve}.
++     */
++    function approve(address to, uint256 tokenId) public virtual {
++        _approve(to, tokenId, _msgSender());
++    }
++
++    /**
++     * @dev See {IERC721-getApproved}.
++     */
++    function getApproved(uint256 tokenId) public view virtual returns (address) {
++        _requireMinted(tokenId);
++
++        return _getApproved(tokenId);
++    }
++
++    /**
++     * @dev See {IERC721-setApprovalForAll}.
++     */
++    function setApprovalForAll(address operator, bool approved) public virtual {
++        _setApprovalForAll(_msgSender(), operator, approved);
++    }
++
++    /**
++     * @dev See {IERC721-isApprovedForAll}.
++     */
++    function isApprovedForAll(address owner, address operator) public view virtual returns (bool) {
++        return _operatorApprovals[owner][operator];
++    }
++
++    /**
++     * @dev See {IERC721-transferFrom}.
++     */
++    function transferFrom(address from, address to, uint256 tokenId) public virtual {
++        if (to == address(0)) {
++            revert ERC721InvalidReceiver(address(0));
++        }
++        // Setting an "auth" arguments enables the `_isAuthorized` check which verifies that the token exists
++        // (from != 0). Therefore, it is not needed to verify that the return value is not 0 here.
++        address previousOwner = _update(to, tokenId, _msgSender());
++        if (previousOwner != from) {
++            revert ERC721IncorrectOwner(from, tokenId, previousOwner);
++        }
++    }
++
++    /**
++     * @dev See {IERC721-safeTransferFrom}.
++     */
++    function safeTransferFrom(address from, address to, uint256 tokenId) public {
++        safeTransferFrom(from, to, tokenId, "");
++    }
++
++    /**
++     * @dev See {IERC721-safeTransferFrom}.
++     */
++    function safeTransferFrom(address from, address to, uint256 tokenId, bytes memory data) public virtual {
++        transferFrom(from, to, tokenId);
++        _checkOnERC721Received(from, to, tokenId, data);
++    }
++
++    /**
++     * @dev Returns the owner of the `tokenId`. Does NOT revert if token doesn't exist
++     *
++     * IMPORTANT: Any overrides to this function that add ownership of tokens not tracked by the
++     * core ERC721 logic MUST be matched with the use of {_increaseBalance} to keep balances
++     * consistent with ownership. The invariant to preserve is that for any address `a` the value returned by
++     * `balanceOf(a)` must be equal to the number of tokens such that `_ownerOf(tokenId)` is `a`.
++     */
++    function _ownerOf(uint256 tokenId) internal view virtual returns (address) {
++        return _owners[tokenId];
++    }
++
++    /**
++     * @dev Returns the approved address for `tokenId`. Returns 0 if `tokenId` is not minted.
++     */
++    function _getApproved(uint256 tokenId) internal view virtual returns (address) {
++        return _tokenApprovals[tokenId];
++    }
++
++    /**
++     * @dev Returns whether `spender` is allowed to manage `owner`'s tokens, or `tokenId` in
++     * particular (ignoring whether it is owned by `owner`).
++     *
++     * WARNING: This function assumes that `owner` is the actual owner of `tokenId` and does not
++     * verify this assumption.
++     */
++    function _isAuthorized(address owner, address spender, uint256 tokenId) internal view virtual returns (bool) {
++        return
++            spender != address(0) &&
++            (owner == spender || isApprovedForAll(owner, spender) || _getApproved(tokenId) == spender);
++    }
++
++    /**
++     * @dev Checks if `spender` can operate on `tokenId`, assuming the provided `owner` is the actual owner.
++     * Reverts if `spender` has not approval for all assets of the provided `owner` nor the actual owner approved the `spender` for the specific `tokenId`.
++     *
++     * WARNING: This function relies on {_isAuthorized}, so it doesn't check whether `owner` is the
++     * actual owner of `tokenId`.
++     */
++    function _checkAuthorized(address owner, address spender, uint256 tokenId) internal view virtual {
++        if (!_isAuthorized(owner, spender, tokenId)) {
++            if (owner == address(0)) {
++                revert ERC721NonexistentToken(tokenId);
++            } else {
++                revert ERC721InsufficientApproval(spender, tokenId);
++            }
++        }
++    }
++
++    /**
++     * @dev Unsafe write access to the balances, used by extensions that "mint" tokens using an {ownerOf} override.
++     *
++     * NOTE: the value is limited to type(uint128).max. This protect against _balance overflow. It is unrealistic that
++     * a uint256 would ever overflow from increments when these increments are bounded to uint128 values.
++     *
++     * WARNING: Increasing an account's balance using this function tends to be paired with an override of the
++     * {_ownerOf} function to resolve the ownership of the corresponding tokens so that balances and ownership
++     * remain consistent with one another.
++     */
++    function _increaseBalance(address account, uint128 value) internal virtual {
++        unchecked {
++            _balances[account] += value;
++        }
++    }
++
++    /**
++     * @dev Transfers `tokenId` from its current owner to `to`, or alternatively mints (or burns) if the current owner
++     * (or `to`) is the zero address. Returns the owner of the `tokenId` before the update.
++     *
++     * The `auth` argument is optional. If the value passed is non 0, then this function will check that
++     * `auth` is either the owner of the token, or approved to operate on the token (by the owner).
++     *
++     * Emits a {Transfer} event.
++     *
++     * NOTE: If overriding this function in a way that tracks balances, see also {_increaseBalance}.
++     */
++    function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
++        address from = _ownerOf(tokenId);
++
++        // Perform (optional) operator check
++        if (auth != address(0)) {
++            _checkAuthorized(from, auth, tokenId);
++        }
++
++        // Execute the update
++        if (from != address(0)) {
++            delete _tokenApprovals[tokenId];
++            unchecked {
++                _balances[from] -= 1;
++            }
++        }
++
++        if (to != address(0)) {
++            unchecked {
++                _balances[to] += 1;
++            }
++        }
++
++        _owners[tokenId] = to;
++
++        emit Transfer(from, to, tokenId);
++
++        return from;
++    }
++
++    /**
++     * @dev Mints `tokenId` and transfers it to `to`.
++     *
++     * WARNING: Usage of this method is discouraged, use {_safeMint} whenever possible
++     *
++     * Requirements:
++     *
++     * - `tokenId` must not exist.
++     * - `to` cannot be the zero address.
++     *
++     * Emits a {Transfer} event.
++     */
++    function _mint(address to, uint256 tokenId) internal {
++        if (to == address(0)) {
++            revert ERC721InvalidReceiver(address(0));
++        }
++        address previousOwner = _update(to, tokenId, address(0));
++        if (previousOwner != address(0)) {
++            revert ERC721InvalidSender(address(0));
++        }
++    }
++
++    /**
++     * @dev Mints `tokenId`, transfers it to `to` and checks for `to` acceptance.
++     *
++     * Requirements:
++     *
++     * - `tokenId` must not exist.
++     * - If `to` refers to a smart contract, it must implement {IERC721Receiver-onERC721Received}, which is called upon a safe transfer.
++     *
++     * Emits a {Transfer} event.
++     */
++    function _safeMint(address to, uint256 tokenId) internal {
++        _safeMint(to, tokenId, "");
++    }
++
++    /**
++     * @dev Same as {xref-ERC721-_safeMint-address-uint256-}[`_safeMint`], with an additional `data` parameter which is
++     * forwarded in {IERC721Receiver-onERC721Received} to contract recipients.
++     */
++    function _safeMint(address to, uint256 tokenId, bytes memory data) internal virtual {
++        _mint(to, tokenId);
++        _checkOnERC721Received(address(0), to, tokenId, data);
++    }
++
++    /**
++     * @dev Destroys `tokenId`.
++     * The approval is cleared when the token is burned.
++     * This is an internal function that does not check if the sender is authorized to operate on the token.
++     *
++     * Requirements:
++     *
++     * - `tokenId` must exist.
++     *
++     * Emits a {Transfer} event.
++     */
++    function _burn(uint256 tokenId) internal {
++        address previousOwner = _update(address(0), tokenId, address(0));
++        if (previousOwner == address(0)) {
++            revert ERC721NonexistentToken(tokenId);
++        }
++    }
++
++    /**
++     * @dev Transfers `tokenId` from `from` to `to`.
++     *  As opposed to {transferFrom}, this imposes no restrictions on msg.sender.
++     *
++     * Requirements:
++     *
++     * - `to` cannot be the zero address.
++     * - `tokenId` token must be owned by `from`.
++     *
++     * Emits a {Transfer} event.
++     */
++    function _transfer(address from, address to, uint256 tokenId) internal {
++        if (to == address(0)) {
++            revert ERC721InvalidReceiver(address(0));
++        }
++        address previousOwner = _update(to, tokenId, address(0));
++        if (previousOwner == address(0)) {
++            revert ERC721NonexistentToken(tokenId);
++        } else if (previousOwner != from) {
++            revert ERC721IncorrectOwner(from, tokenId, previousOwner);
++        }
++    }
++
++    /**
++     * @dev Safely transfers `tokenId` token from `from` to `to`, checking that contract recipients
++     * are aware of the ERC721 standard to prevent tokens from being forever locked.
++     *
++     * `data` is additional data, it has no specified format and it is sent in call to `to`.
++     *
++     * This internal function is like {safeTransferFrom} in the sense that it invokes
++     * {IERC721Receiver-onERC721Received} on the receiver, and can be used to e.g.
++     * implement alternative mechanisms to perform token transfer, such as signature-based.
++     *
++     * Requirements:
++     *
++     * - `tokenId` token must exist and be owned by `from`.
++     * - `to` cannot be the zero address.
++     * - `from` cannot be the zero address.
++     * - If `to` refers to a smart contract, it must implement {IERC721Receiver-onERC721Received}, which is called upon a safe transfer.
++     *
++     * Emits a {Transfer} event.
++     */
++    function _safeTransfer(address from, address to, uint256 tokenId) internal {
++        _safeTransfer(from, to, tokenId, "");
++    }
++
++    /**
++     * @dev Same as {xref-ERC721-_safeTransfer-address-address-uint256-}[`_safeTransfer`], with an additional `data` parameter which is
++     * forwarded in {IERC721Receiver-onERC721Received} to contract recipients.
++     */
++    function _safeTransfer(address from, address to, uint256 tokenId, bytes memory data) internal virtual {
++        _transfer(from, to, tokenId);
++        _checkOnERC721Received(from, to, tokenId, data);
++    }
++
++    /**
++     * @dev Approve `to` to operate on `tokenId`
++     *
++     * The `auth` argument is optional. If the value passed is non 0, then this function will check that `auth` is
++     * either the owner of the token, or approved to operate on all tokens held by this owner.
++     *
++     * Emits an {Approval} event.
++     */
++    function _approve(address to, uint256 tokenId, address auth) internal virtual returns (address) {
++        address owner = ownerOf(tokenId);
++
++        // We do not use _isAuthorized because single-token approvals should not be able to call approve
++        if (auth != address(0) && owner != auth && !isApprovedForAll(owner, auth)) {
++            revert ERC721InvalidApprover(auth);
++        }
++
++        _tokenApprovals[tokenId] = to;
++        emit Approval(owner, to, tokenId);
++
++        return owner;
++    }
++
++    /**
++     * @dev Approve `operator` to operate on all of `owner` tokens
++     *
++     * Requirements:
++     * - operator can't be the address zero.
++     *
++     * Emits an {ApprovalForAll} event.
++     */
++    function _setApprovalForAll(address owner, address operator, bool approved) internal virtual {
++        if (operator == address(0)) {
++            revert ERC721InvalidOperator(operator);
++        }
++        _operatorApprovals[owner][operator] = approved;
++        emit ApprovalForAll(owner, operator, approved);
++    }
++
++    /**
++     * @dev Reverts if the `tokenId` has not been minted yet.
++     */
++    function _requireMinted(uint256 tokenId) internal view virtual {
++        if (_ownerOf(tokenId) == address(0)) {
++            revert ERC721NonexistentToken(tokenId);
++        }
++    }
++
++    /**
++     * @dev Private function to invoke {IERC721Receiver-onERC721Received} on a target address. This will revert if the
++     * recipient doesn't accept the token transfer. The call is not executed if the target address is not a contract.
++     *
++     * @param from address representing the previous owner of the given token ID
++     * @param to target address that will receive the tokens
++     * @param tokenId uint256 ID of the token to be transferred
++     * @param data bytes optional data to send along with the call
++     */
++    function _checkOnERC721Received(address from, address to, uint256 tokenId, bytes memory data) private {
++        if (to.code.length > 0) {
++            try IERC721Receiver(to).onERC721Received(_msgSender(), from, tokenId, data) returns (bytes4 retval) {
++                if (retval != IERC721Receiver.onERC721Received.selector) {
++                    revert ERC721InvalidReceiver(to);
++                }
++            } catch (bytes memory reason) {
++                if (reason.length == 0) {
++                    revert ERC721InvalidReceiver(to);
++                } else {
++                    /// @solidity memory-safe-assembly
++                    assembly {
++                        revert(add(32, reason), mload(reason))
++                    }
++                }
++            }
++        }
++    }
++}

certora/diff/token_ERC721_IERC721Receiver.sol.patch

@@ -0,0 +1,11 @@
+--- token/ERC721/IERC721Receiver.sol	2023-08-11 20:33:54
++++ token/ERC721/IERC721Receiver.sol	2023-08-13 10:10:06
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.6.0) (token/ERC721/IERC721Receiver.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ /**
+  * @title ERC721 token receiver interface

certora/diff/token_ERC721_utils_ERC721Holder.sol.patch

@@ -0,0 +1,11 @@
+--- token/ERC721/utils/ERC721Holder.sol	2023-08-11 20:33:54
++++ token/ERC721/utils/ERC721Holder.sol	2023-08-13 10:10:03
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.9.0) (token/ERC721/utils/ERC721Holder.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {IERC721Receiver} from "../IERC721Receiver.sol";
+ 

certora/diff/utils_Address.sol.patch

@@ -0,0 +1,11 @@
+--- utils/Address.sol	2023-08-11 20:33:54
++++ utils/Address.sol	2023-08-13 10:09:26
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.9.0) (utils/Address.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ /**
+  * @dev Collection of functions related to the address type

certora/harnesses/TimelockControllerHarness.sol

@@ -1,6 +1,6 @@
-pragma solidity ^0.8.20;
+pragma solidity ^0.8.19;
 
-import "../patched/governance/TimelockController.sol";
+import {TimelockController} from "../patched/governance/TimelockController.sol";
 
 contract TimelockControllerHarness is TimelockController {
     constructor(

certora/specs/AccessControlDefaultAdminRules.spec

@@ -12,8 +12,6 @@ use rule onlyGrantCanGrant filtered {
 │ Definitions                                                                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-definition defaultAdminRole() returns bytes32 = to_bytes32(0);
-
 definition timeSanity(env e) returns bool =
   e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48;
 
@@ -38,7 +36,7 @@ definition decreasingDelaySchedule(env e, uint48 newDelay) returns mathint =
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant defaultAdminConsistency(address account)
-  (account == defaultAdmin() && account != 0) <=> hasRole(defaultAdminRole(), account)
+  (account == defaultAdmin() && account != 0) <=> hasRole(DEFAULT_ADMIN_ROLE(), account)
   {
     preserved with (env e) {
       require nonzerosender(e);
@@ -51,7 +49,7 @@ invariant defaultAdminConsistency(address account)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant singleDefaultAdmin(address account, address another)
-  hasRole(defaultAdminRole(), account) && hasRole(defaultAdminRole(), another) => another == account
+  hasRole(DEFAULT_ADMIN_ROLE(), account) && hasRole(DEFAULT_ADMIN_ROLE(), another) => another == account
   {
     preserved {
       requireInvariant defaultAdminConsistency(account);
@@ -65,7 +63,7 @@ invariant singleDefaultAdmin(address account, address another)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant defaultAdminRoleAdminConsistency()
-  getRoleAdmin(defaultAdminRole()) == defaultAdminRole();
+  getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE();
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -96,7 +94,7 @@ rule revokeRoleEffect(env e, bytes32 role) {
     bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
     // liveness
-    assert success <=> isCallerAdmin && role != defaultAdminRole(),
+    assert success <=> isCallerAdmin && role != DEFAULT_ADMIN_ROLE(),
       "roles can only be revoked by their owner except for the default admin role";
 
     // effect
@@ -137,7 +135,7 @@ rule renounceRoleEffect(env e, bytes32 role) {
     assert success <=> (
       account == e.msg.sender &&
       (
-        role    != defaultAdminRole() ||
+        role    != DEFAULT_ADMIN_ROLE() ||
         account != adminBefore        ||
         (
           pendingAdminBefore == 0 &&
@@ -154,7 +152,7 @@ rule renounceRoleEffect(env e, bytes32 role) {
 
     assert success => (
       (
-        role    == defaultAdminRole() &&
+        role    == DEFAULT_ADMIN_ROLE() &&
         account == adminBefore
       ) ? (
         adminAfter        == 0 &&

certora/specs/TimelockController.spec

@@ -1,28 +1,27 @@
-import "helpers/helpers.spec"
-import "methods/IAccessControl.spec"
+import "helpers/helpers.spec";
+import "methods/IAccessControl.spec";
 
 methods {
-    TIMELOCK_ADMIN_ROLE()       returns (bytes32) envfree
-    PROPOSER_ROLE()             returns (bytes32) envfree
-    EXECUTOR_ROLE()             returns (bytes32) envfree
-    CANCELLER_ROLE()            returns (bytes32) envfree
-    isOperation(bytes32)        returns (bool)    envfree
-    isOperationPending(bytes32) returns (bool)    envfree
-    isOperationReady(bytes32)   returns (bool)
-    isOperationDone(bytes32)    returns (bool)    envfree
-    getTimestamp(bytes32)       returns (uint256) envfree
-    getMinDelay()               returns (uint256) envfree
-
-    hashOperation(address, uint256, bytes, bytes32, bytes32)            returns(bytes32) envfree
-    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree
-
-    schedule(address, uint256, bytes, bytes32, bytes32, uint256)
-    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256)
-    execute(address, uint256, bytes, bytes32, bytes32)
-    executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
-    cancel(bytes32)
-
-    updateDelay(uint256)
+    function PROPOSER_ROLE()             returns (bytes32) envfree
+    function EXECUTOR_ROLE()             returns (bytes32) envfree
+    function CANCELLER_ROLE()            returns (bytes32) envfree
+    function isOperation(bytes32)        external returns (bool)    envfree;
+    function isOperationPending(bytes32) external returns (bool)    envfree;
+    function isOperationReady(bytes32)   external returns (bool);
+    function isOperationDone(bytes32)    external returns (bool)    envfree;
+    function getTimestamp(bytes32)       external returns (uint256) envfree;
+    function getMinDelay()               external returns (uint256) envfree;
+
+    function hashOperation(address, uint256, bytes, bytes32, bytes32)            external returns(bytes32) envfree;
+    function hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) external returns(bytes32) envfree;
+
+    function schedule(address, uint256, bytes, bytes32, bytes32, uint256) external;
+    function scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) external;
+    function execute(address, uint256, bytes, bytes32, bytes32) external;
+    function executeBatch(address[], uint256[], bytes[], bytes32, bytes32) external;
+    function cancel(bytes32) external;
+
+    function updateDelay(uint256) external;
 }
 
 /*
@@ -32,11 +31,11 @@ methods {
 */
 // Uniformly handle scheduling of batched and non-batched operations.
 function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
-    if (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) {
+    if (f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) {
         address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
         require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
         schedule@withrevert(e, target, value, data, predecessor, salt, delay);
-    } else if (f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) {
+    } else if (f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) {
         address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt;
         require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
         scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay);
@@ -48,11 +47,11 @@ function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
 
 // Uniformly handle execution of batched and non-batched operations.
 function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) {
-    if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) {
+    if (f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector) {
         address target; uint256 value; bytes data; bytes32 salt;
         require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
         execute@withrevert(e, target, value, data, predecessor, salt);
-    } else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
+    } else if (f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
         address[] targets; uint256[] values; bytes[] payloads; bytes32 salt;
         require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
         executeBatch@withrevert(e, targets, values, payloads, predecessor, salt);
@@ -133,19 +132,19 @@ rule stateTransition(bytes32 id, env e, method f, calldataarg args) {
 
     // UNSET → PENDING: schedule or scheduleBatch
     assert stateBefore == UNSET() && stateAfter == PENDING() => (
-        f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
-        f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
+        f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
+        f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
     );
 
     // PENDING → UNSET: cancel
     assert stateBefore == PENDING() && stateAfter == UNSET() => (
-        f.selector == cancel(bytes32).selector
+        f.selector == sig:cancel(bytes32).selector
     );
 
     // PENDING → DONE: execute or executeBatch
     assert stateBefore == PENDING() && stateAfter == DONE() => (
-        f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector ||
-        f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
+        f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector ||
+        f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
     );
 
     // DONE is final
@@ -163,7 +162,7 @@ rule minDelayOnlyChange(env e) {
     method f; calldataarg args;
     f(e, args);
 
-    assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == updateDelay(uint256).selector), "Unauthorized delay update";
+    assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == sig:updateDelay(uint256).selector), "Unauthorized delay update";
 }
 
 /*
@@ -172,8 +171,8 @@ rule minDelayOnlyChange(env e) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
-    f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
-    f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
+    f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
+    f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
 } {
     require nonpayable(e);
 
@@ -212,8 +211,8 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
-    f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector ||
-    f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
+    f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector ||
+    f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
 } {
     bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
 

certora/specs/methods/IAccessControl.spec

@@ -1,4 +1,5 @@
 methods {
+    function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree;
     function hasRole(bytes32, address) external returns(bool) envfree;
     function getRoleAdmin(bytes32) external returns(bytes32) envfree;
     function grantRole(bytes32, address) external;