Release v4.9.0 (#4272)

Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Francisco <fg@frang.io>

.changeset/beige-buses-drop.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`Initializable`: optimize `_disableInitializers` by using `!=` instead of `<`. ([#3787](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3787))

.changeset/curvy-shrimps-enjoy.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ReentrancyGuard`: Add a `_reentrancyGuardEntered` function to expose the guard status. ([#3714](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3714))

.changeset/curvy-suns-sort.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`Ownable2Step`: make `acceptOwnership` public virtual to enable usecases that require overriding it. ([#3960](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3960))

.changeset/early-oranges-raise.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ERC721Wrapper`: add a new extension of the `ERC721` token which wraps an underlying token. Deposit and withdraw guarantee that the ownership of each token is backed by a corresponding underlying token with the same identifier.

.changeset/famous-rules-burn.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`EnumerableMap`: add a `keys()` function that returns an array containing all the keys. ([#3920](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3920))

.changeset/five-ducks-develop.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`UUPSUpgradeable.sol`: Change visibility to the functions `upgradeTo ` and `upgradeToAndCall ` from `external` to `public`.

.changeset/five-poets-mix.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`TimelockController`: Add the `CallSalt` event to emit on operation schedule.

.changeset/flat-deers-end.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`Governor`: add a public `cancel(uint256)` function.

.changeset/four-bats-sniff.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`Governor`: Enable timestamp operation for blockchains without a stable block time. This is achieved by connecting a Governor's internal clock to match a voting token's EIP-6372 interface.

.changeset/funny-rockets-compete.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-Reformatted codebase with latest version of Prettier Solidity. ([#3898](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3898))

.changeset/gold-chicken-clean.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`Strings`: add `equal` method. ([#3774](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3774))

.changeset/happy-socks-travel.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`IERC5313`: Add an interface for EIP-5313 that is now final.

.changeset/healthy-squids-stare.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`Math`: optimize `log256` rounding check. ([#3745](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3745))

.changeset/lemon-dogs-kiss.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`ERC20Votes`: optimize by using unchecked arithmetic. ([#3748](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3748))

.changeset/little-kiwis-ring.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`Multicall`: annotate `multicall` function as upgrade safe to not raise a flag for its delegatecall. ([#3961](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3961))

.changeset/lovely-dragons-appear.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`IERC4906`: Add an interface for ERC-4906 that is now Final.

.changeset/many-panthers-hide.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`TransparentUpgradeableProxy`: support value passthrough for all ifAdmin function.

.changeset/modern-games-exist.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`StorageSlot`: Add support for `string` and `bytes`.

.changeset/new-ways-own.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`ERC20Pausable`, `ERC721Pausable`, `ERC1155Pausable`: Add note regarding missing public pausing functionality

.changeset/ninety-hornets-kick.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`Votes`, `ERC20Votes`, `ERC721Votes`: support timestamp checkpointing using EIP-6372.

.changeset/perfect-insects-listen.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ERC4626`: Add mitigation to the inflation attack through virtual shares and assets.

.changeset/pretty-hornets-play.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`Strings`: add `toString` method for signed integers. ([#3773](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3773))

.changeset/proud-comics-deliver.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ERC20Wrapper`: Make the `underlying` variable private and add a public accessor.

.changeset/short-roses-judge.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`EIP712`: add EIP-5267 support for better domain discovery.

.changeset/silent-dancers-type.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`AccessControlDefaultAdminRules`: Add an extension of `AccessControl` with additional security rules for the `DEFAULT_ADMIN_ROLE`.

.changeset/slimy-knives-hug.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`SignatureChecker`: Add `isValidERC1271SignatureNow` for checking a signature directly against a smart contract using ERC-1271.

.changeset/small-cars-appear.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`ECDSA`: Add a function `toDataWithIntendedValidatorHash` that encodes data with version 0x00 following EIP-191.

.changeset/small-terms-sleep.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`SafeERC20`: Add a `forceApprove` function to improve compatibility with tokens behaving like USDT.

.changeset/strong-bulldogs-buy.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ERC1967Upgrade`: removed contract-wide `oz-upgrades-unsafe-allow delegatecall` annotation, replaced by granular annotation in `UUPSUpgradeable`.

.changeset/tame-ladybugs-sit.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`MerkleProof`: optimize by using unchecked arithmetic. ([#3745](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3745))

.changeset/thin-dragons-report.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ECDSA`: optimize bytes32 computation by using assembly instead of `abi.encodePacked`.

.changeset/thirty-swans-exercise.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ERC721URIStorage`: Emit ERC-4906 `MetadataUpdate` in `_setTokenURI`.

.changeset/violet-frogs-hide.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`ShortStrings`: Added a library for handling short strings in a gas efficient way, with fallback to storage for longer strings.

.changeset/warm-masks-obey.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`SignatureChecker`: Allow return data length greater than 32 from EIP-1271 signers.

.changeset/yellow-swans-cover.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': minor
----
-
-`UUPSUpgradeable`: added granular `oz-upgrades-unsafe-allow-reachable` annotation to improve upgrade safety checks on latest version of the Upgrades Plugins (starting with `@openzeppelin/upgrades-core@1.21.0`).

.github/workflows/checks.yml

@@ -14,7 +14,6 @@ concurrency:
 
 jobs:
   lint:
-    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -37,19 +36,36 @@ jobs:
       - name: Check linearisation of the inheritance graph
         run: npm run test:inheritance
       - name: Check proceduraly generated contracts are up-to-date
-        if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
         run: npm run test:generation
       - name: Compare gas costs
         uses: ./.github/actions/gas-compare
         with:
           token: ${{ github.token }}
+
+  tests-upgradeable:
+    runs-on: ubuntu-latest
+    env:
+      FORCE_COLOR: 1
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0 # Include history so patch conflicts are resolved automatically
+      - name: Set up environment
+        uses: ./.github/actions/setup
+      - name: Transpile to upgradeable
+        run: bash scripts/upgradeable/transpile.sh
+      - name: Run tests
+        run: npm run test
+        env:
+          NODE_OPTIONS: --max_old_space_size=4096
+      - name: Check linearisation of the inheritance graph
+        run: npm run test:inheritance
       - name: Check storage layout
         uses: ./.github/actions/storage-layout
         with:
           token: ${{ github.token }}
 
-  foundry-tests:
-    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
+  tests-foundry:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -63,7 +79,6 @@ jobs:
         run: forge test -vv
 
   coverage:
-    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -73,9 +88,10 @@ jobs:
         env:
           NODE_OPTIONS: --max_old_space_size=4096
       - uses: codecov/codecov-action@v3
+        with:
+          token: ${{ secrets.CODECOV_TOKEN }}
 
   slither:
-    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -83,9 +99,10 @@ jobs:
         uses: ./.github/actions/setup
       - run: rm foundry.toml
       - uses: crytic/slither-action@v0.3.0
+        with:
+          node-version: 18.15
 
   codespell:
-    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3

.github/workflows/formal-verification.yml

@@ -0,0 +1,68 @@
+name: formal verification
+
+on:
+  pull_request:
+    types:
+      - opened
+      - reopened
+      - synchronize
+      - labeled
+  workflow_dispatch: {}
+
+env:
+  PIP_VERSION: '3.10'
+  JAVA_VERSION: '11'
+  SOLC_VERSION: '0.8.19'
+
+concurrency: ${{ github.workflow }}-${{ github.ref }}
+
+jobs:
+  apply-diff:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Apply patches
+        run: make -C certora apply
+
+  verify:
+    runs-on: ubuntu-latest
+    if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification')
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - name: Set up environment
+        uses: ./.github/actions/setup
+      - name: identify specs that need to be run
+        id: arguments
+        run: |
+          if [[ ${{ github.event_name }} = 'pull_request' ]];
+          then
+            RESULT=$(git diff ${{ github.event.pull_request.head.sha }}..${{ github.event.pull_request.base.sha }} --name-only certora/specs/*.spec | while IFS= read -r file; do [[ -f $file ]] && basename "${file%.spec}"; done | tr "\n" " ")
+          else
+            RESULT='--all'
+          fi
+          echo "result=$RESULT" >> "$GITHUB_OUTPUT"
+      - name: Install python
+        uses: actions/setup-python@v4
+        with:
+          python-version: ${{ env.PIP_VERSION }}
+          cache: 'pip'
+      - name: Install python packages
+        run: pip install -r requirements.txt
+      - name: Install java
+        uses: actions/setup-java@v3
+        with:
+          distribution: temurin
+          java-version: ${{ env.JAVA_VERSION }}
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v${{ env.SOLC_VERSION }}/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+          chmod +x /usr/local/bin/solc
+      - name: Verify specification
+        run: |
+          make -C certora apply
+          node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.github/workflows/upgradeable.yml

@@ -1,4 +1,4 @@
-name: Upgradeable Trigger
+name: transpile upgradeable
 
 on:
   push:
@@ -7,17 +7,24 @@ on:
       - release-v*
 
 jobs:
-  trigger:
+  transpile:
+    environment: push-upgradeable
     runs-on: ubuntu-latest
     steps:
-      - id: app
-        uses: getsentry/action-github-app-token@v2
+      - uses: actions/checkout@v3
         with:
-          app_id: ${{ secrets.UPGRADEABLE_APP_ID }}
-          private_key: ${{ secrets.UPGRADEABLE_APP_PK }}
-      - run: |
-          curl -X POST \
-            https://api.github.com/repos/OpenZeppelin/openzeppelin-contracts-upgradeable/dispatches \
-            -H 'Accept: application/vnd.github.v3+json' \
-            -H 'Authorization: token ${{ steps.app.outputs.token }}' \
-            -d '{ "event_type": "Update", "client_payload": { "ref": "${{ github.ref }}" } }'
+          repository: OpenZeppelin/openzeppelin-contracts-upgradeable
+          fetch-depth: 0
+          token: ${{ secrets.GH_TOKEN_UPGRADEABLE }}
+      - name: Fetch current non-upgradeable branch
+        run: |
+          git fetch "https://github.com/${{ github.repository }}.git" "$REF"
+          git checkout FETCH_HEAD
+        env:
+          REF: ${{ github.ref }}
+      - name: Set up environment
+        uses: ./.github/actions/setup
+      - run: bash scripts/git-user-config.sh
+      - name: Transpile to upgradeable
+        run: bash scripts/upgradeable/transpile-onto.sh ${{ github.ref_name }} origin/${{ github.ref_name }}
+      - run: git push origin ${{ github.ref_name }}

.gitignore

@@ -68,3 +68,4 @@ contracts-exposed
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt

.gitmodules

@@ -1,4 +1,5 @@
 [submodule "lib/forge-std"]
+	branch = v1
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
 [submodule "lib/erc4626-tests"]

CHANGELOG.md

@@ -1,5 +1,44 @@
 # Changelog
 
+
+## 4.9.0 (2023-05-23)
+
+- `ReentrancyGuard`: Add a `_reentrancyGuardEntered` function to expose the guard status. ([#3714](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3714))
+- `ERC721Wrapper`: add a new extension of the `ERC721` token which wraps an underlying token. Deposit and withdraw guarantee that the ownership of each token is backed by a corresponding underlying token with the same identifier. ([#3863](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3863))
+- `EnumerableMap`: add a `keys()` function that returns an array containing all the keys. ([#3920](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3920))
+- `Governor`: add a public `cancel(uint256)` function. ([#3983](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3983))
+- `Governor`: Enable timestamp operation for blockchains without a stable block time. This is achieved by connecting a Governor's internal clock to match a voting token's EIP-6372 interface. ([#3934](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3934))
+- `Strings`: add `equal` method. ([#3774](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3774))
+- `IERC5313`: Add an interface for EIP-5313 that is now final. ([#4013](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4013))
+- `IERC4906`: Add an interface for ERC-4906 that is now Final. ([#4012](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4012))
+- `StorageSlot`: Add support for `string` and `bytes`. ([#4008](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4008))
+- `Votes`, `ERC20Votes`, `ERC721Votes`: support timestamp checkpointing using EIP-6372. ([#3934](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3934))
+- `ERC4626`: Add mitigation to the inflation attack through virtual shares and assets. ([#3979](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3979))
+- `Strings`: add `toString` method for signed integers. ([#3773](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3773))
+- `ERC20Wrapper`: Make the `underlying` variable private and add a public accessor. ([#4029](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4029))
+- `EIP712`: add EIP-5267 support for better domain discovery. ([#3969](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3969))
+- `AccessControlDefaultAdminRules`: Add an extension of `AccessControl` with additional security rules for the `DEFAULT_ADMIN_ROLE`. ([#4009](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4009))
+- `SignatureChecker`: Add `isValidERC1271SignatureNow` for checking a signature directly against a smart contract using ERC-1271. ([#3932](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3932))
+- `SafeERC20`: Add a `forceApprove` function to improve compatibility with tokens behaving like USDT. ([#4067](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4067))
+- `ERC1967Upgrade`: removed contract-wide `oz-upgrades-unsafe-allow delegatecall` annotation, replaced by granular annotation in `UUPSUpgradeable`. ([#3971](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3971))
+- `ERC20Wrapper`: self wrapping and deposit by the wrapper itself are now explicitly forbidden. ([#4100](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4100))
+- `ECDSA`: optimize bytes32 computation by using assembly instead of `abi.encodePacked`. ([#3853](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3853))
+- `ERC721URIStorage`: Emit ERC-4906 `MetadataUpdate` in `_setTokenURI`. ([#4012](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4012))
+- `ShortStrings`: Added a library for handling short strings in a gas efficient way, with fallback to storage for longer strings. ([#4023](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4023))
+- `SignatureChecker`: Allow return data length greater than 32 from EIP-1271 signers. ([#4038](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4038))
+- `UUPSUpgradeable`: added granular `oz-upgrades-unsafe-allow-reachable` annotation to improve upgrade safety checks on latest version of the Upgrades Plugins (starting with `@openzeppelin/upgrades-core@1.21.0`). ([#3971](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3971))
+- `Initializable`: optimize `_disableInitializers` by using `!=` instead of `<`. ([#3787](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3787))
+- `Ownable2Step`: make `acceptOwnership` public virtual to enable usecases that require overriding it. ([#3960](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3960))
+- `UUPSUpgradeable.sol`: Change visibility to the functions `upgradeTo ` and `upgradeToAndCall ` from `external` to `public`. ([#3959](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3959))
+- `TimelockController`: Add the `CallSalt` event to emit on operation schedule. ([#4001](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4001))
+- Reformatted codebase with latest version of Prettier Solidity. ([#3898](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3898))
+- `Math`: optimize `log256` rounding check. ([#3745](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3745))
+- `ERC20Votes`: optimize by using unchecked arithmetic. ([#3748](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3748))
+- `Multicall`: annotate `multicall` function as upgrade safe to not raise a flag for its delegatecall. ([#3961](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3961))
+- `ERC20Pausable`, `ERC721Pausable`, `ERC1155Pausable`: Add note regarding missing public pausing functionality ([#4007](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4007))
+- `ECDSA`: Add a function `toDataWithIntendedValidatorHash` that encodes data with version 0x00 following EIP-191. ([#4063](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4063))
+- `MerkleProof`: optimize by using unchecked arithmetic. ([#3745](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3745))
+
 ### Breaking changes
 
 - `EIP712`: Addition of ERC5267 support requires support for user defined value types, which was released in Solidity version 0.8.8. This requires a pragma change from `^0.8.0` to `^0.8.8`.
@@ -12,6 +51,19 @@
 - `ERC777`: The `ERC777` token standard is no longer supported by OpenZeppelin. Our implementation is now deprecated and will be removed in the next major release. The corresponding standard interfaces remain available. ([#4066](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4066))
 - `ERC1820Implementer`: The `ERC1820` pseudo-introspection mechanism is no longer supported by OpenZeppelin. Our implementation is now deprecated and will be removed in the next major release. The corresponding standard interfaces remain available. ([#4066](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4066))
 
+## 4.8.3 (2023-04-13)
+
+- `GovernorCompatibilityBravo`: Fix encoding of proposal data when signatures are missing.
+- `TransparentUpgradeableProxy`: Fix transparency in case of selector clash with non-decodable calldata or payable mutability. ([#4154](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4154))
+
+## 4.8.2 (2023-03-02)
+
+- `ERC721Consecutive`: Fixed a bug when `_mintConsecutive` is used for batches of size 1 that could lead to balance overflow. Refer to the breaking changes section in the changelog for a note on the behavior of `ERC721._beforeTokenTransfer`.
+
+### Breaking changes
+
+- `ERC721`: The internal function `_beforeTokenTransfer` no longer updates balances, which it previously did when `batchSize` was greater than 1. This change has no consequence unless a custom ERC721 extension is explicitly invoking `_beforeTokenTransfer`. Balance updates in extensions must now be done explicitly using `__unsafe_increaseBalance`, with a name that indicates that there is an invariant that has to be manually verified.
+
 ## 4.8.1 (2023-01-12)
 
 - `ERC4626`: Use staticcall instead of call when fetching underlying ERC-20 decimals. ([#3943](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3943))

README.md

@@ -73,7 +73,7 @@ The engineering guidelines we follow to promote project quality can be found in
 
 Past audits can be found in [`audits/`](./audits).
 
-Smart contracts are a nascent techology and carry a high level of technical risk and uncertainty. Although OpenZeppelin is well known for its security audits, using OpenZeppelin Contracts is not a substitute for a security audit.
+Smart contracts are a nascent technology and carry a high level of technical risk and uncertainty. Although OpenZeppelin is well known for its security audits, using OpenZeppelin Contracts is not a substitute for a security audit.
 
 OpenZeppelin Contracts is made available under the MIT License, which disclaims all warranties in relation to the project and which limits the liability of those that contribute and maintain the project, including OpenZeppelin. As set out further in the Terms, you acknowledge that you are solely responsible for any use of OpenZeppelin Contracts and you assume all risks associated with any such use.
 

audits/README.md

@@ -2,6 +2,7 @@
 
 | Date         | Version | Commit    | Auditor      | Scope                | Links                                                       |
 | ------------ | ------- | --------- | ------------ | -------------------- | ----------------------------------------------------------- |
+| 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)                                         |
 | March 2017   | v1.0.4  | `9c5975a` | New Alchemy  | Everything           | [🔗](./2017-03.md)                                          |

certora/.gitignore

@@ -0,0 +1 @@
+patched

certora/Makefile

@@ -1,24 +1,54 @@
 default: help
 
-PATCH         = applyHarness.patch
-CONTRACTS_DIR = ../contracts
-MUNGED_DIR    = munged
+SRC   := ../contracts
+DST   := patched
+DIFF  := diff
+SRCS  := $(shell find $(SRC) -type f)
+DSTS  := $(shell find $(DST) -type f)
+DIFFS := $(shell find $(DIFF) -type f)
 
+###############################################################################
+# Apply all patches in the $DIFF folder to the $DST folder
+apply: $(DST) $(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$(DIFFS)))
+
+# Reset the $DST folder
+$(DST): FORCE
+	@rm -rf $@
+	@cp -r $(SRC) $@
+
+# Update a solidity file in the $DST directory using the corresponding patch
+$(DST)/%.sol: FORCE
+	@echo Applying patch to $@
+	@patch -p0 -d $(DST) < $(patsubst $(DST)_%,$(DIFF)/%.patch,$(subst /,_,$@))
+
+###############################################################################
+# Record all difference between $SRC and $DST in patches
+record: $(DIFF) $(patsubst %,$(DIFF)/%.patch,$(subst /,_,$(subst $(SRC)/,,$(SRCS)) $(subst $(DST)/,,$(DSTS))))
+
+# Create the $DIFF folder
+$(DIFF): FORCE
+	@rm -rf $@
+	@mkdir $@
+
+# Create the patch file by comparing the source and the destination
+$(DIFF)/%.patch: FORCE
+	@echo Generating patch $@
+	@diff -ruN \
+		$(patsubst $(DIFF)/%.patch,$(SRC)/%,$(subst _,/,$@)) \
+		$(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$@)) \
+		| sed 's+$(SRC)/++g' \
+		| sed 's+$(DST)/++g' \
+		> $@
+	@[ -s $@ ] || rm $@
+
+###############################################################################
 help:
 	@echo "usage:"
+	@echo "  make apply:  create $(DST) directory by applying the patches to $(SRC)"
+	@echo "  make record: record the patches capturing the differences between $(SRC) and $(DST)"
 	@echo "  make clean:  remove all generated files (those ignored by git)"
-	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
-	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
-
-munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
-	rm -rf $@
-	cp -r $(CONTRACTS_DIR) $@
-	patch -p0 -d $@ < $(PATCH)
-
-record:
-	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
 
 clean:
 	git clean -fdX
-	touch $(PATCH)
 
+FORCE: ;

certora/README.md

@@ -1,56 +1,60 @@
 # Running the certora verification tool
 
-These instructions detail the process for running CVT on the OpenZeppelin (Wizard/Governor) contracts.
+These instructions detail the process for running Certora Verification Tool on OpenZeppelin Contracts.
 
-Documentation for CVT and the specification language are available
-[here](https://certora.atlassian.net/wiki/spaces/CPD/overview)
+Documentation for CVT and the specification language are available [here](https://certora.atlassian.net/wiki/spaces/CPD/overview).
+
+## Prerequisites
+
+Follow the [Certora installation guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) in order to get the Certora Prover Package and the `solc` executable folder in your path.
+
+> **Note**
+> An API Key is required for local testing. Although the prover will run on a Github Actions' CI environment on selected Pull Requests.
 
 ## Running the verification
 
-The scripts in the `certora/scripts` directory are used to submit verification
-jobs to the Certora verification service. After the job is complete, the results will be available on
-[the Certora portal](https://vaas-stg.certora.com/).
+The Certora Verification Tool proves specs for contracts, which are defined by the `./specs.json` file along with their pre-configured options.
 
-These scripts should be run from the root directory; for example by running
+The verification script `./run.js` is used to submit verification jobs to the Certora Verification service.
 
-```
-sh certora/scripts/verifyAll.sh <meaningful comment>
+You can run it from the root of the repository with the following command:
+
+```bash
+node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...]
 ```
 
-The most important of these is `verifyAll.sh`, which checks
-all of the harnessed contracts (`certora/harness/Wizard*.sol`) against all of
-the specifications (`certora/spec/*.spec`).
+Where:
 
-The other scripts run a subset of the specifications or the contracts.  You can
-verify different contracts or specifications by changing the `--verify` option,
-and you can run a single rule or method with the `--rule` or `--method` option.
+- `CONTRACT_NAME` matches the `contract` key in the `./spec.json` file and may be empty. It will run all matching contracts if not provided.
+- `SPEC_NAME` refers to a `spec` key from the `./specs.json` file. It will run every spec if not provided.
+- `OPTIONS` extend the [Certora Prover CLI options](https://docs.certora.com/en/latest/docs/prover/cli/options.html#certora-prover-cli-options) and will respect the preconfigured options in the `specs.json` file.
 
-For example, to verify the `WizardFirstPriority` contract against the
-`GovernorCountingSimple` specification, you could change the `--verify` line of
-the `WizardControlFirstPriortity.sh` script to:
+> **Note**
+> A single spec may be configured to run for multiple contracts, whereas a single contract may run multiple specs.
 
-```
---verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \
+Example usage:
+
+```bash
+node certora/run.js AccessControl # Run the AccessControl spec against every contract implementing it
 ```
 
 ## Adapting to changes in the contracts
 
-Some of our rules require the code to be simplified in various ways. Our
-primary tool for performing these simplifications is to run verification on a
-contract that extends the original contracts and overrides some of the methods.
-These "harness" contracts can be found in the `certora/harness` directory.
+Some of our rules require the code to be simplified in various ways. Our primary tool for performing these simplifications is to run verification on a contract that extends the original contracts and overrides some of the methods. These "harness" contracts can be found in the `certora/harness` directory.
 
-This pattern does require some modifications to the original code: some methods
-need to be made virtual or public, for example. These changes are handled by
-applying a patch to the code before verification.
+This pattern does require some modifications to the original code: some methods need to be made virtual or public, for example. These changes are handled by applying a patch
+to the code before verification by running:
 
-When one of the `verify` scripts is executed, it first applies the patch file
-`certora/applyHarness.patch` to the `contracts` directory, placing the output
-in the `certora/munged` directory. We then verify the contracts in the
-`certora/munged` directory.
+```bash
+make -C certora apply
+```
 
-If the original contracts change, it is possible to create a conflict with the
-patch. In this case, the verify scripts will report an error message and output
-rejected changes in the `munged` directory. After merging the changes, run
-`make record` in the `certora` directory; this will regenerate the patch file,
-which can then be checked into git.
+Before running the `certora/run.js` script, it's required to apply the corresponding patches to the `contracts` directory, placing the output in the `certora/patched` directory. Then, the contracts are verified by running the verification for the `certora/patched` directory.
+
+If the original contracts change, it is possible to create a conflict with the patch. In this case, the verify scripts will report an error message and output rejected changes in the `patched` directory. After merging the changes, run `make record` in the `certora` directory; this will regenerate the patch file, which can then be checked into git.
+
+For more information about the `make` scripts available, run:
+
+```bash
+make -C certora help
+```

certora/applyHarness.patch

@@ -1,101 +0,0 @@
-diff -ruN .gitignore .gitignore
---- .gitignore	1969-12-31 19:00:00.000000000 -0500
-+++ .gitignore	2021-12-09 14:46:33.923637220 -0500
-@@ -0,0 +1,2 @@
-+*
-+!.gitignore
-diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol
---- governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-09 14:46:33.923637220 -0500
-@@ -245,7 +245,7 @@
-     /**
-      * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
-      */
--    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
-         ProposalDetails storage details = _proposalDetails[proposalId];
-         return quorum(proposalSnapshot(proposalId)) <= details.forVotes;
-     }
-@@ -253,7 +253,7 @@
-     /**
-      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
-      */
--    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
-         ProposalDetails storage details = _proposalDetails[proposalId];
-         return details.forVotes > details.againstVotes;
-     }
-diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
---- governance/extensions/GovernorCountingSimple.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/extensions/GovernorCountingSimple.sol	2021-12-09 14:46:33.923637220 -0500
-@@ -64,7 +64,7 @@
-     /**
-      * @dev See {Governor-_quorumReached}.
-      */
--    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
-         ProposalVote storage proposalvote = _proposalVotes[proposalId];
- 
-         return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
-@@ -73,7 +73,7 @@
-     /**
-      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
-      */
--    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
-+    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
-         ProposalVote storage proposalvote = _proposalVotes[proposalId];
- 
-         return proposalvote.forVotes > proposalvote.againstVotes;
-diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol
---- governance/extensions/GovernorTimelockControl.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/extensions/GovernorTimelockControl.sol	2021-12-09 14:46:33.923637220 -0500
-@@ -111,7 +111,7 @@
-         bytes[] memory calldatas,
-         bytes32 descriptionHash
-     ) internal virtual override {
--        _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
-+         _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
-     }
- 
-     /**
-diff -ruN governance/Governor.sol governance/Governor.sol
---- governance/Governor.sol	2021-12-03 15:24:56.523654357 -0500
-+++ governance/Governor.sol	2021-12-09 14:46:56.411503587 -0500
-@@ -38,8 +38,8 @@
- 
-     string private _name;
- 
--    mapping(uint256 => ProposalCore) private _proposals;
--
-+    mapping(uint256 => ProposalCore) public _proposals;
-+ 
-     /**
-      * @dev Restrict access to governor executing address. Some module might override the _executor function to make
-      * sure this modifier is consistent with the execution model.
-@@ -167,12 +167,12 @@
-     /**
-      * @dev Amount of votes already cast passes the threshold limit.
-      */
--    function _quorumReached(uint256 proposalId) internal view virtual returns (bool);
-+    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
- 
-     /**
-      * @dev Is the proposal successful or not.
-      */
--    function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
-+    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
- 
-     /**
-      * @dev Register a vote with a given support and voting weight.
-diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
---- token/ERC20/extensions/ERC20Votes.sol	2021-12-03 15:24:56.527654330 -0500
-+++ token/ERC20/extensions/ERC20Votes.sol	2021-12-09 14:46:33.927637196 -0500
-@@ -84,7 +84,7 @@
-      *
-      * - `blockNumber` must have been already mined
-      */
--    function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) {
-+    function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) {
-         require(blockNumber < block.number, "ERC20Votes: block not yet mined");
-         return _checkpointsLookup(_checkpoints[account], blockNumber);
-     }

certora/diff/token_ERC721_ERC721.sol.patch

@@ -0,0 +1,14 @@
+--- token/ERC721/ERC721.sol	2023-03-07 10:48:47.736822221 +0100
++++ token/ERC721/ERC721.sol	2023-03-09 19:49:39.669338673 +0100
+@@ -199,6 +199,11 @@
+         return _owners[tokenId];
+     }
+ 
++    // FV
++    function _getApproved(uint256 tokenId) internal view returns (address) {
++        return _tokenApprovals[tokenId];
++    }
++
+     /**
+      * @dev Returns whether `tokenId` exists.
+      *

certora/harnesses/AccessControlDefaultAdminRulesHarness.sol

@@ -0,0 +1,47 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/AccessControlDefaultAdminRules.sol";
+
+contract AccessControlDefaultAdminRulesHarness is AccessControlDefaultAdminRules {
+    uint48 private _delayIncreaseWait;
+
+    constructor(
+        uint48 initialDelay,
+        address initialDefaultAdmin,
+        uint48 delayIncreaseWait
+    ) AccessControlDefaultAdminRules(initialDelay, initialDefaultAdmin) {
+        _delayIncreaseWait = delayIncreaseWait;
+    }
+
+    // FV
+    function pendingDefaultAdmin_() external view returns (address) {
+        (address newAdmin, ) = pendingDefaultAdmin();
+        return newAdmin;
+    }
+
+    function pendingDefaultAdminSchedule_() external view returns (uint48) {
+        (, uint48 schedule) = pendingDefaultAdmin();
+        return schedule;
+    }
+
+    function pendingDelay_() external view returns (uint48) {
+        (uint48 newDelay, ) = pendingDefaultAdminDelay();
+        return newDelay;
+    }
+
+    function pendingDelaySchedule_() external view returns (uint48) {
+        (, uint48 schedule) = pendingDefaultAdminDelay();
+        return schedule;
+    }
+
+    function delayChangeWait_(uint48 newDelay) external view returns (uint48) {
+        return _delayChangeWait(newDelay);
+    }
+
+    // Overrides
+    function defaultAdminDelayIncreaseWait() public view override returns (uint48) {
+        return _delayIncreaseWait;
+    }
+}

certora/harnesses/AccessControlHarness.sol

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/AccessControl.sol";
+
+contract AccessControlHarness is AccessControl {}

certora/harnesses/DoubleEndedQueueHarness.sol

@@ -0,0 +1,59 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/utils/structs/DoubleEndedQueue.sol";
+
+contract DoubleEndedQueueHarness {
+    using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque;
+
+    DoubleEndedQueue.Bytes32Deque private _deque;
+
+    function pushFront(bytes32 value) external {
+        _deque.pushFront(value);
+    }
+
+    function pushBack(bytes32 value) external {
+        _deque.pushBack(value);
+    }
+
+    function popFront() external returns (bytes32 value) {
+        return _deque.popFront();
+    }
+
+    function popBack() external returns (bytes32 value) {
+        return _deque.popBack();
+    }
+
+    function clear() external {
+        _deque.clear();
+    }
+
+    function begin() external view returns (int128) {
+        return _deque._begin;
+    }
+
+    function end() external view returns (int128) {
+        return _deque._end;
+    }
+
+    function length() external view returns (uint256) {
+        return _deque.length();
+    }
+
+    function empty() external view returns (bool) {
+        return _deque.empty();
+    }
+
+    function front() external view returns (bytes32 value) {
+        return _deque.front();
+    }
+
+    function back() external view returns (bytes32 value) {
+        return _deque.back();
+    }
+
+    function at_(uint256 index) external view returns (bytes32 value) {
+        return _deque.at(index);
+    }
+}

certora/harnesses/ERC20FlashMintHarness.sol

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/ERC20.sol";
+import "../patched/token/ERC20/extensions/ERC20Permit.sol";
+import "../patched/token/ERC20/extensions/ERC20FlashMint.sol";
+
+contract ERC20FlashMintHarness is ERC20, ERC20Permit, ERC20FlashMint {
+    uint256 someFee;
+    address someFeeReceiver;
+
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
+
+    function mint(address account, uint256 amount) external {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) external {
+        _burn(account, amount);
+    }
+
+    // public accessor
+    function flashFeeReceiver() public view returns (address) {
+        return someFeeReceiver;
+    }
+
+    // internal hook
+    function _flashFee(address, uint256) internal view override returns (uint256) {
+        return someFee;
+    }
+
+    function _flashFeeReceiver() internal view override returns (address) {
+        return someFeeReceiver;
+    }
+}

certora/harnesses/ERC20PermitHarness.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/extensions/ERC20Permit.sol";
+
+contract ERC20PermitHarness is ERC20Permit {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
+
+    function mint(address account, uint256 amount) external {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) external {
+        _burn(account, amount);
+    }
+}

certora/harnesses/ERC20VotesHarness.sol

@@ -1,28 +0,0 @@
-import "../munged/token/ERC20/extensions/ERC20Votes.sol";
-
-contract ERC20VotesHarness is ERC20Votes {
-    constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
-
-    mapping(address => mapping(uint256 => uint256)) public _getPastVotes;
-
-    function _afterTokenTransfer(
-        address from,
-        address to,
-        uint256 amount
-    ) internal virtual override {
-        super._afterTokenTransfer(from, to, amount);
-        _getPastVotes[from][block.number] -= amount;
-        _getPastVotes[to][block.number] += amount;
-    }
-
-    /**
-     * @dev Change delegation for `delegator` to `delegatee`.
-     *
-     * Emits events {DelegateChanged} and {DelegateVotesChanged}.
-     */
-    function _delegate(address delegator, address delegatee) internal virtual override{
-        super._delegate(delegator, delegatee);
-        _getPastVotes[delegator][block.number] -= balanceOf(delegator);
-        _getPastVotes[delegatee][block.number] += balanceOf(delegator);
-    }
-}

certora/harnesses/ERC20WrapperHarness.sol

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
+
+contract ERC20WrapperHarness is ERC20Wrapper {
+    constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {}
+
+    function underlyingTotalSupply() public view returns (uint256) {
+        return underlying().totalSupply();
+    }
+
+    function underlyingBalanceOf(address account) public view returns (uint256) {
+        return underlying().balanceOf(account);
+    }
+
+    function underlyingAllowanceToThis(address account) public view returns (uint256) {
+        return underlying().allowance(account, address(this));
+    }
+
+    function recover(address account) public returns (uint256) {
+        return _recover(account);
+    }
+}

certora/harnesses/ERC3156FlashBorrowerHarness.sol

@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: MIT
+
+import "../patched/interfaces/IERC3156FlashBorrower.sol";
+
+pragma solidity ^0.8.0;
+
+contract ERC3156FlashBorrowerHarness is IERC3156FlashBorrower {
+    bytes32 somethingToReturn;
+
+    function onFlashLoan(address, address, uint256, uint256, bytes calldata) external view override returns (bytes32) {
+        return somethingToReturn;
+    }
+}

certora/harnesses/ERC721Harness.sol

@@ -0,0 +1,37 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC721/ERC721.sol";
+
+contract ERC721Harness is ERC721 {
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
+
+    function mint(address account, uint256 tokenId) external {
+        _mint(account, tokenId);
+    }
+
+    function safeMint(address to, uint256 tokenId) external {
+        _safeMint(to, tokenId);
+    }
+
+    function safeMint(address to, uint256 tokenId, bytes memory data) external {
+        _safeMint(to, tokenId, data);
+    }
+
+    function burn(uint256 tokenId) external {
+        _burn(tokenId);
+    }
+
+    function tokenExists(uint256 tokenId) external view returns (bool) {
+        return _exists(tokenId);
+    }
+
+    function unsafeOwnerOf(uint256 tokenId) external view returns (address) {
+        return _ownerOf(tokenId);
+    }
+
+    function unsafeGetApproved(uint256 tokenId) external view returns (address) {
+        return _getApproved(tokenId);
+    }
+}

certora/harnesses/ERC721ReceiverHarness.sol

@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/interfaces/IERC721Receiver.sol";
+
+contract ERC721ReceiverHarness is IERC721Receiver {
+    function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
+        return this.onERC721Received.selector;
+    }
+}

certora/harnesses/EnumerableMapHarness.sol

@@ -0,0 +1,55 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/utils/structs/EnumerableMap.sol";
+
+contract EnumerableMapHarness {
+    using EnumerableMap for EnumerableMap.Bytes32ToBytes32Map;
+
+    EnumerableMap.Bytes32ToBytes32Map private _map;
+
+    function set(bytes32 key, bytes32 value) public returns (bool) {
+        return _map.set(key, value);
+    }
+
+    function remove(bytes32 key) public returns (bool) {
+        return _map.remove(key);
+    }
+
+    function contains(bytes32 key) public view returns (bool) {
+        return _map.contains(key);
+    }
+
+    function length() public view returns (uint256) {
+        return _map.length();
+    }
+
+    function key_at(uint256 index) public view returns (bytes32) {
+        (bytes32 key,) = _map.at(index);
+        return key;
+    }
+
+    function value_at(uint256 index) public view returns (bytes32) {
+        (,bytes32 value) = _map.at(index);
+        return value;
+    }
+
+    function tryGet_contains(bytes32 key) public view returns (bool) {
+        (bool contained,) = _map.tryGet(key);
+        return contained;
+    }
+
+    function tryGet_value(bytes32 key) public view returns (bytes32) {
+        (,bytes32 value) = _map.tryGet(key);
+        return value;
+    }
+
+    function get(bytes32 key) public view returns (bytes32) {
+        return _map.get(key);
+    }
+
+    function _indexOf(bytes32 key) public view returns (uint256) {
+        return _map._keys._inner._indexes[key];
+    }
+}

certora/harnesses/EnumerableSetHarness.sol

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/utils/structs/EnumerableSet.sol";
+
+contract EnumerableSetHarness {
+    using EnumerableSet for EnumerableSet.Bytes32Set;
+
+    EnumerableSet.Bytes32Set private _set;
+
+    function add(bytes32 value) public returns (bool) {
+        return _set.add(value);
+    }
+
+    function remove(bytes32 value) public returns (bool) {
+        return _set.remove(value);
+    }
+
+    function contains(bytes32 value) public view returns (bool) {
+        return _set.contains(value);
+    }
+
+    function length() public view returns (uint256) {
+        return _set.length();
+    }
+
+    function at_(uint256 index) public view returns (bytes32) {
+        return _set.at(index);
+    }
+
+    function _indexOf(bytes32 value) public view returns (uint256) {
+        return _set._inner._indexes[value];
+    }
+}

certora/harnesses/InitializableHarness.sol

@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../patched/proxy/utils/Initializable.sol";
+
+contract InitializableHarness is Initializable {
+    function initialize()          public initializer      {}
+    function reinitialize(uint8 n) public reinitializer(n) {}
+    function disable()             public { _disableInitializers(); }
+
+    function nested_init_init()                     public initializer      { initialize();    }
+    function nested_init_reinit(uint8 m)            public initializer      { reinitialize(m); }
+    function nested_reinit_init(uint8 n)            public reinitializer(n) { initialize();    }
+    function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); }
+
+    function version() public view returns (uint8) {
+        return _getInitializedVersion();
+    }
+
+    function initializing() public view returns (bool) {
+        return _isInitializing();
+    }
+}

certora/harnesses/Ownable2StepHarness.sol

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/Ownable2Step.sol";
+
+contract Ownable2StepHarness is Ownable2Step {
+  function restricted() external onlyOwner {}
+}

certora/harnesses/OwnableHarness.sol

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/Ownable.sol";
+
+contract OwnableHarness is Ownable {
+  function restricted() external onlyOwner {}
+}

certora/harnesses/PausableHarness.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/security/Pausable.sol";
+
+contract PausableHarness is Pausable {
+    function pause() external {
+        _pause();
+    }
+
+    function unpause() external {
+        _unpause();
+    }
+
+    function onlyWhenPaused() external whenPaused {}
+
+    function onlyWhenNotPaused() external whenNotPaused {}
+}

certora/harnesses/TimelockControllerHarness.sol

@@ -0,0 +1,12 @@
+pragma solidity ^0.8.0;
+
+import "../patched/governance/TimelockController.sol";
+
+contract TimelockControllerHarness is TimelockController {
+    constructor(
+        uint256 minDelay,
+        address[] memory proposers,
+        address[] memory executors,
+        address admin
+    ) TimelockController(minDelay, proposers, executors, admin) {}
+}

certora/harnesses/WizardControlFirstPriority.sol

@@ -1,150 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.2;
-
-import "../munged/governance/Governor.sol";
-import "../munged/governance/extensions/GovernorCountingSimple.sol";
-import "../munged/governance/extensions/GovernorVotes.sol";
-import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
-import "../munged/governance/extensions/GovernorTimelockControl.sol";
-import "../munged/governance/extensions/GovernorProposalThreshold.sol";
-
-/* 
-Wizard options:
-ProposalThreshhold = 10
-ERC20Votes
-TimelockController
-*/
-
-contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
-    constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction)
-        Governor(name)
-        GovernorVotes(_token)
-        GovernorVotesQuorumFraction(quorumFraction)
-        GovernorTimelockControl(_timelock)
-    {}
-
-    //HARNESS
-
-    function isExecuted(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].executed;
-    }
-    
-    function isCanceled(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].canceled;
-    }
-
-    uint256 _votingDelay;
-
-    uint256 _votingPeriod;
-
-    uint256 _proposalThreshold;
-
-    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
-
-    function _castVote(
-        uint256 proposalId,
-        address account,
-        uint8 support,
-        string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
-        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
-
-        return deltaWeight;        
-    }
-    
-    function snapshot(uint256 proposalId) public view returns (uint64) {
-        return _proposals[proposalId].voteStart._deadline;
-    }
-
-
-    function getExecutor() public view returns (address){
-        return _executor();
-    }
-
-    // original code, harnessed
-
-    function votingDelay() public view override returns (uint256) {     // HARNESS: pure -> view
-        return _votingDelay;                                            // HARNESS: parametric
-    }
-
-    function votingPeriod() public view override returns (uint256) {    // HARNESS: pure -> view
-        return _votingPeriod;                                           // HARNESS: parametric
-    }
-
-    function proposalThreshold() public view override returns (uint256) {   // HARNESS: pure -> view
-        return _proposalThreshold;                                          // HARNESS: parametric
-    }
-
-    // original code, not harnessed
-    // The following functions are overrides required by Solidity.
-
-    function quorum(uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotesQuorumFraction)
-        returns (uint256)
-    {
-        return super.quorum(blockNumber);
-    }
-
-    function getVotes(address account, uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotes)
-        returns (uint256)
-    {
-        return super.getVotes(account, blockNumber);
-    }
-
-    function state(uint256 proposalId)
-        public
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (ProposalState)
-    {
-        return super.state(proposalId);
-    }
-
-    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
-        public
-        override(Governor, GovernorProposalThreshold, IGovernor)
-        returns (uint256)
-    {
-        return super.propose(targets, values, calldatas, description);
-    }
-
-    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockControl)
-    {
-        super._execute(proposalId, targets, values, calldatas, descriptionHash);
-    }
-
-    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockControl)
-        returns (uint256)
-    {
-        return super._cancel(targets, values, calldatas, descriptionHash);
-    }
-
-    function _executor()
-        internal
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (address)
-    {
-        return super._executor();
-    }
-
-    function supportsInterface(bytes4 interfaceId)
-        public
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (bool)
-    {
-        return super.supportsInterface(interfaceId);
-    }
-}

certora/harnesses/WizardFirstTry.sol

@@ -1,141 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.2;
-
-import "../munged/governance/Governor.sol";
-import "../munged/governance/extensions/GovernorCountingSimple.sol";
-import "../munged/governance/extensions/GovernorVotes.sol";
-import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
-import "../munged/governance/extensions/GovernorTimelockCompound.sol";
-
-/* 
-Wizard options:
-ERC20Votes
-TimelockCompound
-*/
-
-contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
-    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
-        Governor(name)
-        GovernorVotes(_token)
-        GovernorVotesQuorumFraction(quorumFraction)
-        GovernorTimelockCompound(_timelock)
-    {}
-
-    //HARNESS
-
-    function isExecuted(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].executed;
-    }
-    
-    function isCanceled(uint256 proposalId) public view returns (bool) {
-        return _proposals[proposalId].canceled;
-    }
-
-    function snapshot(uint256 proposalId) public view returns (uint64) {
-        return _proposals[proposalId].voteStart._deadline;
-    }
-
-    function getExecutor() public view returns (address){
-        return _executor();
-    }
-
-    uint256 _votingDelay;
-
-    uint256 _votingPeriod;
-
-    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
-
-    function _castVote(
-        uint256 proposalId,
-        address account,
-        uint8 support,
-        string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
-        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
-
-        return deltaWeight;        
-    }
-
-    // original code, harnessed
-
-    function votingDelay() public view override virtual returns (uint256) {     // HARNESS: pure -> view
-        return _votingDelay;                                                    // HARNESS: parametric
-    }
-
-    function votingPeriod() public view override virtual returns (uint256) {    // HARNESS: pure -> view
-        return _votingPeriod;                                                   // HARNESS: parametric
-    }
-
-    // original code, not harnessed
-    // The following functions are overrides required by Solidity.
-
-    function quorum(uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotesQuorumFraction)
-        returns (uint256)
-    {
-        return super.quorum(blockNumber);
-    }
-
-    function getVotes(address account, uint256 blockNumber)
-        public
-        view
-        override(IGovernor, GovernorVotes)
-        returns (uint256)
-    {
-        return super.getVotes(account, blockNumber);
-    }
-
-    function state(uint256 proposalId)
-        public
-        view
-        override(Governor, GovernorTimelockCompound)
-        returns (ProposalState)
-    {
-        return super.state(proposalId);
-    }
-
-    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
-        public
-        override(Governor, IGovernor)
-        returns (uint256)
-    {
-        return super.propose(targets, values, calldatas, description);
-    }
-
-    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockCompound)
-    {
-        super._execute(proposalId, targets, values, calldatas, descriptionHash);
-    }
-
-    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockCompound)
-        returns (uint256)
-    {
-        return super._cancel(targets, values, calldatas, descriptionHash);
-    }
-
-    function _executor()
-        internal
-        view
-        override(Governor, GovernorTimelockCompound)
-        returns (address)
-    {
-        return super._executor();
-    }
-
-    function supportsInterface(bytes4 interfaceId)
-        public
-        view
-        override(Governor, GovernorTimelockCompound)
-        returns (bool)
-    {
-        return super.supportsInterface(interfaceId);
-    }
-}

certora/munged/.gitignore

@@ -1,2 +0,0 @@
-*
-!.gitignore

certora/run.js

@@ -0,0 +1,146 @@
+#!/usr/bin/env node
+
+// USAGE:
+//    node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH]
+// EXAMPLES:
+//    node certora/run.js --all
+//    node certora/run.js AccessControl
+//    node certora/run.js AccessControlHarness:AccessControl
+
+const proc = require('child_process');
+const { PassThrough } = require('stream');
+const events = require('events');
+
+const argv = require('yargs')
+  .env('')
+  .options({
+    all: {
+      alias: 'a',
+      type: 'boolean',
+    },
+    spec: {
+      alias: 's',
+      type: 'string',
+      default: __dirname + '/specs.json',
+    },
+    parallel: {
+      alias: 'p',
+      type: 'number',
+      default: 4,
+    },
+    options: {
+      alias: 'o',
+      type: 'array',
+      default: [],
+    },
+  }).argv;
+
+function match(entry, request) {
+  const [reqSpec, reqContract] = request.split(':').reverse();
+  return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
+}
+
+const specs = require(argv.spec).filter(s => argv.all || argv._.some(r => match(s, r)));
+const limit = require('p-limit')(argv.parallel);
+
+if (argv._.length == 0 && !argv.all) {
+  console.error(`Warning: No specs requested. Did you forgot to toggle '--all'?`);
+}
+
+for (const r of argv._) {
+  if (!specs.some(s => match(s, r))) {
+    console.error(`Error: Requested spec '${r}' not found in ${argv.spec}`);
+    process.exitCode = 1;
+  }
+}
+
+if (process.exitCode) {
+  process.exit(process.exitCode);
+}
+
+for (const { spec, contract, files, options = [] } of specs) {
+  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]);
+}
+
+// Run certora, aggregate the output and print it at the end
+async function runCertora(spec, contract, files, options = []) {
+  const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
+  const child = proc.spawn('certoraRun', args);
+
+  const stream = new PassThrough();
+  const output = collect(stream);
+
+  child.stdout.pipe(stream, { end: false });
+  child.stderr.pipe(stream, { end: false });
+
+  // as soon as we have a job id, print the output link
+  stream.on('data', function logStatusUrl(data) {
+    const { '-DjobId': jobId, '-DuserId': userId } = Object.fromEntries(
+      data
+        .toString('utf8')
+        .match(/-D\S+=\S+/g)
+        ?.map(s => s.split('=')) || [],
+    );
+
+    if (jobId && userId) {
+      console.error(`[${spec}] https://prover.certora.com/output/${userId}/${jobId}/`);
+      stream.off('data', logStatusUrl);
+    }
+  });
+
+  // wait for process end
+  const [code, signal] = await events.once(child, 'exit');
+
+  // error
+  if (code || signal) {
+    console.error(`[${spec}] Exited with code ${code || signal}`);
+    process.exitCode = 1;
+  }
+
+  // get all output
+  stream.end();
+
+  // write results in markdown format
+  writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]);
+
+  // write all details
+  console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));
+}
+
+// Collects stream data into a string
+async function collect(stream) {
+  const buffers = [];
+  for await (const data of stream) {
+    const buf = Buffer.isBuffer(data) ? data : Buffer.from(data);
+    buffers.push(buf);
+  }
+  return Buffer.concat(buffers).toString('utf8');
+}
+
+// Formatting
+let hasHeader = false;
+
+function formatRow(...array) {
+  return ['', ...array, ''].join(' | ');
+}
+
+function writeHeader() {
+  console.log(formatRow('spec', 'contract', 'result', 'status', 'output'));
+  console.log(formatRow('-', '-', '-', '-', '-'));
+}
+
+function writeEntry(spec, contract, success, url) {
+  if (!hasHeader) {
+    hasHeader = true;
+    writeHeader();
+  }
+  console.log(
+    formatRow(
+      spec,
+      contract,
+      success ? ':x:' : ':heavy_check_mark:',
+      url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error',
+      url ? `[link](${url})` : 'error',
+    ),
+  );
+}

certora/scripts/Governor.sh

@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
-    --verify GovernorHarness:certora/specs/GovernorBase.spec \
-    --solc solc8.0 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule voteStartBeforeVoteEnd \
-    --msg "$1"

certora/scripts/GovernorCountingSimple-counting.sh

@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
-    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
-    --solc solc8.2 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule hasVotedCorrelation \
-    --msg "$1"

certora/scripts/WizardControlFirstPriority.sh

@@ -1,12 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
-    --link WizardControlFirstPriority:token=ERC20VotesHarness \
-    --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
-    --solc solc8.2 \
-    --disableLocalTypeChecking \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --settings -copyLoopUnroll=4 \
-    --rule canVoteDuringVotingPeriod \
-    --msg "$1"

certora/scripts/WizardFirstTry.sh

@@ -1,10 +0,0 @@
-make -C certora munged
-
-certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
-    --verify WizardFirstTry:certora/specs/GovernorBase.spec \
-    --solc solc8.2 \
-    --staging shelly/forSasha \
-    --optimistic_loop \
-    --disableLocalTypeChecking \
-    --settings -copyLoopUnroll=4 \
-    --msg "$1"

certora/scripts/sanity.sh

@@ -1,14 +0,0 @@
-make -C certora munged
-
-for f in certora/harnesses/Wizard*.sol
-do
-    echo "Processing $f"
-    file="$(basename $f)"
-    echo ${file%.*}
-    certoraRun certora/harnesses/$file \
-    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
-    --solc solc8.2 --staging shelly/forSasha \
-    --optimistic_loop \
-    --msg "checking sanity on ${file%.*}"
-    --settings -copyLoopUnroll=4
-done

certora/scripts/verifyAll.sh

@@ -1,39 +0,0 @@
-#!/bin/bash
-
-make -C certora munged
-
-for contract in certora/harnesses/Wizard*.sol;
-do
-    for spec in certora/specs/*.spec;
-    do      
-        contractFile="$(basename $contract)"
-        specFile="$(basename $spec)"
-        if [[ "${specFile%.*}" != "RulesInProgress" ]];
-        then
-            echo "Processing ${contractFile%.*} with $specFile"
-            if [[ "${contractFile%.*}" = *"WizardControl"* ]];
-            then
-                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
-                --link ${contractFile%.*}:token=ERC20VotesHarness \
-                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
-                --staging shelly/forSasha \
-                --disableLocalTypeChecking \
-                --optimistic_loop \
-                --settings -copyLoopUnroll=4 \
-                --send_only \
-                --msg "checking $specFile on ${contractFile%.*}"
-            else
-                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
-                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
-                --solc solc8.2 \
-                --staging shelly/forSasha \
-                --disableLocalTypeChecking \
-                --optimistic_loop \
-                --settings -copyLoopUnroll=4 \
-                --send_only \
-                --msg "checking $specFile on ${contractFile%.*}"
-            fi
-        fi
-    done
-done

certora/specs.json

@@ -0,0 +1,86 @@
+[
+  {
+    "spec": "Pausable",
+    "contract": "PausableHarness",
+    "files": ["certora/harnesses/PausableHarness.sol"]
+  },
+  {
+    "spec": "AccessControl",
+    "contract": "AccessControlHarness",
+    "files": ["certora/harnesses/AccessControlHarness.sol"]
+  },
+  {
+    "spec": "AccessControlDefaultAdminRules",
+    "contract": "AccessControlDefaultAdminRulesHarness",
+    "files": ["certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"]
+  },
+  {
+    "spec": "DoubleEndedQueue",
+    "contract": "DoubleEndedQueueHarness",
+    "files": ["certora/harnesses/DoubleEndedQueueHarness.sol"]
+  },
+  {
+    "spec": "Ownable",
+    "contract": "OwnableHarness",
+    "files": ["certora/harnesses/OwnableHarness.sol"]
+  },
+  {
+    "spec": "Ownable2Step",
+    "contract": "Ownable2StepHarness",
+    "files": ["certora/harnesses/Ownable2StepHarness.sol"]
+  },
+  {
+    "spec": "ERC20",
+    "contract": "ERC20PermitHarness",
+    "files": ["certora/harnesses/ERC20PermitHarness.sol"],
+    "options": ["--optimistic_loop"]
+  },
+  {
+    "spec": "ERC20FlashMint",
+    "contract": "ERC20FlashMintHarness",
+    "files": [
+      "certora/harnesses/ERC20FlashMintHarness.sol",
+      "certora/harnesses/ERC3156FlashBorrowerHarness.sol"
+    ],
+    "options": ["--optimistic_loop"]
+  },
+  {
+    "spec": "ERC20Wrapper",
+    "contract": "ERC20WrapperHarness",
+    "files": [
+      "certora/harnesses/ERC20PermitHarness.sol",
+      "certora/harnesses/ERC20WrapperHarness.sol"
+    ],
+    "options": [
+      "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
+      "--optimistic_loop"
+    ]
+  },
+  {
+    "spec": "ERC721",
+    "contract": "ERC721Harness",
+    "files": ["certora/harnesses/ERC721Harness.sol", "certora/harnesses/ERC721ReceiverHarness.sol"],
+    "options": ["--optimistic_loop"]
+  },
+  {
+    "spec": "Initializable",
+    "contract": "InitializableHarness",
+    "files": ["certora/harnesses/InitializableHarness.sol"]
+  },
+  {
+    "spec": "EnumerableSet",
+    "contract": "EnumerableSetHarness",
+    "files": ["certora/harnesses/EnumerableSetHarness.sol"]
+  },
+  {
+    "spec": "EnumerableMap",
+    "contract": "EnumerableMapHarness",
+    "files": ["certora/harnesses/EnumerableMapHarness.sol"]
+  },
+  {
+    "spec": "TimelockController",
+    "contract": "TimelockControllerHarness",
+    "files": ["certora/harnesses/TimelockControllerHarness.sol"],
+    "options": ["--optimistic_hashing", "--optimistic_loop"]
+  }
+]

certora/specs/AccessControl.spec

@@ -0,0 +1,126 @@
+import "helpers/helpers.spec"
+import "methods/IAccessControl.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition DEFAULT_ADMIN_ROLE() returns bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) {
+    calldataarg args;
+
+    bool hasRoleBefore = hasRole(role, account);
+    f(e, args);
+    bool hasRoleAfter = hasRole(role, account);
+
+    assert (
+        !hasRoleBefore &&
+        hasRoleAfter
+    ) => (
+        f.selector == grantRole(bytes32, address).selector
+    );
+
+    assert (
+        hasRoleBefore &&
+        !hasRoleAfter
+    ) => (
+        f.selector == revokeRole(bytes32, address).selector ||
+        f.selector == renounceRole(bytes32, address).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: grantRole only affects the specified user/role combo                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule grantRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    grantRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: revokeRole only affects the specified user/role combo                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule revokeRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    revokeRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceRole only affects the specified user/role combo                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    renounceRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> account == e.msg.sender;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
+}

certora/specs/AccessControlDefaultAdminRules.spec

@@ -0,0 +1,500 @@
+import "helpers/helpers.spec"
+import "methods/IAccessControlDefaultAdminRules.spec"
+import "methods/IAccessControl.spec"
+import "AccessControl.spec"
+
+use rule onlyGrantCanGrant filtered {
+  f -> f.selector != acceptDefaultAdminTransfer().selector
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+function max_uint48() returns mathint {
+    return (1 << 48) - 1;
+}
+
+function nonZeroAccount(address account) returns bool {
+  return account != 0;
+}
+
+function timeSanity(env e) returns bool {
+  return
+    e.block.timestamp > 0 && // Avoids 0 schedules
+    e.block.timestamp + defaultAdminDelay(e) < max_uint48();
+}
+
+function delayChangeWaitSanity(env e, uint48 newDelay) returns bool {
+  return e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48();
+}
+
+function isSet(uint48 schedule) returns bool {
+  return schedule != 0;
+}
+
+function hasPassed(env e, uint48 schedule) returns bool {
+  return schedule < e.block.timestamp;
+}
+
+function min(uint48 a, uint48 b) returns mathint {
+  return a < b ? a : b;
+}
+
+function increasingDelaySchedule(env e, uint48 newDelay) returns mathint {
+  return e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait());
+}
+
+function decreasingDelaySchedule(env e, uint48 newDelay) returns mathint {
+  return e.block.timestamp + defaultAdminDelay(e) - newDelay;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: defaultAdmin holds the DEFAULT_ADMIN_ROLE                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant defaultAdminConsistency(address account)
+  defaultAdmin() == account <=> hasRole(DEFAULT_ADMIN_ROLE(), account)
+  {
+    preserved {
+      // defaultAdmin() returns the zero address when there's no default admin
+      require nonZeroAccount(account);
+    }
+  }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Only one account holds the DEFAULT_ADMIN_ROLE                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant singleDefaultAdmin(address account, address another)
+  hasRole(DEFAULT_ADMIN_ROLE(), account) && hasRole(DEFAULT_ADMIN_ROLE(), another) => another == account
+  // We filter here because we couldn't find a way to force Certora to have an initial state with
+  // only one DEFAULT_ADMIN_ROLE enforced, so a counter example is a different default admin since inception
+  // triggering the transfer, which is known to be impossible by definition.
+  filtered { f -> f.selector != acceptDefaultAdminTransfer().selector }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: DEFAULT_ADMIN_ROLE's admin is always DEFAULT_ADMIN_ROLE                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant defaultAdminRoleAdminConsistency()
+  getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: owner is the defaultAdmin                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant ownerConsistency()
+  defaultAdmin() == owner()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: revokeRole only affects the specified user/role combo                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule revokeRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    revokeRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> isCallerAdmin && role != DEFAULT_ADMIN_ROLE(),
+      "roles can only be revoked by their owner except for the default admin role";
+
+    // effect
+    assert success => !hasRole(role, account), "role is revoked";
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount),
+      "no other role is affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceRole only affects the specified user/role combo                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+    uint48 scheduleBefore = pendingDefaultAdminSchedule_();
+    address pendingAdminBefore = pendingDefaultAdmin_();
+
+    renounceRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> (
+      account == e.msg.sender &&
+      (
+        (
+          role != DEFAULT_ADMIN_ROLE()
+        ) || (
+          role == DEFAULT_ADMIN_ROLE() &&
+          pendingAdminBefore == 0 &&
+          isSet(scheduleBefore) &&
+          hasPassed(e, scheduleBefore)
+        )
+      )
+    ), "an account only can renounce by itself with a delay for the default admin role";
+
+    // effect
+    assert success => !hasRole(role, account), "role is renounced";
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount),
+      "no other role is affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: defaultAdmin is only affected by accepting an admin transfer or renoucing                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDefaultAdminChange(env e, method f, calldataarg args) {
+  require nonZeroAccount(e.msg.sender);
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  address adminBefore = defaultAdmin();
+  f(e, args);
+  address adminAfter = defaultAdmin();
+
+  assert adminBefore != adminAfter => (
+    f.selector == acceptDefaultAdminTransfer().selector ||
+    f.selector == renounceRole(bytes32,address).selector
+  ), "default admin is only affected by accepting an admin transfer or renoucing";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pendingDefaultAdmin is only affected by beginning, accepting or canceling an admin transfer                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noPendingDefaultAdminChange(env e, method f, calldataarg args) {
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  address pendingAdminBefore = pendingDefaultAdmin_();
+  address scheduleBefore = pendingDefaultAdminSchedule_();
+  f(e, args);
+  address pendingAdminAfter = pendingDefaultAdmin_();
+  address scheduleAfter = pendingDefaultAdminSchedule_();
+
+  assert (
+    pendingAdminBefore != pendingAdminAfter ||
+    scheduleBefore != scheduleAfter
+  ) => (
+    f.selector == beginDefaultAdminTransfer(address).selector ||
+    f.selector == acceptDefaultAdminTransfer().selector ||
+    f.selector == cancelDefaultAdminTransfer().selector
+  ), "pending admin and its schedule is only affected by beginning, accepting or cancelling an admin transfer";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: defaultAdminDelay can't be changed atomically by any function                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDefaultAdminDelayChange(env e, method f, calldataarg args) {
+  uint48 delayBefore = defaultAdminDelay(e);
+  f(e, args);
+  uint48 delayAfter = defaultAdminDelay(e);
+
+  assert delayBefore == delayAfter, "delay can't be changed atomically by any function";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pendingDefaultAdminDelay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) {
+  uint48 pendingDelayBefore = pendingDelay_(e);
+  f(e, args);
+  uint48 pendingDelayAfter = pendingDelay_(e);
+
+  assert pendingDelayBefore != pendingDelayAfter => (
+    f.selector == changeDefaultAdminDelay(uint48).selector ||
+    f.selector == rollbackDefaultAdminDelay().selector
+  ), "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: defaultAdminDelayIncreaseWait can't be changed atomically by any function                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDefaultAdminDelayIncreaseWaitChange(env e, method f, calldataarg args) {
+  uint48 delayIncreaseWaitBefore = defaultAdminDelayIncreaseWait();
+  f(e, args);
+  uint48 delayIncreaseWaitAfter = defaultAdminDelayIncreaseWait();
+
+  assert delayIncreaseWaitBefore == delayIncreaseWaitAfter,
+    "delay increase wait can't be changed atomically by any function";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: beginDefaultAdminTransfer sets a pending default admin and its schedule                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule beginDefaultAdminTransfer(env e, address newAdmin) {
+  require nonpayable(e);
+  require timeSanity(e);
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  beginDefaultAdminTransfer@withrevert(e, newAdmin);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can begin a transfer";
+
+  // effect
+  assert success => pendingDefaultAdmin_() == newAdmin,
+    "pending default admin is set";
+  assert success => pendingDefaultAdminSchedule_() == e.block.timestamp + defaultAdminDelay(e),
+    "pending default admin delay is set";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A default admin can't change in less than the applied schedule                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args, address newAdmin) {
+  require e1.block.timestamp < e2.block.timestamp;
+
+  uint48 delayBefore = defaultAdminDelay(e1);
+  address adminBefore = defaultAdmin();
+  // There might be a better way to generalize this without requiring `beginDefaultAdminTransfer`, but currently
+  // it's the only way in which we can attest that only `delayBefore` has passed before a change.
+  beginDefaultAdminTransfer(e1, newAdmin);
+  f(e2, args);
+  address adminAfter = defaultAdmin();
+
+  assert adminAfter == newAdmin => ((e2.block.timestamp >= e1.block.timestamp + delayBefore) || adminBefore == newAdmin),
+    "A delay can't change in less than applied schedule";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: acceptDefaultAdminTransfer updates defaultAdmin resetting the pending admin and its schedule  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule acceptDefaultAdminTransfer(env e) {
+  require nonpayable(e);
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  address pendingAdminBefore = pendingDefaultAdmin_();
+  uint48 scheduleAfter = pendingDefaultAdminSchedule_();
+
+  acceptDefaultAdminTransfer@withrevert(e);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == pendingAdminBefore && isSet(scheduleAfter) && hasPassed(e, scheduleAfter),
+    "only the pending default admin can accept the role after the schedule has been set and passed";
+
+  // effect
+  assert success => defaultAdmin() == pendingAdminBefore,
+    "Default admin is set to the previous pending default admin";
+  assert success => pendingDefaultAdmin_() == 0,
+    "Pending default admin is reset";
+  assert success => pendingDefaultAdminSchedule_() == 0,
+    "Pending default admin delay is reset";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: cancelDefaultAdminTransfer resets pending default admin and its schedule                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cancelDefaultAdminTransfer(env e) {
+  require nonpayable(e);
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  cancelDefaultAdminTransfer@withrevert(e);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can cancel a transfer";
+
+  // effect
+  assert success => pendingDefaultAdmin_() == 0,
+    "Pending default admin is reset";
+  assert success => pendingDefaultAdminSchedule_() == 0,
+    "Pending default admin delay is reset";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: changeDefaultAdminDelay sets a pending default admin delay and its schedule                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule changeDefaultAdminDelay(env e, uint48 newDelay) {
+  require nonpayable(e);
+  require timeSanity(e);
+  require delayChangeWaitSanity(e, newDelay);
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  uint48 delayBefore = defaultAdminDelay(e);
+
+  changeDefaultAdminDelay@withrevert(e, newDelay);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can begin a delay change";
+
+  // effect
+  assert success => pendingDelay_(e) == newDelay, "pending delay is set";
+  assert success => (
+    pendingDelaySchedule_(e) > e.block.timestamp ||
+    delayBefore == newDelay || // Interpreted as decreasing, x - x = 0
+    defaultAdminDelayIncreaseWait() == 0
+  ),
+    "pending delay schedule is set in the future unless accepted edge cases";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A delay can't change in less than the applied schedule                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48 newDelay) {
+  require e1.block.timestamp < e2.block.timestamp;
+
+  uint48 delayBefore = defaultAdminDelay(e1);
+  changeDefaultAdminDelay(e1, newDelay);
+  f(e2, args);
+  uint48 delayAfter = defaultAdminDelay(e2);
+
+  mathint delayWait = newDelay > delayBefore ? increasingDelaySchedule(e1, newDelay) : decreasingDelaySchedule(e1, newDelay);
+
+  assert delayAfter == newDelay => (e2.block.timestamp >= delayWait || delayBefore == newDelay),
+    "A delay can't change in less than applied schedule";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pending delay wait is set depending on increasing or decreasing the delay                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pendingDelayWait(env e, uint48 newDelay) {
+  uint48 oldDelay = defaultAdminDelay(e);
+  changeDefaultAdminDelay(e, newDelay);
+
+  assert newDelay > oldDelay => pendingDelaySchedule_(e) == increasingDelaySchedule(e, newDelay),
+    "Delay wait is the minimum between the new delay and a threshold when the delay is increased";
+  assert newDelay <= oldDelay => pendingDelaySchedule_(e) == decreasingDelaySchedule(e, newDelay),
+    "Delay wait is the difference between the current and the new delay when the delay is decreased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: rollbackDefaultAdminDelay resets the delay and its schedule                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule rollbackDefaultAdminDelay(env e) {
+  require nonpayable(e);
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  rollbackDefaultAdminDelay@withrevert(e);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can rollback a delay change";
+
+  // effect
+  assert success => pendingDelay_(e) == 0,
+    "Pending default admin is reset";
+  assert success => pendingDelaySchedule_(e) == 0,
+    "Pending default admin delay is reset";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pending default admin and the delay can only change along with their corresponding schedules                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pendingValueAndScheduleCoupling(env e, address newAdmin, uint48 newDelay) {
+  requireInvariant defaultAdminConsistency(defaultAdmin());
+  requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
+
+  // Pending admin
+  address pendingAdminBefore = pendingDefaultAdmin_();
+  uint48 pendingAdminScheduleBefore = pendingDefaultAdminSchedule_();
+
+  beginDefaultAdminTransfer(e, newAdmin);
+
+  address pendingAdminAfter = pendingDefaultAdmin_();
+  uint48 pendingAdminScheduleAfter = pendingDefaultAdminSchedule_();
+
+  assert (
+    pendingAdminScheduleBefore != pendingDefaultAdminSchedule_() &&
+    pendingAdminBefore == pendingAdminAfter
+  ) => newAdmin == pendingAdminBefore, "pending admin stays the same if the new admin set is the same";
+
+  assert (
+    pendingAdminBefore != pendingAdminAfter &&
+    pendingAdminScheduleBefore == pendingDefaultAdminSchedule_()
+  ) => (
+    // Schedule doesn't change if:
+    // - The defaultAdminDelay was reduced to a value such that added to the block.timestamp is equal to previous schedule
+    e.block.timestamp + defaultAdminDelay(e) == pendingAdminScheduleBefore
+  ), "pending admin stays the same if a default admin transfer is begun on accepted edge cases";
+
+  // Pending delay
+  address pendingDelayBefore = pendingDelay_(e);
+  uint48 pendingDelayScheduleBefore = pendingDelaySchedule_(e);
+
+  changeDefaultAdminDelay(e, newDelay);
+
+  address pendingDelayAfter = pendingDelay_(e);
+  uint48 pendingDelayScheduleAfter = pendingDelaySchedule_(e);
+
+  assert (
+    pendingDelayScheduleBefore != pendingDelayScheduleAfter &&
+    pendingDelayBefore == pendingDelayAfter
+  ) => newDelay == pendingDelayBefore || pendingDelayBefore == 0, "pending delay stays the same if the new delay set is the same";
+
+  assert (
+    pendingDelayBefore != pendingDelayAfter &&
+    pendingDelayScheduleBefore == pendingDelayScheduleAfter
+  ) => (
+    increasingDelaySchedule(e, newDelay) == pendingDelayScheduleBefore ||
+    decreasingDelaySchedule(e, newDelay) == pendingDelayScheduleBefore
+  ), "pending delay stays the same if a default admin transfer is begun on accepted edge cases";
+}

certora/specs/DoubleEndedQueue.spec

@@ -0,0 +1,366 @@
+import "helpers/helpers.spec"
+
+methods {
+    pushFront(bytes32)                    envfree
+    pushBack(bytes32)                     envfree
+    popFront()          returns (bytes32) envfree
+    popBack()           returns (bytes32) envfree
+    clear()                               envfree
+
+    // exposed for FV
+    begin()             returns (int128)  envfree
+    end()               returns (int128)  envfree
+
+    // view
+    length()            returns (uint256) envfree
+    empty()             returns (bool)    envfree
+    front()             returns (bytes32) envfree
+    back()              returns (bytes32) envfree
+    at_(uint256)        returns (bytes32) envfree // at is a reserved word
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+function min_int128() returns mathint {
+    return -(1 << 127);
+}
+
+function max_int128() returns mathint {
+    return (1 << 127) - 1;
+}
+
+// Could be broken in theory, but not in practice
+function boundedQueue() returns bool {
+    return
+        max_int128() > to_mathint(end()) &&
+        min_int128() < to_mathint(begin());
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: end is larger or equal than begin                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant boundariesConsistency()
+    end() >= begin()
+    filtered { f -> !f.isView }
+    { preserved { require boundedQueue(); } }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: length is end minus begin                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant lengthConsistency()
+    length() == to_mathint(end()) - to_mathint(begin())
+    filtered { f -> !f.isView }
+    { preserved { require boundedQueue(); } }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: empty() is length 0 and no element exists                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant emptiness()
+    empty() <=> length() == 0
+    filtered { f -> !f.isView }
+    { preserved { require boundedQueue(); } }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: front points to the first index and back points to the last one                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant queueEndings()
+    at_(length() - 1) == back() && at_(0) == front()
+    filtered { f -> !f.isView }
+    {
+        preserved {
+            requireInvariant boundariesConsistency();
+            require boundedQueue();
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: pushFront adds an element at the beginning of the queue                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushFront(bytes32 value) {
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+
+    pushFront@withrevert(value);
+
+    // liveness
+    assert !lastReverted, "never reverts";
+
+    // effect
+    assert front() == value, "front set to value";
+    assert length() == lengthBefore + 1, "queue extended";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pushFront preserves the previous values in the queue with a +1 offset                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushFrontConsistency(uint256 index) {
+    require boundedQueue();
+
+    bytes32 beforeAt = at_(index);
+
+    bytes32 value;
+    pushFront(value);
+
+    // try to read value
+    bytes32 afterAt = at_@withrevert(index + 1);
+
+    assert !lastReverted, "value still there";
+    assert afterAt == beforeAt, "data is preserved";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: pushBack adds an element at the end of the queue                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushBack(bytes32 value) {
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+
+    pushBack@withrevert(value);
+
+    // liveness
+    assert !lastReverted, "never reverts";
+
+    // effect
+    assert back() == value, "back set to value";
+    assert length() == lengthBefore + 1, "queue increased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pushBack preserves the previous values in the queue                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pushBackConsistency(uint256 index) {
+    require boundedQueue();
+
+    bytes32 beforeAt = at_(index);
+
+    bytes32 value;
+    pushBack(value);
+
+    // try to read value
+    bytes32 afterAt = at_@withrevert(index);
+
+    assert !lastReverted, "value still there";
+    assert afterAt == beforeAt, "data is preserved";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: popFront removes an element from the beginning of the queue                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popFront {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+    bytes32 frontBefore = front@withrevert();
+
+    bytes32 popped = popFront@withrevert();
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> lengthBefore != 0, "never reverts if not previously empty";
+
+    // effect
+    assert success => frontBefore == popped, "previous front is returned";
+    assert success => length() == lengthBefore - 1, "queue decreased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: at(x) is preserved and offset to at(x - 1) after calling popFront                                             |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popFrontConsistency(uint256 index) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    // Read (any) value that is not the front (this asserts the value exists / the queue is long enough)
+    require index > 1;
+    bytes32 before = at_(index);
+
+    popFront();
+
+    // try to read value
+    bytes32 after = at_@withrevert(index - 1);
+
+    assert !lastReverted, "value still exists in the queue";
+    assert before == after, "values are offset and not modified";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: popBack removes an element from the end of the queue                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popBack {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    uint256 lengthBefore = length();
+    bytes32 backBefore = back@withrevert();
+
+    bytes32 popped = popBack@withrevert();
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> lengthBefore != 0, "never reverts if not previously empty";
+
+    // effect
+    assert success => backBefore == popped, "previous back is returned";
+    assert success => length() == lengthBefore - 1, "queue decreased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: at(x) is preserved after calling popBack                                                                     |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule popBackConsistency(uint256 index) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    // Read (any) value that is not the back (this asserts the value exists / the queue is long enough)
+    require index < length() - 1;
+    bytes32 before = at_(index);
+
+    popBack();
+
+    // try to read value
+    bytes32 after = at_@withrevert(index);
+
+    assert !lastReverted, "value still exists in the queue";
+    assert before == after, "values are offset and not modified";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: clear sets length to 0                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule clear {
+    clear@withrevert();
+
+    // liveness
+    assert !lastReverted, "never reverts";
+
+    // effect
+    assert length() == 0, "sets length to 0";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: front/back access reverts only if the queue is empty or querying out of bounds                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyEmptyRevert(env e) {
+    require nonpayable(e);
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    method f;
+    calldataarg args;
+
+    bool emptyBefore = empty();
+
+    f@withrevert(e, args);
+
+    assert lastReverted => (
+        (f.selector == front().selector && emptyBefore) ||
+        (f.selector == back().selector && emptyBefore) ||
+        (f.selector == popFront().selector  && emptyBefore) ||
+        (f.selector == popBack().selector  && emptyBefore) ||
+        f.selector == at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert
+    ), "only revert if empty or out of bounds";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: at(index) only reverts if index is out of bounds                                                                  |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyOutOfBoundsRevert(uint256 index) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    at_@withrevert(index);
+
+    assert lastReverted <=> index >= length(), "only reverts if index is out of bounds";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only clear/push/pop operations can change the length of the queue                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noLengthChange(env e) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    method f;
+    calldataarg args;
+
+    uint256 lengthBefore = length();
+    f(e, args);
+    uint256 lengthAfter = length();
+
+    assert lengthAfter != lengthBefore => (
+        (f.selector == pushFront(bytes32).selector && lengthAfter == lengthBefore + 1) ||
+        (f.selector == pushBack(bytes32).selector && lengthAfter == lengthBefore + 1) ||
+        (f.selector == popBack().selector && lengthAfter == lengthBefore - 1) ||
+        (f.selector == popFront().selector && lengthAfter == lengthBefore - 1) ||
+        (f.selector == clear().selector && lengthAfter == 0)
+    ), "length is only affected by clear/pop/push operations";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: only push/pop can change values bounded in the queue (outside values aren't cleared)                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDataChange(env e) {
+    requireInvariant boundariesConsistency();
+    require boundedQueue();
+
+    method f;
+    calldataarg args;
+
+    uint256 index;
+    bytes32 atBefore = at_(index);
+    f(e, args);
+    bytes32 atAfter = at_@withrevert(index);
+    bool atAfterSuccess = !lastReverted;
+
+    assert !atAfterSuccess <=> (
+        f.selector == clear().selector ||
+        (f.selector == popBack().selector && index == length()) ||
+        (f.selector == popFront().selector && index == length())
+    ), "indexes of the queue are only removed by clear or pop";
+
+    assert atAfterSuccess && atAfter != atBefore => (
+        f.selector == popFront().selector ||
+        f.selector == pushFront(bytes32).selector
+    ), "values of the queue are only changed by popFront or pushFront";
+}

certora/specs/ERC20.spec

@@ -0,0 +1,414 @@
+import "helpers/helpers.spec"
+import "methods/IERC20.spec"
+import "methods/IERC2612.spec"
+
+methods {
+    // non standard ERC20 functions
+    increaseAllowance(address,uint256) returns (bool)
+    decreaseAllowance(address,uint256) returns (bool)
+
+    // exposed for FV
+    mint(address,uint256)
+    burn(address,uint256)
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost & hooks: sum of all balances                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost sumOfBalances() returns uint256 {
+  init_state axiom sumOfBalances() == 0;
+}
+
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: totalSupply is the sum of all balances                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant totalSupplyIsSumOfBalances()
+    totalSupply() == sumOfBalances()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: balance of address(0) is 0                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant zeroAddressNoBalance()
+    balanceOf(0) == 0
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only mint and burn can change total supply                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noChangeTotalSupply(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    method f;
+    calldataarg args;
+
+    uint256 totalSupplyBefore = totalSupply();
+    f(e, args);
+    uint256 totalSupplyAfter = totalSupply();
+
+    assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector;
+    assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAuthorizedCanTransfer(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    method f;
+    calldataarg args;
+    address account;
+
+    uint256 allowanceBefore = allowance(account, e.msg.sender);
+    uint256 balanceBefore   = balanceOf(account);
+    f(e, args);
+    uint256 balanceAfter    = balanceOf(account);
+
+    assert (
+        balanceAfter < balanceBefore
+    ) => (
+        f.selector == burn(address,uint256).selector ||
+        e.msg.sender == account ||
+        balanceBefore - balanceAfter <= allowanceBefore
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder (or a permit) can increase allowance. The spender can decrease it by using it          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyHolderOfSpenderCanChangeAllowance(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    method f;
+    calldataarg args;
+    address holder;
+    address spender;
+
+    uint256 allowanceBefore = allowance(holder, spender);
+    f(e, args);
+    uint256 allowanceAfter = allowance(holder, spender);
+
+    assert (
+        allowanceAfter > allowanceBefore
+    ) => (
+        (f.selector == approve(address,uint256).selector           && e.msg.sender == holder) ||
+        (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
+        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+    );
+
+    assert (
+        allowanceAfter < allowanceBefore
+    ) => (
+        (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
+        (f.selector == approve(address,uint256).selector              && e.msg.sender == holder ) ||
+        (f.selector == decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
+        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: mint behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mint(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address to;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 toBalanceBefore    = balanceOf(to);
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // run transaction
+    mint@withrevert(e, to, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert to == 0 || totalSupplyBefore + amount > max_uint256;
+    } else {
+        // updates balance and totalSupply
+        assert balanceOf(to) == toBalanceBefore   + amount;
+        assert totalSupply() == totalSupplyBefore + amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == to;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: burn behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule burn(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address from;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 fromBalanceBefore  = balanceOf(from);
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // run transaction
+    burn@withrevert(e, from, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert from == 0 || fromBalanceBefore < amount;
+    } else {
+        // updates balance and totalSupply
+        assert balanceOf(from) == fromBalanceBefore   - amount;
+        assert totalSupply()   == totalSupplyBefore - amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == from;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transfer behavior and side effects                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transfer(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address recipient;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 holderBalanceBefore    = balanceOf(holder);
+    uint256 recipientBalanceBefore = balanceOf(recipient);
+    uint256 otherBalanceBefore     = balanceOf(other);
+
+    // run transaction
+    transfer@withrevert(e, recipient, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || recipient == 0 || amount > holderBalanceBefore;
+    } else {
+        // balances of holder and recipient are updated
+        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transferFrom behavior and side effects                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferFrom(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+
+    address spender = e.msg.sender;
+    address holder;
+    address recipient;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 allowanceBefore        = allowance(holder, spender);
+    uint256 holderBalanceBefore    = balanceOf(holder);
+    uint256 recipientBalanceBefore = balanceOf(recipient);
+    uint256 otherBalanceBefore     = balanceOf(other);
+
+    // run transaction
+    transferFrom@withrevert(e, holder, recipient, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore;
+    } else {
+        // allowance is valid & updated
+        assert allowanceBefore            >= amount;
+        assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
+
+        // balances of holder and recipient are updated
+        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: approve behavior and side effects                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approve(env e) {
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // cache state
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    approve@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || spender == 0;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: increaseAllowance behavior and side effects                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule increaseAllowance(env e) {
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    increaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == allowanceBefore + amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: decreaseAllowance behavior and side effects                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule decreaseAllowance(env e) {
+    require nonpayable(e);
+
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    decreaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || spender == 0 || allowanceBefore < amount;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == allowanceBefore - amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: permit behavior and side effects                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule permit(env e) {
+    require nonpayable(e);
+
+    address holder;
+    address spender;
+    uint256 amount;
+    uint256 deadline;
+    uint8 v;
+    bytes32 r;
+    bytes32 s;
+
+    address account1;
+    address account2;
+    address account3;
+
+    // cache state
+    uint256 nonceBefore          = nonces(holder);
+    uint256 otherNonceBefore     = nonces(account1);
+    uint256 otherAllowanceBefore = allowance(account2, account3);
+
+    // sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice
+    require nonceBefore      < max_uint256;
+    require otherNonceBefore < max_uint256;
+
+    // run transaction
+    permit@withrevert(e, holder, spender, amount, deadline, v, r, s);
+
+    // check outcome
+    if (lastReverted) {
+        // Without formally checking the signature, we can't verify exactly the revert causes
+        assert true;
+    } else {
+        // allowance and nonce are updated
+        assert allowance(holder, spender) == amount;
+        assert nonces(holder) == nonceBefore + 1;
+
+        // deadline was respected
+        assert deadline >= e.block.timestamp;
+
+        // no other allowance or nonce is modified
+        assert nonces(account1)              != otherNonceBefore     => account1 == holder;
+        assert allowance(account2, account3) != otherAllowanceBefore => (account2 == holder && account3 == spender);
+    }
+}

certora/specs/ERC20FlashMint.spec

@@ -0,0 +1,48 @@
+import "helpers/helpers.spec"
+import "methods/IERC20.spec"
+import "methods/IERC3156.spec"
+
+methods {
+    // non standard ERC3156 functions
+    flashFeeReceiver() returns (address) envfree
+
+    // function summaries below
+    _mint(address account, uint256 amount)              => specMint(account, amount)
+    _burn(address account, uint256 amount)              => specBurn(account, amount)
+    _transfer(address from, address to, uint256 amount) => specTransfer(from, to, amount)
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost: track mint and burns in the CVL                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost mapping(address => uint256)                     trackedMintAmount;
+ghost mapping(address => uint256)                     trackedBurnAmount;
+ghost mapping(address => mapping(address => uint256)) trackedTransferedAmount;
+
+function specMint(address account, uint256 amount)              returns bool { trackedMintAmount[account] = amount;        return true; }
+function specBurn(address account, uint256 amount)              returns bool { trackedBurnAmount[account] = amount;        return true; }
+function specTransfer(address from, address to, uint256 amount) returns bool { trackedTransferedAmount[from][to] = amount; return true; }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: When doing a flashLoan, "amount" is minted and burnt, additionally, the fee is either burnt                   │
+│ (if the fee recipient is 0) or transferred (if the fee recipient is not 0)                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule checkMintAndBurn(env e) {
+    address receiver;
+    address token;
+    uint256 amount;
+    bytes data;
+
+    uint256 fees = flashFee(token, amount);
+    address recipient = flashFeeReceiver();
+
+    flashLoan(e, receiver, token, amount, data);
+
+    assert trackedMintAmount[receiver] == amount;
+    assert trackedBurnAmount[receiver] == amount + (recipient == 0 ? fees : 0);
+    assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == fees;
+}

certora/specs/ERC20Wrapper.spec

@@ -0,0 +1,198 @@
+import "helpers/helpers.spec"
+import "ERC20.spec"
+
+methods {
+    underlying()                       returns(address) envfree
+    underlyingTotalSupply()            returns(uint256) envfree
+    underlyingBalanceOf(address)       returns(uint256) envfree
+    underlyingAllowanceToThis(address) returns(uint256) envfree
+
+    depositFor(address, uint256)       returns(bool)
+    withdrawTo(address, uint256)       returns(bool)
+    recover(address)                   returns(uint256)
+}
+
+use invariant totalSupplyIsSumOfBalances
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool {
+    return underlyingBalanceOf(a) <= underlyingTotalSupply();
+}
+
+function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool {
+    return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply();
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: wrapped token can't be undercollateralized (solvency of the wrapper)                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant totalSupplyIsSmallerThanUnderlyingBalance()
+    totalSupply() <= underlyingBalanceOf(currentContract) &&
+    underlyingBalanceOf(currentContract) <= underlyingTotalSupply() &&
+    underlyingTotalSupply() <= max_uint256
+    {
+        preserved {
+            requireInvariant totalSupplyIsSumOfBalances;
+            require underlyingBalancesLowerThanUnderlyingSupply(currentContract);
+        }
+        preserved depositFor(address account, uint256 amount) with (env e) {
+            require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract);
+        }
+    }
+
+invariant noSelfWrap()
+    currentContract != underlying()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: depositFor liveness and effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule depositFor(env e) {
+    require nonpayable(e);
+
+    address sender = e.msg.sender;
+    address receiver;
+    address other;
+    uint256 amount;
+
+    // sanity
+    requireInvariant noSelfWrap;
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+    require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, sender);
+
+    uint256 balanceBefore                   = balanceOf(receiver);
+    uint256 supplyBefore                    = totalSupply();
+    uint256 senderUnderlyingBalanceBefore   = underlyingBalanceOf(sender);
+    uint256 senderUnderlyingAllowanceBefore = underlyingAllowanceToThis(sender);
+    uint256 wrapperUnderlyingBalanceBefore  = underlyingBalanceOf(currentContract);
+    uint256 underlyingSupplyBefore          = underlyingTotalSupply();
+
+    uint256 otherBalanceBefore              = balanceOf(other);
+    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
+
+    depositFor@withrevert(e, receiver, amount);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        sender   != currentContract               && // invalid sender
+        sender   != 0                             && // invalid sender
+        receiver != 0                             && // invalid receiver
+        amount   <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
+        amount   <= senderUnderlyingAllowanceBefore  // deposit doesn't exceed allowance
+    );
+
+    // effects
+    assert success => (
+        balanceOf(receiver) == balanceBefore + amount &&
+        totalSupply() == supplyBefore + amount &&
+        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount &&
+        underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount
+    );
+
+    // no side effect
+    assert underlyingTotalSupply() == underlyingSupplyBefore;
+    assert balanceOf(other)           != otherBalanceBefore           => other == receiver;
+    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: withdrawTo liveness and effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule withdrawTo(env e) {
+    require nonpayable(e);
+
+    address sender = e.msg.sender;
+    address receiver;
+    address other;
+    uint256 amount;
+
+    // sanity
+    requireInvariant noSelfWrap;
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+    require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, receiver);
+
+    uint256 balanceBefore                   = balanceOf(sender);
+    uint256 supplyBefore                    = totalSupply();
+    uint256 receiverUnderlyingBalanceBefore = underlyingBalanceOf(receiver);
+    uint256 wrapperUnderlyingBalanceBefore  = underlyingBalanceOf(currentContract);
+    uint256 underlyingSupplyBefore          = underlyingTotalSupply();
+
+    uint256 otherBalanceBefore              = balanceOf(other);
+    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
+
+    withdrawTo@withrevert(e, receiver, amount);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        sender   != 0          && // invalid sender
+        receiver != 0          && // invalid receiver
+        amount   <= balanceBefore // withdraw doesn't exceed balance
+    );
+
+    // effects
+    assert success => (
+        balanceOf(sender) == balanceBefore - amount &&
+        totalSupply() == supplyBefore - amount &&
+        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
+        underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
+    );
+
+    // no side effect
+    assert underlyingTotalSupply() == underlyingSupplyBefore;
+    assert balanceOf(other)           != otherBalanceBefore           => other == sender;
+    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: recover liveness and effects                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule recover(env e) {
+    require nonpayable(e);
+
+    address receiver;
+    address other;
+
+    // sanity
+    requireInvariant noSelfWrap;
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+
+    uint256 value                        = underlyingBalanceOf(currentContract) - totalSupply();
+    uint256 supplyBefore                 = totalSupply();
+    uint256 balanceBefore                = balanceOf(receiver);
+
+    uint256 otherBalanceBefore           = balanceOf(other);
+    uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other);
+
+    recover@withrevert(e, receiver);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> receiver != 0;
+
+    // effect
+    assert success => (
+        balanceOf(receiver) == balanceBefore + value &&
+        totalSupply() == supplyBefore + value &&
+        totalSupply() == underlyingBalanceOf(currentContract)
+    );
+
+    // no side effect
+    assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore;
+    assert balanceOf(other) != otherBalanceBefore => other == receiver;
+}

certora/specs/ERC721.spec

@@ -0,0 +1,589 @@
+import "helpers/helpers.spec"
+import "methods/IERC721.spec"
+
+methods {
+    // exposed for FV
+    mint(address,uint256)
+    safeMint(address,uint256)
+    safeMint(address,uint256,bytes)
+    burn(uint256)
+
+    tokenExists(uint256) returns (bool) envfree
+    unsafeOwnerOf(uint256) returns (address) envfree
+    unsafeGetApproved(uint256) returns (address) envfree
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+// Could be broken in theory, but not in practice
+function balanceLimited(address account) returns bool {
+    return balanceOf(account) < max_uint256;
+}
+
+function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
+    if (f.selector == transferFrom(address,address,uint256).selector) {
+        transferFrom@withrevert(e, from, to, tokenId);
+    } else if (f.selector == safeTransferFrom(address,address,uint256).selector) {
+        safeTransferFrom@withrevert(e, from, to, tokenId);
+    } else if (f.selector == safeTransferFrom(address,address,uint256,bytes).selector) {
+        bytes params;
+        require params.length < 0xffff;
+        safeTransferFrom@withrevert(e, from, to, tokenId, params);
+    } else {
+        calldataarg args;
+        f@withrevert(e, args);
+    }
+}
+
+function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
+    if (f.selector == mint(address,uint256).selector) {
+        mint@withrevert(e, to, tokenId);
+    } else if (f.selector == safeMint(address,uint256).selector) {
+        safeMint@withrevert(e, to, tokenId);
+    } else if (f.selector == safeMint(address,uint256,bytes).selector) {
+        bytes params;
+        require params.length < 0xffff;
+        safeMint@withrevert(e, to, tokenId, params);
+    } else {
+        require false;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost & hooks: ownership count                                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost ownedTotal() returns uint256 {
+  init_state axiom ownedTotal() == 0;
+}
+
+ghost mapping(address => uint256) ownedByUser {
+    init_state axiom forall address a. ownedByUser[a] == 0;
+}
+
+hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE {
+    ownedByUser[newOwner] = ownedByUser[newOwner] + to_uint256(newOwner != 0 ? 1 : 0);
+    ownedByUser[oldOwner] = ownedByUser[oldOwner] - to_uint256(oldOwner != 0 ? 1 : 0);
+
+    havoc ownedTotal assuming ownedTotal@new() == ownedTotal@old()
+        + to_uint256(newOwner != 0 ? 1 : 0)
+        - to_uint256(oldOwner != 0 ? 1 : 0);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost & hooks: sum of all balances                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost sumOfBalances() returns uint256 {
+  init_state axiom sumOfBalances() == 0;
+}
+
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
+}
+
+ghost mapping(address => uint256) ghostBalanceOf {
+    init_state axiom forall address a. ghostBalanceOf[a] == 0;
+}
+
+hook Sload uint256 value _balances[KEY address user] STORAGE {
+    require ghostBalanceOf[user] == value;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: ownedTotal is the sum of all balances                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant ownedTotalIsSumOfBalances()
+    ownedTotal() == sumOfBalances()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: balanceOf is the number of tokens owned                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant balanceOfConsistency(address user)
+    balanceOf(user) == ownedByUser[user] &&
+    balanceOf(user) == ghostBalanceOf[user]
+    {
+        preserved {
+            require balanceLimited(user);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: owner of a token must have some balance                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant ownerHasBalance(uint256 tokenId)
+    balanceOf(ownerOf(tokenId)) > 0
+    {
+        preserved {
+            requireInvariant balanceOfConsistency(ownerOf(tokenId));
+            require balanceLimited(ownerOf(tokenId));
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: tokens that do not exist are not owned and not approved                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant notMintedUnset(uint256 tokenId)
+    (!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) &&
+    (!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0)
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: ownerOf and getApproved revert if token does not exist                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule notMintedRevert(uint256 tokenId) {
+    requireInvariant notMintedUnset(tokenId);
+
+    bool e = tokenExists(tokenId);
+
+    address owner = ownerOf@withrevert(tokenId);
+    assert e <=> !lastReverted;
+    assert e => owner == unsafeOwnerOf(tokenId); // notMintedUnset tells us this is non-zero
+
+    address approved = getApproved@withrevert(tokenId);
+    assert e <=> !lastReverted;
+    assert e => approved == unsafeGetApproved(tokenId);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule unsafeDontRevert(uint256 tokenId) {
+    unsafeOwnerOf@withrevert(tokenId);
+    assert !lastReverted;
+
+    unsafeGetApproved@withrevert(tokenId);
+    assert !lastReverted;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: balance of address(0) is 0                                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule zeroAddressBalanceRevert() {
+    balanceOf@withrevert(0);
+    assert lastReverted;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: total supply can only change through mint and burn                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule supplyChange(env e) {
+    uint256 supplyBefore = ownedTotal();
+    method f; calldataarg args; f(e, args);
+    uint256 supplyAfter = ownedTotal();
+
+    assert supplyAfter > supplyBefore => (
+        supplyAfter == supplyBefore + 1 &&
+        (
+            f.selector == mint(address,uint256).selector ||
+            f.selector == safeMint(address,uint256).selector ||
+            f.selector == safeMint(address,uint256,bytes).selector
+        )
+    );
+    assert supplyAfter < supplyBefore => (
+        supplyAfter == supplyBefore - 1 &&
+        f.selector == burn(uint256).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1.           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule balanceChange(env e, address account) {
+    requireInvariant balanceOfConsistency(account);
+    require balanceLimited(account);
+
+    uint256 balanceBefore = balanceOf(account);
+    method f; calldataarg args; f(e, args);
+    uint256 balanceAfter  = balanceOf(account);
+
+    // balance can change by at most 1
+    assert balanceBefore != balanceAfter => (
+        balanceAfter == balanceBefore - 1 ||
+        balanceAfter == balanceBefore + 1
+    );
+
+    // only selected function can change balances
+    assert balanceBefore != balanceAfter => (
+        f.selector == transferFrom(address,address,uint256).selector ||
+        f.selector == safeTransferFrom(address,address,uint256).selector ||
+        f.selector == safeTransferFrom(address,address,uint256,bytes).selector ||
+        f.selector == mint(address,uint256).selector ||
+        f.selector == safeMint(address,uint256).selector ||
+        f.selector == safeMint(address,uint256,bytes).selector ||
+        f.selector == burn(uint256).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: ownership can only change through mint, burn or transfers.                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule ownershipChange(env e, uint256 tokenId) {
+    address ownerBefore = unsafeOwnerOf(tokenId);
+    method f; calldataarg args; f(e, args);
+    address ownerAfter  = unsafeOwnerOf(tokenId);
+
+    assert ownerBefore == 0 && ownerAfter != 0 => (
+        f.selector == mint(address,uint256).selector ||
+        f.selector == safeMint(address,uint256).selector ||
+        f.selector == safeMint(address,uint256,bytes).selector
+    );
+
+    assert ownerBefore != 0 && ownerAfter == 0 => (
+        f.selector == burn(uint256).selector
+    );
+
+    assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
+        f.selector == transferFrom(address,address,uint256).selector ||
+        f.selector == safeTransferFrom(address,address,uint256).selector ||
+        f.selector == safeTransferFrom(address,address,uint256,bytes).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approvalChange(env e, uint256 tokenId) {
+    address approvalBefore = unsafeGetApproved(tokenId);
+    method f; calldataarg args; f(e, args);
+    address approvalAfter  = unsafeGetApproved(tokenId);
+
+    // approve can set any value, other functions reset
+    assert approvalBefore != approvalAfter => (
+        f.selector == approve(address,uint256).selector ||
+        (
+            (
+                f.selector == transferFrom(address,address,uint256).selector ||
+                f.selector == safeTransferFrom(address,address,uint256).selector ||
+                f.selector == safeTransferFrom(address,address,uint256,bytes).selector ||
+                f.selector == burn(uint256).selector
+            ) && approvalAfter == 0
+        )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: approval for all tokens can only change through isApprovedForAll.                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approvedForAllChange(env e, address owner, address spender) {
+    bool approvedForAllBefore = isApprovedForAll(owner, spender);
+    method f; calldataarg args; f(e, args);
+    bool approvedForAllAfter  = isApprovedForAll(owner, spender);
+
+    assert approvedForAllBefore != approvedForAllAfter => f.selector == setApprovalForAll(address,bool).selector;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transferFrom behavior and side effects                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferFrom(env e, address from, address to, uint256 tokenId) {
+    require nonpayable(e);
+
+    address operator = e.msg.sender;
+    uint256 otherTokenId;
+    address otherAccount;
+
+    requireInvariant ownerHasBalance(tokenId);
+    require balanceLimited(to);
+
+    uint256 balanceOfFromBefore  = balanceOf(from);
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+    address approvalBefore       = unsafeGetApproved(tokenId);
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    transferFrom@withrevert(e, from, to, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        from == ownerBefore &&
+        from != 0 &&
+        to   != 0 &&
+        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
+    );
+
+    // effect
+    assert success => (
+        balanceOf(from)            == balanceOfFromBefore - to_uint256(from != to ? 1 : 0) &&
+        balanceOf(to)              == balanceOfToBefore   + to_uint256(from != to ? 1 : 0) &&
+        unsafeOwnerOf(tokenId)     == to &&
+        unsafeGetApproved(tokenId) == 0
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
+    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: safeTransferFrom behavior and side effects                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
+    f.selector == safeTransferFrom(address,address,uint256).selector ||
+    f.selector == safeTransferFrom(address,address,uint256,bytes).selector
+} {
+    require nonpayable(e);
+
+    address operator = e.msg.sender;
+    uint256 otherTokenId;
+    address otherAccount;
+
+    requireInvariant ownerHasBalance(tokenId);
+    require balanceLimited(to);
+
+    uint256 balanceOfFromBefore  = balanceOf(from);
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+    address approvalBefore       = unsafeGetApproved(tokenId);
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    helperTransferWithRevert(e, f, from, to, tokenId);
+    bool success = !lastReverted;
+
+    assert success <=> (
+        from == ownerBefore &&
+        from != 0 &&
+        to   != 0 &&
+        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
+    );
+
+    // effect
+    assert success => (
+        balanceOf(from)            == balanceOfFromBefore - to_uint256(from != to ? 1: 0) &&
+        balanceOf(to)              == balanceOfToBefore   + to_uint256(from != to ? 1: 0) &&
+        unsafeOwnerOf(tokenId)     == to &&
+        unsafeGetApproved(tokenId) == 0
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
+    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: mint behavior and side effects                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mint(env e, address to, uint256 tokenId) {
+    require nonpayable(e);
+    requireInvariant notMintedUnset(tokenId);
+
+    uint256 otherTokenId;
+    address otherAccount;
+
+    require balanceLimited(to);
+
+    uint256 supplyBefore         = ownedTotal();
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+
+    mint@withrevert(e, to, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        ownerBefore == 0 &&
+        to != 0
+    );
+
+    // effect
+    assert success => (
+        ownedTotal()           == supplyBefore + 1 &&
+        balanceOf(to)          == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId) == to
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
+    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: safeMint behavior and side effects                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
+    f.selector == safeMint(address,uint256).selector ||
+    f.selector == safeMint(address,uint256,bytes).selector
+} {
+    require nonpayable(e);
+    requireInvariant notMintedUnset(tokenId);
+
+    uint256 otherTokenId;
+    address otherAccount;
+
+    require balanceLimited(to);
+
+    uint256 supplyBefore         = ownedTotal();
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+
+    helperMintWithRevert(e, f, to, tokenId);
+    bool success = !lastReverted;
+
+    assert success <=> (
+        ownerBefore == 0 &&
+        to != 0
+    );
+
+    // effect
+    assert success => (
+        ownedTotal()           == supplyBefore + 1 &&
+        balanceOf(to)          == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId) == to
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
+    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: burn behavior and side effects                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule burn(env e, uint256 tokenId) {
+    require nonpayable(e);
+
+    address from = unsafeOwnerOf(tokenId);
+    uint256 otherTokenId;
+    address otherAccount;
+
+    requireInvariant ownerHasBalance(tokenId);
+
+    uint256 supplyBefore         = ownedTotal();
+    uint256 balanceOfFromBefore  = balanceOf(from);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    burn@withrevert(e, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        ownerBefore != 0
+    );
+
+    // effect
+    assert success => (
+        ownedTotal()               == supplyBefore   - 1 &&
+        balanceOf(from)            == balanceOfFromBefore - 1 &&
+        unsafeOwnerOf(tokenId)     == 0 &&
+        unsafeGetApproved(tokenId) == 0
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
+    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: approve behavior and side effects                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approve(env e, address spender, uint256 tokenId) {
+    require nonpayable(e);
+
+    address caller = e.msg.sender;
+    address owner = unsafeOwnerOf(tokenId);
+    uint256 otherTokenId;
+
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    approve@withrevert(e, spender, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        owner != 0 &&
+        owner != spender &&
+        (owner == caller || isApprovedForAll(owner, caller))
+    );
+
+    // effect
+    assert success => unsafeGetApproved(tokenId) == spender;
+
+    // no side effect
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: setApprovalForAll behavior and side effects                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule setApprovalForAll(env e, address operator, bool approved) {
+    require nonpayable(e);
+
+    address owner = e.msg.sender;
+    address otherOwner;
+    address otherOperator;
+
+    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);
+
+    setApprovalForAll@withrevert(e, operator, approved);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> owner != operator;
+
+    // effect
+    assert success => isApprovedForAll(owner, operator) == approved;
+
+    // no side effect
+    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
+        otherOwner    == owner &&
+        otherOperator == operator
+    );
+}

certora/specs/EnumerableMap.spec

@@ -0,0 +1,334 @@
+import "helpers/helpers.spec"
+
+methods {
+    // library
+    set(bytes32,bytes32)     returns (bool)    envfree
+    remove(bytes32)          returns (bool)    envfree
+    contains(bytes32)        returns (bool)    envfree
+    length()                 returns (uint256) envfree
+    key_at(uint256)          returns (bytes32) envfree
+    value_at(uint256)        returns (bytes32) envfree
+    tryGet_contains(bytes32) returns (bool)    envfree
+    tryGet_value(bytes32)    returns (bytes32) envfree
+    get(bytes32)             returns (bytes32) envfree
+
+    // FV
+    _indexOf(bytes32) returns (uint256) envfree
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function sanity() returns bool {
+    return length() < max_uint256;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: the value mapping is empty for keys that are not in the EnumerableMap.                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant noValueIfNotContained(bytes32 key)
+    !contains(key) => tryGet_value(key) == 0
+    {
+        preserved set(bytes32 otherKey, bytes32 someValue) {
+            require sanity();
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: All indexed keys are contained                                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant indexedContained(uint256 index)
+    index < length() => contains(key_at(index))
+    {
+        preserved {
+            requireInvariant consistencyIndex(index);
+            requireInvariant consistencyIndex(to_uint256(length() - 1));
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A value can only be stored at a single location                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant atUniqueness(uint256 index1, uint256 index2)
+    index1 == index2 <=> key_at(index1) == key_at(index2)
+    {
+        preserved remove(bytes32 key) {
+            requireInvariant atUniqueness(index1, to_uint256(length() - 1));
+            requireInvariant atUniqueness(index2, to_uint256(length() - 1));
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: index <> value relationship is consistent                                                                │
+│                                                                                                                     │
+│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another.  │
+│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are set    │
+│ and removed from the EnumerableMap).                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant consistencyIndex(uint256 index)
+    index < length() => _indexOf(key_at(index)) == index + 1
+    {
+        preserved remove(bytes32 key) {
+            requireInvariant consistencyIndex(to_uint256(length() - 1));
+        }
+    }
+
+invariant consistencyKey(bytes32 key)
+    contains(key) => (
+        _indexOf(key) > 0 &&
+        _indexOf(key) <= length() &&
+        key_at(to_uint256(_indexOf(key) - 1)) == key
+    )
+    {
+        preserved remove(bytes32 otherKey) {
+            requireInvariant consistencyKey(otherKey);
+            requireInvariant atUniqueness(
+                to_uint256(_indexOf(key) - 1),
+                to_uint256(_indexOf(otherKey) - 1)
+            );
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: state only changes by setting or removing elements                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateChange(env e, bytes32 key) {
+    require sanity();
+    requireInvariant consistencyKey(key);
+
+    uint256 lengthBefore   = length();
+    bool    containsBefore = contains(key);
+    bytes32 valueBefore    = tryGet_value(key);
+
+    method f;
+    calldataarg args;
+    f(e, args);
+
+    uint256 lengthAfter   = length();
+    bool    containsAfter = contains(key);
+    bytes32 valueAfter    = tryGet_value(key);
+
+    assert lengthBefore != lengthAfter => (
+        (f.selector == set(bytes32,bytes32).selector && lengthAfter == lengthBefore + 1) ||
+        (f.selector == remove(bytes32).selector      && lengthAfter == lengthBefore - 1)
+    );
+
+    assert containsBefore != containsAfter => (
+        (f.selector == set(bytes32,bytes32).selector && containsAfter) ||
+        (f.selector == remove(bytes32).selector      && !containsAfter)
+    );
+
+    assert valueBefore != valueAfter => (
+        (f.selector == set(bytes32,bytes32).selector && containsAfter) ||
+        (f.selector == remove(bytes32).selector      && !containsAfter && valueAfter == 0)
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: check liveness of view functions.                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule liveness_1(bytes32 key) {
+    requireInvariant consistencyKey(key);
+
+    // contains never revert
+    bool contains = contains@withrevert(key);
+    assert !lastReverted;
+
+    // tryGet never reverts (key)
+    tryGet_contains@withrevert(key);
+    assert !lastReverted;
+
+    // tryGet never reverts (value)
+    tryGet_value@withrevert(key);
+    assert !lastReverted;
+
+    // get reverts iff  the key is not in the map
+    get@withrevert(key);
+    assert !lastReverted <=> contains;
+}
+
+rule liveness_2(uint256 index) {
+    requireInvariant consistencyIndex(index);
+
+    // length never revert
+    uint256 length = length@withrevert();
+    assert !lastReverted;
+
+    // key_at reverts iff the index is out of bound
+    key_at@withrevert(index);
+    assert !lastReverted <=> index < length;
+
+    // value_at reverts iff the index is out of bound
+    value_at@withrevert(index);
+    assert !lastReverted <=> index < length;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: get and tryGet return the expected values.                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule getAndTryGet(bytes32 key) {
+    requireInvariant noValueIfNotContained(key);
+
+    bool    contained    = contains(key);
+    bool    tryContained = tryGet_contains(key);
+    bytes32 tryValue     = tryGet_value(key);
+    bytes32 value        = get@withrevert(key); // revert is not contained
+
+    assert contained == tryContained;
+    assert contained => tryValue == value;
+    assert !contained => tryValue == 0;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: set key-value in EnumerableMap                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule set(bytes32 key, bytes32 value, bytes32 otherKey) {
+    require sanity();
+
+    uint256 lengthBefore        = length();
+    bool    containsBefore      = contains(key);
+    bool    containsOtherBefore = contains(otherKey);
+    bytes32 otherValueBefore    = tryGet_value(otherKey);
+
+    bool added = set@withrevert(key, value);
+    bool success = !lastReverted;
+
+    assert success && contains(key) && get(key) == value,
+        "liveness & immediate effect";
+
+    assert added <=> !containsBefore,
+        "return value: added iff not contained";
+
+    assert length() == lengthBefore + to_mathint(added ? 1 : 0),
+        "effect: length increases iff added";
+
+    assert added => (key_at(lengthBefore) == key && value_at(lengthBefore) == value),
+        "effect: add at the end";
+
+    assert containsOtherBefore != contains(otherKey) => (added && key == otherKey),
+        "side effect: other keys are not affected";
+
+    assert otherValueBefore != tryGet_value(otherKey) => key == otherKey,
+        "side effect: values attached to other keys are not affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: remove key from EnumerableMap                                                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule remove(bytes32 key, bytes32 otherKey) {
+    requireInvariant consistencyKey(key);
+    requireInvariant consistencyKey(otherKey);
+
+    uint256 lengthBefore        = length();
+    bool    containsBefore      = contains(key);
+    bool    containsOtherBefore = contains(otherKey);
+    bytes32 otherValueBefore    = tryGet_value(otherKey);
+
+    bool removed = remove@withrevert(key);
+    bool success = !lastReverted;
+
+    assert success && !contains(key),
+        "liveness & immediate effect";
+
+    assert removed <=> containsBefore,
+        "return value: removed iff contained";
+
+    assert length() == lengthBefore - to_mathint(removed ? 1 : 0),
+        "effect: length decreases iff removed";
+
+    assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey),
+        "side effect: other keys are not affected";
+
+    assert otherValueBefore != tryGet_value(otherKey) => key == otherKey,
+        "side effect: values attached to other keys are not affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: when adding a new key, the other keys remain in set, at the same index.                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule setEnumerability(bytes32 key, bytes32 value, uint256 index) {
+    require sanity();
+
+    bytes32 atKeyBefore = key_at(index);
+    bytes32 atValueBefore = value_at(index);
+
+    set(key, value);
+
+    bytes32 atKeyAfter = key_at@withrevert(index);
+    assert !lastReverted;
+
+    bytes32 atValueAfter = value_at@withrevert(index);
+    assert !lastReverted;
+
+    assert atKeyAfter == atKeyBefore;
+    assert atValueAfter != atValueBefore => (
+        key == atKeyBefore &&
+        value == atValueAfter
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: when removing a existing key, the other keys remain in set, at the same index (except for the last one).      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule removeEnumerability(bytes32 key, uint256 index) {
+    uint256 last = length() - 1;
+
+    requireInvariant consistencyKey(key);
+    requireInvariant consistencyIndex(index);
+    requireInvariant consistencyIndex(last);
+
+    bytes32 atKeyBefore     = key_at(index);
+    bytes32 atValueBefore   = value_at(index);
+    bytes32 lastKeyBefore   = key_at(last);
+    bytes32 lastValueBefore = value_at(last);
+
+    remove(key);
+
+    // can't read last value & keys (length decreased)
+    bytes32 atKeyAfter = key_at@withrevert(index);
+    assert lastReverted <=> index == last;
+
+    bytes32 atValueAfter = value_at@withrevert(index);
+    assert lastReverted <=> index == last;
+
+    // One value that is allowed to change is if previous value was removed,
+    // in that case the last value before took its place.
+    assert (
+        index != last &&
+        atKeyBefore != atKeyAfter
+    ) => (
+        atKeyBefore == key &&
+        atKeyAfter == lastKeyBefore
+    );
+
+    assert (
+        index != last &&
+        atValueBefore != atValueAfter
+    ) => (
+        atValueAfter == lastValueBefore
+    );
+}

certora/specs/EnumerableSet.spec

@@ -0,0 +1,247 @@
+import "helpers/helpers.spec"
+
+methods {
+    // library
+    add(bytes32)      returns (bool)    envfree
+    remove(bytes32)   returns (bool)    envfree
+    contains(bytes32) returns (bool)    envfree
+    length()          returns (uint256) envfree
+    at_(uint256)      returns (bytes32) envfree
+
+    // FV
+    _indexOf(bytes32) returns (uint256) envfree
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function sanity() returns bool {
+    return length() < max_uint256;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: All indexed keys are contained                                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant indexedContained(uint256 index)
+    index < length() => contains(at_(index))
+    {
+        preserved {
+            requireInvariant consistencyIndex(index);
+            requireInvariant consistencyIndex(to_uint256(length() - 1));
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A value can only be stored at a single location                                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant atUniqueness(uint256 index1, uint256 index2)
+    index1 == index2 <=> at_(index1) == at_(index2)
+    {
+        preserved remove(bytes32 key) {
+            requireInvariant atUniqueness(index1, to_uint256(length() - 1));
+            requireInvariant atUniqueness(index2, to_uint256(length() - 1));
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: index <> key relationship is consistent                                                                  │
+│                                                                                                                     │
+│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another.  │
+│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are added  │
+│ and removed from the EnumerableSet).                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant consistencyIndex(uint256 index)
+    index < length() => _indexOf(at_(index)) == index + 1
+    {
+        preserved remove(bytes32 key) {
+            requireInvariant consistencyIndex(to_uint256(length() - 1));
+        }
+    }
+
+invariant consistencyKey(bytes32 key)
+    contains(key) => (
+        _indexOf(key) > 0 &&
+        _indexOf(key) <= length() &&
+        at_(to_uint256(_indexOf(key) - 1)) == key
+    )
+    {
+        preserved remove(bytes32 otherKey) {
+            requireInvariant consistencyKey(otherKey);
+            requireInvariant atUniqueness(
+                to_uint256(_indexOf(key) - 1),
+                to_uint256(_indexOf(otherKey) - 1)
+            );
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: state only changes by adding or removing elements                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateChange(env e, bytes32 key) {
+    require sanity();
+    requireInvariant consistencyKey(key);
+
+    uint256 lengthBefore   = length();
+    bool    containsBefore = contains(key);
+
+    method f;
+    calldataarg args;
+    f(e, args);
+
+    uint256 lengthAfter   = length();
+    bool    containsAfter = contains(key);
+
+    assert lengthBefore != lengthAfter => (
+        (f.selector == add(bytes32).selector    && lengthAfter == lengthBefore + 1) ||
+        (f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1)
+    );
+
+    assert containsBefore != containsAfter => (
+        (f.selector == add(bytes32).selector    && containsAfter) ||
+        (f.selector == remove(bytes32).selector && containsBefore)
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: check liveness of view functions.                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule liveness_1(bytes32 key) {
+    requireInvariant consistencyKey(key);
+
+    // contains never revert
+    contains@withrevert(key);
+    assert !lastReverted;
+}
+
+rule liveness_2(uint256 index) {
+    requireInvariant consistencyIndex(index);
+
+    // length never revert
+    uint256 length = length@withrevert();
+    assert !lastReverted;
+
+    // at reverts iff the index is out of bound
+    at_@withrevert(index);
+    assert !lastReverted <=> index < length;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: add key to EnumerableSet if not already contained                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule add(bytes32 key, bytes32 otherKey) {
+    require sanity();
+
+    uint256 lengthBefore        = length();
+    bool    containsBefore      = contains(key);
+    bool    containsOtherBefore = contains(otherKey);
+
+    bool added = add@withrevert(key);
+    bool success = !lastReverted;
+
+    assert success && contains(key),
+        "liveness & immediate effect";
+
+    assert added <=> !containsBefore,
+        "return value: added iff not contained";
+
+    assert length() == lengthBefore + to_mathint(added ? 1 : 0),
+        "effect: length increases iff added";
+
+    assert added => at_(lengthBefore) == key,
+        "effect: add at the end";
+
+    assert containsOtherBefore != contains(otherKey) => (added && key == otherKey),
+        "side effect: other keys are not affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: remove key from EnumerableSet if already contained                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule remove(bytes32 key, bytes32 otherKey) {
+    requireInvariant consistencyKey(key);
+    requireInvariant consistencyKey(otherKey);
+
+    uint256 lengthBefore        = length();
+    bool    containsBefore      = contains(key);
+    bool    containsOtherBefore = contains(otherKey);
+
+    bool removed = remove@withrevert(key);
+    bool success = !lastReverted;
+
+    assert success && !contains(key),
+        "liveness & immediate effect";
+
+    assert removed <=> containsBefore,
+        "return value: removed iff contained";
+
+    assert length() == lengthBefore - to_mathint(removed ? 1 : 0),
+        "effect: length decreases iff removed";
+
+    assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey),
+        "side effect: other keys are not affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: when adding a new key, the other keys remain in set, at the same index.                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule addEnumerability(bytes32 key, uint256 index) {
+    require sanity();
+
+    bytes32 atBefore = at_(index);
+    add(key);
+    bytes32 atAfter = at_@withrevert(index);
+    bool atAfterSuccess = !lastReverted;
+
+    assert atAfterSuccess;
+    assert atBefore == atAfter;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: when removing a existing key, the other keys remain in set, at the same index (except for the last one).      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule removeEnumerability(bytes32 key, uint256 index) {
+    uint256 last = length() - 1;
+
+    requireInvariant consistencyKey(key);
+    requireInvariant consistencyIndex(index);
+    requireInvariant consistencyIndex(last);
+
+    bytes32 atBefore = at_(index);
+    bytes32 lastBefore = at_(last);
+
+    remove(key);
+
+    // can't read last value (length decreased)
+    bytes32 atAfter = at_@withrevert(index);
+    assert lastReverted <=> index == last;
+
+    // One value that is allowed to change is if previous value was removed,
+    // in that case the last value before took its place.
+    assert (
+        index != last &&
+        atBefore != atAfter
+    ) => (
+        atBefore == key &&
+        atAfter == lastBefore
+    );
+}

certora/specs/GovernorBase.spec

@@ -1,333 +0,0 @@
-//////////////////////////////////////////////////////////////////////////////
-///////////////////// Governor.sol base definitions //////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
-    proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd
-    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
-    isExecuted(uint256) returns bool envfree
-    isCanceled(uint256) returns bool envfree
-    execute(address[], uint256[], bytes[], bytes32) returns uint256
-    hasVoted(uint256, address) returns bool
-    castVote(uint256, uint8) returns uint256
-    updateQuorumNumerator(uint256)
-    queue(address[], uint256[], bytes[], bytes32) returns uint256
-
-    // internal functions made public in harness:
-    _quorumReached(uint256) returns bool
-    _voteSucceeded(uint256) returns bool envfree
-
-    // function summarization
-    proposalThreshold() returns uint256 envfree
-
-    getVotes(address, uint256) returns uint256 => DISPATCHER(true)
-
-    getPastTotalSupply(uint256 t) returns uint256      => PER_CALLEE_CONSTANT
-    getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT
-
-    //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
-    //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
-}
-
-//////////////////////////////////////////////////////////////////////////////
-//////////////////////////////// Definitions /////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-// proposal was created - relation proved in noStartBeforeCreation
-definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////// Helper Functions ///////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
-    address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash;
-    uint8 support; uint8 v; bytes32 r; bytes32 s;
-	if (f.selector == propose(address[], uint256[], bytes[], string).selector) {
-		uint256 result = propose@withrevert(e, targets, values, calldatas, reason);
-        require(result == proposalId);
-	} else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) {
-		uint256 result = execute@withrevert(e, targets, values, calldatas, descriptionHash);
-        require(result == proposalId);
-	} else if (f.selector == castVote(uint256, uint8).selector) {
-		castVote@withrevert(e, proposalId, support);
-	} else if  (f.selector == castVoteWithReason(uint256, uint8, string).selector) {
-        castVoteWithReason@withrevert(e, proposalId, support, reason);
-	} else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) {
-		castVoteBySig@withrevert(e, proposalId, support, v, r, s);
-    } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) {
-        queue@withrevert(e, targets, values, calldatas, descriptionHash);
-	} else {
-        calldataarg args;
-        f@withrevert(e, args);
-    }
-}
-
-/*
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
- ///////////////////////////////////////////////////// State Diagram //////////////////////////////////////////////////////////
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
- //                                                                                                                          //
- //                                                                castVote(s)()                                             //
- //  -------------  propose()  ----------------------  time pass  ---------------       time passes         -----------      //
- // | No Proposal | --------> | Before Start (Delay) | --------> | Voting Period | ----------------------> | execute() |     //
- //  -------------             ----------------------             --------------- -> Executed/Canceled      -----------      //
- //  ------------------------------------------------------------|---------------|-------------------------|-------------->  //
- // t                                                          start            end                     timelock             //
- //                                                                                                                          //
- //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-*/
-
-
-///////////////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// Global Valid States /////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * Start and end date are either initialized (non zero) or uninitialized (zero) simultaneously
- * This invariant assumes that the block number cannot be 0 at any stage of the contract cycle
- * This is very safe assumption as usually the 0 block is genesis block which is uploaded with data
- * by the developers and will not be valid to raise proposals (at the current way that block chain is functioning)
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant startAndEndDatesNonZero(uint256 pId)
-        proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0
-        { preserved with (env e){
-                require e.block.number > 0;
-        }}
-
-
-/*
- * If a proposal is canceled it must have a start and an end date
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant canceledImplyStartAndEndDateNonZero(uint pId)
-        isCanceled(pId) => proposalSnapshot(pId) != 0
-        {preserved with (env e){
-                require e.block.number > 0;
-        }}
-
-
-/*
- * If a proposal is executed it must have a start and an end date
- */
- // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
-invariant executedImplyStartAndEndDateNonZero(uint pId)
-        isExecuted(pId) => proposalSnapshot(pId) != 0
-        { preserved with (env e){
-            requireInvariant startAndEndDatesNonZero(pId);
-            require e.block.number > 0;
-        }}
-
-
-/*
- * A proposal starting block number must be less or equal than the proposal end date
- */
-invariant voteStartBeforeVoteEnd(uint256 pId)
-        // from < to <= because snapshot and deadline can be the same block number if delays are set to 0
-        // This is possible before the integration of GovernorSettings.sol to the system.
-        // After integration of GovernorSettings.sol the invariant expression should be changed from <= to <
-        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) <= proposalDeadline(pId))
-        // (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) <= proposalDeadline(pId))
-        { preserved {
-            requireInvariant startAndEndDatesNonZero(pId);
-        }}
-
-
-/*
- * A proposal cannot be both executed and canceled simultaneously.
- */
-invariant noBothExecutedAndCanceled(uint256 pId)
-        !isExecuted(pId) || !isCanceled(pId)
-
-
-/*
- * A proposal could be executed only if quorum was reached and vote succeeded
- */
-rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){
-    bool isExecutedBefore = isExecuted(pId);
-    bool quorumReachedBefore = _quorumReached(e, pId);
-    bool voteSucceededBefore = _voteSucceeded(pId);
-
-    calldataarg args;
-    f(e, args);
-
-    bool isExecutedAfter = isExecuted(pId);
-    assert (!isExecutedBefore && isExecutedAfter) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed";
-}
-
-///////////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////// In-State Rules /////////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-//==========================================
-//------------- Voting Period --------------
-//==========================================
-
-/*
- * A user cannot vote twice
- */
- // Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on
- // the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute.
- // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
- // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
- // We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete
- // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
-rule doubleVoting(uint256 pId, uint8 sup, method f) {
-    env e;
-    address user = e.msg.sender;
-    bool votedCheck = hasVoted(e, pId, user);
-
-    castVote@withrevert(e, pId, sup);
-
-    assert votedCheck => lastReverted, "double voting occurred";
-}
-
-
-///////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////// State Transitions Rules //////////////////////////////////
-///////////////////////////////////////////////////////////////////////////////////////
-
-//===========================================
-//-------- Propose() --> End of Time --------
-//===========================================
-
-
-/*
- * Once a proposal is created, voteStart and voteEnd are immutable
- */
-rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
-    uint256 _voteStart = proposalSnapshot(pId);
-    uint256 _voteEnd = proposalDeadline(pId);
-
-    require proposalCreated(pId); // startDate > 0
-
-    env e; calldataarg arg;
-    f(e, arg);
-
-    uint256 voteStart_ = proposalSnapshot(pId);
-    uint256 voteEnd_ = proposalDeadline(pId);
-    assert _voteStart == voteStart_, "Start date was changed";
-    assert _voteEnd == voteEnd_, "End date was changed";
-}
-
-
-/*
- * Voting cannot start at a block number prior to proposal’s creation block number
- */
-rule noStartBeforeCreation(uint256 pId) {
-    uint256 previousStart = proposalSnapshot(pId);
-    // This line makes sure that we see only cases where start date is changed from 0, i.e. creation of proposal
-    // We proved in immutableFieldsAfterProposalCreation that once dates set for proposal, it cannot be changed
-    require !proposalCreated(pId); // previousStart == 0;
-
-    env e; calldataarg args;
-    propose(e, args);
-
-    uint256 newStart = proposalSnapshot(pId);
-    // if created, start is after current block number (creation block)
-    assert(newStart != previousStart => newStart >= e.block.number);
-}
-
-
-//============================================
-//--- End of Voting Period --> End of Time ---
-//============================================
-
-
-/*
- * A proposal can neither be executed nor canceled before it ends
- */
- // By induction it cannot be executed nor canceled before it starts, due to voteStartBeforeVoteEnd
-rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
-    require !isExecuted(pId) && !isCanceled(pId);
-
-    env e; calldataarg args;
-    f(e, args);
-
-    assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline";
-}
-
-////////////////////////////////////////////////////////////////////////////////
-////////////////////// Integrity Of Functions (Unit Tests) /////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////// High Level Rules ////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////////////
-///////////////////////////// Not Categorized Yet //////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * All proposal specific (non-view) functions should revert if proposal is executed
- */
- // In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID,
- // non of the proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc
- // we connected the executed attribute to the execute() function, showing that only execute() can
- // change it, and that it will always change it.
-rule allFunctionsRevertIfExecuted(method f) filtered { f ->
-    !f.isView && !f.isFallback
-      && f.selector != updateTimelock(address).selector
-      && f.selector != updateQuorumNumerator(uint256).selector
-      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
-      && f.selector != relay(address,uint256,bytes).selector
-      && f.selector != 0xb9a61961 // __acceptAdmin()
-} {
-    env e; calldataarg args;
-    uint256 pId;
-    require(isExecuted(pId));
-    requireInvariant noBothExecutedAndCanceled(pId);
-    requireInvariant executedImplyStartAndEndDateNonZero(pId);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    assert(lastReverted, "Function was not reverted");
-}
-
-/*
- * All proposal specific (non-view) functions should revert if proposal is canceled
- */
-rule allFunctionsRevertIfCanceled(method f) filtered {
-    f -> !f.isView && !f.isFallback
-      && f.selector != updateTimelock(address).selector
-      && f.selector != updateQuorumNumerator(uint256).selector
-      && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
-      && f.selector != relay(address,uint256,bytes).selector
-      && f.selector != 0xb9a61961 // __acceptAdmin()
-} {
-    env e; calldataarg args;
-    uint256 pId;
-    require(isCanceled(pId));
-    requireInvariant noBothExecutedAndCanceled(pId);
-    requireInvariant canceledImplyStartAndEndDateNonZero(pId);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    assert(lastReverted, "Function was not reverted");
-}
-
-/*
- * Proposal can be switched to executed only via execute() function
- */
-rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) {
-    env e; calldataarg args;
-    uint256 pId;
-    bool executedBefore = isExecuted(pId);
-    require(!executedBefore);
-
-    helperFunctionsWithRevert(pId, f, e);
-
-    bool executedAfter = isExecuted(pId);
-    assert(executedAfter != executedBefore => f.selector == execute(address[], uint256[], bytes[], bytes32).selector, "isExecuted only changes in the execute method");
-}

certora/specs/GovernorCountingSimple.spec

@@ -1,221 +0,0 @@
-import "GovernorBase.spec"
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
-
-    quorum(uint256) returns uint256
-    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
-
-    quorumNumerator() returns uint256
-    _executor() returns address
-
-    erc20votes._getPastVotes(address, uint256) returns uint256
-
-    getExecutor() returns address
-
-    timelock() returns address
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// GHOSTS /////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//////////// ghosts to keep track of votes counting ////////////
-
-/*
- * the sum of voting power of those who voted
- */
-ghost sum_all_votes_power() returns uint256 {
-	init_state axiom sum_all_votes_power() == 0;
-}
-
-hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
-	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
-}
-
-/*
- * sum of all votes casted per proposal
- */
-ghost tracked_weight(uint256) returns uint256 {
-	init_state axiom forall uint256 p. tracked_weight(p) == 0;
-}
-
-/*
- * sum of all votes casted
- */
-ghost sum_tracked_weight() returns uint256 {
-	init_state axiom sum_tracked_weight() == 0;
-}
-
-/*
- * getter for _proposalVotes.againstVotes
- */
-ghost votesAgainst() returns uint256 {
-    init_state axiom votesAgainst() == 0;
-}
-
-/*
- * getter for _proposalVotes.forVotes
- */
-ghost votesFor() returns uint256 {
-    init_state axiom votesFor() == 0;
-}
-
-/*
- * getter for _proposalVotes.abstainVotes
- */
-ghost votesAbstain() returns uint256 {
-    init_state axiom votesAbstain() == 0;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-////////////////////////////// INVARIANTS ////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal
- */
-invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId) 
-	tracked_weight(pId) == ghost_sum_vote_power_by_id(pId)
-
-
-/*
- * sum of all votes casted is equal to the sum of voting power of those who voted
- */
-invariant SumOfVotesCastEqualSumOfPowerOfVoted() 
-	sum_tracked_weight() == sum_all_votes_power()
-
-
-/*
-* sum of all votes casted is greater or equal to the sum of voting power of those who voted at a specific proposal
-*/
-invariant OneIsNotMoreThanAll(uint256 pId) 
-	sum_all_votes_power() >= tracked_weight(pId)
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// RULES //////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-/*
- * Only sender's voting status can be changed by execution of any cast vote function
- */
-// Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on
- // the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute.
- // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
- // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
- // We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete 
- // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
-rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) {
-    env e; calldataarg args;
-
-    address voter = e.msg.sender;
-    address user;
-
-    bool hasVotedBefore_User = hasVoted(e, pId, user);
-
-    castVote@withrevert(e, pId, sup);
-    require(!lastReverted);
-
-    bool hasVotedAfter_User = hasVoted(e, pId, user);
-
-    assert user != voter => hasVotedBefore_User == hasVotedAfter_User;
-}
-
-
-/*
-* Total voting tally is monotonically non-decreasing in every operation 
-*/
-rule votingWeightMonotonicity(method f){
-    uint256 votingWeightBefore = sum_tracked_weight();
-
-    env e; 
-    calldataarg args;
-    f(e, args);
-
-    uint256 votingWeightAfter = sum_tracked_weight();
-
-    assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow";
-}
-
-
-/*
-* A change in hasVoted must be correlated with an non-decreasing of the vote supports (nondecrease because user can vote with weight 0)
-*/
-rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
-    address acc = e.msg.sender;
-    
-    uint256 againstBefore = votesAgainst();
-    uint256 forBefore = votesFor();
-    uint256 abstainBefore = votesAbstain();
-
-    bool hasVotedBefore = hasVoted(e, pId, acc);
-
-    helperFunctionsWithRevert(pId, f, e);
-    require(!lastReverted);
-
-    uint256 againstAfter = votesAgainst();
-    uint256 forAfter = votesFor();
-    uint256 abstainAfter = votesAbstain();
-    
-    bool hasVotedAfter = hasVoted(e, pId, acc);
-
-    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
-}
-
-
-/*
-* Only privileged users can execute privileged operations, e.g. change _quorumNumerator or _timelock
-*/
-rule privilegedOnlyNumerator(method f, uint256 newQuorumNumerator){
-    env e;
-    calldataarg arg;
-    uint256 quorumNumBefore = quorumNumerator(e);
-
-    f(e, arg);
-
-    uint256 quorumNumAfter = quorumNumerator(e);
-    address executorCheck = getExecutor(e);
-
-    assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non privileged user changed quorum numerator";
-}
-
-rule privilegedOnlyTimelock(method f, uint256 newQuorumNumerator){
-    env e;
-    calldataarg arg;
-    uint256 timelockBefore = timelock(e);
-
-    f(e, arg);
-
-    uint256 timelockAfter = timelock(e);
-
-    assert timelockBefore != timelockAfter => e.msg.sender == timelockBefore, "non privileged user changed timelock";
-}

