Migrate FV specs to CVL2 (#4527)

Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>

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,15 @@
-import "helpers/helpers.spec"
-import "methods/IERC20.spec"
-import "methods/IERC2612.spec"
+import "helpers/helpers.spec";
+import "methods/IERC20.spec";
+import "methods/IERC2612.spec";
 
 methods {
     // non standard ERC20 functions
-    increaseAllowance(address,uint256) returns (bool)
-    decreaseAllowance(address,uint256) returns (bool)
+    function increaseAllowance(address,uint256) external returns (bool);
+    function decreaseAllowance(address,uint256) external returns (bool);
 
     // exposed for FV
-    mint(address,uint256)
-    burn(address,uint256)
+    function mint(address,uint256) external;
+    function burn(address,uint256) external;
 }
 
 /*
@@ -17,12 +17,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 +41,7 @@ hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STOR
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant totalSupplyIsSumOfBalances()
-    totalSupply() == sumOfBalances()
+    to_mathint(totalSupply()) == sumOfBalances;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -39,7 +49,7 @@ invariant totalSupplyIsSumOfBalances()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant zeroAddressNoBalance()
-    balanceOf(0) == 0
+    balanceOf(0) == 0;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -56,8 +66,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 +90,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 +116,18 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) {
     assert (
         allowanceAfter > allowanceBefore
     ) => (
-        (f.selector == approve(address,uint256).selector           && e.msg.sender == holder) ||
-        (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
-        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+        (f.selector == sig:approve(address,uint256).selector           && e.msg.sender == holder) ||
+        (f.selector == sig:increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
+        (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
     );
 
     assert (
         allowanceAfter < allowanceBefore
     ) => (
-        (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
-        (f.selector == approve(address,uint256).selector              && e.msg.sender == holder ) ||
-        (f.selector == decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
-        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+        (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
+        (f.selector == sig:approve(address,uint256).selector              && e.msg.sender == holder ) ||
+        (f.selector == sig:decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
+        (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
     );
 }
 
@@ -147,8 +157,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 +191,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 +226,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 +264,11 @@ rule transferFrom(env e) {
     } else {
         // allowance is valid & updated
         assert allowanceBefore            >= amount;
-        assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
+        assert to_mathint(allowance(holder, spender)) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount);
 
         // balances of holder and recipient are updated
-        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
-        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+        assert to_mathint(balanceOf(holder))    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
 
         // no other balance is modified
         assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
@@ -323,7 +333,7 @@ rule increaseAllowance(env e) {
         assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256;
     } else {
         // allowance is updated
-        assert allowance(holder, spender) == allowanceBefore + amount;
+        assert to_mathint(allowance(holder, spender)) == allowanceBefore + amount;
 
         // other allowances are untouched
         assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
@@ -356,7 +366,7 @@ rule decreaseAllowance(env e) {
         assert holder == 0 || spender == 0 || allowanceBefore < amount;
     } else {
         // allowance is updated
-        assert allowance(holder, spender) == allowanceBefore - amount;
+        assert to_mathint(allowance(holder, spender)) == allowanceBefore - amount;
 
         // other allowances are untouched
         assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
@@ -402,7 +412,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;
 }

requirements.txt

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