Merge branch 'master' into feat/access-manager

.changeset/clever-bats-kick.md

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

.changeset/green-pumpkins-end.md

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

.changeset/six-frogs-turn.md

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

.changeset/wet-bears-heal.md

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

.github/actions/setup/action.yml

@@ -5,7 +5,7 @@ runs:
   steps:
     - uses: actions/setup-node@v3
       with:
-        node-version: 14.x
+        node-version: 16.x
     - uses: actions/cache@v3
       id: cache
       with:

.github/workflows/actionlint.yml

@@ -9,7 +9,7 @@ jobs:
   lint:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Add problem matchers
         run: |
           # https://github.com/rhysd/actionlint/blob/3a2f2c7/docs/usage.md#problem-matchers

.github/workflows/changeset.yml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-latest
     if: ${{ !contains(github.event.pull_request.labels.*.name, 'ignore-changeset') }}
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0 # Include history so Changesets finds merge-base
       - name: Set up environment

.github/workflows/checks.yml

@@ -20,7 +20,7 @@ jobs:
   lint:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - run: npm run lint
@@ -31,7 +31,7 @@ jobs:
       FORCE_COLOR: 1
       GAS: true
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - name: Run tests and generate gas report
@@ -51,7 +51,7 @@ jobs:
     env:
       FORCE_COLOR: 1
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0 # Include history so patch conflicts are resolved automatically
       - name: Set up environment
@@ -72,7 +72,7 @@ jobs:
   tests-foundry:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
       - name: Install Foundry
@@ -85,7 +85,7 @@ jobs:
   coverage:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - run: npm run coverage
@@ -96,7 +96,7 @@ jobs:
   slither:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - run: rm foundry.toml
@@ -107,7 +107,7 @@ jobs:
   codespell:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Run CodeSpell
         uses: codespell-project/actions-codespell@v2.0
         with:

.github/workflows/docs.yml

@@ -11,7 +11,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - run: bash scripts/git-user-config.sh

.github/workflows/formal-verification.yml

@@ -20,7 +20,7 @@ jobs:
   apply-diff:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Apply patches
         run: make -C certora apply
 
@@ -28,7 +28,7 @@ jobs:
     runs-on: ubuntu-latest
     if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification')
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0
       - name: Set up environment

.github/workflows/release-cycle.yml

@@ -27,7 +27,7 @@ jobs:
       pull-requests: read
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - id: state
@@ -58,7 +58,7 @@ jobs:
     if: needs.state.outputs.start == 'true'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - run: bash scripts/git-user-config.sh
@@ -81,7 +81,7 @@ jobs:
     if: needs.state.outputs.promote == 'true'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - run: bash scripts/git-user-config.sh
@@ -102,7 +102,7 @@ jobs:
     if: needs.state.outputs.changesets == 'true'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0 # To get all tags
       - name: Set up environment
@@ -134,7 +134,7 @@ jobs:
     if: needs.state.outputs.publish == 'true'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up environment
         uses: ./.github/actions/setup
       - id: pack
@@ -171,7 +171,7 @@ jobs:
     name: Tarball Integrity Check
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Download tarball artifact
         id: artifact
         # Replace with actions/upload-artifact@v3 when
@@ -195,7 +195,7 @@ jobs:
     env:
       MERGE_BRANCH: merge/${{ github.ref_name }}
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0 # All branches
       - name: Set up environment

.github/workflows/upgradeable.yml

@@ -11,7 +11,7 @@ jobs:
     environment: push-upgradeable
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           repository: OpenZeppelin/openzeppelin-contracts-upgradeable
           fetch-depth: 0

certora/diff/token_ERC721_ERC721.sol.patch

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

