dexorder

lib_openzeppelin_contracts/certora/specs/AccessControl.spec

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

lib_openzeppelin_contracts/certora/specs/AccessControlDefaultAdminRules.spec

@@ -0,0 +1,464 @@
+import "helpers/helpers.spec";
+import "methods/IAccessControlDefaultAdminRules.spec";
+import "methods/IAccessControl.spec";
+import "AccessControl.spec";
+
+use rule onlyGrantCanGrant filtered {
+  f -> f.selector != sig:acceptDefaultAdminTransfer().selector
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition timeSanity(env e) returns bool =
+  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;
+
+definition isSet(uint48 schedule) returns bool =
+  schedule != 0;
+
+definition hasPassed(env e, uint48 schedule) returns bool =
+  assert_uint256(schedule) < e.block.timestamp;
+
+definition increasingDelaySchedule(env e, uint48 newDelay) returns mathint =
+  e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait());
+
+definition decreasingDelaySchedule(env e, uint48 newDelay) returns mathint =
+  e.block.timestamp + defaultAdminDelay(e) - newDelay;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: defaultAdmin holds the DEFAULT_ADMIN_ROLE                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant defaultAdminConsistency(address account)
+  (account == defaultAdmin() && account != 0) <=> hasRole(DEFAULT_ADMIN_ROLE(), account)
+  {
+    preserved with (env e) {
+      require nonzerosender(e);
+    }
+  }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: Only one account holds the DEFAULT_ADMIN_ROLE                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant singleDefaultAdmin(address account, address another)
+  hasRole(DEFAULT_ADMIN_ROLE(), account) && hasRole(DEFAULT_ADMIN_ROLE(), another) => another == account
+  {
+    preserved {
+      requireInvariant defaultAdminConsistency(account);
+      requireInvariant defaultAdminConsistency(another);
+    }
+  }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: DEFAULT_ADMIN_ROLE's admin is always DEFAULT_ADMIN_ROLE                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant defaultAdminRoleAdminConsistency()
+  getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE();
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: owner is the defaultAdmin                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant ownerConsistency()
+  defaultAdmin() == owner();
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: revokeRole only affects the specified user/role combo                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule revokeRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    revokeRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> isCallerAdmin && role != DEFAULT_ADMIN_ROLE(),
+      "roles can only be revoked by their owner except for the default admin role";
+
+    // effect
+    assert success => !hasRole(role, account),
+      "role is revoked";
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount),
+      "no other role is affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceRole only affects the specified user/role combo                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool    hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+    address adminBefore        = defaultAdmin();
+    address pendingAdminBefore = pendingDefaultAdmin_();
+    uint48  scheduleBefore     = pendingDefaultAdminSchedule_();
+
+    renounceRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool    hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+    address adminAfter        = defaultAdmin();
+    address pendingAdminAfter = pendingDefaultAdmin_();
+    uint48  scheduleAfter     = pendingDefaultAdminSchedule_();
+
+    // liveness
+    assert success <=> (
+      account == e.msg.sender &&
+      (
+        role    != DEFAULT_ADMIN_ROLE() ||
+        account != adminBefore        ||
+        (
+          pendingAdminBefore == 0 &&
+          isSet(scheduleBefore) &&
+          hasPassed(e, scheduleBefore)
+        )
+      )
+    ),
+      "an account only can renounce by itself with a delay for the default admin role";
+
+    // effect
+    assert success => !hasRole(role, account),
+      "role is renounced";
+
+    assert success => (
+      (
+        role    == DEFAULT_ADMIN_ROLE() &&
+        account == adminBefore
+      ) ? (
+        adminAfter        == 0 &&
+        pendingAdminAfter == 0 &&
+        scheduleAfter     == 0
+      ) : (
+        adminAfter        == adminBefore        &&
+        pendingAdminAfter == pendingAdminBefore &&
+        scheduleAfter     == scheduleBefore
+      )
+    ),
+      "renouncing default admin role cleans state iff called by previous admin";
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (
+      role == otherRole &&
+      account == otherAccount
+    ),
+      "no other role is affected";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: defaultAdmin is only affected by accepting an admin transfer or renoucing                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDefaultAdminChange(env e, method f, calldataarg args) {
+  address adminBefore = defaultAdmin();
+  f(e, args);
+  address adminAfter = defaultAdmin();
+
+  assert adminBefore != adminAfter => (
+    f.selector == sig:acceptDefaultAdminTransfer().selector ||
+    f.selector == sig:renounceRole(bytes32,address).selector
+  ),
+    "default admin is only affected by accepting an admin transfer or renoucing";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pendingDefaultAdmin is only affected by beginning, completing (accept or renounce), or canceling an admin     │
+│ transfer                                                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noPendingDefaultAdminChange(env e, method f, calldataarg args) {
+  address pendingAdminBefore = pendingDefaultAdmin_();
+  uint48 scheduleBefore = pendingDefaultAdminSchedule_();
+  f(e, args);
+  address pendingAdminAfter = pendingDefaultAdmin_();
+  uint48 scheduleAfter = pendingDefaultAdminSchedule_();
+
+  assert (
+    pendingAdminBefore != pendingAdminAfter ||
+    scheduleBefore != scheduleAfter
+  ) => (
+    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";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: defaultAdminDelay can't be changed atomically by any function                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDefaultAdminDelayChange(env e, method f, calldataarg args) {
+  uint48 delayBefore = defaultAdminDelay(e);
+  f(e, args);
+  uint48 delayAfter = defaultAdminDelay(e);
+
+  assert delayBefore == delayAfter,
+    "delay can't be changed atomically by any function";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pendingDefaultAdminDelay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) {
+  uint48 pendingDelayBefore = pendingDelay_(e);
+  f(e, args);
+  uint48 pendingDelayAfter = pendingDelay_(e);
+
+  assert pendingDelayBefore != pendingDelayAfter => (
+    f.selector == sig:changeDefaultAdminDelay(uint48).selector ||
+    f.selector == sig:rollbackDefaultAdminDelay().selector
+  ),
+    "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: defaultAdminDelayIncreaseWait can't be changed atomically by any function                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noDefaultAdminDelayIncreaseWaitChange(env e, method f, calldataarg args) {
+  uint48 delayIncreaseWaitBefore = defaultAdminDelayIncreaseWait();
+  f(e, args);
+  uint48 delayIncreaseWaitAfter = defaultAdminDelayIncreaseWait();
+
+  assert delayIncreaseWaitBefore == delayIncreaseWaitAfter,
+    "delay increase wait can't be changed atomically by any function";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: beginDefaultAdminTransfer sets a pending default admin and its schedule                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule beginDefaultAdminTransfer(env e, address newAdmin) {
+  require timeSanity(e);
+  require nonpayable(e);
+  require nonzerosender(e);
+  requireInvariant defaultAdminConsistency(e.msg.sender);
+
+  beginDefaultAdminTransfer@withrevert(e, newAdmin);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can begin a transfer";
+
+  // effect
+  assert success => pendingDefaultAdmin_() == newAdmin,
+    "pending default admin is set";
+  assert success => to_mathint(pendingDefaultAdminSchedule_()) == e.block.timestamp + defaultAdminDelay(e),
+    "pending default admin delay is set";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A default admin can't change in less than the applied schedule                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args, address newAdmin) {
+  require e1.block.timestamp <= e2.block.timestamp;
+
+  uint48 delayBefore = defaultAdminDelay(e1);
+  address adminBefore = defaultAdmin();
+
+  // There might be a better way to generalize this without requiring `beginDefaultAdminTransfer`, but currently
+  // it's the only way in which we can attest that only `delayBefore` has passed before a change.
+  beginDefaultAdminTransfer(e1, newAdmin);
+  f(e2, args);
+
+  address adminAfter = defaultAdmin();
+
+  // change can only happen towards the newAdmin, with the delay
+  assert adminAfter != adminBefore => (
+    adminAfter == newAdmin &&
+    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";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: acceptDefaultAdminTransfer updates defaultAdmin resetting the pending admin and its schedule  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule acceptDefaultAdminTransfer(env e) {
+  require nonpayable(e);
+
+  address pendingAdminBefore = pendingDefaultAdmin_();
+  uint48 scheduleBefore = pendingDefaultAdminSchedule_();
+
+  acceptDefaultAdminTransfer@withrevert(e);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> (
+    e.msg.sender == pendingAdminBefore &&
+    isSet(scheduleBefore) &&
+    hasPassed(e, scheduleBefore)
+  ),
+    "only the pending default admin can accept the role after the schedule has been set and passed";
+
+  // effect
+  assert success => defaultAdmin() == pendingAdminBefore,
+    "Default admin is set to the previous pending default admin";
+  assert success => pendingDefaultAdmin_() == 0,
+    "Pending default admin is reset";
+  assert success => pendingDefaultAdminSchedule_() == 0,
+    "Pending default admin delay is reset";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: cancelDefaultAdminTransfer resets pending default admin and its schedule                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cancelDefaultAdminTransfer(env e) {
+  require nonpayable(e);
+  require nonzerosender(e);
+  requireInvariant defaultAdminConsistency(e.msg.sender);
+
+  cancelDefaultAdminTransfer@withrevert(e);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can cancel a transfer";
+
+  // effect
+  assert success => pendingDefaultAdmin_() == 0,
+    "Pending default admin is reset";
+  assert success => pendingDefaultAdminSchedule_() == 0,
+    "Pending default admin delay is reset";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: changeDefaultAdminDelay sets a pending default admin delay and its schedule                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule changeDefaultAdminDelay(env e, uint48 newDelay) {
+  require timeSanity(e);
+  require nonpayable(e);
+  require nonzerosender(e);
+  require delayChangeWaitSanity(e, newDelay);
+  requireInvariant defaultAdminConsistency(e.msg.sender);
+
+  uint48 delayBefore = defaultAdminDelay(e);
+
+  changeDefaultAdminDelay@withrevert(e, newDelay);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can begin a delay change";
+
+  // effect
+  assert success => pendingDelay_(e) == newDelay,
+    "pending delay is set";
+
+  assert success => (
+    assert_uint256(pendingDelaySchedule_(e)) > e.block.timestamp ||
+    delayBefore == newDelay || // Interpreted as decreasing, x - x = 0
+    defaultAdminDelayIncreaseWait() == 0
+  ),
+    "pending delay schedule is set in the future unless accepted edge cases";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: A delay can't change in less than the applied schedule                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48 newDelay) {
+  require e1.block.timestamp <= e2.block.timestamp;
+
+  uint48 delayBefore = defaultAdminDelay(e1);
+
+  changeDefaultAdminDelay(e1, newDelay);
+  f(e2, args);
+
+  uint48 delayAfter = defaultAdminDelay(e2);
+
+  mathint delayWait = newDelay > delayBefore ? increasingDelaySchedule(e1, newDelay) : decreasingDelaySchedule(e1, newDelay);
+
+  assert delayAfter != delayBefore => (
+    delayAfter == newDelay &&
+    to_mathint(e2.block.timestamp) >= delayWait
+  ),
+    "A delay can only change after the applied schedule";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: pending delay wait is set depending on increasing or decreasing the delay                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pendingDelayWait(env e, uint48 newDelay) {
+  uint48 oldDelay = defaultAdminDelay(e);
+  changeDefaultAdminDelay(e, newDelay);
+
+  assert newDelay > oldDelay => 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 => to_mathint(pendingDelaySchedule_(e)) == decreasingDelaySchedule(e, newDelay),
+    "Delay wait is the difference between the current and the new delay when the delay is decreased";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: rollbackDefaultAdminDelay resets the delay and its schedule                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule rollbackDefaultAdminDelay(env e) {
+  require nonpayable(e);
+  require nonzerosender(e);
+  requireInvariant defaultAdminConsistency(e.msg.sender);
+
+  rollbackDefaultAdminDelay@withrevert(e);
+  bool success = !lastReverted;
+
+  // liveness
+  assert success <=> e.msg.sender == defaultAdmin(),
+    "only the current default admin can rollback a delay change";
+
+  // effect
+  assert success => pendingDelay_(e) == 0,
+    "Pending default admin is reset";
+  assert success => pendingDelaySchedule_(e) == 0,
+    "Pending default admin delay is reset";
+}

lib_openzeppelin_contracts/certora/specs/AccessManaged.spec

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

lib_openzeppelin_contracts/certora/specs/AccessManager.spec

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

lib_openzeppelin_contracts/certora/specs/DoubleEndedQueue.spec

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

lib_openzeppelin_contracts/certora/specs/ERC20.spec

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

lib_openzeppelin_contracts/certora/specs/ERC20FlashMint.spec

@@ -0,0 +1,55 @@
+import "helpers/helpers.spec";
+import "methods/IERC20.spec";
+import "methods/IERC3156FlashLender.spec";
+import "methods/IERC3156FlashBorrower.spec";
+
+methods {
+    // non standard ERC-3156 functions
+    function flashFeeReceiver() external returns (address) envfree;
+
+    // function summaries below
+    function _._update(address from, address to, uint256 amount) internal => specUpdate(from, to, amount) expect void ALL;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost: track mint and burns in the CVL                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+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;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: When doing a flashLoan, "amount" is minted and burnt, additionally, the fee is either burnt                   │
+│ (if the fee recipient is 0) or transferred (if the fee recipient is not 0)                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule checkMintAndBurn(env e) {
+    address receiver;
+    address token;
+    uint256 amount;
+    bytes data;
+
+    uint256 fees = flashFee(token, amount);
+    address recipient = flashFeeReceiver();
+
+    flashLoan(e, receiver, token, amount, data);
+
+    assert trackedMintAmount[receiver] == to_mathint(amount);
+    assert trackedBurnAmount[receiver] == amount + to_mathint(recipient == 0 ? fees : 0);
+    assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == to_mathint(fees);
+}

lib_openzeppelin_contracts/certora/specs/ERC20Wrapper.spec

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

lib_openzeppelin_contracts/certora/specs/ERC721.spec

@@ -0,0 +1,679 @@
+import "helpers/helpers.spec";
+import "methods/IERC721.spec";
+import "methods/IERC721Receiver.spec";
+
+methods {
+    // exposed for FV
+    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;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+definition authSanity(env e) returns bool = e.msg.sender != 0;
+
+// Could be broken in theory, but not in practice
+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 == sig:transferFrom(address,address,uint256).selector) {
+        transferFrom@withrevert(e, from, to, tokenId);
+    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
+        safeTransferFrom@withrevert(e, from, to, tokenId);
+    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
+        bytes params;
+        require params.length < 0xffff;
+        safeTransferFrom@withrevert(e, from, to, tokenId, params);
+    } else {
+        calldataarg args;
+        f@withrevert(e, args);
+    }
+}
+
+function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
+    if (f.selector == sig:mint(address,uint256).selector) {
+        mint@withrevert(e, to, tokenId);
+    } else if (f.selector == sig:safeMint(address,uint256).selector) {
+        safeMint@withrevert(e, to, tokenId);
+    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
+        bytes params;
+        require params.length < 0xffff;
+        safeMint@withrevert(e, to, tokenId, params);
+    } else {
+        require false;
+    }
+}
+
+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 mathint _ownedTotal {
+    init_state axiom _ownedTotal == 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_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);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost & hooks: sum of all balances                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost mathint _supply {
+    init_state axiom _supply == 0;
+}
+
+ghost mapping(address => mathint) _balances {
+    init_state axiom forall address a. _balances[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 _balances[user] == to_mathint(value);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: number of owned tokens is the sum of all balances                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant ownedTotalIsSumOfBalances()
+    _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);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: balanceOf is the number of tokens owned                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant balanceOfConsistency(address user)
+    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
+    to_mathint(balanceOf(user)) == _balances[user]
+    {
+        preserved {
+            require balanceLimited(user);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: owner of a token must have some balance                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant ownerHasBalance(uint256 tokenId)
+    balanceOf(ownerOf(tokenId)) > 0
+    {
+        preserved {
+            requireInvariant balanceOfConsistency(ownerOf(tokenId));
+            require balanceLimited(ownerOf(tokenId));
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: balance of address(0) is 0                                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule zeroAddressBalanceRevert() {
+    balanceOf@withrevert(0);
+    assert lastReverted;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: address(0) has no authorized operator                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant zeroAddressHasNoApprovedOperator(address a)
+    !isApprovedForAll(0, a)
+    {
+        preserved with (env e) {
+            require nonzerosender(e);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: tokens that do not exist are not owned and not approved                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant notMintedUnset(uint256 tokenId)
+    unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert + ownerOf and getApproved revert if token does not exist     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+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;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: total supply can only change through mint and burn                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule supplyChange(env e) {
+    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 == 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 == sig:burn(uint256).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1.           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule balanceChange(env e, address account) {
+    requireInvariant balanceOfConsistency(account);
+    require balanceLimited(account);
+
+    mathint balanceBefore = balanceOf(account);
+    method f; helperSoundFnCall(e, f);
+    mathint balanceAfter  = balanceOf(account);
+
+    // balance can change by at most 1
+    assert balanceBefore != balanceAfter => (
+        balanceAfter == balanceBefore - 1 ||
+        balanceAfter == balanceBefore + 1
+    );
+
+    // only selected function can change balances
+    assert balanceBefore != balanceAfter => (
+        f.selector == 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
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: ownership can only change through mint, burn or transfers.                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule ownershipChange(env e, uint256 tokenId) {
+    require nonzerosender(e);
+    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
+
+    address ownerBefore = unsafeOwnerOf(tokenId);
+    method f; helperSoundFnCall(e, f);
+    address ownerAfter  = unsafeOwnerOf(tokenId);
+
+    assert ownerBefore == 0 && ownerAfter != 0 => (
+        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 == sig:burn(uint256).selector
+    );
+
+    assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
+        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
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approvalChange(env e, uint256 tokenId) {
+    address approvalBefore = unsafeGetApproved(tokenId);
+    method f; helperSoundFnCall(e, f);
+    address approvalAfter  = unsafeGetApproved(tokenId);
+
+    // approve can set any value, other functions reset
+    assert approvalBefore != approvalAfter => (
+        f.selector == sig:approve(address,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
+        )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: approval for all tokens can only change through isApprovedForAll.                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approvedForAllChange(env e, address owner, address spender) {
+    bool approvedForAllBefore = isApprovedForAll(owner, spender);
+    method f; helperSoundFnCall(e, f);
+    bool approvedForAllAfter  = isApprovedForAll(owner, spender);
+
+    assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transferFrom behavior and side effects                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferFrom(env e, address from, address to, uint256 tokenId) {
+    require nonpayable(e);
+    require authSanity(e);
+
+    address operator = e.msg.sender;
+    uint256 otherTokenId;
+    address otherAccount;
+
+    requireInvariant ownerHasBalance(tokenId);
+    require balanceLimited(to);
+
+    uint256 balanceOfFromBefore  = balanceOf(from);
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+    address approvalBefore       = unsafeGetApproved(tokenId);
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    transferFrom@withrevert(e, from, to, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        from == ownerBefore &&
+        from != 0 &&
+        to   != 0 &&
+        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
+    );
+
+    // effect
+    assert success => (
+        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
+    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
+    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: safeTransferFrom behavior and side effects                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
+    f.selector == 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;
+    address otherAccount;
+
+    requireInvariant ownerHasBalance(tokenId);
+    require balanceLimited(to);
+
+    uint256 balanceOfFromBefore  = balanceOf(from);
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+    address approvalBefore       = unsafeGetApproved(tokenId);
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    helperTransferWithRevert(e, f, from, to, tokenId);
+    bool success = !lastReverted;
+
+    assert success <=> (
+        from == ownerBefore &&
+        from != 0 &&
+        to   != 0 &&
+        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
+    );
+
+    // effect
+    assert success => (
+        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
+    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
+    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: mint behavior and side effects                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mint(env e, address to, uint256 tokenId) {
+    require nonpayable(e);
+    requireInvariant notMintedUnset(tokenId);
+
+    uint256 otherTokenId;
+    address otherAccount;
+
+    require balanceLimited(to);
+
+    mathint supplyBefore         = _supply;
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+
+    mint@withrevert(e, to, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        ownerBefore == 0 &&
+        to != 0
+    );
+
+    // effect
+    assert success => (
+        _supply                   == supplyBefore + 1 &&
+        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId)    == to
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
+    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: safeMint behavior and side effects                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
+    f.selector == sig:safeMint(address,uint256).selector ||
+    f.selector == sig:safeMint(address,uint256,bytes).selector
+} {
+    require nonpayable(e);
+    requireInvariant notMintedUnset(tokenId);
+
+    uint256 otherTokenId;
+    address otherAccount;
+
+    require balanceLimited(to);
+
+    mathint supplyBefore         = _supply;
+    uint256 balanceOfToBefore    = balanceOf(to);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+
+    helperMintWithRevert(e, f, to, tokenId);
+    bool success = !lastReverted;
+
+    assert success <=> (
+        ownerBefore == 0 &&
+        to != 0
+    );
+
+    // effect
+    assert success => (
+        _supply                   == supplyBefore + 1 &&
+        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId)    == to
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
+    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: burn behavior and side effects                                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule burn(env e, uint256 tokenId) {
+    require nonpayable(e);
+
+    address from = unsafeOwnerOf(tokenId);
+    uint256 otherTokenId;
+    address otherAccount;
+
+    requireInvariant ownerHasBalance(tokenId);
+
+    mathint supplyBefore         = _supply;
+    uint256 balanceOfFromBefore  = balanceOf(from);
+    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    burn@withrevert(e, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        ownerBefore != 0
+    );
+
+    // effect
+    assert success => (
+        _supply                     == supplyBefore - 1 &&
+        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
+        unsafeOwnerOf(tokenId)      == 0 &&
+        unsafeGetApproved(tokenId)  == 0
+    );
+
+    // no side effect
+    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
+    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: approve behavior and side effects                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approve(env e, address spender, uint256 tokenId) {
+    require nonpayable(e);
+    require authSanity(e);
+
+    address caller = e.msg.sender;
+    address owner = unsafeOwnerOf(tokenId);
+    uint256 otherTokenId;
+
+    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
+
+    approve@withrevert(e, spender, tokenId);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        owner != 0 &&
+        (owner == caller || isApprovedForAll(owner, caller))
+    );
+
+    // effect
+    assert success => unsafeGetApproved(tokenId) == spender;
+
+    // no side effect
+    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: setApprovalForAll behavior and side effects                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule setApprovalForAll(env e, address operator, bool approved) {
+    require nonpayable(e);
+
+    address owner = e.msg.sender;
+    address otherOwner;
+    address otherOperator;
+
+    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);
+
+    setApprovalForAll@withrevert(e, operator, approved);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> operator != 0;
+
+    // effect
+    assert success => isApprovedForAll(owner, operator) == approved;
+
+    // no side effect
+    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
+        otherOwner    == owner &&
+        otherOperator == operator
+    );
+}

lib_openzeppelin_contracts/certora/specs/EnumerableMap.spec

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

lib_openzeppelin_contracts/certora/specs/EnumerableSet.spec

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

lib_openzeppelin_contracts/certora/specs/Initializable.spec

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

lib_openzeppelin_contracts/certora/specs/Nonces.spec

@@ -0,0 +1,92 @@
+import "helpers/helpers.spec";
+
+methods {
+    function nonces(address) external returns (uint256) envfree;
+    function useNonce(address) external returns (uint256) envfree;
+    function useCheckedNonce(address,uint256) external envfree;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helpers                                                                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function nonceSanity(address account) returns bool {
+    return nonces(account) < max_uint256;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: useNonce uses nonce                                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule useNonce(address account) {
+    require nonceSanity(account);
+
+    address other;
+
+    mathint nonceBefore = nonces(account);
+    mathint otherNonceBefore = nonces(other);
+
+    mathint nonceUsed = useNonce@withrevert(account);
+    bool success = !lastReverted;
+
+    mathint nonceAfter = nonces(account);
+    mathint otherNonceAfter = nonces(other);
+
+    // liveness
+    assert success, "doesn't revert";
+
+    // effect
+    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";
+
+    // no side effect
+    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: useCheckedNonce uses only the current nonce                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule useCheckedNonce(address account, uint256 currentNonce) {
+    require nonceSanity(account);
+
+    address other;
+
+    mathint nonceBefore = nonces(account);
+    mathint otherNonceBefore = nonces(other);
+
+    useCheckedNonce@withrevert(account, currentNonce);
+    bool success = !lastReverted;
+
+    mathint nonceAfter = nonces(account);
+    mathint otherNonceAfter = nonces(other);
+
+    // liveness
+    assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";
+
+    // effect
+    assert success => nonceAfter == nonceBefore + 1, "nonce is used";
+
+    // no side effect
+    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: nonce only increments                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule nonceOnlyIncrements(address account) {
+    require nonceSanity(account);
+
+    mathint nonceBefore = nonces(account);
+
+    env e; method f; calldataarg args;
+    f(e, args);
+
+    mathint nonceAfter = nonces(account);
+
+    assert nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1, "nonce only increments";
+}

lib_openzeppelin_contracts/certora/specs/Ownable.spec

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

lib_openzeppelin_contracts/certora/specs/Ownable2Step.spec

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

lib_openzeppelin_contracts/certora/specs/Pausable.spec

@@ -0,0 +1,96 @@
+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()";
+}

lib_openzeppelin_contracts/certora/specs/TimelockController.spec

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

lib_openzeppelin_contracts/certora/specs/helpers/helpers.spec

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

lib_openzeppelin_contracts/certora/specs/methods/IAccessControl.spec

@@ -0,0 +1,8 @@
+methods {
+    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;
+}

lib_openzeppelin_contracts/certora/specs/methods/IAccessControlDefaultAdminRules.spec

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

lib_openzeppelin_contracts/certora/specs/methods/IAccessManaged.spec

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

lib_openzeppelin_contracts/certora/specs/methods/IAccessManager.spec

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

lib_openzeppelin_contracts/certora/specs/methods/IERC20.spec

@@ -0,0 +1,11 @@
+methods {
+    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);
+}

lib_openzeppelin_contracts/certora/specs/methods/IERC2612.spec

@@ -0,0 +1,5 @@
+methods {
+    function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external;
+    function nonces(address)    external returns (uint256) envfree;
+    function DOMAIN_SEPARATOR() external returns (bytes32) envfree;
+}

lib_openzeppelin_contracts/certora/specs/methods/IERC3156FlashBorrower.spec

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

lib_openzeppelin_contracts/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);
+}

lib_openzeppelin_contracts/certora/specs/methods/IERC5313.spec

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

lib_openzeppelin_contracts/certora/specs/methods/IERC721.spec

@@ -0,0 +1,17 @@
+methods {
+    // IERC721
+    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
+    function name()                                          external returns (string);
+    function symbol()                                        external returns (string);
+    function tokenURI(uint256)                               external returns (string);
+}

lib_openzeppelin_contracts/certora/specs/methods/IERC721Receiver.spec

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

lib_openzeppelin_contracts/certora/specs/methods/IOwnable.spec

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

lib_openzeppelin_contracts/certora/specs/methods/IOwnable2Step.spec

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