diff --git a/certora/diff/governance_TimelockController.sol.patch b/certora/diff/governance_TimelockController.sol.patch new file mode 100644 index 000000000..cfe4d3e24 --- /dev/null +++ b/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"; diff --git a/certora/diff/token_ERC1155_IERC1155Receiver.sol.patch b/certora/diff/token_ERC1155_IERC1155Receiver.sol.patch new file mode 100644 index 000000000..3495ce3f9 --- /dev/null +++ b/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"; + diff --git a/certora/diff/token_ERC1155_utils_ERC1155Holder.sol.patch b/certora/diff/token_ERC1155_utils_ERC1155Holder.sol.patch new file mode 100644 index 000000000..c45806475 --- /dev/null +++ b/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"; diff --git a/certora/diff/token_ERC721_ERC721.sol.orig.patch b/certora/diff/token_ERC721_ERC721.sol.orig.patch new file mode 100644 index 000000000..2d32a9266 --- /dev/null +++ b/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)) ++ } ++ } ++ } ++ } ++ } ++} diff --git a/certora/diff/token_ERC721_IERC721Receiver.sol.patch b/certora/diff/token_ERC721_IERC721Receiver.sol.patch new file mode 100644 index 000000000..852e3a424 --- /dev/null +++ b/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 diff --git a/certora/diff/token_ERC721_utils_ERC721Holder.sol.patch b/certora/diff/token_ERC721_utils_ERC721Holder.sol.patch new file mode 100644 index 000000000..6d43310cc --- /dev/null +++ b/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"; + diff --git a/certora/diff/utils_Address.sol.patch b/certora/diff/utils_Address.sol.patch new file mode 100644 index 000000000..ecd04586a --- /dev/null +++ b/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 diff --git a/certora/harnesses/TimelockControllerHarness.sol b/certora/harnesses/TimelockControllerHarness.sol index 476a8376c..985ed24a4 100644 --- a/certora/harnesses/TimelockControllerHarness.sol +++ b/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( diff --git a/certora/specs/AccessControlDefaultAdminRules.spec b/certora/specs/AccessControlDefaultAdminRules.spec index 6b116b637..c9dcaaaa2 100644 --- a/certora/specs/AccessControlDefaultAdminRules.spec +++ b/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 && diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 05ecb1340..d40ebda84 100644 --- a/certora/specs/TimelockController.spec +++ b/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); diff --git a/certora/specs/methods/IAccessControl.spec b/certora/specs/methods/IAccessControl.spec index c75e4ef2d..5c395b088 100644 --- a/certora/specs/methods/IAccessControl.spec +++ b/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;