@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/access/AccessControlDefaultAdminRules.sol";
+import {AccessControlDefaultAdminRules} from "../patched/access/extensions/AccessControlDefaultAdminRules.sol";
 
 contract AccessControlDefaultAdminRulesHarness is AccessControlDefaultAdminRules {
     uint48 private _delayIncreaseWait;

certora/harnesses/AccessControlHarness.sol

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

certora/harnesses/DoubleEndedQueueHarness.sol

@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/utils/structs/DoubleEndedQueue.sol";
+import {DoubleEndedQueue} from "../patched/utils/structs/DoubleEndedQueue.sol";
 
 contract DoubleEndedQueueHarness {
     using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque;

certora/harnesses/ERC20PermitHarness.sol

@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/token/ERC20/extensions/ERC20Permit.sol";
+import {ERC20Permit, ERC20} from "../patched/token/ERC20/extensions/ERC20Permit.sol";
 
 contract ERC20PermitHarness is ERC20Permit {
     constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}

certora/harnesses/ERC20WrapperHarness.sol

@@ -2,10 +2,15 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
+import {ERC20Permit} from "../patched/token/ERC20/extensions/ERC20Permit.sol";
+import {ERC20Wrapper, IERC20, ERC20} from "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
 
-contract ERC20WrapperHarness is ERC20Wrapper {
-    constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {}
+contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper {
+    constructor(
+        IERC20 _underlying,
+        string memory _name,
+        string memory _symbol
+    ) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {}
 
     function underlyingTotalSupply() public view returns (uint256) {
         return underlying().totalSupply();
@@ -22,4 +27,8 @@ contract ERC20WrapperHarness is ERC20Wrapper {
     function recover(address account) public returns (uint256) {
         return _recover(account);
     }
+
+    function decimals() public view override(ERC20Wrapper, ERC20) returns (uint8) {
+        return super.decimals();
+    }
 }

certora/harnesses/ERC3156FlashBorrowerHarness.sol

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: MIT
 
-import "../patched/interfaces/IERC3156FlashBorrower.sol";
+import {IERC3156FlashBorrower} from "../patched/interfaces/IERC3156FlashBorrower.sol";
 
 pragma solidity ^0.8.20;
 

certora/harnesses/ERC721Harness.sol

@@ -2,7 +2,7 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/token/ERC721/ERC721.sol";
+import {ERC721} from "../patched/token/ERC721/ERC721.sol";
 
 contract ERC721Harness is ERC721 {
     constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
@@ -23,10 +23,6 @@ contract ERC721Harness is ERC721 {
         _burn(tokenId);
     }
 
-    function tokenExists(uint256 tokenId) external view returns (bool) {
-        return _exists(tokenId);
-    }
-
     function unsafeOwnerOf(uint256 tokenId) external view returns (address) {
         return _ownerOf(tokenId);
     }

certora/harnesses/EnumerableMapHarness.sol

@@ -2,7 +2,7 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/utils/structs/EnumerableMap.sol";
+import {EnumerableMap} from "../patched/utils/structs/EnumerableMap.sol";
 
 contract EnumerableMapHarness {
     using EnumerableMap for EnumerableMap.Bytes32ToBytes32Map;

certora/harnesses/EnumerableSetHarness.sol

@@ -2,7 +2,7 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/utils/structs/EnumerableSet.sol";
+import {EnumerableSet} from "../patched/utils/structs/EnumerableSet.sol";
 
 contract EnumerableSetHarness {
     using EnumerableSet for EnumerableSet.Bytes32Set;

certora/harnesses/InitializableHarness.sol

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

certora/harnesses/Ownable2StepHarness.sol

@@ -1,9 +1,10 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/access/Ownable2Step.sol";
+import {Ownable2Step, Ownable} from "../patched/access/Ownable2Step.sol";
 
 contract Ownable2StepHarness is Ownable2Step {
-  function restricted() external onlyOwner {}
+    constructor(address initialOwner) Ownable(initialOwner) {}
+
+    function restricted() external onlyOwner {}
 }

certora/harnesses/OwnableHarness.sol

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

certora/harnesses/PausableHarness.sol

@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/utils/Pausable.sol";
+import {Pausable} from "../patched/utils/Pausable.sol";
 
 contract PausableHarness is Pausable {
     function pause() external {

certora/harnesses/TimelockControllerHarness.sol

@@ -1,6 +1,7 @@
+// SPDX-License-Identifier: MIT
 pragma solidity ^0.8.20;
 
-import "../patched/governance/TimelockController.sol";
+import {TimelockController} from "../patched/governance/TimelockController.sol";
 
 contract TimelockControllerHarness is TimelockController {
     constructor(

certora/run.js

@@ -64,7 +64,13 @@ if (process.exitCode) {
 }
 
 for (const { spec, contract, files, options = [] } of specs) {
-  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]);
+  limit(
+    runCertora,
+    spec,
+    contract,
+    files,
+    [...options, ...argv.options].flatMap(opt => opt.split(' ')),
+  );
 }
 
 // Run certora, aggregate the output and print it at the end

certora/specs/AccessControl.spec

@@ -1,126 +1,119 @@
-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);
-}
+import "helpers/helpers.spec";
+import "methods/IAccessControl.spec";
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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 == sig:grantRole(bytes32, address).selector
+    );
+
+    assert (
+        hasRoleBefore &&
+        !hasRoleAfter
+    ) => (
+        f.selector == sig:revokeRole(bytes32, address).selector ||
+        f.selector == sig: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

@@ -1,28 +1,28 @@
-import "helpers/helpers.spec"
-import "methods/IAccessControlDefaultAdminRules.spec"
-import "methods/IAccessControl.spec"
-import "AccessControl.spec"
+import "helpers/helpers.spec";
+import "methods/IAccessControlDefaultAdminRules.spec";
+import "methods/IAccessControl.spec";
+import "AccessControl.spec";
 
 use rule onlyGrantCanGrant filtered {
-  f -> f.selector != acceptDefaultAdminTransfer().selector
+  f -> f.selector != sig:acceptDefaultAdminTransfer().selector
 }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Helpers                                                                                                             │
+│ Definitions                                                                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 definition timeSanity(env e) returns bool =
-  e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48();
+  e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48;
 
 definition delayChangeWaitSanity(env e, uint48 newDelay) returns bool =
-  e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48();
+  e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48;
 
 definition isSet(uint48 schedule) returns bool =
   schedule != 0;
 
 definition hasPassed(env e, uint48 schedule) returns bool =
-  schedule < e.block.timestamp;
+  assert_uint256(schedule) < e.block.timestamp;
 
 definition increasingDelaySchedule(env e, uint48 newDelay) returns mathint =
   e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait());
@@ -63,7 +63,7 @@ invariant singleDefaultAdmin(address account, address another)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant defaultAdminRoleAdminConsistency()
-  getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE()
+  getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE();
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -71,7 +71,7 @@ invariant defaultAdminRoleAdminConsistency()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant ownerConsistency()
-  defaultAdmin() == owner()
+  defaultAdmin() == owner();
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -136,7 +136,7 @@ rule renounceRoleEffect(env e, bytes32 role) {
       account == e.msg.sender &&
       (
         role    != DEFAULT_ADMIN_ROLE() ||
-        account != adminBefore          ||
+        account != adminBefore        ||
         (
           pendingAdminBefore == 0 &&
           isSet(scheduleBefore) &&
@@ -185,8 +185,8 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) {
   address adminAfter = defaultAdmin();
 
   assert adminBefore != adminAfter => (
-    f.selector == acceptDefaultAdminTransfer().selector ||
-    f.selector == renounceRole(bytes32,address).selector
+    f.selector == sig:acceptDefaultAdminTransfer().selector ||
+    f.selector == sig:renounceRole(bytes32,address).selector
   ),
     "default admin is only affected by accepting an admin transfer or renoucing";
 }
@@ -199,19 +199,19 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) {
 */
 rule noPendingDefaultAdminChange(env e, method f, calldataarg args) {
   address pendingAdminBefore = pendingDefaultAdmin_();
-  address scheduleBefore = pendingDefaultAdminSchedule_();
+  uint48 scheduleBefore = pendingDefaultAdminSchedule_();
   f(e, args);
   address pendingAdminAfter = pendingDefaultAdmin_();
-  address scheduleAfter = pendingDefaultAdminSchedule_();
+  uint48 scheduleAfter = pendingDefaultAdminSchedule_();
 
   assert (
     pendingAdminBefore != pendingAdminAfter ||
     scheduleBefore != scheduleAfter
   ) => (
-    f.selector == beginDefaultAdminTransfer(address).selector ||
-    f.selector == acceptDefaultAdminTransfer().selector ||
-    f.selector == cancelDefaultAdminTransfer().selector ||
-    f.selector == renounceRole(bytes32,address).selector
+    f.selector == sig:beginDefaultAdminTransfer(address).selector ||
+    f.selector == sig:acceptDefaultAdminTransfer().selector ||
+    f.selector == sig:cancelDefaultAdminTransfer().selector ||
+    f.selector == sig:renounceRole(bytes32,address).selector
   ),
     "pending admin and its schedule is only affected by beginning, completing, or cancelling an admin transfer";
 }
@@ -241,8 +241,8 @@ rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) {
   uint48 pendingDelayAfter = pendingDelay_(e);
 
   assert pendingDelayBefore != pendingDelayAfter => (
-    f.selector == changeDefaultAdminDelay(uint48).selector ||
-    f.selector == rollbackDefaultAdminDelay().selector
+    f.selector == sig:changeDefaultAdminDelay(uint48).selector ||
+    f.selector == sig:rollbackDefaultAdminDelay().selector
   ),
     "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay";
 }
@@ -282,7 +282,7 @@ rule beginDefaultAdminTransfer(env e, address newAdmin) {
   // effect
   assert success => pendingDefaultAdmin_() == newAdmin,
     "pending default admin is set";
-  assert success => pendingDefaultAdminSchedule_() == e.block.timestamp + defaultAdminDelay(e),
+  assert success => to_mathint(pendingDefaultAdminSchedule_()) == e.block.timestamp + defaultAdminDelay(e),
     "pending default admin delay is set";
 }
 
@@ -307,7 +307,7 @@ rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args
   // change can only happen towards the newAdmin, with the delay
   assert adminAfter != adminBefore => (
     adminAfter == newAdmin &&
-    e2.block.timestamp >= e1.block.timestamp + delayBefore
+    to_mathint(e2.block.timestamp) >= e1.block.timestamp + delayBefore
   ),
     "The admin can only change after the enforced delay and to the previously scheduled new admin";
 }
@@ -393,7 +393,7 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) {
     "pending delay is set";
 
   assert success => (
-    pendingDelaySchedule_(e) > e.block.timestamp ||
+    assert_uint256(pendingDelaySchedule_(e)) > e.block.timestamp ||
     delayBefore == newDelay || // Interpreted as decreasing, x - x = 0
     defaultAdminDelayIncreaseWait() == 0
   ),
@@ -419,7 +419,7 @@ rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48
 
   assert delayAfter != delayBefore => (
     delayAfter == newDelay &&
-    e2.block.timestamp >= delayWait
+    to_mathint(e2.block.timestamp) >= delayWait
   ),
     "A delay can only change after the applied schedule";
 }
@@ -433,9 +433,9 @@ rule pendingDelayWait(env e, uint48 newDelay) {
   uint48 oldDelay = defaultAdminDelay(e);
   changeDefaultAdminDelay(e, newDelay);
 
-  assert newDelay > oldDelay => pendingDelaySchedule_(e) == increasingDelaySchedule(e, newDelay),
+  assert newDelay > oldDelay => to_mathint(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),
+  assert newDelay <= oldDelay => to_mathint(pendingDelaySchedule_(e)) == decreasingDelaySchedule(e, newDelay),
     "Delay wait is the difference between the current and the new delay when the delay is decreased";
 }
 

certora/specs/ERC20.spec

@@ -1,15 +1,11 @@
-import "helpers/helpers.spec"
-import "methods/IERC20.spec"
-import "methods/IERC2612.spec"
+import "helpers/helpers.spec";
+import "methods/IERC20.spec";
+import "methods/IERC2612.spec";
 
 methods {
-    // non standard ERC20 functions
-    increaseAllowance(address,uint256) returns (bool)
-    decreaseAllowance(address,uint256) returns (bool)
-
     // exposed for FV
-    mint(address,uint256)
-    burn(address,uint256)
+    function mint(address,uint256) external;
+    function burn(address,uint256) external;
 }
 
 /*
@@ -17,12 +13,22 @@ methods {
 │ Ghost & hooks: sum of all balances                                                                                  │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-ghost sumOfBalances() returns uint256 {
-  init_state axiom sumOfBalances() == 0;
+ghost mathint sumOfBalances {
+    init_state axiom sumOfBalances == 0;
+}
+
+// Because `balance` has a uint256 type, any balance addition in CVL1 behaved as a `require_uint256()` casting,
+// leaving out the possibility of overflow. This is not the case in CVL2 where casting became more explicit.
+// A counterexample in CVL2 is having an initial state where Alice initial balance is larger than totalSupply, which 
+// overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an 
+// already used address (or upgraded from corrupted state).
+// We restrict such behavior by making sure no balance is greater than the sum of balances.
+hook Sload uint256 balance _balances[KEY address addr] STORAGE {
+    require sumOfBalances >= to_mathint(balance);
 }
 
 hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
-    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
+    sumOfBalances = sumOfBalances - oldValue + newValue;
 }
 
 /*
@@ -31,7 +37,7 @@ hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STOR
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant totalSupplyIsSumOfBalances()
-    totalSupply() == sumOfBalances()
+    to_mathint(totalSupply()) == sumOfBalances;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -39,7 +45,7 @@ invariant totalSupplyIsSumOfBalances()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant zeroAddressNoBalance()
-    balanceOf(0) == 0
+    balanceOf(0) == 0;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -56,8 +62,8 @@ rule noChangeTotalSupply(env e) {
     f(e, args);
     uint256 totalSupplyAfter = totalSupply();
 
-    assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector;
-    assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector;
+    assert totalSupplyAfter > totalSupplyBefore => f.selector == sig:mint(address,uint256).selector;
+    assert totalSupplyAfter < totalSupplyBefore => f.selector == sig:burn(address,uint256).selector;
 }
 
 /*
@@ -80,9 +86,9 @@ rule onlyAuthorizedCanTransfer(env e) {
     assert (
         balanceAfter < balanceBefore
     ) => (
-        f.selector == burn(address,uint256).selector ||
+        f.selector == sig:burn(address,uint256).selector ||
         e.msg.sender == account ||
-        balanceBefore - balanceAfter <= allowanceBefore
+        balanceBefore - balanceAfter <= to_mathint(allowanceBefore)
     );
 }
 
@@ -106,18 +112,16 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) {
     assert (
         allowanceAfter > allowanceBefore
     ) => (
-        (f.selector == approve(address,uint256).selector           && e.msg.sender == holder) ||
-        (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
-        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+        (f.selector == sig:approve(address,uint256).selector           && e.msg.sender == holder) ||
+        (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
     );
 
     assert (
         allowanceAfter < allowanceBefore
     ) => (
-        (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
-        (f.selector == approve(address,uint256).selector              && e.msg.sender == holder ) ||
-        (f.selector == decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
-        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+        (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
+        (f.selector == sig:approve(address,uint256).selector              && e.msg.sender == holder ) ||
+        (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
     );
 }
 
@@ -147,8 +151,8 @@ rule mint(env e) {
         assert to == 0 || totalSupplyBefore + amount > max_uint256;
     } else {
         // updates balance and totalSupply
-        assert balanceOf(to) == toBalanceBefore   + amount;
-        assert totalSupply() == totalSupplyBefore + amount;
+        assert to_mathint(balanceOf(to)) == toBalanceBefore   + amount;
+        assert to_mathint(totalSupply()) == totalSupplyBefore + amount;
 
         // no other balance is modified
         assert balanceOf(other) != otherBalanceBefore => other == to;
@@ -181,8 +185,8 @@ rule burn(env e) {
         assert from == 0 || fromBalanceBefore < amount;
     } else {
         // updates balance and totalSupply
-        assert balanceOf(from) == fromBalanceBefore   - amount;
-        assert totalSupply()   == totalSupplyBefore - amount;
+        assert to_mathint(balanceOf(from)) == fromBalanceBefore   - amount;
+        assert to_mathint(totalSupply())   == totalSupplyBefore - amount;
 
         // no other balance is modified
         assert balanceOf(other) != otherBalanceBefore => other == from;
@@ -216,8 +220,8 @@ rule transfer(env e) {
         assert holder == 0 || recipient == 0 || amount > holderBalanceBefore;
     } else {
         // balances of holder and recipient are updated
-        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
-        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+        assert to_mathint(balanceOf(holder))    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
 
         // no other balance is modified
         assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
@@ -254,11 +258,11 @@ rule transferFrom(env e) {
     } else {
         // allowance is valid & updated
         assert allowanceBefore            >= amount;
-        assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
+        assert to_mathint(allowance(holder, spender)) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount);
 
         // balances of holder and recipient are updated
-        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
-        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+        assert to_mathint(balanceOf(holder))    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
 
         // no other balance is modified
         assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
@@ -297,72 +301,6 @@ rule approve(env e) {
     }
 }
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ 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                                                                              │
@@ -402,7 +340,7 @@ rule permit(env e) {
     } else {
         // allowance and nonce are updated
         assert allowance(holder, spender) == amount;
-        assert nonces(holder) == nonceBefore + 1;
+        assert to_mathint(nonces(holder)) == nonceBefore + 1;
 
         // deadline was respected
         assert deadline >= e.block.timestamp;

certora/specs/ERC20FlashMint.spec

@@ -1,15 +1,14 @@
-import "helpers/helpers.spec"
-import "methods/IERC20.spec"
-import "methods/IERC3156.spec"
+import "helpers/helpers.spec";
+import "methods/IERC20.spec";
+import "methods/IERC3156FlashLender.spec";
+import "methods/IERC3156FlashBorrower.spec";
 
 methods {
     // non standard ERC3156 functions
-    flashFeeReceiver() returns (address) envfree
+    function flashFeeReceiver() external 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)
+    function _._update(address from, address to, uint256 amount) internal => specUpdate(from, to, amount) expect void ALL;
 }
 
 /*
@@ -17,13 +16,21 @@ methods {
 │ 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; }
+ghost mapping(address => mathint)                     trackedMintAmount;
+ghost mapping(address => mathint)                     trackedBurnAmount;
+ghost mapping(address => mapping(address => mathint)) trackedTransferedAmount;
+
+function specUpdate(address from, address to, uint256 amount) {
+    if (from == 0 && to == 0) { assert(false); } // defensive
+
+    if (from == 0) {
+        trackedMintAmount[to] = amount;
+    } else if (to == 0) {
+        trackedBurnAmount[from] = amount;
+    } else {
+        trackedTransferedAmount[from][to] = amount;
+    }
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -42,7 +49,7 @@ rule checkMintAndBurn(env e) {
 
     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;
+    assert trackedMintAmount[receiver] == to_mathint(amount);
+    assert trackedBurnAmount[receiver] == amount + to_mathint(recipient == 0 ? fees : 0);
+    assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == to_mathint(fees);
 }

certora/specs/ERC20Wrapper.spec

@@ -1,31 +1,29 @@
-import "helpers/helpers.spec"
-import "ERC20.spec"
+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)
+    function underlying()                       external returns(address) envfree;
+    function underlyingTotalSupply()            external returns(uint256) envfree;
+    function underlyingBalanceOf(address)       external returns(uint256) envfree;
+    function underlyingAllowanceToThis(address) external returns(uint256) envfree;
+
+    function depositFor(address, uint256)       external returns(bool);
+    function withdrawTo(address, uint256)       external returns(bool);
+    function recover(address)                   external returns(uint256);
 }
 
-use invariant totalSupplyIsSumOfBalances
+use invariant totalSupplyIsSumOfBalances;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying                                           │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool {
-    return underlyingBalanceOf(a) <= underlyingTotalSupply();
-}
+definition underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool =
+    underlyingBalanceOf(a) <= underlyingTotalSupply();
 
-function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool {
-    return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply();
-}
+definition sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool =
+    a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= to_mathint(underlyingTotalSupply());
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -47,7 +45,7 @@ invariant totalSupplyIsSmallerThanUnderlyingBalance()
     }
 
 invariant noSelfWrap()
-    currentContract != underlying()
+    currentContract != underlying();
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -85,6 +83,7 @@ rule depositFor(env e) {
     assert success <=> (
         sender   != currentContract               && // invalid sender
         sender   != 0                             && // invalid sender
+        receiver != currentContract               && // invalid receiver
         receiver != 0                             && // invalid receiver
         amount   <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
         amount   <= senderUnderlyingAllowanceBefore  // deposit doesn't exceed allowance
@@ -92,10 +91,10 @@ rule depositFor(env e) {
 
     // effects
     assert success => (
-        balanceOf(receiver) == balanceBefore + amount &&
-        totalSupply() == supplyBefore + amount &&
-        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount &&
-        underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount
+        to_mathint(balanceOf(receiver)) == balanceBefore + amount &&
+        to_mathint(totalSupply()) == supplyBefore + amount &&
+        to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount &&
+        to_mathint(underlyingBalanceOf(sender)) == senderUnderlyingBalanceBefore - amount
     );
 
     // no side effect
@@ -137,17 +136,18 @@ rule withdrawTo(env e) {
 
     // liveness
     assert success <=> (
-        sender   != 0          && // invalid sender
-        receiver != 0          && // invalid receiver
-        amount   <= balanceBefore // withdraw doesn't exceed balance
+        sender   != 0               && // invalid sender
+        receiver != currentContract && // invalid receiver
+        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)
+        to_mathint(balanceOf(sender)) == balanceBefore - amount &&
+        to_mathint(totalSupply()) == supplyBefore - amount &&
+        to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
+        to_mathint(underlyingBalanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
     );
 
     // no side effect
@@ -172,7 +172,7 @@ rule recover(env e) {
     requireInvariant totalSupplyIsSumOfBalances;
     requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
 
-    uint256 value                        = underlyingBalanceOf(currentContract) - totalSupply();
+    mathint value                        = underlyingBalanceOf(currentContract) - totalSupply();
     uint256 supplyBefore                 = totalSupply();
     uint256 balanceBefore                = balanceOf(receiver);
 
@@ -187,8 +187,8 @@ rule recover(env e) {
 
     // effect
     assert success => (
-        balanceOf(receiver) == balanceBefore + value &&
-        totalSupply() == supplyBefore + value &&
+        to_mathint(balanceOf(receiver)) == balanceBefore + value &&
+        to_mathint(totalSupply()) == supplyBefore + value &&
         totalSupply() == underlyingBalanceOf(currentContract)
     );
 

certora/specs/ERC721.spec

@@ -1,16 +1,16 @@
-import "helpers/helpers.spec"
-import "methods/IERC721.spec"
+import "helpers/helpers.spec";
+import "methods/IERC721.spec";
+import "methods/IERC721Receiver.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
+    function mint(address,uint256) external;
+    function safeMint(address,uint256) external;
+    function safeMint(address,uint256,bytes) external;
+    function burn(uint256) external;
+
+    function unsafeOwnerOf(uint256) external returns (address) envfree;
+    function unsafeGetApproved(uint256) external returns (address) envfree;
 }
 
 /*
@@ -19,17 +19,17 @@ methods {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 
+definition authSanity(env e) returns bool = e.msg.sender != 0;
+
 // Could be broken in theory, but not in practice
-function balanceLimited(address account) returns bool {
-    return balanceOf(account) < max_uint256;
-}
+definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
 
 function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
-    if (f.selector == transferFrom(address,address,uint256).selector) {
+    if (f.selector == sig:transferFrom(address,address,uint256).selector) {
         transferFrom@withrevert(e, from, to, tokenId);
-    } else if (f.selector == safeTransferFrom(address,address,uint256).selector) {
+    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
         safeTransferFrom@withrevert(e, from, to, tokenId);
-    } else if (f.selector == safeTransferFrom(address,address,uint256,bytes).selector) {
+    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
         bytes params;
         require params.length < 0xffff;
         safeTransferFrom@withrevert(e, from, to, tokenId, params);
@@ -40,11 +40,11 @@ function helperTransferWithRevert(env e, method f, address from, address to, uin
 }
 
 function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
-    if (f.selector == mint(address,uint256).selector) {
+    if (f.selector == sig:mint(address,uint256).selector) {
         mint@withrevert(e, to, tokenId);
-    } else if (f.selector == safeMint(address,uint256).selector) {
+    } else if (f.selector == sig:safeMint(address,uint256).selector) {
         safeMint@withrevert(e, to, tokenId);
-    } else if (f.selector == safeMint(address,uint256,bytes).selector) {
+    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
         bytes params;
         require params.length < 0xffff;
         safeMint@withrevert(e, to, tokenId, params);
@@ -53,26 +53,70 @@ function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
     }
 }
 
+function helperSoundFnCall(env e, method f) {
+    if (f.selector == sig:mint(address,uint256).selector) {
+        address to; uint256 tokenId;
+        require balanceLimited(to);
+        requireInvariant notMintedUnset(tokenId);
+        mint(e, to, tokenId);
+    } else if (f.selector == sig:safeMint(address,uint256).selector) {
+        address to; uint256 tokenId;
+        require balanceLimited(to);
+        requireInvariant notMintedUnset(tokenId);
+        safeMint(e, to, tokenId);
+    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
+        address to; uint256 tokenId; bytes data;
+        require data.length < 0xffff;
+        require balanceLimited(to);
+        requireInvariant notMintedUnset(tokenId);
+        safeMint(e, to, tokenId, data);
+    } else if (f.selector == sig:burn(uint256).selector) {
+        uint256 tokenId;
+        requireInvariant ownerHasBalance(tokenId);
+        requireInvariant notMintedUnset(tokenId);
+        burn(e, tokenId);
+    } else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
+        address from; address to; uint256 tokenId;
+        require balanceLimited(to);
+        requireInvariant ownerHasBalance(tokenId);
+        requireInvariant notMintedUnset(tokenId);
+        transferFrom(e, from, to, tokenId);
+    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
+        address from; address to; uint256 tokenId;
+        require balanceLimited(to);
+        requireInvariant ownerHasBalance(tokenId);
+        requireInvariant notMintedUnset(tokenId);
+        safeTransferFrom(e, from, to, tokenId);
+    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
+        address from; address to; uint256 tokenId; bytes data;
+        require data.length < 0xffff;
+        require balanceLimited(to);
+        requireInvariant ownerHasBalance(tokenId);
+        requireInvariant notMintedUnset(tokenId);
+        safeTransferFrom(e, from, to, tokenId, data);
+    } else {
+        calldataarg args;
+        f(e, args);
+    }
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Ghost & hooks: ownership count                                                                                      │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-ghost ownedTotal() returns uint256 {
-  init_state axiom ownedTotal() == 0;
+ghost mathint _ownedTotal {
+    init_state axiom _ownedTotal == 0;
 }
 
-ghost mapping(address => uint256) ownedByUser {
-    init_state axiom forall address a. ownedByUser[a] == 0;
+ghost mapping(address => mathint) _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);
+    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
+    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
+    _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
 }
 
 /*
@@ -80,29 +124,64 @@ hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STO
 │ Ghost & hooks: sum of all balances                                                                                  │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-ghost sumOfBalances() returns uint256 {
-  init_state axiom sumOfBalances() == 0;
+ghost mathint _supply {
+    init_state axiom _supply == 0;
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
-    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
+ghost mapping(address => mathint) _balances {
+    init_state axiom forall address a. _balances[a] == 0;
 }
 
-ghost mapping(address => uint256) ghostBalanceOf {
-    init_state axiom forall address a. ghostBalanceOf[a] == 0;
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+    _supply = _supply - oldValue + newValue;
 }
 
+// TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add
+// many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved.
 hook Sload uint256 value _balances[KEY address user] STORAGE {
-    require ghostBalanceOf[user] == value;
+    require _balances[user] == to_mathint(value);
 }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: ownedTotal is the sum of all balances                                                                    │
+│ Invariant: number of owned tokens is the sum of all balances                                                        │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant ownedTotalIsSumOfBalances()
-    ownedTotal() == sumOfBalances()
+    _ownedTotal == _supply
+    {
+        preserved mint(address to, uint256 tokenId) with (env e) {
+            require balanceLimited(to);
+        }
+        preserved safeMint(address to, uint256 tokenId) with (env e) {
+            require balanceLimited(to);
+        }
+        preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
+            require balanceLimited(to);
+        }
+        preserved burn(uint256 tokenId) with (env e) {
+            requireInvariant ownerHasBalance(tokenId);
+            requireInvariant balanceOfConsistency(ownerOf(tokenId));
+        }
+        preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
+            require balanceLimited(to);
+            requireInvariant ownerHasBalance(tokenId);
+            requireInvariant balanceOfConsistency(from);
+            requireInvariant balanceOfConsistency(to);
+        }
+        preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
+            require balanceLimited(to);
+            requireInvariant ownerHasBalance(tokenId);
+            requireInvariant balanceOfConsistency(from);
+            requireInvariant balanceOfConsistency(to);
+        }
+        preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
+            require balanceLimited(to);
+            requireInvariant ownerHasBalance(tokenId);
+            requireInvariant balanceOfConsistency(from);
+            requireInvariant balanceOfConsistency(to);
+        }
+    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -110,8 +189,8 @@ invariant ownedTotalIsSumOfBalances()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant balanceOfConsistency(address user)
-    balanceOf(user) == ownedByUser[user] &&
-    balanceOf(user) == ghostBalanceOf[user]
+    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
+    to_mathint(balanceOf(user)) == _balances[user]
     {
         preserved {
             require balanceLimited(user);
@@ -134,53 +213,56 @@ invariant ownerHasBalance(uint256 tokenId)
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: tokens that do not exist are not owned and not approved                                                  │
+│ Rule: balance of address(0) is 0                                                                                    │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant notMintedUnset(uint256 tokenId)
-    (!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) &&
-    (!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0)
+rule zeroAddressBalanceRevert() {
+    balanceOf@withrevert(0);
+    assert lastReverted;
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: ownerOf and getApproved revert if token does not exist                                                        │
+│ Invariant: address(0) has no authorized operator                                                                    │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-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);
-}
+invariant zeroAddressHasNoApprovedOperator(address a)
+    !isApprovedForAll(0, a)
+    {
+        preserved with (env e) {
+            require nonzerosender(e);
+        }
+    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert                                                              │
+│ Invariant: tokens that do not exist are not owned and not approved                                                  │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule unsafeDontRevert(uint256 tokenId) {
-    unsafeOwnerOf@withrevert(tokenId);
-    assert !lastReverted;
-
-    unsafeGetApproved@withrevert(tokenId);
-    assert !lastReverted;
-}
+invariant notMintedUnset(uint256 tokenId)
+    unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: balance of address(0) is 0                                                                                    │
+│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert + ownerOf and getApproved revert if token does not exist     │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule zeroAddressBalanceRevert() {
-    balanceOf@withrevert(0);
-    assert lastReverted;
+rule notMintedRevert(uint256 tokenId) {
+    requireInvariant notMintedUnset(tokenId);
+
+    address _owner = unsafeOwnerOf@withrevert(tokenId);
+    assert !lastReverted;
+
+    address _approved = unsafeGetApproved@withrevert(tokenId);
+    assert !lastReverted;
+
+    address owner = ownerOf@withrevert(tokenId);
+    assert lastReverted <=> _owner == 0;
+    assert !lastReverted => _owner == owner;
+
+    address approved = getApproved@withrevert(tokenId);
+    assert lastReverted <=> _owner == 0;
+    assert !lastReverted => _approved == approved;
 }
 
 /*
@@ -189,21 +271,24 @@ rule zeroAddressBalanceRevert() {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule supplyChange(env e) {
-    uint256 supplyBefore = ownedTotal();
-    method f; calldataarg args; f(e, args);
-    uint256 supplyAfter = ownedTotal();
+    require nonzerosender(e);
+    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
+
+    mathint supplyBefore = _supply;
+    method f; helperSoundFnCall(e, f);
+    mathint supplyAfter = _supply;
 
     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
+            f.selector == sig:mint(address,uint256).selector ||
+            f.selector == sig:safeMint(address,uint256).selector ||
+            f.selector == sig:safeMint(address,uint256,bytes).selector
         )
     );
     assert supplyAfter < supplyBefore => (
         supplyAfter == supplyBefore - 1 &&
-        f.selector == burn(uint256).selector
+        f.selector == sig:burn(uint256).selector
     );
 }
 
@@ -216,9 +301,9 @@ 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);
+    mathint balanceBefore = balanceOf(account);
+    method f; helperSoundFnCall(e, f);
+    mathint balanceAfter  = balanceOf(account);
 
     // balance can change by at most 1
     assert balanceBefore != balanceAfter => (
@@ -228,13 +313,13 @@ rule balanceChange(env e, address account) {
 
     // 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
+        f.selector == sig:transferFrom(address,address,uint256).selector ||
+        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
+        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
+        f.selector == sig:mint(address,uint256).selector ||
+        f.selector == sig:safeMint(address,uint256).selector ||
+        f.selector == sig:safeMint(address,uint256,bytes).selector ||
+        f.selector == sig:burn(uint256).selector
     );
 }
 
@@ -244,24 +329,27 @@ rule balanceChange(env e, address account) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule ownershipChange(env e, uint256 tokenId) {
+    require nonzerosender(e);
+    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
+
     address ownerBefore = unsafeOwnerOf(tokenId);
-    method f; calldataarg args; f(e, args);
+    method f; helperSoundFnCall(e, f);
     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
+        f.selector == sig:mint(address,uint256).selector ||
+        f.selector == sig:safeMint(address,uint256).selector ||
+        f.selector == sig:safeMint(address,uint256,bytes).selector
     );
 
     assert ownerBefore != 0 && ownerAfter == 0 => (
-        f.selector == burn(uint256).selector
+        f.selector == sig: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
+        f.selector == sig:transferFrom(address,address,uint256).selector ||
+        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
+        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
     );
 }
 
@@ -272,18 +360,18 @@ rule ownershipChange(env e, uint256 tokenId) {
 */
 rule approvalChange(env e, uint256 tokenId) {
     address approvalBefore = unsafeGetApproved(tokenId);
-    method f; calldataarg args; f(e, args);
+    method f; helperSoundFnCall(e, f);
     address approvalAfter  = unsafeGetApproved(tokenId);
 
     // approve can set any value, other functions reset
     assert approvalBefore != approvalAfter => (
-        f.selector == approve(address,uint256).selector ||
+        f.selector == sig: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
+                f.selector == sig:transferFrom(address,address,uint256).selector ||
+                f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
+                f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
+                f.selector == sig:burn(uint256).selector
             ) && approvalAfter == 0
         )
     );
@@ -296,10 +384,10 @@ rule approvalChange(env e, uint256 tokenId) {
 */
 rule approvedForAllChange(env e, address owner, address spender) {
     bool approvedForAllBefore = isApprovedForAll(owner, spender);
-    method f; calldataarg args; f(e, args);
+    method f; helperSoundFnCall(e, f);
     bool approvedForAllAfter  = isApprovedForAll(owner, spender);
 
-    assert approvedForAllBefore != approvedForAllAfter => f.selector == setApprovalForAll(address,bool).selector;
+    assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
 }
 
 /*
@@ -309,6 +397,7 @@ rule approvedForAllChange(env e, address owner, address spender) {
 */
 rule transferFrom(env e, address from, address to, uint256 tokenId) {
     require nonpayable(e);
+    require authSanity(e);
 
     address operator = e.msg.sender;
     uint256 otherTokenId;
@@ -338,10 +427,10 @@ rule transferFrom(env e, address from, address to, uint256 tokenId) {
 
     // 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
+        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
+        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
+        unsafeOwnerOf(tokenId)                 == to &&
+        unsafeGetApproved(tokenId)             == 0
     );
 
     // no side effect
@@ -356,10 +445,11 @@ rule transferFrom(env e, address from, address to, uint256 tokenId) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 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
+    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
+    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
 } {
     require nonpayable(e);
+    require authSanity(e);
 
     address operator = e.msg.sender;
     uint256 otherTokenId;
@@ -388,10 +478,10 @@ rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId
 
     // 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
+        to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) &&
+        to_mathint(balanceOf(to))   == balanceOfToBefore   + assert_uint256(from != to ? 1: 0) &&
+        unsafeOwnerOf(tokenId)      == to &&
+        unsafeGetApproved(tokenId)  == 0
     );
 
     // no side effect
@@ -414,7 +504,7 @@ rule mint(env e, address to, uint256 tokenId) {
 
     require balanceLimited(to);
 
-    uint256 supplyBefore         = ownedTotal();
+    mathint supplyBefore         = _supply;
     uint256 balanceOfToBefore    = balanceOf(to);
     uint256 balanceOfOtherBefore = balanceOf(otherAccount);
     address ownerBefore          = unsafeOwnerOf(tokenId);
@@ -431,9 +521,9 @@ rule mint(env e, address to, uint256 tokenId) {
 
     // effect
     assert success => (
-        ownedTotal()           == supplyBefore + 1 &&
-        balanceOf(to)          == balanceOfToBefore + 1 &&
-        unsafeOwnerOf(tokenId) == to
+        _supply                   == supplyBefore + 1 &&
+        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId)    == to
     );
 
     // no side effect
@@ -447,8 +537,8 @@ rule mint(env e, address to, uint256 tokenId) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 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
+    f.selector == sig:safeMint(address,uint256).selector ||
+    f.selector == sig:safeMint(address,uint256,bytes).selector
 } {
     require nonpayable(e);
     requireInvariant notMintedUnset(tokenId);
@@ -458,7 +548,7 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
 
     require balanceLimited(to);
 
-    uint256 supplyBefore         = ownedTotal();
+    mathint supplyBefore         = _supply;
     uint256 balanceOfToBefore    = balanceOf(to);
     uint256 balanceOfOtherBefore = balanceOf(otherAccount);
     address ownerBefore          = unsafeOwnerOf(tokenId);
@@ -474,9 +564,9 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
 
     // effect
     assert success => (
-        ownedTotal()           == supplyBefore + 1 &&
-        balanceOf(to)          == balanceOfToBefore + 1 &&
-        unsafeOwnerOf(tokenId) == to
+        _supply                   == supplyBefore + 1 &&
+        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId)    == to
     );
 
     // no side effect
@@ -498,7 +588,7 @@ rule burn(env e, uint256 tokenId) {
 
     requireInvariant ownerHasBalance(tokenId);
 
-    uint256 supplyBefore         = ownedTotal();
+    mathint supplyBefore         = _supply;
     uint256 balanceOfFromBefore  = balanceOf(from);
     uint256 balanceOfOtherBefore = balanceOf(otherAccount);
     address ownerBefore          = unsafeOwnerOf(tokenId);
@@ -515,10 +605,10 @@ rule burn(env e, uint256 tokenId) {
 
     // effect
     assert success => (
-        ownedTotal()               == supplyBefore   - 1 &&
-        balanceOf(from)            == balanceOfFromBefore - 1 &&
-        unsafeOwnerOf(tokenId)     == 0 &&
-        unsafeGetApproved(tokenId) == 0
+        _supply                     == supplyBefore - 1 &&
+        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
+        unsafeOwnerOf(tokenId)      == 0 &&
+        unsafeGetApproved(tokenId)  == 0
     );
 
     // no side effect
@@ -534,6 +624,7 @@ rule burn(env e, uint256 tokenId) {
 */
 rule approve(env e, address spender, uint256 tokenId) {
     require nonpayable(e);
+    require authSanity(e);
 
     address caller = e.msg.sender;
     address owner = unsafeOwnerOf(tokenId);
@@ -547,7 +638,6 @@ rule approve(env e, address spender, uint256 tokenId) {
     // liveness
     assert success <=> (
         owner != 0 &&
-        owner != spender &&
         (owner == caller || isApprovedForAll(owner, caller))
     );
 
@@ -576,7 +666,7 @@ rule setApprovalForAll(env e, address operator, bool approved) {
     bool success = !lastReverted;
 
     // liveness
-    assert success <=> owner != operator;
+    assert success <=> operator != 0;
 
     // effect
     assert success => isApprovedForAll(owner, operator) == approved;

certora/specs/EnumerableMap.spec

@@ -1,19 +1,19 @@
-import "helpers/helpers.spec"
+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
+    function set(bytes32,bytes32)     external returns (bool)    envfree;
+    function remove(bytes32)          external returns (bool)    envfree;
+    function contains(bytes32)        external returns (bool)    envfree;
+    function length()                 external returns (uint256) envfree;
+    function key_at(uint256)          external returns (bytes32) envfree;
+    function value_at(uint256)        external returns (bytes32) envfree;
+    function tryGet_contains(bytes32) external returns (bool)    envfree;
+    function tryGet_value(bytes32)    external returns (bytes32) envfree;
+    function get(bytes32)             external returns (bytes32) envfree;
 
     // FV
-    _indexOf(bytes32) returns (uint256) envfree
+    function _indexOf(bytes32) external returns (uint256) envfree;
 }
 
 /*
@@ -21,9 +21,8 @@ methods {
 │ Helpers                                                                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-function sanity() returns bool {
-    return length() < max_uint256;
-}
+definition sanity() returns bool =
+    length() < max_uint256;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -31,7 +30,7 @@ function sanity() returns bool {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant noValueIfNotContained(bytes32 key)
-    !contains(key) => tryGet_value(key) == 0
+    !contains(key) => tryGet_value(key) == to_bytes32(0)
     {
         preserved set(bytes32 otherKey, bytes32 someValue) {
             require sanity();
@@ -48,7 +47,7 @@ invariant indexedContained(uint256 index)
     {
         preserved {
             requireInvariant consistencyIndex(index);
-            requireInvariant consistencyIndex(to_uint256(length() - 1));
+            requireInvariant consistencyIndex(require_uint256(length() - 1));
         }
     }
 
@@ -61,8 +60,8 @@ 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));
+            requireInvariant atUniqueness(index1, require_uint256(length() - 1));
+            requireInvariant atUniqueness(index2, require_uint256(length() - 1));
         }
     }
 
@@ -76,10 +75,10 @@ invariant atUniqueness(uint256 index1, uint256 index2)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant consistencyIndex(uint256 index)
-    index < length() => _indexOf(key_at(index)) == index + 1
+    index < length() => to_mathint(_indexOf(key_at(index))) == index + 1
     {
         preserved remove(bytes32 key) {
-            requireInvariant consistencyIndex(to_uint256(length() - 1));
+            requireInvariant consistencyIndex(require_uint256(length() - 1));
         }
     }
 
@@ -87,14 +86,14 @@ invariant consistencyKey(bytes32 key)
     contains(key) => (
         _indexOf(key) > 0 &&
         _indexOf(key) <= length() &&
-        key_at(to_uint256(_indexOf(key) - 1)) == key
+        key_at(require_uint256(_indexOf(key) - 1)) == key
     )
     {
         preserved remove(bytes32 otherKey) {
             requireInvariant consistencyKey(otherKey);
             requireInvariant atUniqueness(
-                to_uint256(_indexOf(key) - 1),
-                to_uint256(_indexOf(otherKey) - 1)
+                require_uint256(_indexOf(key) - 1),
+                require_uint256(_indexOf(otherKey) - 1)
             );
         }
     }
@@ -121,18 +120,18 @@ rule stateChange(env e, bytes32 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)
+        (f.selector == sig:set(bytes32,bytes32).selector && to_mathint(lengthAfter) == lengthBefore + 1) ||
+        (f.selector == sig:remove(bytes32).selector      && to_mathint(lengthAfter) == lengthBefore - 1)
     );
 
     assert containsBefore != containsAfter => (
-        (f.selector == set(bytes32,bytes32).selector && containsAfter) ||
-        (f.selector == remove(bytes32).selector      && !containsAfter)
+        (f.selector == sig:set(bytes32,bytes32).selector && containsAfter) ||
+        (f.selector == sig:remove(bytes32).selector      && !containsAfter)
     );
 
     assert valueBefore != valueAfter => (
-        (f.selector == set(bytes32,bytes32).selector && containsAfter) ||
-        (f.selector == remove(bytes32).selector      && !containsAfter && valueAfter == 0)
+        (f.selector == sig:set(bytes32,bytes32).selector && containsAfter) ||
+        (f.selector == sig:remove(bytes32).selector      && !containsAfter && valueAfter == to_bytes32(0))
     );
 }
 
@@ -192,7 +191,7 @@ rule getAndTryGet(bytes32 key) {
 
     assert contained == tryContained;
     assert contained => tryValue == value;
-    assert !contained => tryValue == 0;
+    assert !contained => tryValue == to_bytes32(0);
 }
 
 /*
@@ -217,7 +216,7 @@ rule set(bytes32 key, bytes32 value, bytes32 otherKey) {
     assert added <=> !containsBefore,
         "return value: added iff not contained";
 
-    assert length() == lengthBefore + to_mathint(added ? 1 : 0),
+    assert to_mathint(length()) == lengthBefore + to_mathint(added ? 1 : 0),
         "effect: length increases iff added";
 
     assert added => (key_at(lengthBefore) == key && value_at(lengthBefore) == value),
@@ -253,7 +252,7 @@ rule remove(bytes32 key, bytes32 otherKey) {
     assert removed <=> containsBefore,
         "return value: removed iff contained";
 
-    assert length() == lengthBefore - to_mathint(removed ? 1 : 0),
+    assert to_mathint(length()) == lengthBefore - to_mathint(removed ? 1 : 0),
         "effect: length decreases iff removed";
 
     assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey),
@@ -295,7 +294,7 @@ rule setEnumerability(bytes32 key, bytes32 value, uint256 index) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule removeEnumerability(bytes32 key, uint256 index) {
-    uint256 last = length() - 1;
+    uint256 last = require_uint256(length() - 1);
 
     requireInvariant consistencyKey(key);
     requireInvariant consistencyIndex(index);

certora/specs/EnumerableSet.spec

@@ -1,15 +1,15 @@
-import "helpers/helpers.spec"
+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
+    function add(bytes32)      external returns (bool)    envfree;
+    function remove(bytes32)   external returns (bool)    envfree;
+    function contains(bytes32) external returns (bool)    envfree;
+    function length()          external returns (uint256) envfree;
+    function at_(uint256)      external returns (bytes32) envfree;
 
     // FV
-    _indexOf(bytes32) returns (uint256) envfree
+    function _indexOf(bytes32) external returns (uint256) envfree;
 }
 
 /*
@@ -17,9 +17,8 @@ methods {
 │ Helpers                                                                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-function sanity() returns bool {
-    return length() < max_uint256;
-}
+definition sanity() returns bool =
+    length() < max_uint256;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -31,7 +30,7 @@ invariant indexedContained(uint256 index)
     {
         preserved {
             requireInvariant consistencyIndex(index);
-            requireInvariant consistencyIndex(to_uint256(length() - 1));
+            requireInvariant consistencyIndex(require_uint256(length() - 1));
         }
     }
 
@@ -44,8 +43,8 @@ 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));
+            requireInvariant atUniqueness(index1, require_uint256(length() - 1));
+            requireInvariant atUniqueness(index2, require_uint256(length() - 1));
         }
     }
 
@@ -59,10 +58,10 @@ invariant atUniqueness(uint256 index1, uint256 index2)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant consistencyIndex(uint256 index)
-    index < length() => _indexOf(at_(index)) == index + 1
+    index < length() => _indexOf(at_(index)) == require_uint256(index + 1)
     {
         preserved remove(bytes32 key) {
-            requireInvariant consistencyIndex(to_uint256(length() - 1));
+            requireInvariant consistencyIndex(require_uint256(length() - 1));
         }
     }
 
@@ -70,14 +69,14 @@ invariant consistencyKey(bytes32 key)
     contains(key) => (
         _indexOf(key) > 0 &&
         _indexOf(key) <= length() &&
-        at_(to_uint256(_indexOf(key) - 1)) == key
+        at_(require_uint256(_indexOf(key) - 1)) == key
     )
     {
         preserved remove(bytes32 otherKey) {
             requireInvariant consistencyKey(otherKey);
             requireInvariant atUniqueness(
-                to_uint256(_indexOf(key) - 1),
-                to_uint256(_indexOf(otherKey) - 1)
+                require_uint256(_indexOf(key) - 1),
+                require_uint256(_indexOf(otherKey) - 1)
             );
         }
     }
@@ -102,13 +101,13 @@ rule stateChange(env e, bytes32 key) {
     bool    containsAfter = contains(key);
 
     assert lengthBefore != lengthAfter => (
-        (f.selector == add(bytes32).selector    && lengthAfter == lengthBefore + 1) ||
-        (f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1)
+        (f.selector == sig:add(bytes32).selector    && lengthAfter == require_uint256(lengthBefore + 1)) ||
+        (f.selector == sig:remove(bytes32).selector && lengthAfter == require_uint256(lengthBefore - 1))
     );
 
     assert containsBefore != containsAfter => (
-        (f.selector == add(bytes32).selector    && containsAfter) ||
-        (f.selector == remove(bytes32).selector && containsBefore)
+        (f.selector == sig:add(bytes32).selector    && containsAfter) ||
+        (f.selector == sig:remove(bytes32).selector && containsBefore)
     );
 }
 
@@ -158,7 +157,7 @@ rule add(bytes32 key, bytes32 otherKey) {
     assert added <=> !containsBefore,
         "return value: added iff not contained";
 
-    assert length() == lengthBefore + to_mathint(added ? 1 : 0),
+    assert length() == require_uint256(lengthBefore + to_mathint(added ? 1 : 0)),
         "effect: length increases iff added";
 
     assert added => at_(lengthBefore) == key,
@@ -190,7 +189,7 @@ rule remove(bytes32 key, bytes32 otherKey) {
     assert removed <=> containsBefore,
         "return value: removed iff contained";
 
-    assert length() == lengthBefore - to_mathint(removed ? 1 : 0),
+    assert length() == require_uint256(lengthBefore - to_mathint(removed ? 1 : 0)),
         "effect: length decreases iff removed";
 
     assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey),
@@ -220,7 +219,7 @@ rule addEnumerability(bytes32 key, uint256 index) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule removeEnumerability(bytes32 key, uint256 index) {
-    uint256 last = length() - 1;
+    uint256 last = require_uint256(length() - 1);
 
     requireInvariant consistencyKey(key);
     requireInvariant consistencyIndex(index);

certora/specs/Initializable.spec

@@ -1,19 +1,19 @@
-import "helpers/helpers.spec"
+import "helpers/helpers.spec";
 
 methods {
     // initialize, reinitialize, disable
-    initialize()        envfree
-    reinitialize(uint8) envfree
-    disable()           envfree
+    function initialize()         external envfree;
+    function reinitialize(uint64) external envfree;
+    function disable()            external envfree;
 
-    nested_init_init()            envfree
-    nested_init_reinit(uint8)       envfree
-    nested_reinit_init(uint8)       envfree
-    nested_reinit_reinit(uint8,uint8) envfree
+    function nested_init_init()                  external envfree;
+    function nested_init_reinit(uint64)          external envfree;
+    function nested_reinit_init(uint64)          external envfree;
+    function nested_reinit_reinit(uint64,uint64) external envfree;
 
     // view
-    version()      returns uint8 envfree
-    initializing() returns bool  envfree
+    function version()      external returns uint64 envfree;
+    function initializing() external returns bool   envfree;
 }
 
 /*
@@ -23,7 +23,7 @@ methods {
 */
 definition isUninitialized() returns bool = version() == 0;
 definition isInitialized()   returns bool = version() > 0;
-definition isDisabled()      returns bool = version() == 255;
+definition isDisabled()      returns bool = version() == max_uint64;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -31,7 +31,7 @@ definition isDisabled()      returns bool = version() == 255;
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant notInitializing()
-    !initializing()
+    !initializing();
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -39,7 +39,7 @@ invariant notInitializing()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule increasingVersion(env e) {
-    uint8 versionBefore = version();
+    uint64 versionBefore = version();
     bool disabledBefore = isDisabled();
 
     method f; calldataarg args;
@@ -83,7 +83,7 @@ rule cannotInitializeOnceDisabled() {
 rule cannotReinitializeOnceDisabled() {
     require isDisabled();
 
-    uint8 n;
+    uint64 n;
     reinitialize@withrevert(n);
 
     assert lastReverted, "contract is disabled";
@@ -99,17 +99,17 @@ rule cannotNestInitializers_init_init() {
     assert lastReverted, "nested initializers";
 }
 
-rule cannotNestInitializers_init_reinit(uint8 m) {
+rule cannotNestInitializers_init_reinit(uint64 m) {
     nested_init_reinit@withrevert(m);
     assert lastReverted, "nested initializers";
 }
 
-rule cannotNestInitializers_reinit_init(uint8 n) {
+rule cannotNestInitializers_reinit_init(uint64 n) {
     nested_reinit_init@withrevert(n);
     assert lastReverted, "nested initializers";
 }
 
-rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) {
+rule cannotNestInitializers_reinit_reinit(uint64 n, uint64 m) {
     nested_reinit_reinit@withrevert(n, m);
     assert lastReverted, "nested initializers";
 }
@@ -139,9 +139,9 @@ rule initializeEffects() {
 rule reinitializeEffects() {
     requireInvariant notInitializing();
 
-    uint8 versionBefore = version();
+    uint64 versionBefore = version();
 
-    uint8 n;
+    uint64 n;
     reinitialize@withrevert(n);
     bool success = !lastReverted;
 

certora/specs/Ownable.spec

@@ -1,78 +1,77 @@
-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)
-    );
-}
+import "helpers/helpers.spec";
+import "methods/IOwnable.spec";
+
+methods {
+    function restricted() external;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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 == sig:transferOwnership(address).selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
+    );
+}

certora/specs/Ownable2Step.spec

@@ -1,108 +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)
-    );
-}
+import "helpers/helpers.spec";
+import "methods/IOwnable2Step.spec";
+
+methods {
+    function restricted() external;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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 == sig:acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == sig:renounceOwnership().selector)
+    );
+
+    // If pending changes, must be either acceptance or reset
+    assert oldPending != newPending => (
+        (e.msg.sender == oldCurrent && newCurrent == oldCurrent &&                    f.selector == sig:transferOwnership(address).selector) ||
+        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == sig:acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == sig:renounceOwnership().selector)
+    );
+}

certora/specs/Pausable.spec

@@ -1,96 +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()";
-}
+import "helpers/helpers.spec";
+
+methods {
+    function paused() external returns (bool) envfree;
+    function pause() external;
+    function unpause() external;
+    function onlyWhenPaused() external;
+    function onlyWhenNotPaused() external;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ 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 == sig:unpause().selector) ||
+        (pausedAfter && f.selector == sig:pause().selector)
+    ), "contract's paused status can only be changed by _pause() or _unpause()";
+}

certora/specs/TimelockController.spec

@@ -1,28 +1,27 @@
-import "helpers/helpers.spec"
-import "methods/IAccessControl.spec"
+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)
+    function PROPOSER_ROLE()             external returns (bytes32) envfree;
+    function EXECUTOR_ROLE()             external returns (bytes32) envfree;
+    function CANCELLER_ROLE()            external returns (bytes32) envfree;
+    function isOperation(bytes32)        external returns (bool);
+    function isOperationPending(bytes32) external returns (bool);
+    function isOperationReady(bytes32)   external returns (bool);
+    function isOperationDone(bytes32)    external returns (bool);
+    function getTimestamp(bytes32)       external returns (uint256) envfree;
+    function getMinDelay()               external returns (uint256) envfree;
+
+    function hashOperation(address, uint256, bytes, bytes32, bytes32)            external returns(bytes32) envfree;
+    function hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) external returns(bytes32) envfree;
+
+    function schedule(address, uint256, bytes, bytes32, bytes32, uint256) external;
+    function scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) external;
+    function execute(address, uint256, bytes, bytes32, bytes32) external;
+    function executeBatch(address[], uint256[], bytes[], bytes32, bytes32) external;
+    function cancel(bytes32) external;
+
+    function updateDelay(uint256) external;
 }
 
 /*
@@ -32,11 +31,11 @@ methods {
 */
 // 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) {
