diff --git a/certora/diff/access_AccessControl.sol.patch b/certora/diff/access_AccessControl.sol.patch index c11474a50..364f9720d 100644 --- a/certora/diff/access_AccessControl.sol.patch +++ b/certora/diff/access_AccessControl.sol.patch @@ -1,5 +1,5 @@ --- access/AccessControl.sol 2023-08-10 22:02:18 -+++ access/AccessControl.sol 2023-08-10 22:11:07 ++++ access/AccessControl.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControl.sol) diff --git a/certora/diff/access_IAccessControl.sol.patch b/certora/diff/access_IAccessControl.sol.patch index 979939693..c107a500f 100644 --- a/certora/diff/access_IAccessControl.sol.patch +++ b/certora/diff/access_IAccessControl.sol.patch @@ -1,5 +1,5 @@ --- access/IAccessControl.sol 2023-08-10 22:02:20 -+++ access/IAccessControl.sol 2023-08-10 22:11:07 ++++ access/IAccessControl.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts v4.4.1 (access/IAccessControl.sol) diff --git a/certora/diff/access_Ownable.sol.patch b/certora/diff/access_Ownable.sol.patch index a680e047b..ad45e1cad 100644 --- a/certora/diff/access_Ownable.sol.patch +++ b/certora/diff/access_Ownable.sol.patch @@ -1,5 +1,5 @@ --- access/Ownable.sol 2023-08-09 11:45:05 -+++ access/Ownable.sol 2023-08-11 11:37:19 ++++ access/Ownable.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable.sol) diff --git a/certora/diff/access_Ownable2Step.sol.patch b/certora/diff/access_Ownable2Step.sol.patch index 6cdb69731..5ff6cf34c 100644 --- a/certora/diff/access_Ownable2Step.sol.patch +++ b/certora/diff/access_Ownable2Step.sol.patch @@ -1,5 +1,5 @@ --- access/Ownable2Step.sol 2023-08-09 11:45:05 -+++ access/Ownable2Step.sol 2023-08-11 11:37:27 ++++ access/Ownable2Step.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable2Step.sol) diff --git a/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch b/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch index cc4888a89..d5f36f324 100644 --- a/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch +++ b/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch @@ -1,5 +1,5 @@ --- access/extensions/AccessControlDefaultAdminRules.sol 2023-08-09 11:45:05 -+++ access/extensions/AccessControlDefaultAdminRules.sol 2023-08-10 22:18:05 ++++ access/extensions/AccessControlDefaultAdminRules.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControlDefaultAdminRules.sol) diff --git a/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch b/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch index f1635197c..d83ed3d45 100644 --- a/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch +++ b/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch @@ -1,5 +1,5 @@ --- access/extensions/IAccessControlDefaultAdminRules.sol 2023-08-09 11:45:05 -+++ access/extensions/IAccessControlDefaultAdminRules.sol 2023-08-10 22:18:08 ++++ access/extensions/IAccessControlDefaultAdminRules.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (access/IAccessControlDefaultAdminRules.sol) diff --git a/certora/diff/interfaces_IERC3156FlashBorrower.sol.patch b/certora/diff/interfaces_IERC3156FlashBorrower.sol.patch new file mode 100644 index 000000000..37eeda6fe --- /dev/null +++ b/certora/diff/interfaces_IERC3156FlashBorrower.sol.patch @@ -0,0 +1,11 @@ +--- interfaces/IERC3156FlashBorrower.sol 2023-08-09 11:45:05 ++++ interfaces/IERC3156FlashBorrower.sol 2023-08-11 13:36:59 +@@ -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 diff --git a/certora/diff/interfaces_IERC3156FlashLender.sol.patch b/certora/diff/interfaces_IERC3156FlashLender.sol.patch new file mode 100644 index 000000000..d76972044 --- /dev/null +++ b/certora/diff/interfaces_IERC3156FlashLender.sol.patch @@ -0,0 +1,11 @@ +--- interfaces/IERC3156FlashLender.sol 2023-08-09 11:45:05 ++++ interfaces/IERC3156FlashLender.sol 2023-08-11 13:37:04 +@@ -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"; + diff --git a/certora/diff/interfaces_IERC5267.sol.patch b/certora/diff/interfaces_IERC5267.sol.patch new file mode 100644 index 000000000..95fc8e1aa --- /dev/null +++ b/certora/diff/interfaces_IERC5267.sol.patch @@ -0,0 +1,11 @@ +--- interfaces/IERC5267.sol 2023-08-09 11:45:05 ++++ interfaces/IERC5267.sol 2023-08-11 12:22:17 +@@ -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 { + /** diff --git a/certora/diff/interfaces_IERC5313.sol.patch b/certora/diff/interfaces_IERC5313.sol.patch index d43874bf4..46a20d738 100644 --- a/certora/diff/interfaces_IERC5313.sol.patch +++ b/certora/diff/interfaces_IERC5313.sol.patch @@ -1,5 +1,5 @@ --- interfaces/IERC5313.sol 2023-08-09 11:45:05 -+++ interfaces/IERC5313.sol 2023-08-10 22:18:26 ++++ interfaces/IERC5313.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (interfaces/IERC5313.sol) diff --git a/certora/diff/interfaces_draft-IERC6093.sol.patch b/certora/diff/interfaces_draft-IERC6093.sol.patch new file mode 100644 index 000000000..a386ac7d5 --- /dev/null +++ b/certora/diff/interfaces_draft-IERC6093.sol.patch @@ -0,0 +1,9 @@ +--- interfaces/draft-IERC6093.sol 2023-08-09 11:45:05 ++++ interfaces/draft-IERC6093.sol 2023-08-11 12:22:17 +@@ -1,5 +1,5 @@ + // SPDX-License-Identifier: MIT +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + /** + * @dev Standard ERC20 Errors diff --git a/certora/diff/security_Pausable.sol.patch b/certora/diff/security_Pausable.sol.patch index 7bc32deaa..201a2d09b 100644 --- a/certora/diff/security_Pausable.sol.patch +++ b/certora/diff/security_Pausable.sol.patch @@ -1,5 +1,5 @@ --- security/Pausable.sol 2023-08-10 21:54:54 -+++ security/Pausable.sol 2023-08-10 22:11:07 ++++ security/Pausable.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.7.0) (security/Pausable.sol) diff --git a/certora/diff/token_ERC20_ERC20.sol.patch b/certora/diff/token_ERC20_ERC20.sol.patch new file mode 100644 index 000000000..1c1c39aa4 --- /dev/null +++ b/certora/diff/token_ERC20_ERC20.sol.patch @@ -0,0 +1,11 @@ +--- token/ERC20/ERC20.sol 2023-08-09 11:45:05 ++++ token/ERC20/ERC20.sol 2023-08-11 13:37:08 +@@ -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"; diff --git a/certora/diff/token_ERC20_IERC20.sol.patch b/certora/diff/token_ERC20_IERC20.sol.patch new file mode 100644 index 000000000..176b31f0b --- /dev/null +++ b/certora/diff/token_ERC20_IERC20.sol.patch @@ -0,0 +1,11 @@ +--- token/ERC20/IERC20.sol 2023-08-09 11:45:05 ++++ token/ERC20/IERC20.sol 2023-08-11 12:22:17 +@@ -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. diff --git a/certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch b/certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch new file mode 100644 index 000000000..1e3e887c7 --- /dev/null +++ b/certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch @@ -0,0 +1,11 @@ +--- token/ERC20/extensions/ERC20FlashMint.sol 2023-08-09 11:45:05 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2023-08-11 13:36:55 +@@ -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"; diff --git a/certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch b/certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch new file mode 100644 index 000000000..823536d32 --- /dev/null +++ b/certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch @@ -0,0 +1,11 @@ +--- token/ERC20/extensions/ERC20Permit.sol 2023-08-09 11:45:05 ++++ token/ERC20/extensions/ERC20Permit.sol 2023-08-11 12:22:17 +@@ -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"; diff --git a/certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch b/certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch new file mode 100644 index 000000000..9dd2cebf9 --- /dev/null +++ b/certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch @@ -0,0 +1,11 @@ +--- token/ERC20/extensions/IERC20Metadata.sol 2023-08-09 11:45:05 ++++ token/ERC20/extensions/IERC20Metadata.sol 2023-08-11 12:22:17 +@@ -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"; + diff --git a/certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch b/certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch new file mode 100644 index 000000000..d5dadfb65 --- /dev/null +++ b/certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch @@ -0,0 +1,11 @@ +--- token/ERC20/extensions/IERC20Permit.sol 2023-08-11 12:19:57 ++++ token/ERC20/extensions/IERC20Permit.sol 2023-08-11 12:22:17 +@@ -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 diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch index d29518304..f324da6c3 100644 --- a/certora/diff/token_ERC721_ERC721.sol.patch +++ b/certora/diff/token_ERC721_ERC721.sol.patch @@ -1,5 +1,5 @@ --- token/ERC721/ERC721.sol 2023-08-10 16:45:36 -+++ token/ERC721/ERC721.sol 2023-08-10 22:11:07 ++++ token/ERC721/ERC721.sol 2023-08-11 12:22:17 @@ -208,6 +208,11 @@ return _owners[tokenId]; } diff --git a/certora/diff/utils_Context.sol.patch b/certora/diff/utils_Context.sol.patch index f458c6d6e..439e7f79c 100644 --- a/certora/diff/utils_Context.sol.patch +++ b/certora/diff/utils_Context.sol.patch @@ -1,5 +1,5 @@ --- utils/Context.sol 2023-08-10 21:54:56 -+++ utils/Context.sol 2023-08-10 22:11:07 ++++ utils/Context.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts v4.4.1 (utils/Context.sol) diff --git a/certora/diff/utils_Nonces.sol.patch b/certora/diff/utils_Nonces.sol.patch new file mode 100644 index 000000000..e1d425f83 --- /dev/null +++ b/certora/diff/utils_Nonces.sol.patch @@ -0,0 +1,9 @@ +--- utils/Nonces.sol 2023-08-09 11:45:05 ++++ utils/Nonces.sol 2023-08-11 12:22:17 +@@ -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. diff --git a/certora/diff/utils_ShortStrings.sol.patch b/certora/diff/utils_ShortStrings.sol.patch new file mode 100644 index 000000000..b136afb53 --- /dev/null +++ b/certora/diff/utils_ShortStrings.sol.patch @@ -0,0 +1,11 @@ +--- utils/ShortStrings.sol 2023-08-09 11:45:05 ++++ utils/ShortStrings.sol 2023-08-11 12:22:17 +@@ -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"; + diff --git a/certora/diff/utils_StorageSlot.sol.patch b/certora/diff/utils_StorageSlot.sol.patch new file mode 100644 index 000000000..82e23b6d3 --- /dev/null +++ b/certora/diff/utils_StorageSlot.sol.patch @@ -0,0 +1,11 @@ +--- utils/StorageSlot.sol 2023-08-09 11:45:05 ++++ utils/StorageSlot.sol 2023-08-11 12:22:17 +@@ -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. diff --git a/certora/diff/utils_Strings.sol.patch b/certora/diff/utils_Strings.sol.patch new file mode 100644 index 000000000..da3d37b48 --- /dev/null +++ b/certora/diff/utils_Strings.sol.patch @@ -0,0 +1,11 @@ +--- utils/Strings.sol 2023-08-09 11:45:05 ++++ utils/Strings.sol 2023-08-11 12:22:44 +@@ -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"; diff --git a/certora/diff/utils_cryptography_ECDSA.sol.patch b/certora/diff/utils_cryptography_ECDSA.sol.patch new file mode 100644 index 000000000..ba22b8b56 --- /dev/null +++ b/certora/diff/utils_cryptography_ECDSA.sol.patch @@ -0,0 +1,11 @@ +--- utils/cryptography/ECDSA.sol 2023-08-09 11:45:05 ++++ utils/cryptography/ECDSA.sol 2023-08-11 12:22:17 +@@ -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. diff --git a/certora/diff/utils_cryptography_EIP712.sol.patch b/certora/diff/utils_cryptography_EIP712.sol.patch new file mode 100644 index 000000000..ea92c8e6a --- /dev/null +++ b/certora/diff/utils_cryptography_EIP712.sol.patch @@ -0,0 +1,11 @@ +--- utils/cryptography/EIP712.sol 2023-08-09 11:45:05 ++++ utils/cryptography/EIP712.sol 2023-08-11 12:22:17 +@@ -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"; diff --git a/certora/diff/utils_cryptography_MessageHashUtils.sol.patch b/certora/diff/utils_cryptography_MessageHashUtils.sol.patch new file mode 100644 index 000000000..21db04759 --- /dev/null +++ b/certora/diff/utils_cryptography_MessageHashUtils.sol.patch @@ -0,0 +1,10 @@ +--- utils/cryptography/MessageHashUtils.sol 2023-08-09 11:45:05 ++++ utils/cryptography/MessageHashUtils.sol 2023-08-11 12:22:17 +@@ -1,6 +1,6 @@ + // SPDX-License-Identifier: MIT + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + import {Strings} from "../Strings.sol"; + diff --git a/certora/diff/utils_introspection_ERC165.sol.patch b/certora/diff/utils_introspection_ERC165.sol.patch index d0ec74e92..ad5462127 100644 --- a/certora/diff/utils_introspection_ERC165.sol.patch +++ b/certora/diff/utils_introspection_ERC165.sol.patch @@ -1,5 +1,5 @@ --- utils/introspection/ERC165.sol 2023-08-10 22:02:24 -+++ utils/introspection/ERC165.sol 2023-08-10 22:11:07 ++++ utils/introspection/ERC165.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts v4.4.1 (utils/introspection/ERC165.sol) diff --git a/certora/diff/utils_introspection_IERC165.sol.patch b/certora/diff/utils_introspection_IERC165.sol.patch index b100b173e..3c3c756ed 100644 --- a/certora/diff/utils_introspection_IERC165.sol.patch +++ b/certora/diff/utils_introspection_IERC165.sol.patch @@ -1,5 +1,5 @@ --- utils/introspection/IERC165.sol 2023-08-09 11:45:05 -+++ utils/introspection/IERC165.sol 2023-08-10 22:11:07 ++++ utils/introspection/IERC165.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts v4.4.1 (utils/introspection/IERC165.sol) diff --git a/certora/diff/utils_math_Math.sol.patch b/certora/diff/utils_math_Math.sol.patch index 5cd5cb6a0..2dcf53c57 100644 --- a/certora/diff/utils_math_Math.sol.patch +++ b/certora/diff/utils_math_Math.sol.patch @@ -1,5 +1,5 @@ --- utils/math/Math.sol 2023-08-09 11:45:05 -+++ utils/math/Math.sol 2023-08-10 22:18:22 ++++ utils/math/Math.sol 2023-08-11 12:22:17 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (utils/math/Math.sol) diff --git a/certora/diff/utils_math_SafeCast.sol.patch b/certora/diff/utils_math_SafeCast.sol.patch index ff15ee72e..d7a9d0a77 100644 --- a/certora/diff/utils_math_SafeCast.sol.patch +++ b/certora/diff/utils_math_SafeCast.sol.patch @@ -1,5 +1,5 @@ --- utils/math/SafeCast.sol 2023-08-09 11:45:05 -+++ utils/math/SafeCast.sol 2023-08-10 22:18:17 ++++ utils/math/SafeCast.sol 2023-08-11 12:22:17 @@ -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. diff --git a/certora/diff/utils_math_SignedMath.sol.patch b/certora/diff/utils_math_SignedMath.sol.patch new file mode 100644 index 000000000..a777bbd8b --- /dev/null +++ b/certora/diff/utils_math_SignedMath.sol.patch @@ -0,0 +1,11 @@ +--- utils/math/SignedMath.sol 2023-08-09 11:45:05 ++++ utils/math/SignedMath.sol 2023-08-11 12:22:51 +@@ -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. diff --git a/certora/diff/utils_structs_DoubleEndedQueue.sol.patch b/certora/diff/utils_structs_DoubleEndedQueue.sol.patch index c6c45476a..98fe810b5 100644 --- a/certora/diff/utils_structs_DoubleEndedQueue.sol.patch +++ b/certora/diff/utils_structs_DoubleEndedQueue.sol.patch @@ -1,5 +1,5 @@ --- utils/structs/DoubleEndedQueue.sol 2023-08-09 11:45:05 -+++ utils/structs/DoubleEndedQueue.sol 2023-08-10 23:15:17 ++++ utils/structs/DoubleEndedQueue.sol 2023-08-11 12:22:17 @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v4.9.0) (utils/structs/DoubleEndedQueue.sol) diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol index 1041c1715..d4c346247 100644 --- a/certora/harnesses/ERC20PermitHarness.sol +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -1,8 +1,8 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.20; +pragma solidity ^0.8.19; -import "../patched/token/ERC20/extensions/ERC20Permit.sol"; +import {ERC20Permit, ERC20} from "../patched/token/ERC20/extensions/ERC20Permit.sol"; contract ERC20PermitHarness is ERC20Permit { constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 3bd2b38ba..3eca1d4f3 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -1,15 +1,15 @@ -import "helpers/helpers.spec" -import "methods/IERC20.spec" -import "methods/IERC2612.spec" +import "helpers/helpers.spec"; +import "methods/IERC20.spec"; +import "methods/IERC2612.spec"; methods { // non standard ERC20 functions - increaseAllowance(address,uint256) returns (bool) - decreaseAllowance(address,uint256) returns (bool) + function increaseAllowance(address,uint256) external returns (bool); + function decreaseAllowance(address,uint256) external returns (bool); // exposed for FV - mint(address,uint256) - burn(address,uint256) + function mint(address,uint256) external; + function burn(address,uint256) external; } /* @@ -17,7 +17,7 @@ methods { │ Ghost & hooks: sum of all balances │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -ghost sumOfBalances() returns uint256 { +ghost sumOfBalances() returns mathint { init_state axiom sumOfBalances() == 0; } @@ -31,7 +31,7 @@ hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STOR └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant totalSupplyIsSumOfBalances() - totalSupply() == sumOfBalances() + to_mathint(totalSupply()) == sumOfBalances(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -39,7 +39,7 @@ invariant totalSupplyIsSumOfBalances() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant zeroAddressNoBalance() - balanceOf(0) == 0 + balanceOf(0) == 0; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -56,8 +56,8 @@ rule noChangeTotalSupply(env e) { f(e, args); uint256 totalSupplyAfter = totalSupply(); - assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector; - assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector; + assert totalSupplyAfter > totalSupplyBefore => f.selector == sig:mint(address,uint256).selector; + assert totalSupplyAfter < totalSupplyBefore => f.selector == sig:burn(address,uint256).selector; } /* @@ -80,9 +80,9 @@ rule onlyAuthorizedCanTransfer(env e) { assert ( balanceAfter < balanceBefore ) => ( - f.selector == burn(address,uint256).selector || + f.selector == sig:burn(address,uint256).selector || e.msg.sender == account || - balanceBefore - balanceAfter <= allowanceBefore + balanceBefore - balanceAfter <= to_mathint(allowanceBefore) ); } @@ -106,18 +106,18 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) { assert ( allowanceAfter > allowanceBefore ) => ( - (f.selector == approve(address,uint256).selector && e.msg.sender == holder) || - (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) || - (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) + (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder) || + (f.selector == sig:increaseAllowance(address,uint256).selector && e.msg.sender == holder) || + (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) ); assert ( allowanceAfter < allowanceBefore ) => ( - (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) || - (f.selector == approve(address,uint256).selector && e.msg.sender == holder ) || - (f.selector == decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) || - (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) + (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) || + (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == sig:decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) ); } @@ -147,8 +147,8 @@ rule mint(env e) { assert to == 0 || totalSupplyBefore + amount > max_uint256; } else { // updates balance and totalSupply - assert balanceOf(to) == toBalanceBefore + amount; - assert totalSupply() == totalSupplyBefore + amount; + assert to_mathint(balanceOf(to)) == toBalanceBefore + amount; + assert to_mathint(totalSupply()) == totalSupplyBefore + amount; // no other balance is modified assert balanceOf(other) != otherBalanceBefore => other == to; @@ -181,8 +181,8 @@ rule burn(env e) { assert from == 0 || fromBalanceBefore < amount; } else { // updates balance and totalSupply - assert balanceOf(from) == fromBalanceBefore - amount; - assert totalSupply() == totalSupplyBefore - amount; + assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount; + assert to_mathint(totalSupply()) == totalSupplyBefore - amount; // no other balance is modified assert balanceOf(other) != otherBalanceBefore => other == from; @@ -216,8 +216,8 @@ rule transfer(env e) { assert holder == 0 || recipient == 0 || amount > holderBalanceBefore; } else { // balances of holder and recipient are updated - assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); - assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); // no other balance is modified assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); @@ -254,11 +254,11 @@ rule transferFrom(env e) { } else { // allowance is valid & updated assert allowanceBefore >= amount; - assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount); + assert to_mathint(allowance(holder, spender)) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount); // balances of holder and recipient are updated - assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); - assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); // no other balance is modified assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); @@ -323,7 +323,7 @@ rule increaseAllowance(env e) { assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256; } else { // allowance is updated - assert allowance(holder, spender) == allowanceBefore + amount; + assert to_mathint(allowance(holder, spender)) == allowanceBefore + amount; // other allowances are untouched assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); @@ -356,7 +356,7 @@ rule decreaseAllowance(env e) { assert holder == 0 || spender == 0 || allowanceBefore < amount; } else { // allowance is updated - assert allowance(holder, spender) == allowanceBefore - amount; + assert to_mathint(allowance(holder, spender)) == allowanceBefore - amount; // other allowances are untouched assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); @@ -402,7 +402,7 @@ rule permit(env e) { } else { // allowance and nonce are updated assert allowance(holder, spender) == amount; - assert nonces(holder) == nonceBefore + 1; + assert to_mathint(nonces(holder)) == nonceBefore + 1; // deadline was respected assert deadline >= e.block.timestamp; diff --git a/certora/specs/methods/IERC20.spec b/certora/specs/methods/IERC20.spec index cfa454e13..100901a04 100644 --- a/certora/specs/methods/IERC20.spec +++ b/certora/specs/methods/IERC20.spec @@ -1,11 +1,11 @@ methods { - name() returns (string) envfree => DISPATCHER(true) - symbol() returns (string) envfree => DISPATCHER(true) - decimals() returns (uint8) envfree => DISPATCHER(true) - totalSupply() returns (uint256) envfree => DISPATCHER(true) - balanceOf(address) returns (uint256) envfree => DISPATCHER(true) - allowance(address,address) returns (uint256) envfree => DISPATCHER(true) - approve(address,uint256) returns (bool) => DISPATCHER(true) - transfer(address,uint256) returns (bool) => DISPATCHER(true) - transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) + function name() external returns (string) envfree; + function symbol() external returns (string) envfree; + function decimals() external returns (uint8) envfree; + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function allowance(address,address) external returns (uint256) envfree; + function approve(address,uint256) external returns (bool); + function transfer(address,uint256) external returns (bool); + function transferFrom(address,address,uint256) external returns (bool); }