Merge remote-tracking branch 'upstream' into fv/Governor

certora/harnesses/AccessControlDefaultAdminRulesHarness.sol

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

certora/run.js

@@ -78,7 +78,7 @@ async function runCertora(spec, contract, files, options = []) {
   child.stdout.pipe(stream, { end: false });
   child.stderr.pipe(stream, { end: false });
 
-  // as soon as we have a jobStatus link, print it
+  // as soon as we have a job id, print the output link
   stream.on('data', function logStatusUrl(data) {
     const { '-DjobId': jobId, '-DuserId': userId } = Object.fromEntries(
       data

certora/specs.js

@@ -7,6 +7,11 @@ module.exports = [].concat(
     contract: 'AccessControlHarness',
     files: ['certora/harnesses/AccessControlHarness.sol'],
   },
+  {
+    spec: 'AccessControlDefaultAdminRules',
+    contract: 'AccessControlDefaultAdminRulesHarness',
+    files: ['certora/harnesses/AccessControlDefaultAdminRulesHarness.sol'],
+  },
   {
     spec: 'Ownable',
     contract: 'OwnableHarness',

certora/specs/AccessControl.spec

@@ -1,13 +1,20 @@
 import "helpers/helpers.spec"
 import "methods/IAccessControl.spec"
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition DEFAULT_ADMIN_ROLE() returns bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000;
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule onlyGrantCanGrant(env e, bytes32 role, address account) {
-    method f; calldataarg args;
+rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) {
+    calldataarg args;
 
     bool hasRoleBefore = hasRole(role, account);
     f(e, args);
@@ -34,10 +41,9 @@ rule onlyGrantCanGrant(env e, bytes32 role, address account) {
 │ Function correctness: grantRole only affects the specified user/role combo                                          │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule grantRoleEffect(env e) {
+rule grantRoleEffect(env e, bytes32 role) {
     require nonpayable(e);
 
-    bytes32 role;
     bytes32 otherRole;
     address account;
     address otherAccount;
@@ -65,10 +71,9 @@ rule grantRoleEffect(env e) {
 │ Function correctness: revokeRole only affects the specified user/role combo                                         │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule revokeRoleEffect(env e) {
+rule revokeRoleEffect(env e, bytes32 role) {
     require nonpayable(e);
 
-    bytes32 role;
     bytes32 otherRole;
     address account;
     address otherAccount;
@@ -96,10 +101,9 @@ rule revokeRoleEffect(env e) {
 │ Function correctness: renounceRole only affects the specified user/role combo                                       │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule renounceRoleEffect(env e) {
+rule renounceRoleEffect(env e, bytes32 role) {
     require nonpayable(e);
 
-    bytes32 role;
     bytes32 otherRole;
     address account;
     address otherAccount;

certora/specs/AccessControlDefaultAdminRules.spec

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

certora/specs/methods/IAccessControlDefaultAdminRules.spec

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

certora/specs/methods/IERC5313.spec

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

contracts/access/AccessControlDefaultAdminRules.sol

@@ -53,6 +53,7 @@ abstract contract AccessControlDefaultAdminRules is IAccessControlDefaultAdminRu
      * @dev Sets the initial values for {defaultAdminDelay} and {defaultAdmin} address.
      */
     constructor(uint48 initialDelay, address initialDefaultAdmin) {
+        require(initialDefaultAdmin != address(0), "AccessControl: 0 default admin");
         _currentDelay = initialDelay;
         _grantRole(DEFAULT_ADMIN_ROLE, initialDefaultAdmin);
     }

contracts/token/ERC20/extensions/ERC20Votes.sol

@@ -114,7 +114,7 @@ abstract contract ERC20Votes is ERC20Permit, IERC5805 {
      * @dev Lookup a value in a list of (sorted) checkpoints.
      */
     function _checkpointsLookup(Checkpoint[] storage ckpts, uint256 timepoint) private view returns (uint256) {
-        // We run a binary search to look for the earliest checkpoint taken after `timepoint`.
+        // We run a binary search to look for the last (most recent) checkpoint taken before (or at) `timepoint`.
         //
         // Initially we check if the block is recent to narrow the search range.
         // During the loop, the index of the wanted checkpoint remains in the range [low-1, high).

contracts/utils/Checkpoints.sol

@@ -151,7 +151,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Return the index of the oldest checkpoint whose key is greater than the search key, or `high` if there is none.
+     * @dev Return the index of the last (most recent) checkpoint with key lower or equal than the search key, or `high` if there is none.
      * `low` and `high` define a section where to do the search, with inclusive `low` and exclusive `high`.
      *
      * WARNING: `high` should not be greater than the array's length.
@@ -174,7 +174,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Return the index of the oldest checkpoint whose key is greater or equal than the search key, or `high` if there is none.
+     * @dev Return the index of the first (oldest) checkpoint with key is greater or equal than the search key, or `high` if there is none.
      * `low` and `high` define a section where to do the search, with inclusive `low` and exclusive `high`.
      *
      * WARNING: `high` should not be greater than the array's length.
@@ -225,7 +225,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Returns the value in the oldest checkpoint with key greater or equal than the search key, or zero if there is none.
+     * @dev Returns the value in the first (oldest) checkpoint with key greater or equal than the search key, or zero if there is none.
      */
     function lowerLookup(Trace224 storage self, uint32 key) internal view returns (uint224) {
         uint256 len = self._checkpoints.length;
@@ -234,7 +234,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Returns the value in the most recent checkpoint with key lower or equal than the search key.
+     * @dev Returns the value in the last (most recent) checkpoint with key lower or equal than the search key.
      */
     function upperLookup(Trace224 storage self, uint32 key) internal view returns (uint224) {
         uint256 len = self._checkpoints.length;
@@ -243,7 +243,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Returns the value in the most recent checkpoint with key lower or equal than the search key.
+     * @dev Returns the value in the last (most recent) checkpoint with key lower or equal than the search key.
      *
      * NOTE: This is a variant of {upperLookup} that is optimised to find "recent" checkpoint (checkpoints with high keys).
      */
@@ -324,7 +324,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Return the index of the oldest checkpoint whose key is greater than the search key, or `high` if there is none.
+     * @dev Return the index of the last (most recent) checkpoint with key lower or equal than the search key, or `high` if there is none.
      * `low` and `high` define a section where to do the search, with inclusive `low` and exclusive `high`.
      *
      * WARNING: `high` should not be greater than the array's length.
@@ -347,7 +347,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Return the index of the oldest checkpoint whose key is greater or equal than the search key, or `high` if there is none.
+     * @dev Return the index of the first (oldest) checkpoint with key is greater or equal than the search key, or `high` if there is none.
      * `low` and `high` define a section where to do the search, with inclusive `low` and exclusive `high`.
      *
      * WARNING: `high` should not be greater than the array's length.
@@ -401,7 +401,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Returns the value in the oldest checkpoint with key greater or equal than the search key, or zero if there is none.
+     * @dev Returns the value in the first (oldest) checkpoint with key greater or equal than the search key, or zero if there is none.
      */
     function lowerLookup(Trace160 storage self, uint96 key) internal view returns (uint160) {
         uint256 len = self._checkpoints.length;
@@ -410,7 +410,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Returns the value in the most recent checkpoint with key lower or equal than the search key.
+     * @dev Returns the value in the last (most recent) checkpoint with key lower or equal than the search key.
      */
     function upperLookup(Trace160 storage self, uint96 key) internal view returns (uint160) {
         uint256 len = self._checkpoints.length;
@@ -419,7 +419,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Returns the value in the most recent checkpoint with key lower or equal than the search key.
+     * @dev Returns the value in the last (most recent) checkpoint with key lower or equal than the search key.
      *
      * NOTE: This is a variant of {upperLookup} that is optimised to find "recent" checkpoint (checkpoints with high keys).
      */
@@ -500,7 +500,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Return the index of the oldest checkpoint whose key is greater than the search key, or `high` if there is none.
+     * @dev Return the index of the last (most recent) checkpoint with key lower or equal than the search key, or `high` if there is none.
      * `low` and `high` define a section where to do the search, with inclusive `low` and exclusive `high`.
      *
      * WARNING: `high` should not be greater than the array's length.
@@ -523,7 +523,7 @@ library Checkpoints {
     }
 
     /**
-     * @dev Return the index of the oldest checkpoint whose key is greater or equal than the search key, or `high` if there is none.
+     * @dev Return the index of the first (oldest) checkpoint with key is greater or equal than the search key, or `high` if there is none.
      * `low` and `high` define a section where to do the search, with inclusive `low` and exclusive `high`.
      *
      * WARNING: `high` should not be greater than the array's length.

contracts/utils/cryptography/EIP712.sol

@@ -111,6 +111,8 @@ abstract contract EIP712 is IERC5267 {
 
     /**
      * @dev See {EIP-5267}.
+     *
+     * _Available since v4.9._
      */
     function eip712Domain()
         public

package.json

@@ -32,7 +32,7 @@
     "test:inheritance": "scripts/checks/inheritance-ordering.js artifacts/build-info/*",
     "test:generation": "scripts/checks/generation.sh",
     "gas-report": "env ENABLE_GAS_REPORT=true npm run test",
-    "slither": "npm run clean && slither . --detect reentrancy-eth,reentrancy-no-eth,reentrancy-unlimited-gas"
+    "slither": "npm run clean && slither ."
   },
   "repository": {
     "type": "git",

scripts/generate/templates/Checkpoints.js

@@ -46,7 +46,7 @@ function push(
 }
 
 /**
- * @dev Returns the value in the oldest checkpoint with key greater or equal than the search key, or zero if there is none.
+ * @dev Returns the value in the first (oldest) checkpoint with key greater or equal than the search key, or zero if there is none.
  */
 function lowerLookup(${opts.historyTypeName} storage self, ${opts.keyTypeName} key) internal view returns (${opts.valueTypeName}) {
     uint256 len = self.${opts.checkpointFieldName}.length;
@@ -55,7 +55,7 @@ function lowerLookup(${opts.historyTypeName} storage self, ${opts.keyTypeName} k
 }
 
 /**
- * @dev Returns the value in the most recent checkpoint with key lower or equal than the search key.
+ * @dev Returns the value in the last (most recent) checkpoint with key lower or equal than the search key.
  */
 function upperLookup(${opts.historyTypeName} storage self, ${opts.keyTypeName} key) internal view returns (${opts.valueTypeName}) {
     uint256 len = self.${opts.checkpointFieldName}.length;
@@ -64,7 +64,7 @@ function upperLookup(${opts.historyTypeName} storage self, ${opts.keyTypeName} k
 }
 
 /**
- * @dev Returns the value in the most recent checkpoint with key lower or equal than the search key.
+ * @dev Returns the value in the last (most recent) checkpoint with key lower or equal than the search key.
  *
  * NOTE: This is a variant of {upperLookup} that is optimised to find "recent" checkpoint (checkpoints with high keys).
  */
@@ -227,7 +227,7 @@ function _insert(
 }
 
 /**
- * @dev Return the index of the oldest checkpoint whose key is greater than the search key, or \`high\` if there is none.
+ * @dev Return the index of the last (most recent) checkpoint with key lower or equal than the search key, or \`high\` if there is none.
  * \`low\` and \`high\` define a section where to do the search, with inclusive \`low\` and exclusive \`high\`.
  *
  * WARNING: \`high\` should not be greater than the array's length.
@@ -250,7 +250,7 @@ function _upperBinaryLookup(
 }
 
 /**
- * @dev Return the index of the oldest checkpoint whose key is greater or equal than the search key, or \`high\` if there is none.
+ * @dev Return the index of the first (oldest) checkpoint with key is greater or equal than the search key, or \`high\` if there is none.
  * \`low\` and \`high\` define a section where to do the search, with inclusive \`low\` and exclusive \`high\`.
  *
  * WARNING: \`high\` should not be greater than the array's length.

slither.config.json

@@ -1,5 +1,5 @@
 {
-    "detectors_to_run": "reentrancy-eth,reentrancy-no-eth,reentrancy-unlimited-gas",
-    "filter_paths": "contracts/mocks",
+    "detectors_to_run": "arbitrary-send-erc20,array-by-reference,incorrect-shift,name-reused,rtlo,suicidal,uninitialized-state,uninitialized-storage,arbitrary-send-erc20-permit,controlled-array-length,controlled-delegatecall,delegatecall-loop,msg-value-loop,reentrancy-eth,unchecked-transfer,weak-prng,domain-separator-collision,erc20-interface,erc721-interface,locked-ether,mapping-deletion,shadowing-abstract,tautology,write-after-write,boolean-cst,reentrancy-no-eth,reused-constructor,tx-origin,unchecked-lowlevel,unchecked-send,variable-scope,void-cst,events-access,events-maths,incorrect-unary,boolean-equal,cyclomatic-complexity,deprecated-standards,erc20-indexed,function-init-state,pragma,unused-state,reentrancy-unlimited-gas,constable-states,immutable-states,var-read-using-this",
+    "filter_paths": "contracts/mocks,contracts-exposed",
     "compile_force_framework": "hardhat"
-}
+}

test/access/AccessControlDefaultAdminRules.test.js

@@ -1,4 +1,4 @@
-const { time } = require('@openzeppelin/test-helpers');
+const { time, constants, expectRevert } = require('@openzeppelin/test-helpers');
 const {
   shouldBehaveLikeAccessControl,
   shouldBehaveLikeAccessControlDefaultAdminRules,
@@ -13,6 +13,13 @@ contract('AccessControlDefaultAdminRules', function (accounts) {
     this.accessControl = await AccessControlDefaultAdminRules.new(delay, accounts[0], { from: accounts[0] });
   });
 
+  it('initial admin not zero', async function () {
+    await expectRevert(
+      AccessControlDefaultAdminRules.new(delay, constants.ZERO_ADDRESS),
+      'AccessControl: 0 default admin',
+    );
+  });
+
   shouldBehaveLikeAccessControl('AccessControl', ...accounts);
   shouldBehaveLikeAccessControlDefaultAdminRules('AccessControl', delay, ...accounts);
 });

test/utils/cryptography/EIP712.test.js

@@ -6,65 +6,98 @@ const { getChainId } = require('../../helpers/chainid');
 const { mapValues } = require('../../helpers/map-values');
 
 const EIP712Verifier = artifacts.require('$EIP712Verifier');
+const Clones = artifacts.require('$Clones');
 
 contract('EIP712', function (accounts) {
   const [mailTo] = accounts;
 
-  const name = 'A Name';
-  const version = '1';
+  const shortName = 'A Name';
+  const shortVersion = '1';
 
-  beforeEach('deploying', async function () {
-    this.eip712 = await EIP712Verifier.new(name, version);
+  const longName = 'A'.repeat(40);
+  const longVersion = 'B'.repeat(40);
 
-    this.domain = {
-      name,
-      version,
-      chainId: await getChainId(),
-      verifyingContract: this.eip712.address,
-    };
-    this.domainType = domainType(this.domain);
-  });
+  const cases = [
+    ['short', shortName, shortVersion],
+    ['long', longName, longVersion],
+  ];
 
-  describe('domain separator', function () {
-    it('is internally available', async function () {
-      const expected = await domainSeparator(this.domain);
+  for (const [shortOrLong, name, version] of cases) {
+    describe(`with ${shortOrLong} name and version`, function () {
+      beforeEach('deploying', async function () {
+        this.eip712 = await EIP712Verifier.new(name, version);
 
-      expect(await this.eip712.$_domainSeparatorV4()).to.equal(expected);
-    });
+        this.domain = {
+          name,
+          version,
+          chainId: await getChainId(),
+          verifyingContract: this.eip712.address,
+        };
+        this.domainType = domainType(this.domain);
+      });
+
+      describe('domain separator', function () {
+        it('is internally available', async function () {
+          const expected = await domainSeparator(this.domain);
+
+          expect(await this.eip712.$_domainSeparatorV4()).to.equal(expected);
+        });
+
+        it("can be rebuilt using EIP-5267's eip712Domain", async function () {
+          const rebuildDomain = await getDomain(this.eip712);
+          expect(mapValues(rebuildDomain, String)).to.be.deep.equal(mapValues(this.domain, String));
+        });
+
+        if (shortOrLong === 'short') {
+          // Long strings are in storage, and the proxy will not be properly initialized unless
+          // the upgradeable contract variant is used and the initializer is invoked.
+
+          it('adjusts when behind proxy', async function () {
+            const factory = await Clones.new();
+            const cloneReceipt = await factory.$clone(this.eip712.address);
+            const cloneAddress = cloneReceipt.logs.find(({ event }) => event === 'return$clone').args.instance;
+            const clone = new EIP712Verifier(cloneAddress);
+
+            const cloneDomain = { ...this.domain, verifyingContract: clone.address };
+
+            const expectedSeparator = await domainSeparator(cloneDomain);
+            expect(await clone.$_domainSeparatorV4()).to.equal(expectedSeparator);
+
+            const reportedDomain = await getDomain(clone);
+            expect(mapValues(reportedDomain, String)).to.be.deep.equal(mapValues(cloneDomain, String));
+          });
+        }
+      });
+
+      it('hash digest', async function () {
+        const structhash = web3.utils.randomHex(32);
+        expect(await this.eip712.$_hashTypedDataV4(structhash)).to.be.equal(hashTypedData(this.domain, structhash));
+      });
+
+      it('digest', async function () {
+        const message = {
+          to: mailTo,
+          contents: 'very interesting',
+        };
+
+        const data = {
+          types: {
+            EIP712Domain: this.domainType,
+            Mail: [
+              { name: 'to', type: 'address' },
+              { name: 'contents', type: 'string' },
+            ],
+          },
+          domain: this.domain,
+          primaryType: 'Mail',
+          message,
+        };
+
+        const wallet = Wallet.generate();
+        const signature = ethSigUtil.signTypedMessage(wallet.getPrivateKey(), { data });
 
-    it("can be rebuilt using EIP-5267's eip712Domain", async function () {
-      const rebuildDomain = await getDomain(this.eip712);
-      expect(mapValues(rebuildDomain, String)).to.be.deep.equal(mapValues(this.domain, String));
+        await this.eip712.verify(signature, wallet.getAddressString(), message.to, message.contents);
+      });
     });
-  });
-
-  it('hash digest', async function () {
-    const structhash = web3.utils.randomHex(32);
-    expect(await this.eip712.$_hashTypedDataV4(structhash)).to.be.equal(hashTypedData(this.domain, structhash));
-  });
-
-  it('digest', async function () {
-    const message = {
-      to: mailTo,
-      contents: 'very interesting',
-    };
-
-    const data = {
-      types: {
-        EIP712Domain: this.domainType,
-        Mail: [
-          { name: 'to', type: 'address' },
-          { name: 'contents', type: 'string' },
-        ],
-      },
-      domain: this.domain,
-      primaryType: 'Mail',
-      message,
-    };
-
-    const wallet = Wallet.generate();
-    const signature = ethSigUtil.signTypedMessage(wallet.getPrivateKey(), { data });
-
-    await this.eip712.verify(signature, wallet.getAddressString(), message.to, message.contents);
-  });
+  }
 });