+    if (f.selector == sig: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) {
+    } else if (f.selector == sig: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);
@@ -48,11 +47,11 @@ function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
 
 // 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) {
+    if (f.selector == sig: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) {
+    } else if (f.selector == sig: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);
@@ -72,30 +71,30 @@ 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);
+definition isUnset(env e, bytes32 id)   returns bool  = !isOperation(e, id);
+definition isPending(env e, bytes32 id) returns bool  = isOperationPending(e, id);
+definition isDone(env e, bytes32 id)    returns bool  = isOperationDone(e, id);
+definition state(env e, bytes32 id)     returns uint8 = (isUnset(e, id) ? UNSET() : 0) | (isPending(e, id) ? PENDING() : 0) | (isDone(e, id) ? DONE() : 0);
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariants: consistency of accessors                                                                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant isOperationCheck(bytes32 id)
-    isOperation(id) <=> getTimestamp(id) > 0
+invariant isOperationCheck(env e, bytes32 id)
+    isOperation(e, id) <=> getTimestamp(id) > 0
     filtered { f -> !f.isView }
 
-invariant isOperationPendingCheck(bytes32 id)
-    isOperationPending(id) <=> getTimestamp(id) > DONE_TIMESTAMP()
+invariant isOperationPendingCheck(env e, bytes32 id)
+    isOperationPending(e, id) <=> getTimestamp(id) > DONE_TIMESTAMP()
     filtered { f -> !f.isView }
 
