From a0f7548bfc566d647d85087c2377980c12ac5b91 Mon Sep 17 00:00:00 2001 From: ernestognw Date: Thu, 10 Aug 2023 23:12:26 -0600 Subject: [PATCH] Finis AccessControlDefaultAdminRules --- ...s_AccessControlDefaultAdminRules.sol.patch | 11 +++ ..._IAccessControlDefaultAdminRules.sol.patch | 11 +++ certora/diff/interfaces_IERC5313.sol.patch | 11 +++ certora/diff/utils_math_Math.sol.patch | 11 +++ certora/diff/utils_math_SafeCast.sol.patch | 11 +++ .../AccessControlDefaultAdminRulesHarness.sol | 4 +- .../specs/AccessControlDefaultAdminRules.spec | 68 ++++++++++--------- 7 files changed, 92 insertions(+), 35 deletions(-) create mode 100644 certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch create mode 100644 certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch create mode 100644 certora/diff/interfaces_IERC5313.sol.patch create mode 100644 certora/diff/utils_math_Math.sol.patch create mode 100644 certora/diff/utils_math_SafeCast.sol.patch diff --git a/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch b/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch new file mode 100644 index 000000000..cc4888a89 --- /dev/null +++ b/certora/diff/access_extensions_AccessControlDefaultAdminRules.sol.patch @@ -0,0 +1,11 @@ +--- access/extensions/AccessControlDefaultAdminRules.sol 2023-08-09 11:45:05 ++++ access/extensions/AccessControlDefaultAdminRules.sol 2023-08-10 22:18:05 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControlDefaultAdminRules.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + import {IAccessControlDefaultAdminRules} from "./IAccessControlDefaultAdminRules.sol"; + import {AccessControl, IAccessControl} from "../AccessControl.sol"; diff --git a/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch b/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch new file mode 100644 index 000000000..f1635197c --- /dev/null +++ b/certora/diff/access_extensions_IAccessControlDefaultAdminRules.sol.patch @@ -0,0 +1,11 @@ +--- access/extensions/IAccessControlDefaultAdminRules.sol 2023-08-09 11:45:05 ++++ access/extensions/IAccessControlDefaultAdminRules.sol 2023-08-10 22:18:08 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts (last updated v4.9.0) (access/IAccessControlDefaultAdminRules.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + import {IAccessControl} from "../IAccessControl.sol"; + diff --git a/certora/diff/interfaces_IERC5313.sol.patch b/certora/diff/interfaces_IERC5313.sol.patch new file mode 100644 index 000000000..d43874bf4 --- /dev/null +++ b/certora/diff/interfaces_IERC5313.sol.patch @@ -0,0 +1,11 @@ +--- interfaces/IERC5313.sol 2023-08-09 11:45:05 ++++ interfaces/IERC5313.sol 2023-08-10 22:18:26 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts (last updated v4.9.0) (interfaces/IERC5313.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + /** + * @dev Interface for the Light Contract Ownership Standard. diff --git a/certora/diff/utils_math_Math.sol.patch b/certora/diff/utils_math_Math.sol.patch new file mode 100644 index 000000000..5cd5cb6a0 --- /dev/null +++ b/certora/diff/utils_math_Math.sol.patch @@ -0,0 +1,11 @@ +--- utils/math/Math.sol 2023-08-09 11:45:05 ++++ utils/math/Math.sol 2023-08-10 22:18:22 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts (last updated v4.9.0) (utils/math/Math.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + /** + * @dev Standard math utilities missing in the Solidity language. diff --git a/certora/diff/utils_math_SafeCast.sol.patch b/certora/diff/utils_math_SafeCast.sol.patch new file mode 100644 index 000000000..ff15ee72e --- /dev/null +++ b/certora/diff/utils_math_SafeCast.sol.patch @@ -0,0 +1,11 @@ +--- utils/math/SafeCast.sol 2023-08-09 11:45:05 ++++ utils/math/SafeCast.sol 2023-08-10 22:18:17 +@@ -2,7 +2,7 @@ + // OpenZeppelin Contracts (last updated v4.8.0) (utils/math/SafeCast.sol) + // This file was procedurally generated from scripts/generate/templates/SafeCast.js. + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + /** + * @dev Wrappers over Solidity's uintXX/intXX casting operators with added overflow diff --git a/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol b/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol index 145f65b76..913ce48d9 100644 --- a/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol +++ b/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol @@ -1,8 +1,8 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.20; +pragma solidity ^0.8.19; -import "../patched/access/AccessControlDefaultAdminRules.sol"; +import {AccessControlDefaultAdminRules} from "../patched/access/extensions/AccessControlDefaultAdminRules.sol"; contract AccessControlDefaultAdminRulesHarness is AccessControlDefaultAdminRules { uint48 private _delayIncreaseWait; diff --git a/certora/specs/AccessControlDefaultAdminRules.spec b/certora/specs/AccessControlDefaultAdminRules.spec index 58b9d1202..ab9074fcf 100644 --- a/certora/specs/AccessControlDefaultAdminRules.spec +++ b/certora/specs/AccessControlDefaultAdminRules.spec @@ -1,28 +1,30 @@ -import "helpers/helpers.spec" -import "methods/IAccessControlDefaultAdminRules.spec" -import "methods/IAccessControl.spec" -import "AccessControl.spec" +import "helpers/helpers.spec"; +import "methods/IAccessControlDefaultAdminRules.spec"; +import "methods/IAccessControl.spec"; +import "AccessControl.spec"; use rule onlyGrantCanGrant filtered { - f -> f.selector != acceptDefaultAdminTransfer().selector + f -> f.selector != sig:acceptDefaultAdminTransfer().selector } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Helpers │ +│ Definitions │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +definition defaultAdminRole() returns bytes32 = to_bytes32(0); + definition timeSanity(env e) returns bool = - e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48(); + e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48; definition delayChangeWaitSanity(env e, uint48 newDelay) returns bool = - e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48(); + e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48; definition isSet(uint48 schedule) returns bool = schedule != 0; definition hasPassed(env e, uint48 schedule) returns bool = - schedule < e.block.timestamp; + assert_uint256(schedule) < e.block.timestamp; definition increasingDelaySchedule(env e, uint48 newDelay) returns mathint = e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait()); @@ -36,7 +38,7 @@ definition decreasingDelaySchedule(env e, uint48 newDelay) returns mathint = └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant defaultAdminConsistency(address account) - (account == defaultAdmin() && account != 0) <=> hasRole(DEFAULT_ADMIN_ROLE(), account) + (account == defaultAdmin() && account != 0) <=> hasRole(defaultAdminRole(), account) { preserved with (env e) { require nonzerosender(e); @@ -49,7 +51,7 @@ invariant defaultAdminConsistency(address account) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant singleDefaultAdmin(address account, address another) - hasRole(DEFAULT_ADMIN_ROLE(), account) && hasRole(DEFAULT_ADMIN_ROLE(), another) => another == account + hasRole(defaultAdminRole(), account) && hasRole(defaultAdminRole(), another) => another == account { preserved { requireInvariant defaultAdminConsistency(account); @@ -63,7 +65,7 @@ invariant singleDefaultAdmin(address account, address another) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant defaultAdminRoleAdminConsistency() - getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE() + getRoleAdmin(defaultAdminRole()) == defaultAdminRole(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -71,7 +73,7 @@ invariant defaultAdminRoleAdminConsistency() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant ownerConsistency() - defaultAdmin() == owner() + defaultAdmin() == owner(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -94,7 +96,7 @@ rule revokeRoleEffect(env e, bytes32 role) { bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); // liveness - assert success <=> isCallerAdmin && role != DEFAULT_ADMIN_ROLE(), + assert success <=> isCallerAdmin && role != defaultAdminRole(), "roles can only be revoked by their owner except for the default admin role"; // effect @@ -135,8 +137,8 @@ rule renounceRoleEffect(env e, bytes32 role) { assert success <=> ( account == e.msg.sender && ( - role != DEFAULT_ADMIN_ROLE() || - account != adminBefore || + role != defaultAdminRole() || + account != adminBefore || ( pendingAdminBefore == 0 && isSet(scheduleBefore) && @@ -152,7 +154,7 @@ rule renounceRoleEffect(env e, bytes32 role) { assert success => ( ( - role == DEFAULT_ADMIN_ROLE() && + role == defaultAdminRole() && account == adminBefore ) ? ( adminAfter == 0 && @@ -185,8 +187,8 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) { address adminAfter = defaultAdmin(); assert adminBefore != adminAfter => ( - f.selector == acceptDefaultAdminTransfer().selector || - f.selector == renounceRole(bytes32,address).selector + f.selector == sig:acceptDefaultAdminTransfer().selector || + f.selector == sig:renounceRole(bytes32,address).selector ), "default admin is only affected by accepting an admin transfer or renoucing"; } @@ -199,19 +201,19 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) { */ rule noPendingDefaultAdminChange(env e, method f, calldataarg args) { address pendingAdminBefore = pendingDefaultAdmin_(); - address scheduleBefore = pendingDefaultAdminSchedule_(); + uint48 scheduleBefore = pendingDefaultAdminSchedule_(); f(e, args); address pendingAdminAfter = pendingDefaultAdmin_(); - address scheduleAfter = pendingDefaultAdminSchedule_(); + uint48 scheduleAfter = pendingDefaultAdminSchedule_(); assert ( pendingAdminBefore != pendingAdminAfter || scheduleBefore != scheduleAfter ) => ( - f.selector == beginDefaultAdminTransfer(address).selector || - f.selector == acceptDefaultAdminTransfer().selector || - f.selector == cancelDefaultAdminTransfer().selector || - f.selector == renounceRole(bytes32,address).selector + f.selector == sig:beginDefaultAdminTransfer(address).selector || + f.selector == sig:acceptDefaultAdminTransfer().selector || + f.selector == sig:cancelDefaultAdminTransfer().selector || + f.selector == sig:renounceRole(bytes32,address).selector ), "pending admin and its schedule is only affected by beginning, completing, or cancelling an admin transfer"; } @@ -241,8 +243,8 @@ rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) { uint48 pendingDelayAfter = pendingDelay_(e); assert pendingDelayBefore != pendingDelayAfter => ( - f.selector == changeDefaultAdminDelay(uint48).selector || - f.selector == rollbackDefaultAdminDelay().selector + f.selector == sig:changeDefaultAdminDelay(uint48).selector || + f.selector == sig:rollbackDefaultAdminDelay().selector ), "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay"; } @@ -282,7 +284,7 @@ rule beginDefaultAdminTransfer(env e, address newAdmin) { // effect assert success => pendingDefaultAdmin_() == newAdmin, "pending default admin is set"; - assert success => pendingDefaultAdminSchedule_() == e.block.timestamp + defaultAdminDelay(e), + assert success => pendingDefaultAdminSchedule_() == assert_uint48(e.block.timestamp + defaultAdminDelay(e)), "pending default admin delay is set"; } @@ -307,7 +309,7 @@ rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args // change can only happen towards the newAdmin, with the delay assert adminAfter != adminBefore => ( adminAfter == newAdmin && - e2.block.timestamp >= e1.block.timestamp + delayBefore + e2.block.timestamp >= assert_uint256(e1.block.timestamp + delayBefore) ), "The admin can only change after the enforced delay and to the previously scheduled new admin"; } @@ -393,7 +395,7 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) { "pending delay is set"; assert success => ( - pendingDelaySchedule_(e) > e.block.timestamp || + pendingDelaySchedule_(e) > assert_uint48(e.block.timestamp) || delayBefore == newDelay || // Interpreted as decreasing, x - x = 0 defaultAdminDelayIncreaseWait() == 0 ), @@ -419,7 +421,7 @@ rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48 assert delayAfter != delayBefore => ( delayAfter == newDelay && - e2.block.timestamp >= delayWait + e2.block.timestamp >= assert_uint256(delayWait) ), "A delay can only change after the applied schedule"; } @@ -433,9 +435,9 @@ rule pendingDelayWait(env e, uint48 newDelay) { uint48 oldDelay = defaultAdminDelay(e); changeDefaultAdminDelay(e, newDelay); - assert newDelay > oldDelay => pendingDelaySchedule_(e) == increasingDelaySchedule(e, newDelay), + assert newDelay > oldDelay => pendingDelaySchedule_(e) == assert_uint48(increasingDelaySchedule(e, newDelay)), "Delay wait is the minimum between the new delay and a threshold when the delay is increased"; - assert newDelay <= oldDelay => pendingDelaySchedule_(e) == decreasingDelaySchedule(e, newDelay), + assert newDelay <= oldDelay => pendingDelaySchedule_(e) == assert_uint48(decreasingDelaySchedule(e, newDelay)), "Delay wait is the difference between the current and the new delay when the delay is decreased"; }