certora/specs/Initializable.spec

@@ -0,0 +1,165 @@
+import "helpers/helpers.spec"
+
+methods {
+    // initialize, reinitialize, disable
+    initialize()        envfree
+    reinitialize(uint8) envfree
+    disable()           envfree
+
+    nested_init_init()            envfree
+    nested_init_reinit(uint8)       envfree
+    nested_reinit_init(uint8)       envfree
+    nested_reinit_reinit(uint8,uint8) envfree
+
+    // view
+    version()      returns uint8 envfree
+    initializing() returns bool  envfree
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition isUninitialized() returns bool = version() == 0;
+definition isInitialized()   returns bool = version() > 0;
+definition isDisabled()      returns bool = version() == 255;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A contract must only ever be in an initializing state while in the middle of a transaction execution.    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant notInitializing()
+    !initializing()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: The version cannot decrease & disable state is irrevocable.                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule increasingVersion(env e) {
+    uint8 versionBefore = version();
+    bool disabledBefore = isDisabled();
+
+    method f; calldataarg args;
+    f(e, args);
+
+    assert versionBefore <= version(), "_initialized must only increase";
+    assert disabledBefore => isDisabled(), "a disabled initializer must stay disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot initialize a contract that is already initialized.                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotInitializeTwice() {
+    require isInitialized();
+
+    initialize@withrevert();
+
+    assert lastReverted, "contract must only be initialized once";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot initialize once disabled.                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotInitializeOnceDisabled() {
+    require isDisabled();
+
+    initialize@withrevert();
+
+    assert lastReverted, "contract is disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot reinitialize once disabled.                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotReinitializeOnceDisabled() {
+    require isDisabled();
+
+    uint8 n;
+    reinitialize@withrevert(n);
+
+    assert lastReverted, "contract is disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot nest initializers (after construction).                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotNestInitializers_init_init() {
+    nested_init_init@withrevert();
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_init_reinit(uint8 m) {
+    nested_init_reinit@withrevert(m);
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_reinit_init(uint8 n) {
+    nested_reinit_init@withrevert(n);
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) {
+    nested_reinit_reinit@withrevert(n, m);
+    assert lastReverted, "nested initializers";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Initialize correctly sets the version.                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule initializeEffects() {
+    requireInvariant notInitializing();
+
+    bool isUninitializedBefore = isUninitialized();
+
+    initialize@withrevert();
+    bool success = !lastReverted;
+
+    assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts";
+    assert success => version() == 1,         "initialize must set version() to 1";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Reinitialize correctly sets the version.                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule reinitializeEffects() {
+    requireInvariant notInitializing();
+
+    uint8 versionBefore = version();
+
+    uint8 n;
+    reinitialize@withrevert(n);
+    bool success = !lastReverted;
+
+    assert success <=> versionBefore < n, "can only reinitialize to a latter versions";
+    assert success => version() == n,     "reinitialize must set version() to n";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Can disable.                                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule disableEffect() {
+    requireInvariant notInitializing();
+
+    disable@withrevert();
+    bool success = !lastReverted;
+
+    assert success,      "call to _disableInitializers failed";
+    assert isDisabled(), "disable state not set";
+}

certora/specs/Ownable.spec

@@ -0,0 +1,78 @@
+import "helpers/helpers.spec"
+import "methods/IOwnable.spec"
+
+methods {
+    restricted()
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: transferOwnership changes ownership                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferOwnership(env e) {
+    require nonpayable(e);
+
+    address newOwner;
+    address current = owner();
+
+    transferOwnership@withrevert(e, newOwner);
+    bool success = !lastReverted;
+
+    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
+    assert success => owner() == newOwner, "current owner changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceOwnership removes the owner                                                           │
+
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceOwnership(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    renounceOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => owner() == 0, "owner not cleared";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Access control: only current owner can call restricted functions                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    calldataarg args;
+    restricted@withrevert(e, args);
+
+    assert !lastReverted <=> e.msg.sender == current, "access control failed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: ownership can only change in specific ways                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
+    address oldCurrent = owner();
+
+    method f; calldataarg args;
+    f(e, args);
+
+    address newCurrent = owner();
+
+    // If owner changes, must be either transferOwnership or renounceOwnership
+    assert oldCurrent != newCurrent => (
+        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == transferOwnership(address).selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == renounceOwnership().selector)
+    );
+}

certora/specs/Ownable2Step.spec

@@ -0,0 +1,108 @@
+import "helpers/helpers.spec"
+import "methods/IOwnable2Step.spec"
+
+methods {
+    restricted()
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: transferOwnership sets the pending owner                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferOwnership(env e) {
+    require nonpayable(e);
+
+    address newOwner;
+    address current = owner();
+
+    transferOwnership@withrevert(e, newOwner);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => pendingOwner() == newOwner, "pending owner not set";
+    assert success => owner() == current, "current owner changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceOwnership removes the owner and the pendingOwner                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceOwnership(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    renounceOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => pendingOwner() == 0, "pending owner not cleared";
+    assert success => owner() == 0, "owner not cleared";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: acceptOwnership changes owner and reset pending owner                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule acceptOwnership(env e) {
+
+    require nonpayable(e);
+
+    address current = owner();
+    address pending = pendingOwner();
+
+    acceptOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == pending, "unauthorized caller";
+    assert success => pendingOwner() == 0, "pending owner not cleared";
+    assert success => owner() == pending, "owner not transferred";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Access control: only current owner can call restricted functions                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    calldataarg args;
+    restricted@withrevert(e, args);
+
+    assert !lastReverted <=> e.msg.sender == current, "access control failed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: ownership and pending ownership can only change in specific ways                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule ownerOrPendingOwnerChange(env e, method f) {
+    address oldCurrent = owner();
+    address oldPending = pendingOwner();
+
+    calldataarg args;
+    f(e, args);
+
+    address newCurrent = owner();
+    address newPending = pendingOwner();
+
+    // If owner changes, must be either acceptOwnership or renounceOwnership
+    assert oldCurrent != newCurrent => (
+        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
+    );
+
+    // If pending changes, must be either acceptance or reset
+    assert oldPending != newPending => (
+        (e.msg.sender == oldCurrent && newCurrent == oldCurrent &&                    f.selector == transferOwnership(address).selector) ||
+        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
+    );
+}

certora/specs/Pausable.spec

@@ -0,0 +1,96 @@
+import "helpers/helpers.spec"
+
+methods {
+    paused() returns (bool) envfree
+    pause()
+    unpause()
+    onlyWhenPaused()
+    onlyWhenNotPaused()
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: _pause pauses the contract                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pause(env e) {
+    require nonpayable(e);
+
+    bool pausedBefore = paused();
+
+    pause@withrevert(e);
+    bool success = !lastReverted;
+
+    bool pausedAfter = paused();
+
+    // liveness
+    assert success <=> !pausedBefore, "works if and only if the contract was not paused before";
+
+    // effect
+    assert success => pausedAfter, "contract must be paused after a successful call";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: _unpause unpauses the contract                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule unpause(env e) {
+    require nonpayable(e);
+
+    bool pausedBefore = paused();
+
+    unpause@withrevert(e);
+    bool success = !lastReverted;
+
+    bool pausedAfter = paused();
+
+    // liveness
+    assert success <=> pausedBefore, "works if and only if the contract was paused before";
+
+    // effect
+    assert success => !pausedAfter, "contract must be unpaused after a successful call";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: whenPaused modifier can only be called if the contract is paused                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule whenPaused(env e) {
+    require nonpayable(e);
+
+    onlyWhenPaused@withrevert(e);
+    assert !lastReverted <=> paused(), "works if and only if the contract is paused";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule whenNotPaused(env e) {
+    require nonpayable(e);
+
+    onlyWhenNotPaused@withrevert(e);
+    assert !lastReverted <=> !paused(), "works if and only if the contract is not paused";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only _pause and _unpause can change paused status                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noPauseChange(env e) {
+    method f;
+    calldataarg args;
+
+    bool pausedBefore = paused();
+    f(e, args);
+    bool pausedAfter = paused();
+
+    assert pausedBefore != pausedAfter => (
+        (!pausedAfter && f.selector == unpause().selector) ||
+        (pausedAfter && f.selector == pause().selector)
+    ), "contract's paused status can only be changed by _pause() or _unpause()";
+}

certora/specs/RulesInProgress.spec

@@ -1,139 +0,0 @@
-//////////////////////////////////////////////////////////////////////////////
-////////////// THIS SPEC IS A RESERVE FOR NOT IN PROGRESS //////////////
-//////////////////////////////////////////////////////////////////////////////
-
-import "GovernorBase.spec"
-
-using ERC20VotesHarness as erc20votes
-
-methods {
-    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
-
-    quorum(uint256) returns uint256
-    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
-
-    quorumNumerator() returns uint256
-    _executor() returns address
-
-    erc20votes._getPastVotes(address, uint256) returns uint256
-
-    getExecutor() returns address
-
-    timelock() returns address
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// GHOSTS /////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//////////// ghosts to keep track of votes counting ////////////
-
-/*
- * the sum of voting power of those who voted
- */
-ghost sum_all_votes_power() returns uint256 {
-	init_state axiom sum_all_votes_power() == 0;
-}
-
-hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
-	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
-}
-
-/*
- * sum of all votes casted per proposal
- */
-ghost tracked_weight(uint256) returns uint256 {
-	init_state axiom forall uint256 p. tracked_weight(p) == 0;
-}
-
-/*
- * sum of all votes casted
- */
-ghost sum_tracked_weight() returns uint256 {
-	init_state axiom sum_tracked_weight() == 0;
-}
-
-/*
- * getter for _proposalVotes.againstVotes
- */
-ghost votesAgainst() returns uint256 {
-    init_state axiom votesAgainst() == 0;
-}
-
-/*
- * getter for _proposalVotes.forVotes
- */
-ghost votesFor() returns uint256 {
-    init_state axiom votesFor() == 0;
-}
-
-/*
- * getter for _proposalVotes.abstainVotes
- */
-ghost votesAbstain() returns uint256 {
-    init_state axiom votesAbstain() == 0;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
-}
-
-hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
-	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
-	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
-	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
-    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-////////////////////////////// INVARIANTS ////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-
-//////////////////////////////////////////////////////////////////////////////
-///////////////////////////////// RULES //////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////
-
-
-//NOT FINISHED
-/*
-* the sum of voting power of those who voted is less or equal to the maximum possible votes, per each proposal
-*/
-rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
-
-    // add requireinvariant  for all i, j. i = i - 1 && i < j => checkpointlookup[i] < checkpointlookup[j];
-    require tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId));
-
-    uint256 againstB;
-    uint256 forB;
-    uint256 absatinB;
-    againstB, forB, absatinB = proposalVotes(pId);
-
-    calldataarg args;
-    //f(e, args);
-
-    castVote(e, pId, sup);
-
-    uint256 against;
-    uint256 for;
-    uint256 absatin;
-    against, for, absatin = proposalVotes(pId);
-
-    uint256 ps = proposalSnapshot(pId);
-
-    assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
-}

certora/specs/TimelockController.spec

@@ -0,0 +1,275 @@
+import "helpers/helpers.spec"
+import "methods/IAccessControl.spec"
+
+methods {
+    TIMELOCK_ADMIN_ROLE()       returns (bytes32) envfree
+    PROPOSER_ROLE()             returns (bytes32) envfree
+    EXECUTOR_ROLE()             returns (bytes32) envfree
+    CANCELLER_ROLE()            returns (bytes32) envfree
+    isOperation(bytes32)        returns (bool)    envfree
+    isOperationPending(bytes32) returns (bool)    envfree
+    isOperationReady(bytes32)   returns (bool)
+    isOperationDone(bytes32)    returns (bool)    envfree
+    getTimestamp(bytes32)       returns (uint256) envfree
+    getMinDelay()               returns (uint256) envfree
+
+    hashOperation(address, uint256, bytes, bytes32, bytes32)            returns(bytes32) envfree
+    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree
+
+    schedule(address, uint256, bytes, bytes32, bytes32, uint256)
+    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256)
+    execute(address, uint256, bytes, bytes32, bytes32)
+    executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
+    cancel(bytes32)
+
+    updateDelay(uint256)
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+// Uniformly handle scheduling of batched and non-batched operations.
+function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
+    if (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) {
+        address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
+        require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
+        schedule@withrevert(e, target, value, data, predecessor, salt, delay);
+    } else if (f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) {
+        address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt;
+        require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
+        scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay);
+    } else {
+        calldataarg args;
+        f@withrevert(e, args);
+    }
+}
+
+// Uniformly handle execution of batched and non-batched operations.
+function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) {
+    if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) {
+        address target; uint256 value; bytes data; bytes32 salt;
+        require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
+        execute@withrevert(e, target, value, data, predecessor, salt);
+    } else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
+        address[] targets; uint256[] values; bytes[] payloads; bytes32 salt;
+        require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
+        executeBatch@withrevert(e, targets, values, payloads, predecessor, salt);
+    } else {
+        calldataarg args;
+        f@withrevert(e, args);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition DONE_TIMESTAMP()      returns uint256 = 1;
+definition UNSET()               returns uint8   = 0x1;
+definition PENDING()             returns uint8   = 0x2;
+definition DONE()                returns uint8   = 0x4;
+
+definition isUnset(bytes32 id)   returns bool    = !isOperation(id);
+definition isPending(bytes32 id) returns bool    = isOperationPending(id);
+definition isDone(bytes32 id)    returns bool    = isOperationDone(id);
+definition state(bytes32 id)     returns uint8   = (isUnset(id) ? UNSET() : 0) | (isPending(id) ? PENDING() : 0) | (isDone(id) ? DONE() : 0);
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariants: consistency of accessors                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant isOperationCheck(bytes32 id)
+    isOperation(id) <=> getTimestamp(id) > 0
+    filtered { f -> !f.isView }
+
+invariant isOperationPendingCheck(bytes32 id)
+    isOperationPending(id) <=> getTimestamp(id) > DONE_TIMESTAMP()
+    filtered { f -> !f.isView }
+
+invariant isOperationDoneCheck(bytes32 id)
+    isOperationDone(id) <=> getTimestamp(id) == DONE_TIMESTAMP()
+    filtered { f -> !f.isView }
+
+invariant isOperationReadyCheck(env e, bytes32 id)
+    isOperationReady(e, id) <=> (isOperationPending(id) && getTimestamp(id) <= e.block.timestamp)
+    filtered { f -> !f.isView }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: a proposal id is either unset, pending or done                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant stateConsistency(bytes32 id, env e)
+    // Check states are mutually exclusive
+    (isUnset(id)   <=> (!isPending(id) && !isDone(id)   )) &&
+    (isPending(id) <=> (!isUnset(id)   && !isDone(id)   )) &&
+    (isDone(id)    <=> (!isUnset(id)   && !isPending(id))) &&
+    // Check that the state helper behaves as expected:
+    (isUnset(id)   <=> state(id) == UNSET()              ) &&
+    (isPending(id) <=> state(id) == PENDING()            ) &&
+    (isDone(id)    <=> state(id) == DONE()               ) &&
+    // Check substate
+    isOperationReady(e, id) => isPending(id)
+    filtered { f -> !f.isView }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: state transition rules                                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateTransition(bytes32 id, env e, method f, calldataarg args) {
+    require e.block.timestamp > 1; // Sanity
+
+    uint8 stateBefore = state(id);
+    f(e, args);
+    uint8 stateAfter = state(id);
+
+    // Cannot jump from UNSET to DONE
+    assert stateBefore == UNSET() => stateAfter != DONE();
+
+    // UNSET → PENDING: schedule or scheduleBatch
+    assert stateBefore == UNSET() && stateAfter == PENDING() => (
+        f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
+        f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
+    );
+
+    // PENDING → UNSET: cancel
+    assert stateBefore == PENDING() && stateAfter == UNSET() => (
+        f.selector == cancel(bytes32).selector
+    );
+
+    // PENDING → DONE: execute or executeBatch
+    assert stateBefore == PENDING() && stateAfter == DONE() => (
+        f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector ||
+        f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
+    );
+
+    // DONE is final
+    assert stateBefore == DONE() => stateAfter == DONE();
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: minimum delay can only be updated through a timelock execution                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule minDelayOnlyChange(env e) {
+    uint256 delayBefore = getMinDelay();
+
+    method f; calldataarg args;
+    f(e, args);
+
+    assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == updateDelay(uint256).selector), "Unauthorized delay update";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: schedule liveness and effects                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
+    f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
+    f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
+} {
+    require nonpayable(e);
+
+    // Basic timestamp assumptions
+    require e.block.timestamp > 1;
+    require e.block.timestamp + delay < max_uint256;
+    require e.block.timestamp + getMinDelay() < max_uint256;
+
+    bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
+
+    uint8 stateBefore       = state(id);
+    bool  isDelaySufficient = delay >= getMinDelay();
+    bool  isProposerBefore  = hasRole(PROPOSER_ROLE(), e.msg.sender);
+
+    helperScheduleWithRevert(e, f, id, delay);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        stateBefore == UNSET() &&
+        isDelaySufficient &&
+        isProposerBefore
+    );
+
+    // effect
+    assert success => state(id) == PENDING(), "State transition violation";
+    assert success => getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set";
+
+    // no side effect
+    assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: execute liveness and effects                                                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
+    f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector ||
+    f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
+} {
+    bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
+
+    uint8 stateBefore            = state(id);
+    bool  isOperationReadyBefore = isOperationReady(e, id);
+    bool  isExecutorOrOpen       = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0);
+    bool  predecessorDependency  = predecessor == 0 || isDone(predecessor);
+
+    helperExecuteWithRevert(e, f, id, predecessor);
+    bool success = !lastReverted;
+
+    // The underlying transaction can revert, and that would cause the execution to revert. We can check that all non
+    // reverting calls meet the requirements in terms of proposal readiness, access control and predecessor dependency.
+    // We can't however guarantee that these requirements being meet ensure liveness of the proposal, because the
+    // proposal can revert for reasons beyond our control.
+
+    // liveness, should be `<=>` but can only check `=>` (see comment above)
+    assert success => (
+        stateBefore == PENDING() &&
+        isOperationReadyBefore &&
+        predecessorDependency &&
+        isExecutorOrOpen
+    );
+
+    // effect
+    assert success => state(id) == DONE(), "State transition violation";
+
+    // no side effect
+    assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: cancel liveness and effects                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cancel(env e, bytes32 id) {
+    require nonpayable(e);
+
+    bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
+
+    uint8 stateBefore = state(id);
+    bool  isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender);
+
+    cancel@withrevert(e, id);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        stateBefore == PENDING() &&
+        isCanceller
+    );
+
+    // effect
+    assert success => state(id) == UNSET(), "State transition violation";
+
+    // no side effect
+    assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
+}

certora/specs/helpers/helpers.spec

@@ -0,0 +1 @@
+definition nonpayable(env e) returns bool = e.msg.value == 0;

certora/specs/methods/IAccessControl.spec

@@ -0,0 +1,7 @@
+methods {
+    hasRole(bytes32, address) returns(bool) envfree
+    getRoleAdmin(bytes32) returns(bytes32) envfree
+    grantRole(bytes32, address)
+    revokeRole(bytes32, address)
+    renounceRole(bytes32, address)
+}

certora/specs/methods/IAccessControlDefaultAdminRules.spec

@@ -0,0 +1,36 @@
+import "./IERC5313.spec"
+
+methods {
+    // === View ==
+    
+    // Default Admin
+    defaultAdmin() returns(address) envfree
+    pendingDefaultAdmin() returns(address, uint48) envfree
+    
+    // Default Admin Delay
+    defaultAdminDelay() returns(uint48)
+    pendingDefaultAdminDelay() returns(uint48, uint48)
+    defaultAdminDelayIncreaseWait() returns(uint48) envfree
+    
+    // === Mutations ==
+
+    // Default Admin
+    beginDefaultAdminTransfer(address)
+    cancelDefaultAdminTransfer()
+    acceptDefaultAdminTransfer()
+
+    // Default Admin Delay
+    changeDefaultAdminDelay(uint48)
+    rollbackDefaultAdminDelay()
+
+    // == FV ==
+    
+    // Default Admin
+    pendingDefaultAdmin_() returns (address) envfree
+    pendingDefaultAdminSchedule_() returns (uint48) envfree
+    
+    // Default Admin Delay
+    pendingDelay_() returns (uint48)
+    pendingDelaySchedule_() returns (uint48)
+    delayChangeWait_(uint48) returns (uint48)
+}

certora/specs/methods/IERC20.spec

@@ -0,0 +1,11 @@
+methods {
+    name()                                returns (string)  envfree => DISPATCHER(true)
+    symbol()                              returns (string)  envfree => DISPATCHER(true)
+    decimals()                            returns (uint8)   envfree => DISPATCHER(true)
+    totalSupply()                         returns (uint256) envfree => DISPATCHER(true)
+    balanceOf(address)                    returns (uint256) envfree => DISPATCHER(true)
+    allowance(address,address)            returns (uint256) envfree => DISPATCHER(true)
+    approve(address,uint256)              returns (bool)            => DISPATCHER(true)
+    transfer(address,uint256)             returns (bool)            => DISPATCHER(true)
+    transferFrom(address,address,uint256) returns (bool)            => DISPATCHER(true)
+}

certora/specs/methods/IERC2612.spec

@@ -0,0 +1,5 @@
+methods {
+    permit(address,address,uint256,uint256,uint8,bytes32,bytes32) => DISPATCHER(true)
+    nonces(address)    returns (uint256) envfree                  => DISPATCHER(true)
+    DOMAIN_SEPARATOR() returns (bytes32) envfree                  => DISPATCHER(true)
+}

certora/specs/methods/IERC3156.spec

@@ -0,0 +1,5 @@
+methods {
+    maxFlashLoan(address)                    returns (uint256) envfree => DISPATCHER(true)
+    flashFee(address,uint256)                returns (uint256) envfree => DISPATCHER(true)
+    flashLoan(address,address,uint256,bytes) returns (bool)            => DISPATCHER(true)
+}