-invariant isOperationDoneCheck(bytes32 id)
-    isOperationDone(id) <=> getTimestamp(id) == DONE_TIMESTAMP()
+invariant isOperationDoneCheck(env e, bytes32 id)
+    isOperationDone(e, 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)
+    isOperationReady(e, id) <=> (isOperationPending(e, id) && getTimestamp(id) <= e.block.timestamp)
     filtered { f -> !f.isView }
 
 /*
@@ -105,15 +104,15 @@ invariant isOperationReadyCheck(env e, bytes32 id)
 */
 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))) &&
+    (isUnset(e, id)   <=> (!isPending(e, id) && !isDone(e, id)   )) &&
+    (isPending(e, id) <=> (!isUnset(e, id)   && !isDone(e, id)   )) &&
+    (isDone(e, id)    <=> (!isUnset(e, id)   && !isPending(e, id))) &&
     // Check that the state helper behaves as expected:
-    (isUnset(id)   <=> state(id) == UNSET()              ) &&
-    (isPending(id) <=> state(id) == PENDING()            ) &&
-    (isDone(id)    <=> state(id) == DONE()               ) &&
+    (isUnset(e, id)   <=> state(e, id) == UNSET()              ) &&
+    (isPending(e, id) <=> state(e, id) == PENDING()            ) &&
+    (isDone(e, id)    <=> state(e, id) == DONE()               ) &&
     // Check substate
