Upgrade certora-cli to support Solidity 0.8.20

certora/diff/access_AccessControl.sol.patch

@@ -1,11 +0,0 @@
---- access/AccessControl.sol	2023-08-11 20:33:54
-+++ access/AccessControl.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControl.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IAccessControl} from "./IAccessControl.sol";
- import {Context} from "../utils/Context.sol";

certora/diff/access_IAccessControl.sol.patch

@@ -1,11 +0,0 @@
---- access/IAccessControl.sol	2023-08-11 20:33:54
-+++ access/IAccessControl.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts v4.4.1 (access/IAccessControl.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev External interface of AccessControl declared to support ERC165 detection.

certora/diff/access_Ownable.sol.patch

@@ -1,11 +0,0 @@
---- access/Ownable.sol	2023-08-11 20:33:54
-+++ access/Ownable.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {Context} from "../utils/Context.sol";
- 

certora/diff/access_Ownable2Step.sol.patch

@@ -1,11 +0,0 @@
---- access/Ownable2Step.sol	2023-08-11 20:33:54
-+++ access/Ownable2Step.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable2Step.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {Ownable} from "./Ownable.sol";
- 

certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch

@@ -1,11 +0,0 @@
---- access/extensions/AccessControlDefaultAdminRules.sol	2023-08-11 20:33:54
-+++ access/extensions/AccessControlDefaultAdminRules.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControlDefaultAdminRules.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IAccessControlDefaultAdminRules} from "./IAccessControlDefaultAdminRules.sol";
- import {AccessControl, IAccessControl} from "../AccessControl.sol";

certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch

@@ -1,11 +0,0 @@
---- access/extensions/IAccessControlDefaultAdminRules.sol	2023-08-11 20:33:54
-+++ access/extensions/IAccessControlDefaultAdminRules.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (access/IAccessControlDefaultAdminRules.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IAccessControl} from "../IAccessControl.sol";
- 

certora/diff/governance_TimelockController.sol.patch

@@ -1,11 +0,0 @@
---- 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/interfaces_IERC3156FlashBorrower.sol.patch

