From 01aea1b70495a48d82314821a62001ba383fd328 Mon Sep 17 00:00:00 2001
From: ernestognw <ernestognw@gmail.com>
Date: Sun, 13 Aug 2023 10:00:29 -0600
Subject: [PATCH] Finish Initializable

---
 certora/diff/access_AccessControl.sol.patch   |  4 +-
 certora/diff/access_IAccessControl.sol.patch  |  4 +-
 certora/diff/access_Ownable.sol.patch         |  4 +-
 certora/diff/access_Ownable2Step.sol.patch    |  4 +-
 ...s_AccessControlDefaultAdminRules.sol.patch |  4 +-
 ..._IAccessControlDefaultAdminRules.sol.patch |  4 +-
 ...interfaces_IERC3156FlashBorrower.sol.patch |  4 +-
 .../interfaces_IERC3156FlashLender.sol.patch  |  4 +-
 certora/diff/interfaces_IERC5267.sol.patch    |  4 +-
 certora/diff/interfaces_IERC5313.sol.patch    |  4 +-
 .../diff/interfaces_draft-IERC6093.sol.patch  |  4 +-
 .../diff/proxy_utils_Initializable.sol.patch  | 11 ++++++
 certora/diff/security_Pausable.sol.patch      |  4 +-
 certora/diff/token_ERC20_ERC20.sol.patch      |  4 +-
 certora/diff/token_ERC20_IERC20.sol.patch     |  4 +-
 ..._ERC20_extensions_ERC20FlashMint.sol.patch |  4 +-
 ...ken_ERC20_extensions_ERC20Permit.sol.patch |  4 +-
 ..._ERC20_extensions_IERC20Metadata.sol.patch |  4 +-
 ...en_ERC20_extensions_IERC20Permit.sol.patch |  4 +-
 certora/diff/token_ERC721_ERC721.sol.patch    | 10 ++---
 certora/diff/utils_Context.sol.patch          |  4 +-
 certora/diff/utils_Nonces.sol.patch           |  4 +-
 certora/diff/utils_ShortStrings.sol.patch     |  4 +-
 certora/diff/utils_StorageSlot.sol.patch      |  4 +-
 certora/diff/utils_Strings.sol.patch          |  4 +-
 .../diff/utils_cryptography_ECDSA.sol.patch   |  4 +-
 .../diff/utils_cryptography_EIP712.sol.patch  |  4 +-
 ...ls_cryptography_MessageHashUtils.sol.patch |  4 +-
 .../diff/utils_introspection_ERC165.sol.patch |  4 +-
 .../utils_introspection_IERC165.sol.patch     |  4 +-
 certora/diff/utils_math_Math.sol.patch        |  4 +-
 certora/diff/utils_math_SafeCast.sol.patch    |  4 +-
 certora/diff/utils_math_SignedMath.sol.patch  |  4 +-
 .../utils_structs_DoubleEndedQueue.sol.patch  |  4 +-
 certora/harnesses/InitializableHarness.sol    | 14 +++----
 certora/specs/Initializable.spec              | 38 +++++++++----------
 36 files changed, 106 insertions(+), 95 deletions(-)
 create mode 100644 certora/diff/proxy_utils_Initializable.sol.patch