-    isOperationReady(e, id) => isPending(id)
+    isOperationReady(e, id) => isPending(e, id)
     filtered { f -> !f.isView }
 
 /*
@@ -124,28 +123,28 @@ invariant stateConsistency(bytes32 id, env e)
 rule stateTransition(bytes32 id, env e, method f, calldataarg args) {
     require e.block.timestamp > 1; // Sanity
 
-    uint8 stateBefore = state(id);
+    uint8 stateBefore = state(e, id);
     f(e, args);
-    uint8 stateAfter = state(id);
+    uint8 stateAfter = state(e, 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
+        f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
+        f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
     );
 
     // PENDING → UNSET: cancel
     assert stateBefore == PENDING() && stateAfter == UNSET() => (
-        f.selector == cancel(bytes32).selector
+        f.selector == sig: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
+        f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector ||
+        f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
     );
 
     // DONE is final
@@ -163,7 +162,7 @@ rule minDelayOnlyChange(env e) {
     method f; calldataarg args;
     f(e, args);
 
-    assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == updateDelay(uint256).selector), "Unauthorized delay update";
+    assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == sig:updateDelay(uint256).selector), "Unauthorized delay update";
 }
 
 /*
@@ -172,8 +171,8 @@ rule minDelayOnlyChange(env e) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 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
+    f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
+    f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
 } {
     require nonpayable(e);
 
@@ -184,7 +183,7 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
 
     bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
 
-    uint8 stateBefore       = state(id);
+    uint8 stateBefore       = state(e, id);
     bool  isDelaySufficient = delay >= getMinDelay();
     bool  isProposerBefore  = hasRole(PROPOSER_ROLE(), e.msg.sender);
 
@@ -199,8 +198,8 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
     );
 
     // effect
-    assert success => state(id) == PENDING(), "State transition violation";
-    assert success => getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set";
+    assert success => state(e, id) == PENDING(), "State transition violation";
+    assert success => getTimestamp(id) == require_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set";
 
     // no side effect
     assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
@@ -212,15 +211,15 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 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
+    f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector ||
+    f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
 } {
     bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
 
-    uint8 stateBefore            = state(id);
+    uint8 stateBefore            = state(e, id);
     bool  isOperationReadyBefore = isOperationReady(e, id);
     bool  isExecutorOrOpen       = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0);
-    bool  predecessorDependency  = predecessor == 0 || isDone(predecessor);
+    bool  predecessorDependency  = predecessor == to_bytes32(0) || isDone(e, predecessor);
 
     helperExecuteWithRevert(e, f, id, predecessor);
     bool success = !lastReverted;
@@ -239,7 +238,7 @@ rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
     );
 
     // effect
-    assert success => state(id) == DONE(), "State transition violation";
+    assert success => state(e, id) == DONE(), "State transition violation";
 
     // no side effect
     assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
@@ -255,7 +254,7 @@ rule cancel(env e, bytes32 id) {
 
     bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
 
-    uint8 stateBefore = state(id);
+    uint8 stateBefore = state(e, id);
     bool  isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender);
 
     cancel@withrevert(e, id);
@@ -268,7 +267,7 @@ rule cancel(env e, bytes32 id) {
     );
 
     // effect
-    assert success => state(id) == UNSET(), "State transition violation";
+    assert success => state(e, id) == UNSET(), "State transition violation";
 
     // no side effect
     assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";

certora/specs/methods/IAccessControl.spec

@@ -1,7 +1,8 @@
 methods {
-    hasRole(bytes32, address) returns(bool) envfree
-    getRoleAdmin(bytes32) returns(bytes32) envfree
-    grantRole(bytes32, address)
-    revokeRole(bytes32, address)
-    renounceRole(bytes32, address)
+    function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree;
+    function hasRole(bytes32, address) external returns(bool) envfree;
+    function getRoleAdmin(bytes32) external returns(bytes32) envfree;
+    function grantRole(bytes32, address) external;
+    function revokeRole(bytes32, address) external;
+    function renounceRole(bytes32, address) external;
 }

certora/specs/methods/IAccessControlDefaultAdminRules.spec

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

certora/specs/methods/IERC20.spec

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

certora/specs/methods/IERC2612.spec

@@ -1,5 +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)
+    function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external;
+    function nonces(address)    external returns (uint256) envfree;
+    function DOMAIN_SEPARATOR() external returns (bytes32) envfree;
 }

certora/specs/methods/IERC3156.spec

@@ -1,5 +0,0 @@
-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)
-}

certora/specs/methods/IERC3156FlashBorrower.spec

@@ -0,0 +1,3 @@
+methods {
+    function _.onFlashLoan(address,address,uint256,uint256,bytes) external => DISPATCHER(true);
+}

certora/specs/methods/IERC3156FlashLender.spec

@@ -0,0 +1,5 @@
+methods {
+    function maxFlashLoan(address)                    external returns (uint256) envfree;
+    function flashFee(address,uint256)                external returns (uint256) envfree;
+    function flashLoan(address,address,uint256,bytes) external returns (bool);
+}

certora/specs/methods/IERC5313.spec

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

certora/specs/methods/IERC721.spec

@@ -1,20 +1,17 @@
 methods {
     // IERC721
-    balanceOf(address)                              returns (uint256) envfree => DISPATCHER(true)
-    ownerOf(uint256)                                returns (address) envfree => DISPATCHER(true)
-    getApproved(uint256)                            returns (address) envfree => DISPATCHER(true)
-    isApprovedForAll(address,address)               returns (bool)    envfree => DISPATCHER(true)
-    safeTransferFrom(address,address,uint256,bytes)                           => DISPATCHER(true)
-    safeTransferFrom(address,address,uint256)                                 => DISPATCHER(true)
-    transferFrom(address,address,uint256)                                     => DISPATCHER(true)
-    approve(address,uint256)                                                  => DISPATCHER(true)
-    setApprovalForAll(address,bool)                                           => DISPATCHER(true)
+    function balanceOf(address)                              external returns (uint256) envfree;
+    function ownerOf(uint256)                                external returns (address) envfree;
+    function getApproved(uint256)                            external returns (address) envfree;
+    function isApprovedForAll(address,address)               external returns (bool)    envfree;
+    function safeTransferFrom(address,address,uint256,bytes) external;
+    function safeTransferFrom(address,address,uint256)       external;
+    function transferFrom(address,address,uint256)           external;
+    function approve(address,uint256)                        external;
+    function setApprovalForAll(address,bool)                 external;
 
     // IERC721Metadata
-    name()                                          returns (string)          => DISPATCHER(true)
-    symbol()                                        returns (string)          => DISPATCHER(true)
-    tokenURI(uint256)                               returns (string)          => DISPATCHER(true)
-
-    // IERC721Receiver
-    onERC721Received(address,address,uint256,bytes) returns (bytes4)          => DISPATCHER(true)
+    function name()                                          external returns (string);
+    function symbol()                                        external returns (string);
+    function tokenURI(uint256)                               external returns (string);
 }

certora/specs/methods/IERC721Receiver.spec

@@ -0,0 +1,3 @@
+methods {
+  function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
+}

certora/specs/methods/IOwnable.spec

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

certora/specs/methods/IOwnable2Step.spec

@@ -1,7 +1,7 @@
 methods {
-    owner() returns (address) envfree
-    pendingOwner() returns (address) envfree
-    transferOwnership(address)
-    acceptOwnership()
-    renounceOwnership()
+    function owner() external returns (address) envfree;
+    function pendingOwner() external returns (address) envfree;
+    function transferOwnership(address) external;
+    function acceptOwnership() external;
+    function renounceOwnership() external;
 }

contracts/access/Ownable.sol

@@ -36,6 +36,9 @@ abstract contract Ownable is Context {
      * @dev Initializes the contract setting the address provided by the deployer as the initial owner.
      */
     constructor(address initialOwner) {
+        if (initialOwner == address(0)) {
+            revert OwnableInvalidOwner(address(0));
+        }
         _transferOwnership(initialOwner);
     }
 