@@ -1,11 +0,0 @@
---- interfaces/IERC3156FlashBorrower.sol	2023-08-11 20:33:54
-+++ interfaces/IERC3156FlashBorrower.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (interfaces/IERC3156FlashBorrower.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Interface of the ERC3156 FlashBorrower, as defined in

certora/diff/interfaces_IERC3156FlashLender.sol.patch

@@ -1,11 +0,0 @@
---- interfaces/IERC3156FlashLender.sol	2023-08-11 20:33:54
-+++ interfaces/IERC3156FlashLender.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts v4.4.1 (interfaces/IERC3156FlashLender.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IERC3156FlashBorrower} from "./IERC3156FlashBorrower.sol";
- 

certora/diff/interfaces_IERC5267.sol.patch

@@ -1,11 +0,0 @@
---- interfaces/IERC5267.sol	2023-08-11 20:33:54
-+++ interfaces/IERC5267.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (interfaces/IERC5267.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- interface IERC5267 {
-     /**

certora/diff/interfaces_IERC5313.sol.patch

@@ -1,11 +0,0 @@
---- interfaces/IERC5313.sol	2023-08-11 20:33:54
-+++ interfaces/IERC5313.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (interfaces/IERC5313.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Interface for the Light Contract Ownership Standard.

certora/diff/interfaces_draft-IERC6093.sol.patch

@@ -1,9 +0,0 @@
---- interfaces/draft-IERC6093.sol	2023-08-11 20:33:54
-+++ interfaces/draft-IERC6093.sol	2023-08-13 09:56:16
-@@ -1,5 +1,5 @@
- // SPDX-License-Identifier: MIT
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Standard ERC20 Errors

certora/diff/proxy_utils_Initializable.sol.patch

@@ -1,11 +0,0 @@
---- proxy/utils/Initializable.sol	2023-08-11 20:33:54
-+++ proxy/utils/Initializable.sol	2023-08-13 09:56:19
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (proxy/utils/Initializable.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev This is a base contract to aid in writing upgradeable contracts, or any kind of contract that will be deployed

certora/diff/security_Pausable.sol.patch

@@ -1,11 +0,0 @@
---- security/Pausable.sol	2023-08-11 20:33:54
-+++ security/Pausable.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.7.0) (security/Pausable.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {Context} from "../utils/Context.sol";
- 

certora/diff/token_ERC1155_IERC1155Receiver.sol.patch

@@ -1,11 +0,0 @@
---- 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

@@ -1,11 +0,0 @@
---- 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_ERC20_ERC20.sol.patch

@@ -1,11 +0,0 @@
---- token/ERC20/ERC20.sol	2023-08-11 20:33:54
-+++ token/ERC20/ERC20.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (token/ERC20/ERC20.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IERC20} from "./IERC20.sol";
- import {IERC20Metadata} from "./extensions/IERC20Metadata.sol";

certora/diff/token_ERC20_IERC20.sol.patch

@@ -1,11 +0,0 @@
---- token/ERC20/IERC20.sol	2023-08-11 20:33:54
-+++ token/ERC20/IERC20.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (token/ERC20/IERC20.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Interface of the ERC20 standard as defined in the EIP.

certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch

@@ -1,11 +0,0 @@
---- token/ERC20/extensions/ERC20FlashMint.sol	2023-08-11 20:33:54
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.8.0) (token/ERC20/extensions/ERC20FlashMint.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IERC3156FlashBorrower} from "../../../interfaces/IERC3156FlashBorrower.sol";
- import {IERC3156FlashLender} from "../../../interfaces/IERC3156FlashLender.sol";

certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch

@@ -1,11 +0,0 @@
---- token/ERC20/extensions/ERC20Permit.sol	2023-08-11 20:33:54
-+++ token/ERC20/extensions/ERC20Permit.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (token/ERC20/extensions/ERC20Permit.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IERC20Permit} from "./IERC20Permit.sol";
- import {ERC20} from "../ERC20.sol";

certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch

@@ -1,11 +0,0 @@
---- token/ERC20/extensions/IERC20Metadata.sol	2023-08-11 20:33:54
-+++ token/ERC20/extensions/IERC20Metadata.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts v4.4.1 (token/ERC20/extensions/IERC20Metadata.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IERC20} from "../IERC20.sol";
- 

certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch

@@ -1,11 +0,0 @@
---- token/ERC20/extensions/IERC20Permit.sol	2023-08-11 20:33:54
-+++ token/ERC20/extensions/IERC20Permit.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (token/ERC20/extensions/IERC20Permit.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Interface of the ERC20 Permit extension allowing approvals to be made via signatures, as defined in

certora/diff/token_ERC721_ERC721.sol.orig.patch

@@ -1,468 +0,0 @@
---- 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

@@ -1,11 +0,0 @@
---- 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

@@ -1,11 +0,0 @@
---- 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

@@ -1,11 +0,0 @@
---- 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/diff/utils_Context.sol.patch

@@ -1,11 +0,0 @@
---- utils/Context.sol	2023-08-11 20:33:54
-+++ utils/Context.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts v4.4.1 (utils/Context.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Provides information about the current execution context, including the

certora/diff/utils_Nonces.sol.patch

@@ -1,9 +0,0 @@
---- utils/Nonces.sol	2023-08-11 20:33:54
-+++ utils/Nonces.sol	2023-08-13 09:56:16
-@@ -1,5 +1,5 @@
- // SPDX-License-Identifier: MIT
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Provides tracking nonces for addresses. Nonces will only increment.

certora/diff/utils_ShortStrings.sol.patch

@@ -1,11 +0,0 @@
---- utils/ShortStrings.sol	2023-08-11 20:33:54
-+++ utils/ShortStrings.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (utils/ShortStrings.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {StorageSlot} from "./StorageSlot.sol";
- 

certora/diff/utils_StorageSlot.sol.patch

@@ -1,11 +0,0 @@
---- utils/StorageSlot.sol	2023-08-11 20:33:54
-+++ utils/StorageSlot.sol	2023-08-13 09:56:16
-@@ -2,7 +2,7 @@
- // OpenZeppelin Contracts (last updated v4.9.0) (utils/StorageSlot.sol)
- // This file was procedurally generated from scripts/generate/templates/StorageSlot.js.
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Library for reading and writing primitive types to specific storage slots.

certora/diff/utils_Strings.sol.patch

@@ -1,11 +0,0 @@
---- utils/Strings.sol	2023-08-11 20:33:54
-+++ utils/Strings.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (utils/Strings.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {Math} from "./math/Math.sol";
- import {SignedMath} from "./math/SignedMath.sol";

certora/diff/utils_cryptography_ECDSA.sol.patch

@@ -1,11 +0,0 @@
---- utils/cryptography/ECDSA.sol	2023-08-11 20:33:54
-+++ utils/cryptography/ECDSA.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (utils/cryptography/ECDSA.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Elliptic Curve Digital Signature Algorithm (ECDSA) operations.

certora/diff/utils_cryptography_EIP712.sol.patch

@@ -1,11 +0,0 @@
---- utils/cryptography/EIP712.sol	2023-08-11 20:33:54
-+++ utils/cryptography/EIP712.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (utils/cryptography/EIP712.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {MessageHashUtils} from "./MessageHashUtils.sol";
- import {ShortStrings, ShortString} from "../ShortStrings.sol";

certora/diff/utils_cryptography_MessageHashUtils.sol.patch

@@ -1,10 +0,0 @@
---- utils/cryptography/MessageHashUtils.sol	2023-08-11 20:33:54
-+++ utils/cryptography/MessageHashUtils.sol	2023-08-13 09:56:16
-@@ -1,6 +1,6 @@
- // SPDX-License-Identifier: MIT
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {Strings} from "../Strings.sol";
- 

certora/diff/utils_introspection_ERC165.sol.patch

@@ -1,11 +0,0 @@
---- utils/introspection/ERC165.sol	2023-08-11 20:33:54
-+++ utils/introspection/ERC165.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts v4.4.1 (utils/introspection/ERC165.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- import {IERC165} from "./IERC165.sol";
- 

certora/diff/utils_introspection_IERC165.sol.patch

@@ -1,11 +0,0 @@
---- utils/introspection/IERC165.sol	2023-08-11 20:33:54
-+++ utils/introspection/IERC165.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts v4.4.1 (utils/introspection/IERC165.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Interface of the ERC165 standard, as defined in the

certora/diff/utils_math_Math.sol.patch

@@ -1,11 +0,0 @@
---- utils/math/Math.sol	2023-08-11 20:33:54
-+++ utils/math/Math.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (utils/math/Math.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Standard math utilities missing in the Solidity language.

certora/diff/utils_math_SafeCast.sol.patch

@@ -1,11 +0,0 @@
---- utils/math/SafeCast.sol	2023-08-11 20:33:54
-+++ utils/math/SafeCast.sol	2023-08-13 09:56:16
-@@ -2,7 +2,7 @@
- // OpenZeppelin Contracts (last updated v4.8.0) (utils/math/SafeCast.sol)
- // This file was procedurally generated from scripts/generate/templates/SafeCast.js.
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Wrappers over Solidity's uintXX/intXX casting operators with added overflow

certora/diff/utils_math_SignedMath.sol.patch

@@ -1,11 +0,0 @@
---- utils/math/SignedMath.sol	2023-08-11 20:33:54
-+++ utils/math/SignedMath.sol	2023-08-13 09:56:16
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.8.0) (utils/math/SignedMath.sol)
- 
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev Standard signed math utilities missing in the Solidity language.

certora/diff/utils_structs_DoubleEndedQueue.sol.patch

@@ -1,10 +0,0 @@
---- utils/structs/DoubleEndedQueue.sol	2023-08-11 20:33:54
-+++ utils/structs/DoubleEndedQueue.sol	2023-08-13 09:56:16
-@@ -1,6 +1,6 @@
- // SPDX-License-Identifier: MIT
- // OpenZeppelin Contracts (last updated v4.9.0) (utils/structs/DoubleEndedQueue.sol)
--pragma solidity ^0.8.20;
-+pragma solidity ^0.8.19;
- 
- /**
-  * @dev A sequence of items with the ability to efficiently push and pop items (i.e. insert and remove) on both ends of

certora/specs/methods/IERC5313.spec

@@ -1,3 +1,3 @@
 methods {
-    owner() returns (address) envfree
+    function owner() external returns (address) envfree;
 }

requirements.txt

@@ -1 +1 @@
-certora-cli==4.3.1
+certora-cli==4.8.0