diff --git a/certora/diff/access_AccessControl.sol.patch b/certora/diff/access_AccessControl.sol.patch
index 364f9720d..10491ecd1 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/access_IAccessControl.sol.patch b/certora/diff/access_IAccessControl.sol.patch
index c107a500f..4301a7cbc 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/access_Ownable.sol.patch b/certora/diff/access_Ownable.sol.patch
index ad45e1cad..861328c5f 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 12:22:17
+--- 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)
diff --git a/certora/diff/access_Ownable2Step.sol.patch b/certora/diff/access_Ownable2Step.sol.patch
index 5ff6cf34c..308746217 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 12:22:17
+--- 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)
diff --git a/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch b/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch
index d5f36f324..7a2181a14 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch b/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch
index d83ed3d45..d9f2a52d3 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/interfaces_IERC3156FlashBorrower.sol.patch b/certora/diff/interfaces_IERC3156FlashBorrower.sol.patch
index 37eeda6fe..f14e80bba 100644
--- a/certora/diff/interfaces_IERC3156FlashBorrower.sol.patch
+++ b/certora/diff/interfaces_IERC3156FlashBorrower.sol.patch
@@ -1,5 +1,5 @@
---- interfaces/IERC3156FlashBorrower.sol	2023-08-09 11:45:05
-+++ interfaces/IERC3156FlashBorrower.sol	2023-08-11 13:36:59
+--- 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)
diff --git a/certora/diff/interfaces_IERC3156FlashLender.sol.patch b/certora/diff/interfaces_IERC3156FlashLender.sol.patch
index d76972044..7172191de 100644
--- a/certora/diff/interfaces_IERC3156FlashLender.sol.patch
+++ b/certora/diff/interfaces_IERC3156FlashLender.sol.patch
@@ -1,5 +1,5 @@
---- interfaces/IERC3156FlashLender.sol	2023-08-09 11:45:05
-+++ interfaces/IERC3156FlashLender.sol	2023-08-11 13:37:04
+--- 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)
diff --git a/certora/diff/interfaces_IERC5267.sol.patch b/certora/diff/interfaces_IERC5267.sol.patch
index 95fc8e1aa..11fa591f0 100644
--- a/certora/diff/interfaces_IERC5267.sol.patch
+++ b/certora/diff/interfaces_IERC5267.sol.patch
@@ -1,5 +1,5 @@
---- interfaces/IERC5267.sol	2023-08-09 11:45:05
-+++ interfaces/IERC5267.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/interfaces_IERC5313.sol.patch b/certora/diff/interfaces_IERC5313.sol.patch
index 46a20d738..ec9dbde85 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/interfaces_draft-IERC6093.sol.patch b/certora/diff/interfaces_draft-IERC6093.sol.patch
index a386ac7d5..82d6209cc 100644
--- a/certora/diff/interfaces_draft-IERC6093.sol.patch
+++ b/certora/diff/interfaces_draft-IERC6093.sol.patch
@@ -1,5 +1,5 @@
---- interfaces/draft-IERC6093.sol	2023-08-09 11:45:05
-+++ interfaces/draft-IERC6093.sol	2023-08-11 12:22:17
+--- 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;
diff --git a/certora/diff/proxy_utils_Initializable.sol.patch b/certora/diff/proxy_utils_Initializable.sol.patch
new file mode 100644
index 000000000..1e46a45af
--- /dev/null
+++ b/certora/diff/proxy_utils_Initializable.sol.patch
@@ -0,0 +1,11 @@
+--- 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
diff --git a/certora/diff/security_Pausable.sol.patch b/certora/diff/security_Pausable.sol.patch
index 201a2d09b..acfed2aa8 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/token_ERC20_ERC20.sol.patch b/certora/diff/token_ERC20_ERC20.sol.patch
index 1c1c39aa4..9bf1d49cb 100644
--- a/certora/diff/token_ERC20_ERC20.sol.patch
+++ b/certora/diff/token_ERC20_ERC20.sol.patch
@@ -1,5 +1,5 @@
---- token/ERC20/ERC20.sol	2023-08-09 11:45:05
-+++ token/ERC20/ERC20.sol	2023-08-11 13:37:08
+--- 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)
diff --git a/certora/diff/token_ERC20_IERC20.sol.patch b/certora/diff/token_ERC20_IERC20.sol.patch
index 176b31f0b..550527217 100644
--- a/certora/diff/token_ERC20_IERC20.sol.patch
+++ b/certora/diff/token_ERC20_IERC20.sol.patch
@@ -1,5 +1,5 @@
---- token/ERC20/IERC20.sol	2023-08-09 11:45:05
-+++ token/ERC20/IERC20.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch b/certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch
index 1e3e887c7..ea7aca007 100644
--- a/certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch
+++ b/certora/diff/token_ERC20_extensions_ERC20FlashMint.sol.patch
@@ -1,5 +1,5 @@
---- token/ERC20/extensions/ERC20FlashMint.sol	2023-08-09 11:45:05
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2023-08-11 13:36:55
+--- 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)
diff --git a/certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch b/certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch
index 823536d32..84b41daac 100644
--- a/certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch
+++ b/certora/diff/token_ERC20_extensions_ERC20Permit.sol.patch
@@ -1,5 +1,5 @@
---- token/ERC20/extensions/ERC20Permit.sol	2023-08-09 11:45:05
-+++ token/ERC20/extensions/ERC20Permit.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch b/certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch
index 9dd2cebf9..fb706f260 100644
--- a/certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch
+++ b/certora/diff/token_ERC20_extensions_IERC20Metadata.sol.patch
@@ -1,5 +1,5 @@
---- token/ERC20/extensions/IERC20Metadata.sol	2023-08-09 11:45:05
-+++ token/ERC20/extensions/IERC20Metadata.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch b/certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch
index d5dadfb65..96e83cf87 100644
--- a/certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch
+++ b/certora/diff/token_ERC20_extensions_IERC20Permit.sol.patch
@@ -1,5 +1,5 @@
---- token/ERC20/extensions/IERC20Permit.sol	2023-08-11 12:19:57
-+++ token/ERC20/extensions/IERC20Permit.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch
index f324da6c3..399499eff 100644
--- a/certora/diff/token_ERC721_ERC721.sol.patch
+++ b/certora/diff/token_ERC721_ERC721.sol.patch
@@ -1,7 +1,7 @@
---- token/ERC721/ERC721.sol	2023-08-10 16:45:36
-+++ token/ERC721/ERC721.sol	2023-08-11 12:22:17
-@@ -208,6 +208,11 @@
-         return _owners[tokenId];
+--- token/ERC721/ERC721.sol	2023-08-11 20:33:54
++++ token/ERC721/ERC721.sol	2023-08-13 09:56:16
+@@ -214,6 +214,11 @@
+         }
      }
  
 +    // FV