contracts/finance/VestingWallet.sol

@@ -31,11 +31,6 @@ contract VestingWallet is Context, Ownable {
     event EtherReleased(uint256 amount);
     event ERC20Released(address indexed token, uint256 amount);
 
-    /**
-     * @dev The `beneficiary` is not a valid account.
-     */
-    error VestingWalletInvalidBeneficiary(address beneficiary);
-
     uint256 private _released;
     mapping(address token => uint256) private _erc20Released;
     uint64 private immutable _start;
@@ -46,10 +41,6 @@ contract VestingWallet is Context, Ownable {
      * vesting duration of the vesting wallet.
      */
     constructor(address beneficiary, uint64 startTimestamp, uint64 durationSeconds) payable Ownable(beneficiary) {
-        if (beneficiary == address(0)) {
-            revert VestingWalletInvalidBeneficiary(address(0));
-        }
-
         _start = startTimestamp;
         _duration = durationSeconds;
     }

contracts/governance/Governor.sol

@@ -306,8 +306,8 @@ abstract contract Governor is Context, ERC165, EIP712, Nonces, IGovernor, IERC72
         bytes[] memory calldatas,
         string memory description,
         address proposer
-    ) internal virtual returns (uint256) {
-        uint256 proposalId = hashProposal(targets, values, calldatas, keccak256(bytes(description)));
+    ) internal virtual returns (uint256 proposalId) {
+        proposalId = hashProposal(targets, values, calldatas, keccak256(bytes(description)));
 
         if (targets.length != values.length || targets.length != calldatas.length || targets.length == 0) {
             revert GovernorInvalidProposalLength(targets.length, calldatas.length, values.length);
@@ -336,7 +336,7 @@ abstract contract Governor is Context, ERC165, EIP712, Nonces, IGovernor, IERC72
             description
         );
 
-        return proposalId;
+        // Using a named return variable to avoid stack too deep errors
     }
 
     /**

contracts/governance/extensions/GovernorVotes.sol

@@ -12,10 +12,17 @@ import {SafeCast} from "../../utils/math/SafeCast.sol";
  * @dev Extension of {Governor} for voting weight extraction from an {ERC20Votes} token, or since v4.5 an {ERC721Votes} token.
  */
 abstract contract GovernorVotes is Governor {
-    IERC5805 public immutable token;
+    IERC5805 private immutable _token;
 
     constructor(IVotes tokenAddress) {
-        token = IERC5805(address(tokenAddress));
+        _token = IERC5805(address(tokenAddress));
+    }
+
+    /**
+     * @dev The token that voting power is sourced from.
+     */
+    function token() public view virtual returns (IERC5805) {
+        return _token;
     }
 
     /**
@@ -23,7 +30,7 @@ abstract contract GovernorVotes is Governor {
      * does not implement EIP-6372.
      */
     function clock() public view virtual override returns (uint48) {
-        try token.clock() returns (uint48 timepoint) {
+        try token().clock() returns (uint48 timepoint) {
             return timepoint;
         } catch {
             return SafeCast.toUint48(block.number);
@@ -35,7 +42,7 @@ abstract contract GovernorVotes is Governor {
      */
     // solhint-disable-next-line func-name-mixedcase
     function CLOCK_MODE() public view virtual override returns (string memory) {
-        try token.CLOCK_MODE() returns (string memory clockmode) {
+        try token().CLOCK_MODE() returns (string memory clockmode) {
             return clockmode;
         } catch {
             return "mode=blocknumber&from=default";
@@ -50,6 +57,6 @@ abstract contract GovernorVotes is Governor {
         uint256 timepoint,
         bytes memory /*params*/
     ) internal view virtual override returns (uint256) {
-        return token.getPastVotes(account, timepoint);
+        return token().getPastVotes(account, timepoint);
     }
 }

contracts/governance/extensions/GovernorVotesQuorumFraction.sol

@@ -71,7 +71,7 @@ abstract contract GovernorVotesQuorumFraction is GovernorVotes {
      * @dev Returns the quorum for a timepoint, in terms of number of votes: `supply * numerator / denominator`.
      */
     function quorum(uint256 timepoint) public view virtual override returns (uint256) {
-        return (token.getPastTotalSupply(timepoint) * quorumNumerator(timepoint)) / quorumDenominator();
+        return (token().getPastTotalSupply(timepoint) * quorumNumerator(timepoint)) / quorumDenominator();
     }
 
     /**

contracts/mocks/token/ERC20PermitNoRevertMock.sol

@@ -1,35 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.20;
-
-import {ERC20Permit} from "../../token/ERC20/extensions/ERC20Permit.sol";
-
-abstract contract ERC20PermitNoRevertMock is ERC20Permit {
-    function permitThatMayRevert(
-        address owner,
-        address spender,
-        uint256 value,
-        uint256 deadline,
-        uint8 v,
-        bytes32 r,
-        bytes32 s
-    ) public virtual {
-        super.permit(owner, spender, value, deadline, v, r, s);
-    }
-
-    function permit(
-        address owner,
-        address spender,
-        uint256 value,
-        uint256 deadline,
-        uint8 v,
-        bytes32 r,
-        bytes32 s
-    ) public virtual override {
-        try this.permitThatMayRevert(owner, spender, value, deadline, v, r, s) {
-            // do nothing
-        } catch {
-            // do nothing
-        }
-    }
-}

contracts/token/ERC20/ERC20.sol

@@ -30,10 +30,6 @@ import {IERC20Errors} from "../../interfaces/draft-IERC6093.sol";
  * This allows applications to reconstruct the allowance for all accounts just
  * by listening to said events. Other implementations of the EIP may not emit
  * these events, as it isn't required by the specification.
- *
- * Finally, the non-standard {decreaseAllowance} and {increaseAllowance}
- * functions have been added to mitigate the well-known issues around setting
- * allowances. See {IERC20-approve}.
  */
 abstract contract ERC20 is Context, IERC20, IERC20Metadata, IERC20Errors {
     mapping(address account => uint256) private _balances;
@@ -167,54 +163,6 @@ abstract contract ERC20 is Context, IERC20, IERC20Metadata, IERC20Errors {
         return true;
     }
 
-    /**
-     * @dev Atomically increases the allowance granted to `spender` by the caller.
-     *
-     * This is an alternative to {approve} that can be used as a mitigation for
-     * problems described in {IERC20-approve}.
-     *
-     * Emits an {Approval} event indicating the updated allowance.
-     *
-     * Requirements:
-     *
-     * - `spender` cannot be the zero address.
-     */
-    function increaseAllowance(address spender, uint256 addedValue) public virtual returns (bool) {
-        address owner = _msgSender();
-        _approve(owner, spender, allowance(owner, spender) + addedValue);
-        return true;
-    }
-
-    /**
-     * @dev Atomically decreases the allowance granted to `spender` by the caller.
-     *
-     * This is an alternative to {approve} that can be used as a mitigation for
-     * problems described in {IERC20-approve}.
-     *
-     * Emits an {Approval} event indicating the updated allowance.
-     *
-     * Requirements:
-     *
-     * - `spender` cannot be the zero address.
-     * - `spender` must have allowance for the caller of at least
-     * `requestedDecrease`.
-     *
-     * NOTE: Although this function is designed to avoid double spending with {approval},
-     * it can still be frontrunned, preventing any attempt of allowance reduction.
-     */
-    function decreaseAllowance(address spender, uint256 requestedDecrease) public virtual returns (bool) {
-        address owner = _msgSender();
-        uint256 currentAllowance = allowance(owner, spender);
-        if (currentAllowance < requestedDecrease) {
-            revert ERC20FailedDecreaseAllowance(spender, currentAllowance, requestedDecrease);
-        }
-        unchecked {
-            _approve(owner, spender, currentAllowance - requestedDecrease);
-        }
-
-        return true;
-    }
-
     /**
      * @dev Moves a `value` amount of tokens from `from` to `to`.
      *
@@ -287,7 +235,7 @@ abstract contract ERC20 is Context, IERC20, IERC20Metadata, IERC20Errors {
     }
 
     /**
-     * @dev Destroys a `value` amount of tokens from `account`, by transferring it to address(0).
+     * @dev Destroys a `value` amount of tokens from `account`, lowering the total supply.
      * Relies on the `_update` mechanism.
      *
      * Emits a {Transfer} event with `to` set to the zero address.

contracts/token/ERC20/README.adoc

@@ -15,10 +15,10 @@ There are a few core contracts that implement the behavior specified in the EIP:
 
 Additionally there are multiple custom extensions, including:
 
+* {ERC20Permit}: gasless approval of tokens (standardized as ERC2612).
 * {ERC20Burnable}: destruction of own tokens.
 * {ERC20Capped}: enforcement of a cap to the total supply when minting tokens.
 * {ERC20Pausable}: ability to pause token transfers.
-* {ERC20Permit}: gasless approval of tokens (standardized as ERC2612).
 * {ERC20FlashMint}: token level support for flash loans through the minting and burning of ephemeral tokens (standardized as ERC3156).
 * {ERC20Votes}: support for voting and vote delegation.
 * {ERC20Wrapper}: wrapper to create an ERC20 backed by another ERC20, with deposit and withdraw methods. Useful in conjunction with {ERC20Votes}.
@@ -44,14 +44,16 @@ NOTE: This core set of contracts is designed to be unopinionated, allowing devel
 
 == Extensions
 
+{{IERC20Permit}}
+
+{{ERC20Permit}}
+
 {{ERC20Burnable}}
 
 {{ERC20Capped}}
 
 {{ERC20Pausable}}
 
-{{ERC20Permit}}
-
 {{ERC20Votes}}
 
 {{ERC20Wrapper}}

contracts/token/ERC20/extensions/ERC20Permit.sol

@@ -39,7 +39,7 @@ abstract contract ERC20Permit is ERC20, IERC20Permit, EIP712, Nonces {
     constructor(string memory name) EIP712(name, "1") {}
 
     /**
-     * @dev See {IERC20Permit-permit}.
+     * @inheritdoc IERC20Permit
      */
     function permit(
         address owner,
@@ -67,14 +67,14 @@ abstract contract ERC20Permit is ERC20, IERC20Permit, EIP712, Nonces {
     }
 
     /**
-     * @dev See {IERC20Permit-nonces}.
+     * @inheritdoc IERC20Permit
      */
     function nonces(address owner) public view virtual override(IERC20Permit, Nonces) returns (uint256) {
         return super.nonces(owner);
     }
 
     /**
-     * @dev See {IERC20Permit-DOMAIN_SEPARATOR}.
+     * @inheritdoc IERC20Permit
      */
     // solhint-disable-next-line func-name-mixedcase
     function DOMAIN_SEPARATOR() external view virtual returns (bytes32) {

contracts/token/ERC20/extensions/IERC20Permit.sol

@@ -10,6 +10,34 @@ pragma solidity ^0.8.20;
  * Adds the {permit} method, which can be used to change an account's ERC20 allowance (see {IERC20-allowance}) by
  * presenting a message signed by the account. By not relying on {IERC20-approve}, the token holder account doesn't
  * need to send a transaction, and thus is not required to hold Ether at all.
+ *
+ * ==== Security Considerations
+ *
+ * There are two important considerations concerning the use of `permit`. The first is that a valid permit signature
+ * expresses an allowance, and it should not be assumed to convey additional meaning. In particular, it should not be
+ * considered as an intention to spend the allowance in any specific way. The second is that because permits have
+ * built-in replay protection and can be submitted by anyone, they can be frontrun. A protocol that uses permits should
+ * take this into consideration and allow a `permit` call to fail. Combining these two aspects, a pattern that may be
+ * generally recommended is:
+ *
+ * ```solidity
+ * function doThingWithPermit(..., uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) public {
+ *     try token.permit(msg.sender, address(this), value, deadline, v, r, s) {} catch {}
+ *     doThing(..., value);
+ * }
+ *
+ * function doThing(..., uint256 value) public {
+ *     token.safeTransferFrom(msg.sender, address(this), value);
+ *     ...
+ * }
+ * ```
+ *
+ * Observe that: 1) `msg.sender` is used as the owner, leaving no ambiguity as to the signer intent, and 2) the use of
+ * `try/catch` allows the permit to fail and makes the code tolerant to frontrunning. (See also
+ * {SafeERC20-safeTransferFrom}).
+ *
+ * Additionally, note that smart contract wallets (such as Argent or Safe) are not able to produce permit signatures, so
+ * contracts should have entry points that don't rely on permit.
  */
 interface IERC20Permit {
     /**
@@ -32,6 +60,8 @@ interface IERC20Permit {
      * For more information on the signature format, see the
      * https://eips.ethereum.org/EIPS/eip-2612#specification[relevant EIP
      * section].
+     *
+     * CAUTION: See Security Considerations above.
      */
     function permit(
         address owner,

contracts/token/ERC20/utils/SafeERC20.sol

@@ -82,28 +82,6 @@ library SafeERC20 {
         }
     }
 
-    /**
-     * @dev Use a ERC-2612 signature to set the `owner` approval toward `spender` on `token`.
-     * Revert on invalid signature.
-     */
-    function safePermit(
-        IERC20Permit token,
-        address owner,
-        address spender,
-        uint256 value,
-        uint256 deadline,
-        uint8 v,
-        bytes32 r,
-        bytes32 s
-    ) internal {
-        uint256 nonceBefore = token.nonces(owner);
-        token.permit(owner, spender, value, deadline, v, r, s);
-        uint256 nonceAfter = token.nonces(owner);
-        if (nonceAfter != nonceBefore + 1) {
-            revert SafeERC20FailedOperation(address(token));
-        }
-    }
-
     /**
      * @dev Imitates a Solidity high-level call (i.e. a regular function call to a contract), relaxing the requirement
      * on the return value: the return value is optional (but if data is returned, it must not be false).

package-lock.json

@@ -44,8 +44,8 @@
         "semver": "^7.3.5",
         "solhint": "^3.3.6",
         "solhint-plugin-openzeppelin": "file:scripts/solhint-custom",
-        "solidity-ast": "^0.4.25",
-        "solidity-coverage": "^0.8.4",
+        "solidity-ast": "^0.4.50",
+        "solidity-coverage": "^0.8.0",
         "solidity-docgen": "^0.6.0-beta.29",
         "undici": "^5.22.1",
         "web3": "^1.3.0",
@@ -3221,6 +3221,25 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
+    "node_modules/array.prototype.findlast": {
+      "version": "1.2.2",
+      "resolved": "https://registry.npmjs.org/array.prototype.findlast/-/array.prototype.findlast-1.2.2.tgz",
+      "integrity": "sha512-p1YDNPNqA+P6cPX9ATsxg7DKir7gOmJ+jh5dEP3LlumMNYVC1F2Jgnyh6oI3n/qD9FeIkqR2jXfd73G68ImYUQ==",
+      "dev": true,
+      "dependencies": {
+        "call-bind": "^1.0.2",
+        "define-properties": "^1.1.4",
+        "es-abstract": "^1.20.4",
+        "es-shim-unscopables": "^1.0.0",
+        "get-intrinsic": "^1.1.3"
+      },
+      "engines": {
+        "node": ">= 0.4"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/ljharb"
+      }
+    },
     "node_modules/array.prototype.flat": {
       "version": "1.3.1",
       "resolved": "https://registry.npmjs.org/array.prototype.flat/-/array.prototype.flat-1.3.1.tgz",
@@ -12569,10 +12588,13 @@
       }
     },
     "node_modules/solidity-ast": {
-      "version": "0.4.49",
-      "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.49.tgz",
-      "integrity": "sha512-Pr5sCAj1SFqzwFZw1HPKSq0PehlQNdM8GwKyAVYh2DOn7/cCK8LUKD1HeHnKtTgBW7hi9h4nnnan7hpAg5RhWQ==",
-      "dev": true
+      "version": "0.4.50",
+      "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.50.tgz",
+      "integrity": "sha512-WpIhaUibbjcBY4bg8TO2UXFWl8PQPhtH1QtMYJUqFUGxx0rRiEFsVLV+ow8XiWEnSPeu4xPp1/K43P4esxuK1Q==",
+      "dev": true,
+      "dependencies": {
+        "array.prototype.findlast": "^1.2.2"
+      }
     },
     "node_modules/solidity-comments": {
       "version": "0.0.2",
@@ -17853,6 +17875,19 @@
         "es-shim-unscopables": "^1.0.0"
       }
     },
+    "array.prototype.findlast": {
+      "version": "1.2.2",
+      "resolved": "https://registry.npmjs.org/array.prototype.findlast/-/array.prototype.findlast-1.2.2.tgz",
+      "integrity": "sha512-p1YDNPNqA+P6cPX9ATsxg7DKir7gOmJ+jh5dEP3LlumMNYVC1F2Jgnyh6oI3n/qD9FeIkqR2jXfd73G68ImYUQ==",
+      "dev": true,
+      "requires": {
+        "call-bind": "^1.0.2",
+        "define-properties": "^1.1.4",
+        "es-abstract": "^1.20.4",
+        "es-shim-unscopables": "^1.0.0",
+        "get-intrinsic": "^1.1.3"
+      }
+    },
     "array.prototype.flat": {
       "version": "1.3.1",
       "resolved": "https://registry.npmjs.org/array.prototype.flat/-/array.prototype.flat-1.3.1.tgz",
@@ -25144,10 +25179,13 @@
       "version": "file:scripts/solhint-custom"
     },
     "solidity-ast": {
-      "version": "0.4.49",
-      "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.49.tgz",
-      "integrity": "sha512-Pr5sCAj1SFqzwFZw1HPKSq0PehlQNdM8GwKyAVYh2DOn7/cCK8LUKD1HeHnKtTgBW7hi9h4nnnan7hpAg5RhWQ==",
-      "dev": true
+      "version": "0.4.50",
+      "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.50.tgz",
+      "integrity": "sha512-WpIhaUibbjcBY4bg8TO2UXFWl8PQPhtH1QtMYJUqFUGxx0rRiEFsVLV+ow8XiWEnSPeu4xPp1/K43P4esxuK1Q==",
+      "dev": true,
+      "requires": {
+        "array.prototype.findlast": "^1.2.2"
+      }
     },
     "solidity-comments": {
       "version": "0.0.2",

package.json

@@ -85,7 +85,7 @@
     "semver": "^7.3.5",
     "solhint": "^3.3.6",
     "solhint-plugin-openzeppelin": "file:scripts/solhint-custom",
-    "solidity-ast": "^0.4.25",
+    "solidity-ast": "^0.4.50",
     "solidity-coverage": "^0.8.0",
     "solidity-docgen": "^0.6.0-beta.29",
     "undici": "^5.22.1",

requirements.txt

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

scripts/upgradeable/transpile.sh

@@ -22,6 +22,8 @@ fi
 # -i: use included Initializable
 # -x: exclude proxy-related contracts with a few exceptions
 # -p: emit public initializer
+# -n: use namespaces
+# -N: exclude from namespaces transformation
 npx @openzeppelin/upgrade-safe-transpiler@latest -D \
   -b "$build_info" \
   -i contracts/proxy/utils/Initializable.sol \
@@ -32,7 +34,9 @@ npx @openzeppelin/upgrade-safe-transpiler@latest -D \
   -x '!contracts/proxy/ERC1967/ERC1967Utils.sol' \
   -x '!contracts/proxy/utils/UUPSUpgradeable.sol' \
   -x '!contracts/proxy/beacon/IBeacon.sol' \
-  -p 'contracts/**/presets/**/*'
+  -p 'contracts/**/presets/**/*' \
+  -n \
+  -N 'contracts/mocks/**/*'
 
 # delete compilation artifacts of vanilla code
 npm run clean

test/access/Ownable.test.js

@@ -14,6 +14,10 @@ contract('Ownable', function (accounts) {
     this.ownable = await Ownable.new(owner);
   });
 
+  it('rejects zero address for initialOwner', async function () {
+    await expectRevertCustomError(Ownable.new(constants.ZERO_ADDRESS), 'OwnableInvalidOwner', [constants.ZERO_ADDRESS]);
+  });
+
   it('has an owner', async function () {
     expect(await this.ownable.owner()).to.equal(owner);
   });

test/finance/VestingWallet.test.js

@@ -23,7 +23,7 @@ contract('VestingWallet', function (accounts) {
   it('rejects zero address for beneficiary', async function () {
     await expectRevertCustomError(
       VestingWallet.new(constants.ZERO_ADDRESS, this.start, duration),
-      'VestingWalletInvalidBeneficiary',
+      'OwnableInvalidOwner',
       [constants.ZERO_ADDRESS],
     );
   });

test/token/ERC20/ERC20.test.js

@@ -42,167 +42,6 @@ contract('ERC20', function (accounts) {
         expect(await this.token.decimals()).to.be.bignumber.equal('18');
       });
 
-      describe('decrease allowance', function () {
-        describe('when the spender is not the zero address', function () {
-          const spender = recipient;
-
-          function shouldDecreaseApproval(value) {
-            describe('when there was no approved value before', function () {
-              it('reverts', async function () {
-                const allowance = await this.token.allowance(initialHolder, spender);
-                await expectRevertCustomError(
-                  this.token.decreaseAllowance(spender, value, { from: initialHolder }),
-                  'ERC20FailedDecreaseAllowance',
-                  [spender, allowance, value],
-                );
-              });
-            });
-
-            describe('when the spender had an approved value', function () {
-              const approvedValue = value;
-
-              beforeEach(async function () {
-                await this.token.approve(spender, approvedValue, { from: initialHolder });
-              });
-
-              it('emits an approval event', async function () {
-                expectEvent(
-                  await this.token.decreaseAllowance(spender, approvedValue, { from: initialHolder }),
-                  'Approval',
-                  { owner: initialHolder, spender: spender, value: new BN(0) },
-                );
-              });
-
-              it('decreases the spender allowance subtracting the requested value', async function () {
-                await this.token.decreaseAllowance(spender, approvedValue.subn(1), { from: initialHolder });
-
-                expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal('1');
-              });
-
-              it('sets the allowance to zero when all allowance is removed', async function () {
-                await this.token.decreaseAllowance(spender, approvedValue, { from: initialHolder });
-                expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal('0');
-              });
-
-              it('reverts when more than the full allowance is removed', async function () {
-                await expectRevertCustomError(
-                  this.token.decreaseAllowance(spender, approvedValue.addn(1), { from: initialHolder }),
-                  'ERC20FailedDecreaseAllowance',
-                  [spender, approvedValue, approvedValue.addn(1)],
-                );
-              });
-            });
-          }
-
-          describe('when the sender has enough balance', function () {
-            const value = initialSupply;
-
-            shouldDecreaseApproval(value);
-          });
-
-          describe('when the sender does not have enough balance', function () {
-            const value = initialSupply.addn(1);
-
-            shouldDecreaseApproval(value);
-          });
-        });
-
-        describe('when the spender is the zero address', function () {
-          const value = initialSupply;
-          const spender = ZERO_ADDRESS;
-
-          it('reverts', async function () {
-            await expectRevertCustomError(
-              this.token.decreaseAllowance(spender, value, { from: initialHolder }),
-              'ERC20FailedDecreaseAllowance',
-              [spender, 0, value],
-            );
-          });
-        });
-      });
-
-      describe('increase allowance', function () {
-        const value = initialSupply;
-
-        describe('when the spender is not the zero address', function () {
-          const spender = recipient;
-
-          describe('when the sender has enough balance', function () {
-            it('emits an approval event', async function () {
-              expectEvent(await this.token.increaseAllowance(spender, value, { from: initialHolder }), 'Approval', {
-                owner: initialHolder,
-                spender: spender,
-                value: value,
-              });
-            });
-
-            describe('when there was no approved value before', function () {
-              it('approves the requested value', async function () {
-                await this.token.increaseAllowance(spender, value, { from: initialHolder });
-
-                expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value);
-              });
-            });
-
-            describe('when the spender had an approved value', function () {
-              beforeEach(async function () {
-                await this.token.approve(spender, new BN(1), { from: initialHolder });
-              });
-
-              it('increases the spender allowance adding the requested value', async function () {
-                await this.token.increaseAllowance(spender, value, { from: initialHolder });
-
-                expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value.addn(1));
-              });
-            });
-          });
-
-          describe('when the sender does not have enough balance', function () {
-            const value = initialSupply.addn(1);
-
-            it('emits an approval event', async function () {
-              expectEvent(await this.token.increaseAllowance(spender, value, { from: initialHolder }), 'Approval', {
-                owner: initialHolder,
-                spender: spender,
-                value: value,
-              });
-            });
-
-            describe('when there was no approved value before', function () {
-              it('approves the requested value', async function () {
-                await this.token.increaseAllowance(spender, value, { from: initialHolder });
-
-                expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value);
-              });
-            });
-
-            describe('when the spender had an approved value', function () {
-              beforeEach(async function () {
-                await this.token.approve(spender, new BN(1), { from: initialHolder });
-              });
-
-              it('increases the spender allowance adding the requested value', async function () {
-                await this.token.increaseAllowance(spender, value, { from: initialHolder });
-
-                expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value.addn(1));
-              });
-            });
-          });
-        });
-
-        describe('when the spender is the zero address', function () {
-          const spender = ZERO_ADDRESS;
-
-          it('reverts', async function () {
-            await expectRevertCustomError(
-              this.token.increaseAllowance(spender, value, { from: initialHolder }),
-              'ERC20InvalidSpender',
-              [ZERO_ADDRESS],
-            );
-          });
-        });
-      });
-
       describe('_mint', function () {
         const value = new BN(50);
         it('rejects a null account', async function () {

test/token/ERC20/utils/SafeERC20.test.js

@@ -4,16 +4,10 @@ const SafeERC20 = artifacts.require('$SafeERC20');
 const ERC20ReturnFalseMock = artifacts.require('$ERC20ReturnFalseMock');
 const ERC20ReturnTrueMock = artifacts.require('$ERC20'); // default implementation returns true
 const ERC20NoReturnMock = artifacts.require('$ERC20NoReturnMock');
-const ERC20PermitNoRevertMock = artifacts.require('$ERC20PermitNoRevertMock');
 const ERC20ForceApproveMock = artifacts.require('$ERC20ForceApproveMock');
 
-const { getDomain, domainType, Permit } = require('../../../helpers/eip712');
 const { expectRevertCustomError } = require('../../../helpers/customError');
 
-const { fromRpcSig } = require('ethereumjs-util');
-const ethSigUtil = require('eth-sig-util');
-const Wallet = require('ethereumjs-wallet').default;
-
 const name = 'ERC20Mock';
 const symbol = 'ERC20Mock';
 
@@ -122,123 +116,6 @@ contract('SafeERC20', function (accounts) {
     shouldOnlyRevertOnErrors(accounts);
   });
 
-  describe("with token that doesn't revert on invalid permit", function () {
-    const wallet = Wallet.generate();
-    const owner = wallet.getAddressString();
-    const spender = hasNoCode;
-
-    beforeEach(async function () {
-      this.token = await ERC20PermitNoRevertMock.new(name, symbol, name);
-
-      this.data = await getDomain(this.token).then(domain => ({
-        primaryType: 'Permit',
-        types: { EIP712Domain: domainType(domain), Permit },
-        domain,
-        message: { owner, spender, value: '42', nonce: '0', deadline: constants.MAX_UINT256 },
-      }));
-
-      this.signature = fromRpcSig(ethSigUtil.signTypedMessage(wallet.getPrivateKey(), { data: this.data }));
-    });
-
-    it('accepts owner signature', async function () {
-      expect(await this.token.nonces(owner)).to.be.bignumber.equal('0');
-      expect(await this.token.allowance(owner, spender)).to.be.bignumber.equal('0');
-
-      await this.mock.$safePermit(
-        this.token.address,
-        this.data.message.owner,
-        this.data.message.spender,
-        this.data.message.value,
-        this.data.message.deadline,
-        this.signature.v,
-        this.signature.r,
-        this.signature.s,
-      );
-
-      expect(await this.token.nonces(owner)).to.be.bignumber.equal('1');
-      expect(await this.token.allowance(owner, spender)).to.be.bignumber.equal(this.data.message.value);
-    });
-
-    it('revert on reused signature', async function () {
-      expect(await this.token.nonces(owner)).to.be.bignumber.equal('0');
-      // use valid signature and consume nounce
-      await this.mock.$safePermit(
-        this.token.address,
-        this.data.message.owner,
-        this.data.message.spender,
-        this.data.message.value,
-        this.data.message.deadline,
-        this.signature.v,
-        this.signature.r,
-        this.signature.s,
-      );
-      expect(await this.token.nonces(owner)).to.be.bignumber.equal('1');
-      // invalid call does not revert for this token implementation
-      await this.token.permit(
-        this.data.message.owner,
-        this.data.message.spender,
-        this.data.message.value,
-        this.data.message.deadline,
-        this.signature.v,
-        this.signature.r,
-        this.signature.s,
-      );
-      expect(await this.token.nonces(owner)).to.be.bignumber.equal('1');
-      // invalid call revert when called through the SafeERC20 library
-      await expectRevertCustomError(
-        this.mock.$safePermit(
-          this.token.address,
-          this.data.message.owner,
-          this.data.message.spender,
-          this.data.message.value,
-          this.data.message.deadline,
-          this.signature.v,
-          this.signature.r,
-          this.signature.s,
-        ),
-        'SafeERC20FailedOperation',
-        [this.token.address],
-      );
-      expect(await this.token.nonces(owner)).to.be.bignumber.equal('1');
-    });
-
-    it('revert on invalid signature', async function () {
-      // signature that is not valid for owner
-      const invalidSignature = {
-        v: 27,
-        r: '0x71753dc5ecb5b4bfc0e3bc530d79ce5988760ed3f3a234c86a5546491f540775',
-        s: '0x0049cedee5aed990aabed5ad6a9f6e3c565b63379894b5fa8b512eb2b79e485d',
-      };
-
-      // invalid call does not revert for this token implementation
-      await this.token.permit(
-        this.data.message.owner,
-        this.data.message.spender,
-        this.data.message.value,
-        this.data.message.deadline,
-        invalidSignature.v,
-        invalidSignature.r,
-        invalidSignature.s,
-      );
-
-      // invalid call revert when called through the SafeERC20 library
-      await expectRevertCustomError(
-        this.mock.$safePermit(
-          this.token.address,
-          this.data.message.owner,
-          this.data.message.spender,
-          this.data.message.value,
-          this.data.message.deadline,
-          invalidSignature.v,
-          invalidSignature.r,
-          invalidSignature.s,
-        ),
-        'SafeERC20FailedOperation',
-        [this.token.address],
-      );
-    });
-  });
-
   describe('with usdt approval beaviour', function () {
     const spender = hasNoCode;