Update README.md

Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>
Co-authored-by: Francisco Giordano <fg@frang.io>

.changeset/afraid-walls-smell.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC1155Receiver`: Removed in favor of `ERC1155Holder`.

.changeset/angry-ties-switch.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`TimelockController`: Changed the role architecture to use `DEFAULT_ADMIN_ROLE` as the admin for all roles, instead of the bespoke `TIMELOCK_ADMIN_ROLE` that was used previously. This aligns with the general recommendation for `AccessControl` and makes the addition of new roles easier. Accordingly, the `admin` parameter and timelock will now be granted `DEFAULT_ADMIN_ROLE` instead of `TIMELOCK_ADMIN_ROLE`. ([#3799](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3799))

.changeset/big-plums-cover.md

@@ -0,0 +1,4 @@
+---
+'openzeppelin-solidity': major
+---
+Use `abi.encodeCall` in place of `abi.encodeWithSelector` and `abi.encodeWithSignature` for improved type-checking of parameters

.changeset/blue-horses-do.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC2771Forwarder`: Added `deadline` for expiring transactions, batching, and more secure handling of `msg.value`.

.changeset/blue-scissors-design.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`Math`: Make `ceilDiv` to revert on 0 division even if the numerator is 0

.changeset/brave-lobsters-punch.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Governor`: Refactored internals to implement common queuing logic in the core module of the Governor. Added `queue` and `_queueOperations` functions that act at different levels. Modules that implement queuing via timelocks are expected to override `_queueOperations` to implement the timelock-specific logic. Added `_executeOperations` as the equivalent for execution.

.changeset/bright-tomatoes-sing.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC20`, `ERC721`, `ERC1155`: Deleted `_beforeTokenTransfer` and `_afterTokenTransfer` hooks, added a new internal `_update` function for customizations, and refactored all extensions using those hooks to use `_update` instead. ([#3838](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3838), [#3876](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3876), [#4377](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4377))

.changeset/chilled-spiders-attack.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC1155Supply`: add a `totalSupply()` function that returns the total amount of token circulating, this change will restrict the total tokens minted across all ids to 2\*\*256-1 .

.changeset/clever-bats-kick.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`Ownable`: Prevent using address(0) as the initial owner.

.changeset/clever-pumas-beg.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Ownable`: Add an `initialOwner` parameter to the constructor, making the ownership initialization explicit.

.changeset/dull-ghosts-sip.md

@@ -0,0 +1,6 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`AccessManager`, `AccessManaged`, `GovernorTimelockAccess`: Ensure that calldata shorter than 4 bytes is not padded to 4 bytes.
+pr: #4624

.changeset/eight-peaches-guess.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`Proxy`: Removed redundant `receive` function.

.changeset/eighty-crabs-listen.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+Optimize `Strings.equal`

.changeset/eighty-lemons-shake.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC721`: `_approve` no longer allows approving the owner of the tokenId. `_setApprovalForAll` no longer allows setting address(0) as an operator.

.changeset/empty-cheetahs-hunt.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC721URIStorage`: Allow setting the token URI prior to minting.

.changeset/empty-taxis-kiss.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`UUPSUpgradeable`, `TransparentUpgradeableProxy` and `ProxyAdmin`: Removed `upgradeTo` and `upgrade` functions, and made `upgradeToAndCall` and `upgradeAndCall` ignore the data argument if it is empty. It is no longer possible to invoke the receive function (or send value with empty data) along with an upgrade.

.changeset/fair-humans-peel.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC721URIStorage`, `ERC721Royalty`: Stop resetting token-specific URI and royalties when burning.

.changeset/fifty-owls-retire.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Address`: Removed the ability to customize error messages. A common custom error is always used if the underlying revert reason cannot be bubbled up.

.changeset/flat-bottles-wonder.md

@@ -0,0 +1,7 @@
+---
+'openzeppelin-solidity': minor
+---
+
+Replace some uses of `abi.encodePacked` with clearer alternatives (e.g. `bytes.concat`, `string.concat`). (#4504)[https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4504]
+
+pr: #4296

.changeset/fluffy-countries-buy.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`Arrays`: Optimize `findUpperBound` by removing redundant SLOAD.

.changeset/four-adults-knock.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ECDSA`: Use unchecked arithmetic for the `tryRecover` function that receives the `r` and `vs` short-signature fields separately.

.changeset/fresh-birds-kiss.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Checkpoints`: library moved from `utils` to `utils/structs`

.changeset/green-pumpkins-end.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`SafeERC20`: Removed `safePermit` in favor of documentation-only `permit` recommendations.

.changeset/grumpy-bulldogs-call.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Governor`: Optimized use of storage for proposal data

.changeset/grumpy-poets-rush.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+Upgradeable Contracts: No longer transpile interfaces, libraries, and stateless contracts.

.changeset/grumpy-worms-tease.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC1967Utils`: Refactor the `ERC1967Upgrade` abstract contract as a library.

.changeset/happy-falcons-walk.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`TransparentUpgradeableProxy`: Admin is now stored in an immutable variable (set during construction) to avoid unnecessary storage reads on every proxy call. This removed the ability to ever change the admin. Transfer of the upgrade capability is exclusively handled through the ownership of the `ProxyAdmin`.

.changeset/healthy-gorillas-applaud.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`VestingWallet`: Use `Ownable` instead of an immutable `beneficiary`.

.changeset/heavy-drinks-fail.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC20`: Remove `Approval` event previously emitted in `transferFrom` to indicate that part of the allowance was consumed. With this change, allowances are no longer reconstructible from events. See the code for guidelines on how to re-enable this event if needed.

.changeset/hip-beds-provide.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+Move the logic to validate ERC-1822 during an upgrade from `ERC1967Utils` to `UUPSUpgradeable`.

.changeset/hip-goats-fail.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`VestingWallet`: Fix revert during 1 second time window when duration is 0.

.changeset/hot-coins-judge.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`Arrays`: Add `unsafeMemoryAccess` helpers to read from a memory array without checking the length.

.changeset/hot-dingos-kiss.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`MessageHashUtils`: Add a new library for creating message digest to be used along with signing or recovery such as  ECDSA or ERC-1271. These functions are moved from the `ECDSA` library.

.changeset/hot-plums-approve.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`GovernorTimelockControl`: Clean up timelock id on execution for gas refund.

.changeset/large-humans-remain.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`MerkleProof`: Use custom error to report invalid multiproof instead of reverting with overflow panic.

.changeset/lazy-rice-joke.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`Initializable`: Use intermediate variables to improve readability.

.changeset/little-falcons-build.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`EIP712`: Add internal getters for the name and version strings

.changeset/loud-shrimps-play.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`TimelockController`: Add a state getter that returns an `OperationState` enum.

.changeset/lovely-geckos-hide.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+Replace revert strings and require statements with custom errors.

.changeset/mean-walls-watch.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Nonces`: Added a new contract to keep track of user nonces. Used for signatures in `ERC20Permit`, `ERC20Votes`, and `ERC721Votes`. ([#3816](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3816))

.changeset/mighty-donuts-smile.md

@@ -0,0 +1,6 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`Governor`: Add validation in ERC1155 and ERC721 receiver hooks to ensure Governor is the executor.
+

.changeset/orange-apes-draw.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+Switched to using explicit Solidity import statements. Some previously available symbols may now have to be separately imported.

.changeset/pink-suns-mix.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`Math`: Optimized stack operations in `mulDiv`.

.changeset/popular-deers-raise.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Governor`: Add support for casting votes with ERC-1271 signatures by using a `bytes memory signature` instead of `r`, `s` and `v` arguments in the `castVoteBySig` and `castVoteWithReasonAndParamsBySig` functions.

.changeset/proud-seals-complain.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`BeaconProxy`: Use an immutable variable to store the address of the beacon. It is no longer possible for a `BeaconProxy` to upgrade by changing to another beacon.

.changeset/proud-spiders-attend.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC721`: Renamed `_requireMinted` to `_requireOwned` and added a return value with the current owner. Implemented `ownerOf` in terms of `_requireOwned`.

.changeset/purple-cats-cheer.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`GovernorTimelockControl`: Add the Governor instance address as part of the TimelockController operation `salt` to avoid operation id collisions between governors using the same TimelockController.

.changeset/purple-squids-attend.md

@@ -0,0 +1,6 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`AccessManager`: Use named return parameters in functions that return multiple values.
+pr: #4624

.changeset/quiet-trainers-kick.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`AccessManager`: Added a new contract for managing access control of complex systems in a consolidated location.

.changeset/red-dots-fold.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+Overrides are now used internally for a number of functions that were previously hardcoded to their default implementation in certain locations: `ERC1155Supply.totalSupply`, `ERC721.ownerOf`, `ERC721.balanceOf` and `ERC721.totalSupply` in `ERC721Enumerable`, `ERC20.totalSupply` in `ERC20FlashMint`, and `ERC1967._getImplementation` in `ERC1967Proxy`.

.changeset/rotten-insects-wash.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ProxyAdmin`: Removed `getProxyAdmin` and `getProxyImplementation` getters. ([#3820](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3820))

.changeset/serious-books-lie.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ERC1155`: Optimize array allocation.

.changeset/short-eels-enjoy.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+Bump minimum compiler version required to 0.8.20

.changeset/silly-bees-beam.md

@@ -0,0 +1,7 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC20Votes`: Changed internal vote accounting to reusable `Votes` module previously used by `ERC721Votes`. Removed implicit `ERC20Permit` inheritance. Note that the `DOMAIN_SEPARATOR` getter was previously guaranteed to be available for `ERC20Votes` contracts, but is no longer available unless `ERC20Permit` is explicitly used; ERC-5267 support is included in `ERC20Votes` with `EIP712` and is recommended as an alternative.
+
+pr: #3816

.changeset/six-frogs-turn.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC20`: Remove the non-standard `increaseAllowance` and `decreaseAllowance` functions.

.changeset/sixty-numbers-reply.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Governor`: Add `voter` and `nonce` parameters in signed ballots, to avoid forging signatures for random addresses, prevent signature replay, and allow invalidating signatures. Add `voter` as a new parameter in the `castVoteBySig` and `castVoteWithReasonAndParamsBySig` functions.

.changeset/slimy-penguins-attack.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`TransparentUpgradeableProxy`: Removed `admin` and `implementation` getters, which were only callable by the proxy owner and thus not very useful. ([#3820](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3820))

.changeset/smooth-books-wink.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ERC1155`: Remove check for address zero in `balanceOf`.

.changeset/smooth-cougars-jump.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`ReentrancyGuard`, `Pausable`: Moved to `utils` directory.

.changeset/spicy-sheep-eat.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`access`: Move `AccessControl` extensions to a dedicated directory.

.changeset/spotty-hotels-type.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ERC721Consecutive`: Add a `_firstConsecutiveId` internal function that can be overridden to change the id of the first token minted through `_mintConsecutive`.

.changeset/strong-poems-thank.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`DoubleEndedQueue`: refactor internal structure to use `uint128` instead of `int128`. This has no effect on the library interface.

.changeset/swift-bags-divide.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`Governor`: Add a mechanism to restrict the address of the proposer using a suffix in the description.

.changeset/swift-numbers-cry.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`Governor`, `Initializable`, and `UUPSUpgradeable`: Use internal functions in modifiers to optimize bytecode size.

.changeset/tasty-tomatoes-turn.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Strings`: Rename `toString(int256)` to `toStringSigned(int256)`.

.changeset/tender-shirts-turn.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`BeaconProxy`: Reject value in initialization unless a payable function is explicitly invoked.

.changeset/thick-pumpkins-exercise.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Initializable`: Use the namespaced storage pattern to avoid putting critical variables in slot 0. Allow reinitializer versions greater than 256.

.changeset/thin-camels-matter.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`ERC1155`: Bubble errors triggered in the `onERC1155Received` and `onERC1155BatchReceived` hooks.

.changeset/thirty-drinks-happen.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`AccessManager`: Make `schedule` and `execute` more conservative when delay is 0.

.changeset/tough-drinks-hammer.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ERC1155`: Optimize array accesses by skipping bounds checking when unnecessary.

.changeset/two-wasps-punch.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`AccessControl`: Add a boolean return value to the internal `_grantRole` and `_revokeRole` functions indicating whether the role was granted or revoked.

.changeset/unlucky-beans-obey.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ERC2771Context`: Return the forwarder address whenever the `msg.data` of a call originating from a trusted forwarder is not long enough to contain the request signer address (i.e. `msg.data.length` is less than 20 bytes), as specified by ERC-2771.

.changeset/violet-dancers-cough.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+Remove the `override` specifier from functions that only override a single interface function.

.changeset/violet-melons-press.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`GovernorTimelockAccess`: Added a module to connect a governor with an instance of `AccessManager`, allowing the governor to make calls that are delay-restricted by the manager using the normal `queue` workflow.

.changeset/warm-guests-rule.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ERC2771Context`: Prevent revert in `_msgData()` when a call originating from a trusted forwarder is not long enough to contain the request signer address (i.e. `msg.data.length` is less than 20 bytes). Return the full calldata in that case.

.changeset/wet-bears-heal.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+Upgradeable contracts now use namespaced storage (EIP-7201).

.changeset/wild-beds-visit.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`GovernorStorage`: Added a new governor extension that stores the proposal details in storage, with an interface that operates on `proposalId`, as well as proposal enumerability. This replaces the old `GovernorCompatibilityBravo` module.

.changeset/wild-peas-remain.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Votes`: Use Trace208 for checkpoints. This enables EIP-6372 clock support for keys but reduces the max supported voting power to uint208.

.changeset/wild-rockets-rush.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`Math`: Renamed members of `Rounding` enum, and added a new rounding mode for "away from zero".

.changeset/wild-windows-trade.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`SafeERC20`: Refactor `safeDecreaseAllowance` and `safeIncreaseAllowance` to support USDT-like tokens.

CHANGELOG.md

@@ -1,35 +1,12 @@
 # Changelog
 
+## Unreleased
 
-## 5.0.2 (2024-02-29)
+> **Warning** Version 5.0 is under active development and should not be used. Install the releases from npm or use the version tags in the repository.
 
-- `Base64`: Fix issue where dirty memory located just after the input buffer is affecting the result. ([#4926](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4926))
+### Removals
 
-## 5.0.1 (2023-12-07)
-
-- `ERC2771Context` and `Context`: Introduce a `_contextPrefixLength()` getter, used to trim extra information appended to `msg.data`.
-- `Multicall`: Make aware of non-canonical context (i.e. `msg.sender` is not `_msgSender()`), allowing compatibility with `ERC2771Context`.
-
-## 5.0.0 (2023-10-05)
-
-### Additions Summary
-
-The following contracts and libraries were added:
-
-- `AccessManager`: A consolidated system for managing access control in complex systems.
-  - `AccessManaged`: A module for connecting a contract to an authority in charge of its access control.
-  - `GovernorTimelockAccess`: An adapter for time-locking governance proposals using an `AccessManager`.
-  - `AuthorityUtils`: A library of utilities for interacting with authority contracts.
-- `GovernorStorage`: A Governor module that stores proposal details in storage.
-- `ERC2771Forwarder`: An ERC2771 forwarder for meta transactions.
-- `ERC1967Utils`: A library with ERC1967 events, errors and getters.
-- `Nonces`: An abstraction for managing account nonces.
-- `MessageHashUtils`: A library for producing digests for ECDSA operations.
-- `Time`: A library with helpers for manipulating time-related objects.
-
-### Removals Summary
-
-The following contracts, libraries, and functions were removed:
+The following contracts, libraries and functions were removed:
 
 - `Address.isContract` (because of its ambiguous nature and potential for misuse)
 - `Checkpoints.History`
@@ -53,236 +30,51 @@ The following contracts, libraries, and functions were removed:
 
 These removals were implemented in the following PRs: [#3637](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3637), [#3880](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3880), [#3945](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3945), [#4258](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4258), [#4276](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4276), [#4289](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4289)
 
-### Changes by category
-
-#### General
-
-- Replaced revert strings and require statements with custom errors. ([#4261](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4261))
-- Bumped minimum compiler version required to 0.8.20 ([#4288](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4288))
-- Use of `abi.encodeCall` in place of `abi.encodeWithSelector` and `abi.encodeWithSignature` for improved type-checking of parameters ([#4293](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4293))
-- Replaced some uses of `abi.encodePacked` with clearer alternatives (e.g. `bytes.concat`, `string.concat`). ([#4504](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4504)) ([#4296](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4296))
-- Overrides are now used internally for a number of functions that were previously hardcoded to their default implementation in certain locations: `ERC1155Supply.totalSupply`, `ERC721.ownerOf`, `ERC721.balanceOf` and `ERC721.totalSupply` in `ERC721Enumerable`, `ERC20.totalSupply` in `ERC20FlashMint`, and `ERC1967._getImplementation` in `ERC1967Proxy`. ([#4299](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4299))
-- Removed the `override` specifier from functions that only override a single interface function. ([#4315](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4315))
-- Switched to using explicit Solidity import statements. Some previously available symbols may now have to be separately imported. ([#4399](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4399))
-- `Governor`, `Initializable`, and `UUPSUpgradeable`: Use internal functions in modifiers to optimize bytecode size. ([#4472](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4472))
-- Upgradeable contracts now use namespaced storage (EIP-7201). ([#4534](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4534))
-- Upgradeable contracts no longer transpile interfaces and libraries. ([#4628](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4628))
-
-#### Access
-
-- `Ownable`: Added an `initialOwner` parameter to the constructor, making the ownership initialization explicit. ([#4267](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4267))
-- `Ownable`: Prevent using address(0) as the initial owner. ([#4531](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4531))
-- `AccessControl`: Added a boolean return value to the internal `_grantRole` and `_revokeRole` functions indicating whether the role was granted or revoked. ([#4241](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4241))
-- `access`: Moved `AccessControl` extensions to a dedicated directory. ([#4359](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4359))
-- `AccessManager`: Added a new contract for managing access control of complex systems in a consolidated location. ([#4121](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4121))
-- `AccessManager`, `AccessManaged`, `GovernorTimelockAccess`: Ensure that calldata shorter than 4 bytes is not padded to 4 bytes. ([#4624](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4624))
-- `AccessManager`: Use named return parameters in functions that return multiple values. ([#4624](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4624))
-- `AccessManager`: Make `schedule` and `execute` more conservative when delay is 0. ([#4644](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4644))
-
-#### Finance
-
-- `VestingWallet`: Fixed revert during 1 second time window when duration is 0. ([#4502](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4502))
-- `VestingWallet`: Use `Ownable` instead of an immutable `beneficiary`. ([#4508](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4508))
-
-#### Governance
-
-- `Governor`: Optimized use of storage for proposal data ([#4268](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4268))
-- `Governor`: Added validation in ERC1155 and ERC721 receiver hooks to ensure Governor is the executor. ([#4314](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4314))
-- `Governor`: Refactored internals to implement common queuing logic in the core module of the Governor. Added `queue` and `_queueOperations` functions that act at different levels. Modules that implement queuing via timelocks are expected to override `_queueOperations` to implement the timelock-specific logic. Added `_executeOperations` as the equivalent for execution. ([#4360](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4360))
-- `Governor`: Added `voter` and `nonce` parameters in signed ballots, to avoid forging signatures for random addresses, prevent signature replay, and allow invalidating signatures. Add `voter` as a new parameter in the `castVoteBySig` and `castVoteWithReasonAndParamsBySig` functions. ([#4378](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4378))
-- `Governor`: Added support for casting votes with ERC-1271 signatures by using a `bytes memory signature` instead of `r`, `s` and `v` arguments in the `castVoteBySig` and `castVoteWithReasonAndParamsBySig` functions. ([#4418](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4418))
-- `Governor`: Added a mechanism to restrict the address of the proposer using a suffix in the description.
-- `GovernorStorage`: Added a new governor extension that stores the proposal details in storage, with an interface that operates on `proposalId`, as well as proposal enumerability. This replaces the old `GovernorCompatibilityBravo` module. ([#4360](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4360))
-- `GovernorTimelockAccess`: Added a module to connect a governor with an instance of `AccessManager`, allowing the governor to make calls that are delay-restricted by the manager using the normal `queue` workflow. ([#4523](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4523))
-- `GovernorTimelockControl`: Clean up timelock id on execution for gas refund. ([#4118](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4118))
-- `GovernorTimelockControl`: Added the Governor instance address as part of the TimelockController operation `salt` to avoid operation id collisions between governors using the same TimelockController. ([#4432](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4432))
-- `TimelockController`: Changed the role architecture to use `DEFAULT_ADMIN_ROLE` as the admin for all roles, instead of the bespoke `TIMELOCK_ADMIN_ROLE` that was used previously. This aligns with the general recommendation for `AccessControl` and makes the addition of new roles easier. Accordingly, the `admin` parameter and timelock will now be granted `DEFAULT_ADMIN_ROLE` instead of `TIMELOCK_ADMIN_ROLE`. ([#3799](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3799))
-- `TimelockController`: Added a state getter that returns an `OperationState` enum. ([#4358](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4358))
-- `Votes`: Use Trace208 for checkpoints. This enables EIP-6372 clock support for keys but reduces the max supported voting power to uint208. ([#4539](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4539))
-
-#### Metatx
-
-- `ERC2771Forwarder`: Added `deadline` for expiring transactions, batching, and more secure handling of `msg.value`. ([#4346](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4346))
-- `ERC2771Context`: Return the forwarder address whenever the `msg.data` of a call originating from a trusted forwarder is not long enough to contain the request signer address (i.e. `msg.data.length` is less than 20 bytes), as specified by ERC-2771. ([#4481](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4481))
-- `ERC2771Context`: Prevent revert in `_msgData()` when a call originating from a trusted forwarder is not long enough to contain the request signer address (i.e. `msg.data.length` is less than 20 bytes). Return the full calldata in that case. ([#4484](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4484))
-
-#### Proxy
-
-- `ProxyAdmin`: Removed `getProxyAdmin` and `getProxyImplementation` getters. ([#3820](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3820))
-- `TransparentUpgradeableProxy`: Removed `admin` and `implementation` getters, which were only callable by the proxy owner and thus not very useful. ([#3820](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3820))
-- `ERC1967Utils`: Refactored the `ERC1967Upgrade` abstract contract as a library. ([#4325](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4325))
-- `TransparentUpgradeableProxy`: Admin is now stored in an immutable variable (set during construction) to avoid unnecessary storage reads on every proxy call. This removed the ability to ever change the admin. Transfer of the upgrade capability is exclusively handled through the ownership of the `ProxyAdmin`. ([#4354](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4354))
-- Moved the logic to validate ERC-1822 during an upgrade from `ERC1967Utils` to `UUPSUpgradeable`. ([#4356](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4356))
-- `UUPSUpgradeable`, `TransparentUpgradeableProxy` and `ProxyAdmin`: Removed `upgradeTo` and `upgrade` functions, and made `upgradeToAndCall` and `upgradeAndCall` ignore the data argument if it is empty. It is no longer possible to invoke the receive function (or send value with empty data) along with an upgrade. ([#4382](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4382))
-- `BeaconProxy`: Reject value in initialization unless a payable function is explicitly invoked. ([#4382](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4382))
-- `Proxy`: Removed redundant `receive` function. ([#4434](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4434))
-- `BeaconProxy`: Use an immutable variable to store the address of the beacon. It is no longer possible for a `BeaconProxy` to upgrade by changing to another beacon. ([#4435](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4435))
-- `Initializable`: Use the namespaced storage pattern to avoid putting critical variables in slot 0. Allow reinitializer versions greater than 256. ([#4460](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4460))
-- `Initializable`: Use intermediate variables to improve readability. ([#4576](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4576))
-
-#### Token
-
-- `ERC20`, `ERC721`, `ERC1155`: Deleted `_beforeTokenTransfer` and `_afterTokenTransfer` hooks, added a new internal `_update` function for customizations, and refactored all extensions using those hooks to use `_update` instead. ([#3838](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3838), [#3876](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3876), [#4377](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4377))
-- `ERC20`: Removed `Approval` event previously emitted in `transferFrom` to indicate that part of the allowance was consumed. With this change, allowances are no longer reconstructible from events. See the code for guidelines on how to re-enable this event if needed. ([#4370](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4370))
-- `ERC20`: Removed the non-standard `increaseAllowance` and `decreaseAllowance` functions. ([#4585](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4585))
-- `ERC20Votes`: Changed internal vote accounting to reusable `Votes` module previously used by `ERC721Votes`. Removed implicit `ERC20Permit` inheritance. Note that the `DOMAIN_SEPARATOR` getter was previously guaranteed to be available for `ERC20Votes` contracts, but is no longer available unless `ERC20Permit` is explicitly used; ERC-5267 support is included in `ERC20Votes` with `EIP712` and is recommended as an alternative. ([#3816](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3816))
-- `SafeERC20`: Refactored `safeDecreaseAllowance` and `safeIncreaseAllowance` to support USDT-like tokens. ([#4260](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4260))
-- `SafeERC20`: Removed `safePermit` in favor of documentation-only `permit` recommendations. Based on recommendations from @trust1995 ([#4582](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4582))
-- `ERC721`: `_approve` no longer allows approving the owner of the tokenId. ([#4377](https://github.com/OpenZeppelin/openzeppelin-contracts/issues/4377)) `_setApprovalForAll` no longer allows setting address(0) as an operator. ([#4377](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4377))
-- `ERC721`: Renamed `_requireMinted` to `_requireOwned` and added a return value with the current owner. Implemented `ownerOf` in terms of `_requireOwned`. ([#4566](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4566))
-- `ERC721Consecutive`: Added a `_firstConsecutiveId` internal function that can be overridden to change the id of the first token minted through `_mintConsecutive`. ([#4097](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4097))
-- `ERC721URIStorage`: Allow setting the token URI prior to minting. ([#4559](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4559))
-- `ERC721URIStorage`, `ERC721Royalty`: Stop resetting token-specific URI and royalties when burning. ([#4561](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4561))
-- `ERC1155`: Optimized array allocation. ([#4196](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4196))
-- `ERC1155`: Removed check for address zero in `balanceOf`. ([#4263](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4263))
-- `ERC1155`: Optimized array accesses by skipping bounds checking when unnecessary. ([#4300](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4300))
-- `ERC1155`: Bubble errors triggered in the `onERC1155Received` and `onERC1155BatchReceived` hooks. ([#4314](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4314))
-- `ERC1155Supply`: Added a `totalSupply()` function that returns the total amount of token circulating, this change will restrict the total tokens minted across all ids to 2\*\*256-1 . ([#3962](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3962))
-- `ERC1155Receiver`: Removed in favor of `ERC1155Holder`. ([#4450](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4450))
-
-#### Utils
-
-- `Address`: Removed the ability to customize error messages. A common custom error is always used if the underlying revert reason cannot be bubbled up. ([#4502](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4502))
-- `Arrays`: Added `unsafeMemoryAccess` helpers to read from a memory array without checking the length. ([#4300](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4300))
-- `Arrays`: Optimized `findUpperBound` by removing redundant SLOAD. ([#4442](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4442))
-- `Checkpoints`: Library moved from `utils` to `utils/structs` ([#4275](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4275))
-- `DoubleEndedQueue`: Refactored internal structure to use `uint128` instead of `int128`. This has no effect on the library interface. ([#4150](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4150))
-- `ECDSA`: Use unchecked arithmetic for the `tryRecover` function that receives the `r` and `vs` short-signature fields separately. ([#4301](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4301))
-- `EIP712`: Added internal getters for the name and version strings ([#4303](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4303))
-- `Math`: Makes `ceilDiv` to revert on 0 division even if the numerator is 0 ([#4348](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4348))
-- `Math`: Optimized stack operations in `mulDiv`. ([#4494](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4494))
-- `Math`: Renamed members of `Rounding` enum, and added a new rounding mode for "away from zero". ([#4455](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4455))
-- `MerkleProof`: Use custom error to report invalid multiproof instead of reverting with overflow panic. ([#4564](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4564))
-- `MessageHashUtils`: Added a new library for creating message digest to be used along with signing or recovery such as ECDSA or ERC-1271. These functions are moved from the `ECDSA` library. ([#4430](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4430))
-- `Nonces`: Added a new contract to keep track of user nonces. Used for signatures in `ERC20Permit`, `ERC20Votes`, and `ERC721Votes`. ([#3816](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3816))
-- `ReentrancyGuard`, `Pausable`: Moved to `utils` directory. ([#4551](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4551))
-- `Strings`: Renamed `toString(int256)` to `toStringSigned(int256)`. ([#4330](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4330))
-- Optimized `Strings.equal` ([#4262](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4262))
-
-### How to migrate from 4.x
+### How to upgrade from 4.x
 
 #### ERC20, ERC721, and ERC1155
 
-These breaking changes will require modifications to ERC20, ERC721, and ERC1155 contracts, since the `_afterTokenTransfer` and `_beforeTokenTransfer` functions were removed. Thus, any customization made through those hooks should now be done overriding the new `_update` function instead.
+These breaking changes will require modifications to ERC20, ERC721, and ERC1155 contracts, since the `_afterTokenTransfer` and `_beforeTokenTransfer` functions were removed. Any customization made through those hooks should now be done overriding the new `_update` function instead.
 
 Minting and burning are implemented by `_update` and customizations should be done by overriding this function as well. `_transfer`, `_mint` and `_burn` are no longer virtual (meaning they are not overridable) to guard against possible inconsistencies.
 
 For example, a contract using `ERC20`'s `_beforeTokenTransfer` hook would have to be changed in the following way.
 
 ```diff
--function _beforeTokenTransfer(
-+function _update(
-   address from,
-   address to,
-   uint256 amount
- ) internal virtual override {
--  super._beforeTokenTransfer(from, to, amount);
-   require(!condition(), "ERC20: wrong condition");
-+  super._update(from, to, amount);
- }
+- function _beforeTokenTransfer(
++ function _update(
+      address from,
+      address to,
+      uint256 amount
+  ) internal virtual override {
+-     super._beforeTokenTransfer(from, to, amount);
+      require(!condition(), "ERC20: wrong condition");
++     super._update(from, to, amount);
+  }
 ```
 
-#### More about ERC721
+### More about ERC721
 
-In the case of `ERC721`, the `_update` function does not include a `from` parameter, as the sender is implicitly the previous owner of the `tokenId`. The address of this previous owner is returned by the `_update` function, so it can be used for a posteriori checks. In addition to `to` and `tokenId`, a third parameter (`auth`) is present in this function. This parameter enabled an optional check that the caller/spender is approved to do the transfer. This check cannot be performed after the transfer (because the transfer resets the approval), and doing it before `_update` would require a duplicate call to `_ownerOf`.
+In the case of `ERC721`, the `_update` function does not include a `from` parameter, as the sender is implicitly the previous owner of the `tokenId`. The address of
+this previous owner is returned by the `_update` function, so it can be used for a posteriori checks. In addition to `to` and `tokenId`, a third parameter (`auth`) is
+present in this function. This parameter enabled an optional check that the caller/spender is approved to do the transfer. This check cannot be performed after the transfer (because the transfer resets the approval), and doing it before `_update` would require a duplicate call to `_ownerOf`.
 
-In this logic of removing hidden SLOADs, the `_isApprovedOrOwner` function was removed in favor of a new `_isAuthorized` function. Overrides that used to target the `_isApprovedOrOwner` should now be performed on the `_isAuthorized` function. Calls to `_isApprovedOrOwner` that preceded a call to `_transfer`, `_burn` or `_approve` should be removed in favor of using the `auth` argument in `_update` and `_approve`. This is showcased in `ERC721Burnable.burn` and in `ERC721Wrapper.withdrawTo`.
+In this logic of removing hidden SLOADs, the `_isApprovedOrOwner` function was removed in favor of a new `_isAuthorized` function. Overrides that used to target the
+`_isApprovedOrOwner` should now be performed on the `_isAuthorized` function. Calls to `_isApprovedOrOwner` that preceded a call to `_transfer`, `_burn` or `_approve`
+should be removed in favor of using the `auth` argument in `_update` and `_approve`. This is showcased in `ERC721Burnable.burn` and in `ERC721Wrapper.withdrawTo`.
 
 The `_exists` function was removed. Calls to this function can be replaced by `_ownerOf(tokenId) != address(0)`.
 
-#### More about ERC1155
-
-Batch transfers will now emit `TransferSingle` if the batch consists of a single token, while in previous versions the `TransferBatch` event would be used for all transfers initiated through `safeBatchTransferFrom`. Both behaviors are compliant with the ERC-1155 specification.
-
 #### ERC165Storage
 
 Users that were registering EIP-165 interfaces with `_registerInterface` from `ERC165Storage` should instead do so so by overriding the `supportsInterface` function as seen below:
 
 ```solidity
 function supportsInterface(bytes4 interfaceId) public view virtual override returns (bool) {
-  return interfaceId == type(MyInterface).interfaceId || super.supportsInterface(interfaceId);
+    return interfaceId == type(MyInterface).interfaceId || super.supportsInterface(interfaceId);
 }
 ```
 
-#### SafeMath
-
-Methods in SafeMath superseded by native overflow checks in Solidity 0.8.0 were removed along with operations providing an interface for revert strings. The remaining methods were moved to `utils/Math.sol`.
-
-```diff
-- import "@openzeppelin/contracts/utils/math/SafeMath.sol";
-+ import "@openzeppelin/contracts/utils/math/Math.sol";
-
- function tryOperations(uint256 x, uint256 y) external view {
--  (bool overflowsAdd, uint256 resultAdd) = SafeMath.tryAdd(x, y);
-+  (bool overflowsAdd, uint256 resultAdd) = Math.tryAdd(x, y);
--  (bool overflowsSub, uint256 resultSub) = SafeMath.trySub(x, y);
-+  (bool overflowsSub, uint256 resultSub) = Math.trySub(x, y);
--  (bool overflowsMul, uint256 resultMul) = SafeMath.tryMul(x, y);
-+  (bool overflowsMul, uint256 resultMul) = Math.tryMul(x, y);
--  (bool overflowsDiv, uint256 resultDiv) = SafeMath.tryDiv(x, y);
-+  (bool overflowsDiv, uint256 resultDiv) = Math.tryDiv(x, y);
-   // ...
- }
-```
-
-#### Adapting Governor modules
-
-Custom Governor modules that override internal functions may require modifications if migrated to v5. In particular, the new internal functions `_queueOperations` and `_executeOperations` may need to be used. If assistance with this migration is needed reach out via the [OpenZeppelin Support Forum](https://forum.openzeppelin.com/c/support/contracts/18).
-
-#### ECDSA and MessageHashUtils
-
-The `ECDSA` library is now focused on signer recovery. Previously it also included utility methods for producing digests to be used with signing or recovery. These utilities have been moved to the `MessageHashUtils` library and should be imported if needed:
-
-```diff
- import {ECDSA} from "@openzeppelin/contracts/utils/cryptography/ECDSA.sol";
-+import {MessageHashUtils} from "@openzeppelin/contracts/utils/cryptography/MessageHashUtils.sol";
-
- contract Verifier {
-   using ECDSA for bytes32;
-+  using MessageHashUtils for bytes32;
-
-   function _verify(bytes32 data, bytes memory signature, address account) internal pure returns (bool) {
-     return data
-       .toEthSignedMessageHash()
-       .recover(signature) == account;
-   }
- }
-```
-
-#### Interfaces and libraries in upgradeable contracts
-
-The upgradeable version of the contracts library used to include a variant suffixed with `Upgradeable` for every contract. These variants, which are produced automatically, mainly include changes for dealing with storage that don't apply to libraries and interfaces.
-
-The upgradeable library no longer includes upgradeable variants for libraries and interfaces. Projects migrating to 5.0 should replace their library and interface imports with their corresponding non-upgradeable version:
-
-```diff
- // Libraries
--import {AddressUpgradeable} from '@openzeppelin/contracts-upgradeable/utils/AddressUpgradeable.sol';
-+import {Address} from '@openzeppelin/contracts/utils/Address.sol';
-
- // Interfaces
--import {IERC20Upgradeable} from '@openzeppelin/contracts-upgradeable/interfaces/IERC20.sol';
-+import {IERC20} from '@openzeppelin/contracts/interfaces/IERC20.sol';
-```
-
-#### Offchain Considerations
-
-Some changes may affect offchain systems if they rely on assumptions that are changed along with these new breaking changes. These cases are:
-
-##### Relying on revert strings for processing errors
-
-A concrete example is AccessControl, where it was previously advised to catch revert reasons using the following regex:
-
-```
-/^AccessControl: account (0x[0-9a-f]{40}) is missing role (0x[0-9a-f]{64})$/
-```
-
-Instead, contracts now revert with custom errors. Systems that interact with smart contracts outside of the network should consider reliance on revert strings and possibly support the new custom errors.
-
-##### Relying on storage locations for retrieving data
-
-After 5.0, the storage location of some variables were changed. This is the case for `Initializable` and all the upgradeable contracts since they now use namespaced storaged locations. Any system relying on storage locations for retrieving data or detecting capabilities should be updated to support these new locations.
-
 ## 4.9.2 (2023-06-16)
 
 - `MerkleProof`: Fix a bug in `processMultiProof` and `processMultiProofCalldata` that allows proving arbitrary leaves if the tree contains a node with value 0 at depth 1.

README.md

@@ -1,3 +1,7 @@
+> [!NOTE]
+> Version 5.0 is currently in release candidate period. Bug bounty rewards are boosted 50% until the release.  
+> [See more details on Immunefi.](https://immunefi.com/bounty/openzeppelin/)
+
 # <img src="logo.svg" alt="OpenZeppelin" height="40px">
 
 [![NPM Package](https://img.shields.io/npm/v/@openzeppelin/contracts.svg)](https://www.npmjs.org/package/@openzeppelin/contracts)
@@ -14,7 +18,7 @@
 
 :mage: **Not sure how to get started?** Check out [Contracts Wizard](https://wizard.openzeppelin.com/) — an interactive smart contract generator.
 
-:building_construction: **Want to scale your decentralized application?** Check out [OpenZeppelin Defender](https://openzeppelin.com/defender) — a mission-critical developer security platform to code, audit, deploy, monitor, and operate with confidence.
+:building_construction: **Want to scale your decentralized application?** Check out [OpenZeppelin Defender](https://openzeppelin.com/defender) — a secure platform for automating and monitoring your operations.
 
 > [!IMPORTANT]
 > OpenZeppelin Contracts uses semantic versioning to communicate backwards compatibility of its API and storage layout. For upgradeable contracts, the storage layout of different major versions should be assumed incompatible, for example, it is unsafe to upgrade from 4.9.3 to 5.0.0. Learn more at [Backwards Compatibility](https://docs.openzeppelin.com/contracts/backwards-compatibility).
@@ -23,7 +27,7 @@
 
 ### Installation
 
-#### Hardhat, Truffle (npm)
+#### Hardhat (npm)
 
 ```
 $ npm install @openzeppelin/contracts
@@ -31,18 +35,19 @@ $ npm install @openzeppelin/contracts
 
 #### Foundry (git)
 
-> [!WARNING]
-> When installing via git, it is a common error to use the `master` branch. This is a development branch that should be avoided in favor of tagged releases. The release process involves security measures that the `master` branch does not guarantee.
-
-> [!WARNING]
-> Foundry installs the latest version initially, but subsequent `forge update` commands will use the `master` branch.
-
 ```
 $ forge install OpenZeppelin/openzeppelin-contracts
 ```
 
 Add `@openzeppelin/contracts/=lib/openzeppelin-contracts/contracts/` in `remappings.txt.` 
 
+> [!WARNING]
+> <details>
+> <summary>Avoid installing the `master` branch.</summary>
+> When installing via git, it is a common error to use the `master` branch. This is a development branch that should be avoided in favor of tagged releases. The release process involves security measures that the `master` branch does not guarantee.
+> Note that `forge install` gets the latest version initially, but subsequent `forge update` commands will use the `master` branch.
+> </details>
+
 ### Usage
 
 Once installed, you can use the contracts in the library by importing them:

audits/README.md

@@ -2,7 +2,6 @@
 
 | Date         | Version | Commit    | Auditor      | Scope                | Links                                                       |
 | ------------ | ------- | --------- | ------------ | -------------------- | ----------------------------------------------------------- |
-| October 2023 | v5.0.0  | `b5a3e69` | OpenZeppelin | v5.0 Changes         | [🔗](./2023-10-v5.0.pdf)                                    |
 | May 2023     | v4.9.0  | `91df66c` | OpenZeppelin | v4.9 Changes         | [🔗](./2023-05-v4.9.pdf)                                    |
 | October 2022 | v4.8.0  | `14f98db` | OpenZeppelin | ERC4626, Checkpoints | [🔗](./2022-10-ERC4626.pdf) [🔗](./2022-10-Checkpoints.pdf) |
 | October 2018 | v2.0.0  | `dac5bcc` | LevelK       | Everything           | [🔗](./2018-10.pdf)                                         |

certora/Makefile

@@ -17,7 +17,7 @@ $(DST): FORCE
 	@cp -r $(SRC) $@
 
 # Update a solidity file in the $DST directory using the corresponding patch
-$(DST)/%.sol: FORCE
+$(DST)/%.sol: FORCE | $(DST)
 	@echo Applying patch to $@
 	@patch -p0 -d $(DST) < $(patsubst $(DST)_%,$(DIFF)/%.patch,$(subst /,_,$@))
 
@@ -31,7 +31,7 @@ $(DIFF): FORCE
 	@mkdir $@
 
 # Create the patch file by comparing the source and the destination
-$(DIFF)/%.patch: FORCE
+$(DIFF)/%.patch: FORCE | $(DIFF)
 	@echo Generating patch $@
 	@diff -ruN \
 		$(patsubst $(DIFF)/%.patch,$(SRC)/%,$(subst _,/,$@)) \

certora/diff/access_manager_AccessManager.sol.patch

@@ -1,5 +1,5 @@
---- access/manager/AccessManager.sol	2023-10-05 12:17:09.694051809 -0300
-+++ access/manager/AccessManager.sol	2023-10-05 12:26:18.498688718 -0300
+--- access/manager/AccessManager.sol	2023-10-04 11:20:52.802378968 +0200
++++ access/manager/AccessManager.sol	2023-10-04 14:49:43.126279234 +0200
 @@ -6,7 +6,6 @@
  import {IAccessManaged} from "./IAccessManaged.sol";
  import {Address} from "../../utils/Address.sol";
@@ -8,7 +8,7 @@
  import {Math} from "../../utils/math/Math.sol";
  import {Time} from "../../utils/types/Time.sol";
  
-@@ -57,7 +56,8 @@
+@@ -48,7 +47,8 @@
   * mindful of the danger associated with functions such as {{Ownable-renounceOwnership}} or
   * {{AccessControl-renounceRole}}.
   */
@@ -18,17 +18,17 @@
      using Time for *;
  
      // Structure that stores the details for a target contract.
-@@ -105,7 +105,7 @@
+@@ -93,7 +93,7 @@
+     mapping(bytes32 operationId => Schedule) private _schedules;
  
-     // Used to identify operations that are currently being executed via {execute}.
      // This should be transient storage when supported by the EVM.
 -    bytes32 private _executionId;
 +    bytes32 internal _executionId; // private → internal for FV
  
      /**
       * @dev Check that the caller is authorized to perform the operation, following the restrictions encoded in
-@@ -253,6 +253,11 @@
-         _setGrantDelay(roleId, newDelay);
+@@ -185,6 +185,11 @@
+         return _targets[target].adminDelay.get();
      }
  
 +    // Exposed for FV
@@ -37,10 +37,10 @@
 +    }
 +
      /**
-      * @dev Internal version of {grantRole} without access control. Returns true if the role was newly granted.
+      * @dev Get the id of the role that acts as an admin for given role.
       *
-@@ -287,6 +292,11 @@
-         return newMember;
+@@ -213,6 +218,11 @@
+         return _roles[roleId].grantDelay.get();
      }
  
 +    // Exposed for FV
@@ -49,9 +49,18 @@
 +    }
 +
      /**
-      * @dev Internal version of {revokeRole} without access control. This logic is also used by {renounceRole}.
-      * Returns true if the role was previously granted.
-@@ -586,7 +596,7 @@
+      * @dev Get the access details for a given account for a given role. These details include the timepoint at which
+      * membership becomes active, and the delay applied to all operation by this user that requires this permission
+@@ -749,7 +759,7 @@
+     /**
+      * @dev Hashing function for execute protection
+      */
+-    function _hashExecutionId(address target, bytes4 selector) private pure returns (bytes32) {
++    function _hashExecutionId(address target, bytes4 selector) internal pure returns (bytes32) { // private → internal for FV
+         return keccak256(abi.encode(target, selector));
+     }
+ 
+@@ -769,7 +779,7 @@
      /**
       * @dev Check if the current call is authorized according to admin logic.
       */
@@ -60,7 +69,7 @@
          address caller = _msgSender();
          (bool immediate, uint32 delay) = _canCallSelf(caller, _msgData());
          if (!immediate) {
-@@ -609,7 +619,7 @@
+@@ -792,7 +802,7 @@
       */
      function _getAdminRestrictions(
          bytes calldata data
@@ -69,7 +78,7 @@
          if (data.length < 4) {
              return (false, 0, 0);
          }
-@@ -662,7 +672,7 @@
+@@ -847,7 +857,7 @@
          address caller,
          address target,
          bytes calldata data
@@ -78,7 +87,7 @@
          if (target == address(this)) {
              return _canCallSelf(caller, data);
          } else {
-@@ -716,14 +726,14 @@
+@@ -901,7 +911,7 @@
      /**
       * @dev Extracts the selector from calldata. Panics if data is not at least 4 bytes
       */
@@ -86,12 +95,4 @@
 +    function _checkSelector(bytes calldata data) internal pure returns (bytes4) { // private → internal for FV
          return bytes4(data[0:4]);
      }
- 
-     /**
-      * @dev Hashing function for execute protection
-      */
--    function _hashExecutionId(address target, bytes4 selector) private pure returns (bytes32) {
-+    function _hashExecutionId(address target, bytes4 selector) internal pure returns (bytes32) { // private → internal for FV
-         return keccak256(abi.encode(target, selector));
-     }
  }

certora/harnesses/AccessManagedHarness.sol

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.20;
+
+import "../patched/access/manager/IAccessManager.sol";
+import "../patched/access/manager/AccessManaged.sol";
+
+contract AccessManagedHarness is AccessManaged {
+    bytes internal SOME_FUNCTION_CALLDATA = abi.encodeCall(this.someFunction, ());
+
+    constructor(address initialAuthority) AccessManaged(initialAuthority) {}
+
+    function someFunction() public restricted() {
+        // Sanity for FV: the msg.data when calling this function should be the same as the data used when checking
+        // the schedule. This is a reformulation of `msg.data == SOME_FUNCTION_CALLDATA` that focuses on the operation
+        // hash for this call.
+        require(
+            IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data)
+            ==
+            IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA)
+        );
+    }
+
+    function authority_canCall_immediate(address caller) public view returns (bool result) {
+        (result,) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
+    }
+
+    function authority_canCall_delay(address caller) public view returns (uint32 result) {
+        (,result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
+    }
+
+    function authority_getSchedule(address caller) public view returns (uint48) {
+        IAccessManager manager = IAccessManager(authority());
+        return manager.getSchedule(manager.hashOperation(caller, address(this), SOME_FUNCTION_CALLDATA));
+    }
+}

certora/harnesses/AccessManagerHarness.sol

@@ -0,0 +1,116 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.20;
+
+import "../patched/access/manager/AccessManager.sol";
+
+contract AccessManagerHarness is AccessManager {
+    // override with a storage slot that can basically take any value.
+    uint32 private _minSetback;
+
+    constructor(address initialAdmin) AccessManager(initialAdmin) {}
+
+    // FV
+    function minSetback() public view override returns (uint32) {
+        return _minSetback;
+    }
+
+    function canCall_immediate(address caller, address target, bytes4 selector) external view returns (bool result) {
+        (result,) = canCall(caller, target, selector);
+    }
+
+    function canCall_delay(address caller, address target, bytes4 selector) external view returns (uint32 result) {
+        (,result) = canCall(caller, target, selector);
+    }
+
+    function canCallExtended(address caller, address target, bytes calldata data) external view returns (bool, uint32) {
+        return _canCallExtended(caller, target, data);
+    }
+
+    function canCallExtended_immediate(address caller, address target, bytes calldata data) external view returns (bool result) {
+        (result,) = _canCallExtended(caller, target, data);
+    }
+
+    function canCallExtended_delay(address caller, address target, bytes calldata data) external view returns (uint32 result) {
+        (,result) = _canCallExtended(caller, target, data);
+    }
+
+    function getAdminRestrictions_restricted(bytes calldata data) external view returns (bool result) {
+        (result,,) = _getAdminRestrictions(data);
+    }
+
+    function getAdminRestrictions_roleAdminId(bytes calldata data) external view returns (uint64 result) {
+        (,result,) = _getAdminRestrictions(data);
+    }
+
+    function getAdminRestrictions_executionDelay(bytes calldata data) external view returns (uint32 result) {
+        (,,result) = _getAdminRestrictions(data);
+    }
+
+    function hasRole_isMember(uint64 roleId, address account) external view returns (bool result) {
+        (result,) = hasRole(roleId, account);
+    }
+
+    function hasRole_executionDelay(uint64 roleId, address account) external view returns (uint32 result) {
+        (,result) = hasRole(roleId, account);
+    }
+
+    function getAccess_since(uint64 roleId, address account) external view returns (uint48 result) {
+        (result,,,) = getAccess(roleId, account);
+    }
+
+    function getAccess_currentDelay(uint64 roleId, address account) external view returns (uint32 result) {
+        (,result,,) = getAccess(roleId, account);
+    }
+
+    function getAccess_pendingDelay(uint64 roleId, address account) external view returns (uint32 result) {
+        (,,result,) = getAccess(roleId, account);
+    }
+
+    function getAccess_effect(uint64 roleId, address account) external view returns (uint48 result) {
+        (,,,result) = getAccess(roleId, account);
+    }
+
+    function getTargetAdminDelay_after(address target) public view virtual returns (uint32 result) {
+        (,result,) = _getTargetAdminDelayFull(target);
+    }
+
+    function getTargetAdminDelay_effect(address target) public view virtual returns (uint48 result) {
+        (,,result) = _getTargetAdminDelayFull(target);
+    }
+
+    function getRoleGrantDelay_after(uint64 roleId) public view virtual returns (uint32 result) {
+        (,result,) = _getRoleGrantDelayFull(roleId);
+    }
+
+    function getRoleGrantDelay_effect(uint64 roleId) public view virtual returns (uint48 result) {
+        (,,result) = _getRoleGrantDelayFull(roleId);
+    }
+
+    function hashExecutionId(address target, bytes4 selector) external pure returns (bytes32) {
+        return _hashExecutionId(target, selector);
+    }
+
+    function executionId() external view returns (bytes32) {
+        return _executionId;
+    }
+
+    // Pad with zeros (and don't revert) if data is too short.
+    function getSelector(bytes calldata data) external pure returns (bytes4) {
+        return bytes4(data);
+    }
+
+    function getFirstArgumentAsAddress(bytes calldata data) external pure returns (address) {
+        return abi.decode(data[0x04:0x24], (address));
+    }
+
+    function getFirstArgumentAsUint64(bytes calldata data) external pure returns (uint64) {
+        return abi.decode(data[0x04:0x24], (uint64));
+    }
+
+    function _checkAuthorized() internal override {
+        // We need this hack otherwise certora will assume _checkSelector(_msgData()) can return anything :/
+        require(msg.sig == _checkSelector(_msgData()));
+        super._checkAuthorized();
+    }
+}

certora/specs.json

@@ -14,6 +14,25 @@
     "contract": "AccessControlDefaultAdminRulesHarness",
     "files": ["certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"]
   },
+  {
+    "spec": "AccessManager",
+    "contract": "AccessManagerHarness",
+    "files": ["certora/harnesses/AccessManagerHarness.sol"],
+    "options": ["--optimistic_hashing", "--optimistic_loop"]
+  },
+  {
+    "spec": "AccessManaged",
+    "contract": "AccessManagedHarness",
+    "files": [
+      "certora/harnesses/AccessManagedHarness.sol",
+      "certora/harnesses/AccessManagerHarness.sol"
+    ],
+    "options": [
+      "--optimistic_hashing",
+      "--optimistic_loop",
+      "--link AccessManagedHarness:_authority=AccessManagerHarness"
+    ]
+  },
   {
     "spec": "DoubleEndedQueue",
     "contract": "DoubleEndedQueueHarness",

certora/specs/AccessManaged.spec

@@ -0,0 +1,34 @@
+import "helpers/helpers.spec";
+import "methods/IAccessManaged.spec";
+
+methods {
+    // FV
+    function someFunction()                       external;
+    function authority_canCall_immediate(address) external returns (bool);
+    function authority_canCall_delay(address)     external returns (uint32);
+    function authority_getSchedule(address)       external returns (uint48);
+}
+
+invariant isConsumingScheduledOpClean()
+    isConsumingScheduledOp() == to_bytes4(0);
+
+rule callRestrictedFunction(env e) {
+    bool   immediate      = authority_canCall_immediate(e, e.msg.sender);
+    uint32 delay          = authority_canCall_delay(e, e.msg.sender);
+    uint48 scheduleBefore = authority_getSchedule(e, e.msg.sender);
+
+    someFunction@withrevert(e);
+    bool success = !lastReverted;
+
+    uint48 scheduleAfter  = authority_getSchedule(e, e.msg.sender);
+
+    // can only call if immediate, or (with delay) by consuming a scheduled op
+    assert success => (
+        immediate ||
+        (
+            delay > 0 &&
+            isSetAndPast(e, scheduleBefore) &&
+            scheduleAfter == 0
+        )
+    );
+}

certora/specs/AccessManager.spec

@@ -0,0 +1,826 @@
+import "helpers/helpers.spec";
+import "methods/IAccessManager.spec";
+
+methods {
+    // FV
+    function canCall_immediate(address,address,bytes4)        external returns (bool);
+    function canCall_delay(address,address,bytes4)            external returns (uint32);
+    function canCallExtended(address,address,bytes)           external returns (bool,uint32);
+    function canCallExtended_immediate(address,address,bytes) external returns (bool);
+    function canCallExtended_delay(address,address,bytes)     external returns (uint32);
+    function getAdminRestrictions_restricted(bytes)           external returns (bool);
+    function getAdminRestrictions_roleAdminId(bytes)          external returns (uint64);
+    function getAdminRestrictions_executionDelay(bytes)       external returns (uint32);
+    function hasRole_isMember(uint64,address)                 external returns (bool);
+    function hasRole_executionDelay(uint64,address)           external returns (uint32);
+    function getAccess_since(uint64,address)                  external returns (uint48);
+    function getAccess_currentDelay(uint64,address)           external returns (uint32);
+    function getAccess_pendingDelay(uint64,address)           external returns (uint32);
+    function getAccess_effect(uint64,address)                 external returns (uint48);
+    function getTargetAdminDelay_after(address target)        external returns (uint32);
+    function getTargetAdminDelay_effect(address target)       external returns (uint48);
+    function getRoleGrantDelay_after(uint64 roleId)           external returns (uint32);
+    function getRoleGrantDelay_effect(uint64 roleId)          external returns (uint48);
+    function hashExecutionId(address,bytes4)                  external returns (bytes32) envfree;
+    function executionId()                                    external returns (bytes32) envfree;
+    function getSelector(bytes)                               external returns (bytes4)  envfree;
+    function getFirstArgumentAsAddress(bytes)                 external returns (address) envfree;
+    function getFirstArgumentAsUint64(bytes)                  external returns (uint64)  envfree;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition isOnlyAuthorized(bytes4 selector) returns bool =
+    selector == to_bytes4(sig:labelRole(uint64,string).selector                      ) ||
+    selector == to_bytes4(sig:setRoleAdmin(uint64,uint64).selector                   ) ||
+    selector == to_bytes4(sig:setRoleGuardian(uint64,uint64).selector                ) ||
+    selector == to_bytes4(sig:setGrantDelay(uint64,uint32).selector                  ) ||
+    selector == to_bytes4(sig:setTargetAdminDelay(address,uint32).selector           ) ||
+    selector == to_bytes4(sig:updateAuthority(address,address).selector              ) ||
+    selector == to_bytes4(sig:setTargetClosed(address,bool).selector                 ) ||
+    selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector) ||
+    selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector              ) ||
+    selector == to_bytes4(sig:revokeRole(uint64,address).selector                    );
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: executionId must be clean when not in the middle of a call                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant cleanExecutionId()
+    executionId() == to_bytes32(0);
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: public role                                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant publicRole(env e, address account)
+    hasRole_isMember(e, PUBLIC_ROLE(), account)        &&
+    hasRole_executionDelay(e, PUBLIC_ROLE(), account)   == 0 &&
+    getAccess_since(e, PUBLIC_ROLE(), account) == 0 &&
+    getAccess_currentDelay(e, PUBLIC_ROLE(), account) == 0 &&
+    getAccess_pendingDelay(e, PUBLIC_ROLE(), account) == 0 &&
+    getAccess_effect(e, PUBLIC_ROLE(), account) == 0;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: hasRole is consistent with getAccess                                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant hasRoleGetAccessConsistency(env e, uint64 roleId, address account)
+    hasRole_isMember(e, roleId, account) == (roleId == PUBLIC_ROLE() || isSetAndPast(e, getAccess_since(e, roleId, account))) &&
+    hasRole_executionDelay(e, roleId, account) == getAccess_currentDelay(e, roleId, account);
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Functions: canCall, canCallExtended, getAccess, hasRole, isTargetClosed and getTargetFunctionRole do NOT revert     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noRevert(env e) {
+    require nonpayable(e);
+    require sanity(e);
+
+    address caller;
+    address target;
+    bytes   data;
+    bytes4  selector;
+    uint64  roleId;
+
+    canCall@withrevert(e, caller, target, selector);
+    assert !lastReverted;
+
+    // require data.length <= max_uint64;
+    //
+    // canCallExtended@withrevert(e, caller, target, data);
+    // assert !lastReverted;
+
+    getAccess@withrevert(e, roleId, caller);
+    assert !lastReverted;
+
+    hasRole@withrevert(e, roleId, caller);
+    assert !lastReverted;
+
+    isTargetClosed@withrevert(target);
+    assert !lastReverted;
+
+    getTargetFunctionRole@withrevert(target, selector);
+    assert !lastReverted;
+
+    // Not covered:
+    // - getAdminRestrictions (_1, _2 & _3)
+    // - getSelector
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Functions: admin restrictions are correct                                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getAdminRestrictions(env e, bytes data) {
+    bool   restricted = getAdminRestrictions_restricted(e, data);
+    uint64 roleId     = getAdminRestrictions_roleAdminId(e, data);
+    uint32 delay      = getAdminRestrictions_executionDelay(e, data);
+    bytes4 selector   = getSelector(data);
+
+    if (data.length < 4) {
+        assert restricted == false;
+        assert roleId     == 0;
+        assert delay      == 0;
+    } else {
+        assert restricted ==
+            isOnlyAuthorized(selector);
+
+        assert roleId == (
+            (restricted && selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector)) ||
+            (restricted && selector == to_bytes4(sig:revokeRole(uint64,address).selector      ))
+            ? getRoleAdmin(getFirstArgumentAsUint64(data))
+            : ADMIN_ROLE()
+        );
+
+        assert delay == (
+            (restricted && selector == to_bytes4(sig:updateAuthority(address,address).selector              )) ||
+            (restricted && selector == to_bytes4(sig:setTargetClosed(address,bool).selector                 )) ||
+            (restricted && selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector))
+            ? getTargetAdminDelay(e, getFirstArgumentAsAddress(data))
+            : 0
+        );
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Functions: canCall                                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule canCall(env e) {
+    address caller;
+    address target;
+    bytes4 selector;
+
+    // Get relevant values
+    bool   immediate    = canCall_immediate(e, caller, target, selector);
+    uint32 delay        = canCall_delay(e, caller, target, selector);
+    bool   closed       = isTargetClosed(target);
+    uint64 roleId       = getTargetFunctionRole(target, selector);
+    bool   isMember     = hasRole_isMember(e, roleId, caller);
+    uint32 currentDelay = hasRole_executionDelay(e, roleId, caller);
+
+    // Can only execute without delay in specific cases:
+    // - target not closed
+    // - if self-execution: `executionId` must match
+    // - if third party execution: must be member with no delay
+    assert immediate <=> (
+        !closed &&
+        (
+            (caller == currentContract && executionId() == hashExecutionId(target, selector))
+            ||
+            (caller != currentContract && isMember && currentDelay == 0)
+        )
+    );
+
+    // Can only execute with delay in specific cases:
+    // - target not closed
+    // - third party execution
+    // - caller is a member and has an execution delay
+    assert delay > 0 <=> (
+        !closed &&
+        caller != currentContract &&
+        isMember &&
+        currentDelay > 0
+    );
+
+    // If there is a delay, then it must be the caller's execution delay
+    assert delay > 0 => delay == currentDelay;
+
+    // Immediate execute means no delayed execution
+    assert immediate => delay == 0;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Functions: canCallExtended                                                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule canCallExtended(env e) {
+    address caller;
+    address target;
+    bytes   data;
+    bytes4  selector = getSelector(data);
+
+    bool   immediate      = canCallExtended_immediate(e, caller, target, data);
+    uint32 delay          = canCallExtended_delay(e, caller, target, data);
+    bool   enabled        = getAdminRestrictions_restricted(e, data);
+    uint64 roleId         = getAdminRestrictions_roleAdminId(e, data);
+    uint32 operationDelay = getAdminRestrictions_executionDelay(e, data);
+    bool   inRole         = hasRole_isMember(e, roleId, caller);
+    uint32 executionDelay = hasRole_executionDelay(e, roleId, caller);
+
+    if (target == currentContract) {
+        // Can only execute without delay in the specific cases:
+        // - caller is the AccessManager and the executionId is set
+        // or
+        // - data matches an admin restricted function
+        // - caller has the necessary role
+        // - operation delay is not set
+        // - execution delay is not set
+        assert immediate <=> (
+            (
+                caller         == currentContract &&
+                data.length    >= 4               &&
+                executionId()  == hashExecutionId(target, selector)
+            ) || (
+                caller         != currentContract &&
+                enabled                           &&
+                inRole                            &&
+                operationDelay == 0               &&
+                executionDelay == 0
+            )
+        );
+
+        // Immediate execute means no delayed execution
+        // This is equivalent to "delay > 0 => !immediate"
+        assert immediate => delay == 0;
+
+        // Can only execute with delay in specific cases:
+        // - caller is a third party
+        // - data matches an admin restricted function
+        // - caller has the necessary role
+        // -operation delay or execution delay is set
+        assert delay > 0 <=> (
+            caller != currentContract &&
+            enabled                   &&
+            inRole                    &&
+            (operationDelay > 0 || executionDelay > 0)
+        );
+
+        // If there is a delay, then it must be the maximum of caller's execution delay and the operation delay
+        assert delay > 0 => to_mathint(delay) == max(operationDelay, executionDelay);
+    } else if (data.length < 4) {
+        assert immediate == false;
+        assert delay     == 0;
+    } else {
+        // results are equivalent when targeting third party contracts
+        assert immediate == canCall_immediate(e, caller, target, selector);
+        assert delay     == canCall_delay(e, caller, target, selector);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: getAccess                                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getAccessChangeTime(uint64 roleId, address account) {
+    env e1;
+    env e2;
+
+    // values before
+    mathint getAccess1Before = getAccess_since(e1, roleId, account);
+    mathint getAccess2Before = getAccess_currentDelay(e1, roleId, account);
+    mathint getAccess3Before = getAccess_pendingDelay(e1, roleId, account);
+    mathint getAccess4Before = getAccess_effect(e1, roleId, account);
+
+    // time pass: e1 → e2
+    require clock(e1) <= clock(e2);
+
+    // values after
+    mathint getAccess1After  = getAccess_since(e2, roleId, account);
+    mathint getAccess2After  = getAccess_currentDelay(e2, roleId, account);
+    mathint getAccess3After  = getAccess_pendingDelay(e2, roleId, account);
+    mathint getAccess4After  = getAccess_effect(e2, roleId, account);
+
+    // member "since" cannot change as a consequence of time passing
+    assert getAccess1Before == getAccess1After;
+
+    // any change of any other value should be a consequence of the effect timepoint being reached
+    assert (
+        getAccess2Before != getAccess2After ||
+        getAccess3Before != getAccess3After ||
+        getAccess4Before != getAccess4After
+    ) => (
+        getAccess4Before != 0 &&
+        getAccess4Before >  clock(e1) &&
+        getAccess4Before <= clock(e2) &&
+        getAccess2After  == getAccess3Before &&
+        getAccess3After  == 0 &&
+        getAccess4After  == 0
+    );
+}
+
+rule getAccessChangeCall(uint64 roleId, address account) {
+    env e;
+
+    // sanity
+    require sanity(e);
+
+    // values before
+    mathint getAccess1Before = getAccess_since(e, roleId, account);
+    mathint getAccess2Before = getAccess_currentDelay(e, roleId, account);
+    mathint getAccess3Before = getAccess_pendingDelay(e, roleId, account);
+    mathint getAccess4Before = getAccess_effect(e, roleId, account);
+
+    // arbitrary function call
+    method f; calldataarg args; f(e, args);
+
+    // values before
+    mathint getAccess1After = getAccess_since(e, roleId, account);
+    mathint getAccess2After = getAccess_currentDelay(e, roleId, account);
+    mathint getAccess3After = getAccess_pendingDelay(e, roleId, account);
+    mathint getAccess4After = getAccess_effect(e, roleId, account);
+
+    // transitions
+    assert (
+        getAccess1Before != getAccess1After ||
+        getAccess2Before != getAccess2After ||
+        getAccess3Before != getAccess3After ||
+        getAccess4Before != getAccess4After
+    ) => (
+        (
+            f.selector == sig:grantRole(uint64,address,uint32).selector &&
+            getAccess1After > 0
+        ) || (
+            (
+                f.selector == sig:revokeRole(uint64,address).selector ||
+                f.selector == sig:renounceRole(uint64,address).selector
+            ) &&
+            getAccess1After == 0 &&
+            getAccess2After == 0 &&
+            getAccess3After == 0 &&
+            getAccess4After == 0
+        )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: isTargetClosed                                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule isTargetClosedChangeTime(address target) {
+    env e1;
+    env e2;
+
+    // values before
+    bool isClosedBefore = isTargetClosed(e1, target);
+
+    // time pass: e1 → e2
+    require clock(e1) <= clock(e2);
+
+    // values after
+    bool isClosedAfter = isTargetClosed(e2, target);
+
+    // transitions
+    assert isClosedBefore == isClosedAfter;
+}
+
+rule isTargetClosedChangeCall(address target) {
+    env e;
+
+    // values before
+    bool isClosedBefore = isTargetClosed(e, target);
+
+    // arbitrary function call
+    method f; calldataarg args; f(e, args);
+
+    // values after
+    bool isClosedAfter = isTargetClosed(e, target);
+
+    // transitions
+    assert isClosedBefore != isClosedAfter => (
+        f.selector == sig:setTargetClosed(address,bool).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: getTargetFunctionRole                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getTargetFunctionRoleChangeTime(address target, bytes4 selector) {
+    env e1;
+    env e2;
+
+    // values before
+    mathint roleIdBefore = getTargetFunctionRole(e1, target, selector);
+
+    // time pass: e1 → e2
+    require clock(e1) <= clock(e2);
+
+    // values after
+    mathint roleIdAfter = getTargetFunctionRole(e2, target, selector);
+
+    // transitions
+    assert roleIdBefore == roleIdAfter;
+}
+
+rule getTargetFunctionRoleChangeCall(address target, bytes4 selector) {
+    env e;
+
+    // values before
+    mathint roleIdBefore = getTargetFunctionRole(e, target, selector);
+
+    // arbitrary function call
+    method f; calldataarg args; f(e, args);
+
+    // values after
+    mathint roleIdAfter = getTargetFunctionRole(e, target, selector);
+
+    // transitions
+    assert roleIdBefore != roleIdAfter => (
+        f.selector == sig:setTargetFunctionRole(address,bytes4[],uint64).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: getTargetAdminDelay                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getTargetAdminDelayChangeTime(address target) {
+    env e1;
+    env e2;
+
+    // values before
+    mathint delayBefore        = getTargetAdminDelay(e1, target);
+    mathint delayPendingBefore = getTargetAdminDelay_after(e1, target);
+    mathint delayEffectBefore  = getTargetAdminDelay_effect(e1, target);
+
+    // time pass: e1 → e2
+    require clock(e1) <= clock(e2);
+
+    // values after
+    mathint delayAfter        = getTargetAdminDelay(e2, target);
+    mathint delayPendingAfter = getTargetAdminDelay_after(e2, target);
+    mathint delayEffectAfter  = getTargetAdminDelay_effect(e2, target);
+
+    assert (
+        delayBefore        != delayAfter        ||
+        delayPendingBefore != delayPendingAfter ||
+        delayEffectBefore  != delayEffectAfter
+    ) => (
+        delayEffectBefore >  clock(e1)          &&
+        delayEffectBefore <= clock(e2)          &&
+        delayAfter        == delayPendingBefore &&
+        delayPendingAfter == 0                  &&
+        delayEffectAfter  == 0
+    );
+}
+
+rule getTargetAdminDelayChangeCall(address target) {
+    env e;
+
+    // values before
+    mathint delayBefore        = getTargetAdminDelay(e, target);
+    mathint delayPendingBefore = getTargetAdminDelay_after(e, target);
+    mathint delayEffectBefore  = getTargetAdminDelay_effect(e, target);
+
+    // arbitrary function call
+    method f; calldataarg args; f(e, args);
+
+    // values after
+    mathint delayAfter        = getTargetAdminDelay(e, target);
+    mathint delayPendingAfter = getTargetAdminDelay_after(e, target);
+    mathint delayEffectAfter  = getTargetAdminDelay_effect(e, target);
+
+    // if anything changed ...
+    assert (
+        delayBefore        != delayAfter        ||
+        delayPendingBefore != delayPendingAfter ||
+        delayEffectBefore  != delayEffectAfter
+    ) => (
+        (
+            // ... it was the consequence of a call to setTargetAdminDelay
+            f.selector == sig:setTargetAdminDelay(address,uint32).selector
+        ) && (
+            // ... delay cannot decrease instantly
+            delayAfter >= delayBefore
+        ) && (
+            // ... if setback is not 0, value cannot change instantly
+            minSetback() > 0 => (
+                delayBefore == delayAfter
+            )
+        ) && (
+            // ... if the value did not change and there is a minSetback, there must be something scheduled in the future
+            delayAfter == delayBefore && minSetback() > 0 => (
+                delayEffectAfter >= clock(e) + minSetback()
+            )
+            // note: if there is no minSetback, and if the caller "confirms" the current value,
+            // then this as immediate effect and nothing is scheduled
+        ) && (
+            // ... if the value changed, then no further change should be scheduled
+            delayAfter != delayBefore => (
+                delayPendingAfter == 0 &&
+                delayEffectAfter  == 0
+            )
+        )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: getRoleGrantDelay                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getRoleGrantDelayChangeTime(uint64 roleId) {
+    env e1;
+    env e2;
+
+    // values before
+    mathint delayBefore        = getRoleGrantDelay(e1, roleId);
+    mathint delayPendingBefore = getRoleGrantDelay_after(e1, roleId);
+    mathint delayEffectBefore  = getRoleGrantDelay_effect(e1, roleId);
+
+    // time pass: e1 → e2
+    require clock(e1) <= clock(e2);
+
+    // values after
+    mathint delayAfter        = getRoleGrantDelay(e2, roleId);
+    mathint delayPendingAfter = getRoleGrantDelay_after(e2, roleId);
+    mathint delayEffectAfter  = getRoleGrantDelay_effect(e2, roleId);
+
+    assert (
+        delayBefore        != delayAfter        ||
+        delayPendingBefore != delayPendingAfter ||
+        delayEffectBefore  != delayEffectAfter
+    ) => (
+        delayEffectBefore >  clock(e1)          &&
+        delayEffectBefore <= clock(e2)          &&
+        delayAfter        == delayPendingBefore &&
+        delayPendingAfter == 0                  &&
+        delayEffectAfter  == 0
+    );
+}
+
+rule getRoleGrantDelayChangeCall(uint64 roleId) {
+    env e;
+
+    // values before
+    mathint delayBefore        = getRoleGrantDelay(e, roleId);
+    mathint delayPendingBefore = getRoleGrantDelay_after(e, roleId);
+    mathint delayEffectBefore  = getRoleGrantDelay_effect(e, roleId);
+
+    // arbitrary function call
+    method f; calldataarg args; f(e, args);
+
+    // values after
+    mathint delayAfter        = getRoleGrantDelay(e, roleId);
+    mathint delayPendingAfter = getRoleGrantDelay_after(e, roleId);
+    mathint delayEffectAfter  = getRoleGrantDelay_effect(e, roleId);
+
+    // if anything changed ...
+    assert (
+        delayBefore        != delayAfter        ||
+        delayPendingBefore != delayPendingAfter ||
+        delayEffectBefore  != delayEffectAfter
+    ) => (
+        (
+            // ... it was the consequence of a call to setTargetAdminDelay
+            f.selector == sig:setGrantDelay(uint64,uint32).selector
+        ) && (
+            // ... delay cannot decrease instantly
+            delayAfter >= delayBefore
+        ) && (
+            // ... if setback is not 0, value cannot change instantly
+            minSetback() > 0 => (
+                delayBefore == delayAfter
+            )
+        ) && (
+            // ... if the value did not change and there is a minSetback, there must be something scheduled in the future
+            delayAfter == delayBefore && minSetback() > 0 => (
+                delayEffectAfter >= clock(e) + minSetback()
+            )
+            // note: if there is no minSetback, and if the caller "confirms" the current value,
+            // then this as immediate effect and nothing is scheduled
+        ) && (
+            // ... if the value changed, then no further change should be scheduled
+            delayAfter != delayBefore => (
+                delayPendingAfter == 0 &&
+                delayEffectAfter  == 0
+            )
+        )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: getRoleAdmin & getRoleGuardian                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getRoleAdminChangeCall(uint64 roleId) {
+    // values before
+    mathint adminIdBefore = getRoleAdmin(roleId);
+
+    // arbitrary function call
+    env e; method f; calldataarg args; f(e, args);
+
+    // values after
+    mathint adminIdAfter = getRoleAdmin(roleId);
+
+    // transitions
+    assert adminIdBefore != adminIdAfter => f.selector == sig:setRoleAdmin(uint64,uint64).selector;
+}
+
+rule getRoleGuardianChangeCall(uint64 roleId) {
+    // values before
+    mathint guardianIdBefore = getRoleGuardian(roleId);
+
+    // arbitrary function call
+    env e; method f; calldataarg args; f(e, args);
+
+    // values after
+    mathint guardianIdAfter = getRoleGuardian(roleId);
+
+    // transitions
+    assert guardianIdBefore != guardianIdAfter => (
+        f.selector == sig:setRoleGuardian(uint64,uint64).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: getNonce                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getNonceChangeCall(bytes32 operationId) {
+    // values before
+    mathint nonceBefore = getNonce(operationId);
+
+    // reasonable assumption
+    require nonceBefore < max_uint32;
+
+    // arbitrary function call
+    env e; method f; calldataarg args; f(e, args);
+
+    // values after
+    mathint nonceAfter = getNonce(operationId);
+
+    // transitions
+    assert nonceBefore != nonceAfter => (
+        f.selector == sig:schedule(address,bytes,uint48).selector &&
+        nonceAfter == nonceBefore + 1
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ State transitions: getSchedule                                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getScheduleChangeTime(bytes32 operationId) {
+    env e1;
+    env e2;
+
+    // values before
+    mathint scheduleBefore = getSchedule(e1, operationId);
+
+    // time pass: e1 → e2
+    require clock(e1) <= clock(e2);
+
+    // values after
+    mathint scheduleAfter = getSchedule(e2, operationId);
+
+    // transition
+    assert scheduleBefore != scheduleAfter => (
+        scheduleBefore + expiration() >  clock(e1) &&
+        scheduleBefore + expiration() <= clock(e2) &&
+        scheduleAfter == 0
+    );
+}
+
+rule getScheduleChangeCall(bytes32 operationId) {
+    env e;
+
+    // values before
+    mathint scheduleBefore = getSchedule(e, operationId);
+
+    // arbitrary function call
+    method f; calldataarg args; f(e, args);
+
+    // values after
+    mathint scheduleAfter = getSchedule(e, operationId);
+
+    // transitions
+    assert scheduleBefore != scheduleAfter => (
+        (f.selector == sig:schedule(address,bytes,uint48).selector    && scheduleAfter >= clock(e)) ||
+        (f.selector == sig:execute(address,bytes).selector            && scheduleAfter == 0       ) ||
+        (f.selector == sig:cancel(address,address,bytes).selector     && scheduleAfter == 0       ) ||
+        (f.selector == sig:consumeScheduledOp(address,bytes).selector && scheduleAfter == 0       ) ||
+        (isOnlyAuthorized(to_bytes4(f.selector))                      && scheduleAfter == 0       )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Functions: restricted functions can only be called by owner                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule restrictedFunctions(env e) {
+    require nonpayable(e);
+    require sanity(e);
+
+    method f;
+    calldataarg args;
+
+    f(e,args);
+
+    assert (
+        f.selector == sig:labelRole(uint64,string).selector ||
+        f.selector == sig:setRoleAdmin(uint64,uint64).selector ||
+        f.selector == sig:setRoleGuardian(uint64,uint64).selector ||
+        f.selector == sig:setGrantDelay(uint64,uint32).selector ||
+        f.selector == sig:setTargetAdminDelay(address,uint32).selector ||
+        f.selector == sig:updateAuthority(address,address).selector ||
+        f.selector == sig:setTargetClosed(address,bool).selector ||
+        f.selector == sig:setTargetFunctionRole(address,bytes4[],uint64).selector
+    ) => (
+        hasRole_isMember(e, ADMIN_ROLE(), e.msg.sender) || e.msg.sender == currentContract
+    );
+}
+
+rule restrictedFunctionsGrantRole(env e) {
+    require nonpayable(e);
+    require sanity(e);
+
+    uint64 roleId;
+    address account;
+    uint32 executionDelay;
+
+    // We want to check that the caller has the admin role before we possibly grant it.
+    bool hasAdminRoleBefore = hasRole_isMember(e, getRoleAdmin(roleId), e.msg.sender);
+
+    grantRole(e, roleId, account, executionDelay);
+
+    assert hasAdminRoleBefore || e.msg.sender == currentContract;
+}
+
+rule restrictedFunctionsRevokeRole(env e) {
+    require nonpayable(e);
+    require sanity(e);
+
+    uint64 roleId;
+    address account;
+
+    // This is needed if roleId is self-administered, the `revokeRole` call could target
+    // e.msg.sender and remove the very role that is necessary for authorizing the call.
+    bool hasAdminRoleBefore = hasRole_isMember(e, getRoleAdmin(roleId), e.msg.sender);
+
+    revokeRole(e, roleId, account);
+
+    assert hasAdminRoleBefore || e.msg.sender == currentContract;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Functions: canCall delay is enforced for calls to execute (only for others target)                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+// getScheduleChangeCall proves that only {schedule} can set an operation schedule to a non 0 value
+rule callDelayEnforce_scheduleInTheFuture(env e) {
+    address target;
+    bytes   data;
+    uint48  when;
+
+    // Condition: calling a third party with a delay
+    mathint delay = canCallExtended_delay(e, e.msg.sender, target, data);
+    require delay > 0;
+
+    // Schedule
+    schedule(e, target, data, when);
+
+    // Get operation schedule
+    mathint timepoint = getSchedule(e, hashOperation(e.msg.sender, target, data));
+
+    // Schedule is far enough in the future
+    assert timepoint == max(clock(e) + delay, when);
+}
+
+rule callDelayEnforce_executeAfterDelay(env e) {
+    address target;
+    bytes   data;
+
+    // Condition: calling a third party with a delay
+    mathint delay = canCallExtended_delay(e, e.msg.sender, target, data);
+
+    // Get operation schedule before
+    mathint scheduleBefore = getSchedule(e, hashOperation(e.msg.sender, target, data));
+
+    // Do call
+    execute@withrevert(e, target, data);
+    bool success = !lastReverted;
+
+    // Get operation schedule after
+    mathint scheduleAfter = getSchedule(e, hashOperation(e.msg.sender, target, data));
+
+    // Can only execute if delay is set and has passed
+    assert success => (
+        delay > 0 => (
+            scheduleBefore != 0 &&
+            scheduleBefore <= clock(e)
+        ) &&
+        scheduleAfter == 0
+    );
+}

certora/specs/helpers/helpers.spec

@@ -1,7 +1,12 @@
 // environment
 definition nonpayable(env e) returns bool = e.msg.value == 0;
 definition nonzerosender(env e) returns bool = e.msg.sender != 0;
+definition sanity(env e) returns bool = clock(e) > 0 && clock(e) <= max_uint48;
 
 // math
 definition min(mathint a, mathint b) returns mathint = a < b ? a : b;
 definition max(mathint a, mathint b) returns mathint = a > b ? a : b;
+
+// time
+definition clock(env e) returns mathint = to_mathint(e.block.timestamp);
+definition isSetAndPast(env e, uint48 timepoint) returns bool = timepoint != 0 && to_mathint(timepoint) <= clock(e);

certora/specs/methods/IAccessManaged.spec

@@ -0,0 +1,5 @@
+methods {
+    function authority()              external returns (address) envfree;
+    function isConsumingScheduledOp() external returns (bytes4)  envfree;
+    function setAuthority(address)    external;
+}

certora/specs/methods/IAccessManager.spec

@@ -0,0 +1,33 @@
+methods {
+    function ADMIN_ROLE()                                   external returns (uint64) envfree;
+    function PUBLIC_ROLE()                                  external returns (uint64) envfree;
+    function canCall(address,address,bytes4)                external returns (bool,uint32);
+    function expiration()                                   external returns (uint32) envfree;
+    function minSetback() external returns (uint32) envfree;
+    function isTargetClosed(address)                        external returns (bool) envfree;
+    function getTargetFunctionRole(address,bytes4)          external returns (uint64) envfree;
+    function getTargetAdminDelay(address)                   external returns (uint32);
+    function getRoleAdmin(uint64)                           external returns (uint64) envfree;
+    function getRoleGuardian(uint64)                        external returns (uint64) envfree;
+    function getRoleGrantDelay(uint64)                      external returns (uint32);
+    function getAccess(uint64,address)                      external returns (uint48,uint32,uint32,uint48);
+    function hasRole(uint64,address)                        external returns (bool,uint32);
+    function labelRole(uint64,string)                       external;
+    function grantRole(uint64,address,uint32)               external;
+    function revokeRole(uint64,address)                     external;
+    function renounceRole(uint64,address)                   external;
+    function setRoleAdmin(uint64,uint64)                    external;
+    function setRoleGuardian(uint64,uint64)                 external;
+    function setGrantDelay(uint64,uint32)                   external;
+    function setTargetFunctionRole(address,bytes4[],uint64) external;
+    function setTargetAdminDelay(address,uint32)            external;
+    function setTargetClosed(address,bool)                  external;
+    function hashOperation(address,address,bytes)           external returns (bytes32) envfree;
+    function getNonce(bytes32)                              external returns (uint32) envfree;
+    function getSchedule(bytes32)                           external returns (uint48);
+    function schedule(address,bytes,uint48)                 external returns (bytes32,uint32);
+    function execute(address,bytes)                         external returns (uint32);
+    function cancel(address,address,bytes)                  external returns (uint32);
+    function consumeScheduledOp(address,bytes)              external;
+    function updateAuthority(address,address)               external;
+}

contracts/access/AccessControl.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-// OpenZeppelin Contracts (last updated v5.0.0) (access/AccessControl.sol)
+// OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControl.sol)
 
 pragma solidity ^0.8.20;
 

contracts/access/IAccessControl.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-// OpenZeppelin Contracts (last updated v5.0.0) (access/IAccessControl.sol)
+// OpenZeppelin Contracts v4.4.1 (access/IAccessControl.sol)
 
 pragma solidity ^0.8.20;
 

contracts/access/Ownable.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-// OpenZeppelin Contracts (last updated v5.0.0) (access/Ownable.sol)
+// OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable.sol)
 
 pragma solidity ^0.8.20;
 

contracts/access/Ownable2Step.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-// OpenZeppelin Contracts (last updated v5.0.0) (access/Ownable2Step.sol)
+// OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable2Step.sol)
 
 pragma solidity ^0.8.20;
 

contracts/access/README.adoc

@@ -5,9 +5,7 @@ NOTE: This document is better viewed at https://docs.openzeppelin.com/contracts/
 
 This directory provides ways to restrict who can access the functions of a contract or when they can do it.
 
-- {AccessManager} is a full-fledged access control solution for smart contract systems. Allows creating and assigning multiple hierarchical roles with execution delays for each account across various contracts.
-- {AccessManaged} delegates its access control to an authority that dictates the permissions of the managed contract. It's compatible with an AccessManager as an authority.
-- {AccessControl} provides a per-contract role based access control mechanism. Multiple hierarchical roles can be created and assigned each to multiple accounts within the same instance.
+- {AccessControl} provides a general role based access control mechanism. Multiple hierarchical roles can be created and assigned each to multiple accounts.
 - {Ownable} is a simpler mechanism with a single owner "role" that can be assigned to a single account. This simpler mechanism can be useful for quick tests but projects with production concerns are likely to outgrow it.
 
 == Core
@@ -34,12 +32,8 @@ This directory provides ways to restrict who can access the functions of a contr
 
 {{IAuthority}}
 
-{{IAccessManager}}
-
 {{AccessManager}}
 
-{{IAccessManaged}}
-
 {{AccessManaged}}
 
-{{AuthorityUtils}}
+{{AccessManagerAdapter}}

contracts/access/extensions/AccessControlDefaultAdminRules.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-// OpenZeppelin Contracts (last updated v5.0.0) (access/extensions/AccessControlDefaultAdminRules.sol)
+// OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControlDefaultAdminRules.sol)
 
 pragma solidity ^0.8.20;