@@ -10,5 +10,5 @@
 +    }
 +
      /**
-      * @dev Returns whether `tokenId` exists.
+      * @dev Unsafe write access to the balances, used by extensions that "mint" tokens using an {ownerOf} override.
       *
diff --git a/certora/diff/utils_Context.sol.patch b/certora/diff/utils_Context.sol.patch
index 439e7f79c..faa0fbca3 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/utils_Nonces.sol.patch b/certora/diff/utils_Nonces.sol.patch
index e1d425f83..623ebf5fb 100644
--- a/certora/diff/utils_Nonces.sol.patch
+++ b/certora/diff/utils_Nonces.sol.patch
@@ -1,5 +1,5 @@
---- utils/Nonces.sol	2023-08-09 11:45:05
-+++ utils/Nonces.sol	2023-08-11 12:22:17
+--- 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;
diff --git a/certora/diff/utils_ShortStrings.sol.patch b/certora/diff/utils_ShortStrings.sol.patch
index b136afb53..bda9de096 100644
--- a/certora/diff/utils_ShortStrings.sol.patch
+++ b/certora/diff/utils_ShortStrings.sol.patch
@@ -1,5 +1,5 @@
---- utils/ShortStrings.sol	2023-08-09 11:45:05
-+++ utils/ShortStrings.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/utils_StorageSlot.sol.patch b/certora/diff/utils_StorageSlot.sol.patch
index 82e23b6d3..b4b114604 100644
--- a/certora/diff/utils_StorageSlot.sol.patch
+++ b/certora/diff/utils_StorageSlot.sol.patch
@@ -1,5 +1,5 @@
---- utils/StorageSlot.sol	2023-08-09 11:45:05
-+++ utils/StorageSlot.sol	2023-08-11 12:22:17
+--- 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.
diff --git a/certora/diff/utils_Strings.sol.patch b/certora/diff/utils_Strings.sol.patch
index da3d37b48..6d9b47d21 100644
--- a/certora/diff/utils_Strings.sol.patch
+++ b/certora/diff/utils_Strings.sol.patch
@@ -1,5 +1,5 @@
---- utils/Strings.sol	2023-08-09 11:45:05
-+++ utils/Strings.sol	2023-08-11 12:22:44
+--- 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)
diff --git a/certora/diff/utils_cryptography_ECDSA.sol.patch b/certora/diff/utils_cryptography_ECDSA.sol.patch
index ba22b8b56..1e773a820 100644
--- a/certora/diff/utils_cryptography_ECDSA.sol.patch
+++ b/certora/diff/utils_cryptography_ECDSA.sol.patch
@@ -1,5 +1,5 @@
---- utils/cryptography/ECDSA.sol	2023-08-09 11:45:05
-+++ utils/cryptography/ECDSA.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/utils_cryptography_EIP712.sol.patch b/certora/diff/utils_cryptography_EIP712.sol.patch
index ea92c8e6a..569f8f68a 100644
--- a/certora/diff/utils_cryptography_EIP712.sol.patch
+++ b/certora/diff/utils_cryptography_EIP712.sol.patch
@@ -1,5 +1,5 @@
---- utils/cryptography/EIP712.sol	2023-08-09 11:45:05
-+++ utils/cryptography/EIP712.sol	2023-08-11 12:22:17
+--- 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)
diff --git a/certora/diff/utils_cryptography_MessageHashUtils.sol.patch b/certora/diff/utils_cryptography_MessageHashUtils.sol.patch
index 21db04759..ff51c1f57 100644
--- a/certora/diff/utils_cryptography_MessageHashUtils.sol.patch
+++ b/certora/diff/utils_cryptography_MessageHashUtils.sol.patch
@@ -1,5 +1,5 @@
---- utils/cryptography/MessageHashUtils.sol	2023-08-09 11:45:05
-+++ utils/cryptography/MessageHashUtils.sol	2023-08-11 12:22:17
+--- 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
  
diff --git a/certora/diff/utils_introspection_ERC165.sol.patch b/certora/diff/utils_introspection_ERC165.sol.patch
index ad5462127..506fe1061 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/utils_introspection_IERC165.sol.patch b/certora/diff/utils_introspection_IERC165.sol.patch
index 3c3c756ed..787b6bdea 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/utils_math_Math.sol.patch b/certora/diff/utils_math_Math.sol.patch
index 2dcf53c57..430a88e33 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-11 12:22:17
+--- 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)
diff --git a/certora/diff/utils_math_SafeCast.sol.patch b/certora/diff/utils_math_SafeCast.sol.patch
index d7a9d0a77..14e7a39ea 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-11 12:22:17
+--- 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.
diff --git a/certora/diff/utils_math_SignedMath.sol.patch b/certora/diff/utils_math_SignedMath.sol.patch
index a777bbd8b..0d8c6a51e 100644
--- a/certora/diff/utils_math_SignedMath.sol.patch
+++ b/certora/diff/utils_math_SignedMath.sol.patch
@@ -1,5 +1,5 @@
---- utils/math/SignedMath.sol	2023-08-09 11:45:05
-+++ utils/math/SignedMath.sol	2023-08-11 12:22:51
+--- 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)
diff --git a/certora/diff/utils_structs_DoubleEndedQueue.sol.patch b/certora/diff/utils_structs_DoubleEndedQueue.sol.patch
index 98fe810b5..24e04f9b7 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-11 12:22:17
+--- 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)
diff --git a/certora/harnesses/InitializableHarness.sol b/certora/harnesses/InitializableHarness.sol
index 0d0c0a4e4..e9f4aada8 100644
--- a/certora/harnesses/InitializableHarness.sol
+++ b/certora/harnesses/InitializableHarness.sol
@@ -1,19 +1,19 @@
 // SPDX-License-Identifier: MIT
-pragma solidity ^0.8.20;
+pragma solidity ^0.8.19;
 
-import "../patched/proxy/utils/Initializable.sol";
+import {Initializable} from "../patched/proxy/utils/Initializable.sol";
 
 contract InitializableHarness is Initializable {
     function initialize()          public initializer      {}
-    function reinitialize(uint8 n) public reinitializer(n) {}
+    function reinitialize(uint64 n) public reinitializer(n) {}
     function disable()             public { _disableInitializers(); }
 
     function nested_init_init()                     public initializer      { initialize();    }
-    function nested_init_reinit(uint8 m)            public initializer      { reinitialize(m); }
-    function nested_reinit_init(uint8 n)            public reinitializer(n) { initialize();    }
-    function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); }
+    function nested_init_reinit(uint64 m)            public initializer      { reinitialize(m); }
+    function nested_reinit_init(uint64 n)            public reinitializer(n) { initialize();    }
+    function nested_reinit_reinit(uint64 n, uint64 m) public reinitializer(n) { reinitialize(m); }
 
-    function version() public view returns (uint8) {
+    function version() public view returns (uint64) {
         return _getInitializedVersion();
     }
 
diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec
index 0e0b1b714..fe99a016d 100644
--- a/certora/specs/Initializable.spec
+++ b/certora/specs/Initializable.spec
@@ -1,19 +1,19 @@
-import "helpers/helpers.spec"
+import "helpers/helpers.spec";
 
 methods {
     // initialize, reinitialize, disable
-    initialize()        envfree
-    reinitialize(uint8) envfree
-    disable()           envfree
+    function initialize()        external envfree;
+    function reinitialize(uint64) external envfree;
+    function disable()           external envfree;
 
-    nested_init_init()            envfree
-    nested_init_reinit(uint8)       envfree
-    nested_reinit_init(uint8)       envfree
-    nested_reinit_reinit(uint8,uint8) envfree
+    function nested_init_init()            external envfree;
+    function nested_init_reinit(uint64)       external envfree;
+    function nested_reinit_init(uint64)       external envfree;
+    function nested_reinit_reinit(uint64,uint64) external envfree;
 
     // view
-    version()      returns uint8 envfree
-    initializing() returns bool  envfree
+    function version()      external returns uint64 envfree;
+    function initializing() external returns bool  envfree;
 }
 
 /*
@@ -23,7 +23,7 @@ methods {
 */
 definition isUninitialized() returns bool = version() == 0;
 definition isInitialized()   returns bool = version() > 0;
-definition isDisabled()      returns bool = version() == 255;
+definition isDisabled()      returns bool = version() == max_uint64;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -31,7 +31,7 @@ definition isDisabled()      returns bool = version() == 255;
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant notInitializing()
-    !initializing()
+    !initializing();
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -39,7 +39,7 @@ invariant notInitializing()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule increasingVersion(env e) {
-    uint8 versionBefore = version();
+    uint64 versionBefore = version();
     bool disabledBefore = isDisabled();
 
     method f; calldataarg args;
@@ -83,7 +83,7 @@ rule cannotInitializeOnceDisabled() {
 rule cannotReinitializeOnceDisabled() {
     require isDisabled();
 
-    uint8 n;
+    uint64 n;
     reinitialize@withrevert(n);
 
     assert lastReverted, "contract is disabled";
@@ -99,17 +99,17 @@ rule cannotNestInitializers_init_init() {
     assert lastReverted, "nested initializers";
 }
 
-rule cannotNestInitializers_init_reinit(uint8 m) {
+rule cannotNestInitializers_init_reinit(uint64 m) {
     nested_init_reinit@withrevert(m);
     assert lastReverted, "nested initializers";
 }
 
-rule cannotNestInitializers_reinit_init(uint8 n) {
+rule cannotNestInitializers_reinit_init(uint64 n) {
     nested_reinit_init@withrevert(n);
     assert lastReverted, "nested initializers";
 }
 
-rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) {
+rule cannotNestInitializers_reinit_reinit(uint64 n, uint64 m) {
     nested_reinit_reinit@withrevert(n, m);
     assert lastReverted, "nested initializers";
 }
@@ -139,9 +139,9 @@ rule initializeEffects() {
 rule reinitializeEffects() {
     requireInvariant notInitializing();
 
-    uint8 versionBefore = version();
+    uint64 versionBefore = version();
 
-    uint8 n;
+    uint64 n;
     reinitialize@withrevert(n);
     bool success = !lastReverted;