From dfef6a68ee18dbd2e1f5a099061a3b8a0e404485 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Fri, 19 May 2023 23:49:23 +0200 Subject: [PATCH 1/3] Fix error when running hardhat test with parameters (#4265) --- hardhat/task-test-get-files.js | 34 ++++++++++++---------------------- 1 file changed, 12 insertions(+), 22 deletions(-) diff --git a/hardhat/task-test-get-files.js b/hardhat/task-test-get-files.js index 896bf1274af..108f40a42c0 100644 --- a/hardhat/task-test-get-files.js +++ b/hardhat/task-test-get-files.js @@ -3,33 +3,23 @@ const { TASK_TEST_GET_TEST_FILES } = require('hardhat/builtin-tasks/task-names') // Modifies `hardhat test` to skip the proxy tests after proxies are removed by the transpiler for upgradeability. -internalTask(TASK_TEST_GET_TEST_FILES).setAction(async ({ testFiles }, { config }) => { - if (testFiles.length !== 0) { - return testFiles; - } - - const globAsync = require('glob'); +internalTask(TASK_TEST_GET_TEST_FILES).setAction(async (args, hre, runSuper) => { const path = require('path'); const { promises: fs } = require('fs'); - const { promisify } = require('util'); - - const glob = promisify(globAsync); const hasProxies = await fs - .access(path.join(config.paths.sources, 'proxy/Proxy.sol')) + .access(path.join(hre.config.paths.sources, 'proxy/Proxy.sol')) .then(() => true) .catch(() => false); - return await glob(path.join(config.paths.tests, '**/*.js'), { - ignore: hasProxies - ? [] - : [ - 'proxy/beacon/BeaconProxy.test.js', - 'proxy/beacon/UpgradeableBeacon.test.js', - 'proxy/ERC1967/ERC1967Proxy.test.js', - 'proxy/transparent/ProxyAdmin.test.js', - 'proxy/transparent/TransparentUpgradeableProxy.test.js', - 'proxy/utils/UUPSUpgradeable.test.js', - ].map(p => path.join(config.paths.tests, p)), - }); + const ignoredIfProxy = [ + 'proxy/beacon/BeaconProxy.test.js', + 'proxy/beacon/UpgradeableBeacon.test.js', + 'proxy/ERC1967/ERC1967Proxy.test.js', + 'proxy/transparent/ProxyAdmin.test.js', + 'proxy/transparent/TransparentUpgradeableProxy.test.js', + 'proxy/utils/UUPSUpgradeable.test.js', + ].map(p => path.join(hre.config.paths.tests, p)); + + return (await runSuper(args)).filter(file => hasProxies || !ignoredIfProxy.includes(file)); }); From a1d57bac505eab080f7b5009cfd5f98dd2e779a2 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 23 May 2023 20:54:34 +0200 Subject: [PATCH 2/3] Improve FV specifications for AccessControlDefaultAdminRules (#4223) Co-authored-by: ernestognw Co-authored-by: Francisco --- .../specs/AccessControlDefaultAdminRules.spec | 244 ++++++++---------- certora/specs/helpers/helpers.spec | 9 + 2 files changed, 113 insertions(+), 140 deletions(-) diff --git a/certora/specs/AccessControlDefaultAdminRules.spec b/certora/specs/AccessControlDefaultAdminRules.spec index a4baa1871a9..58b9d1202aa 100644 --- a/certora/specs/AccessControlDefaultAdminRules.spec +++ b/certora/specs/AccessControlDefaultAdminRules.spec @@ -12,44 +12,23 @@ use rule onlyGrantCanGrant filtered { │ Helpers │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +definition timeSanity(env e) returns bool = + e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48(); -function max_uint48() returns mathint { - return (1 << 48) - 1; -} +definition delayChangeWaitSanity(env e, uint48 newDelay) returns bool = + e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48(); -function nonZeroAccount(address account) returns bool { - return account != 0; -} +definition isSet(uint48 schedule) returns bool = + schedule != 0; -function timeSanity(env e) returns bool { - return - e.block.timestamp > 0 && // Avoids 0 schedules - e.block.timestamp + defaultAdminDelay(e) < max_uint48(); -} +definition hasPassed(env e, uint48 schedule) returns bool = + schedule < e.block.timestamp; -function delayChangeWaitSanity(env e, uint48 newDelay) returns bool { - return e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48(); -} +definition increasingDelaySchedule(env e, uint48 newDelay) returns mathint = + e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait()); -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; -} +definition decreasingDelaySchedule(env e, uint48 newDelay) returns mathint = + e.block.timestamp + defaultAdminDelay(e) - newDelay; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -57,11 +36,10 @@ function decreasingDelaySchedule(env e, uint48 newDelay) returns mathint { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant defaultAdminConsistency(address account) - defaultAdmin() == account <=> hasRole(DEFAULT_ADMIN_ROLE(), account) + (account == defaultAdmin() && account != 0) <=> hasRole(DEFAULT_ADMIN_ROLE(), account) { - preserved { - // defaultAdmin() returns the zero address when there's no default admin - require nonZeroAccount(account); + preserved with (env e) { + require nonzerosender(e); } } @@ -72,10 +50,12 @@ invariant defaultAdminConsistency(address account) */ 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 } + { + preserved { + requireInvariant defaultAdminConsistency(account); + requireInvariant defaultAdminConsistency(another); + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -118,7 +98,8 @@ rule revokeRoleEffect(env e, bytes32 role) { "roles can only be revoked by their owner except for the default admin role"; // effect - assert success => !hasRole(role, account), "role is revoked"; + assert success => !hasRole(role, account), + "role is revoked"; // no side effect assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount), @@ -137,35 +118,59 @@ rule renounceRoleEffect(env e, bytes32 role) { address account; address otherAccount; - bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - uint48 scheduleBefore = pendingDefaultAdminSchedule_(); + 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); + 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 || ( - 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"; + ), + "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 => !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), + assert hasOtherRoleBefore != hasOtherRoleAfter => ( + role == otherRole && + account == otherAccount + ), "no other role is affected"; } @@ -175,10 +180,6 @@ rule renounceRoleEffect(env e, bytes32 role) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ 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(); @@ -186,18 +187,17 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) { 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"; + ), + "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: pendingDefaultAdmin is only affected by beginning, completing (accept or renounce), 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); @@ -210,8 +210,10 @@ rule noPendingDefaultAdminChange(env e, method f, calldataarg args) { ) => ( 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"; + f.selector == cancelDefaultAdminTransfer().selector || + f.selector == renounceRole(bytes32,address).selector + ), + "pending admin and its schedule is only affected by beginning, completing, or cancelling an admin transfer"; } /* @@ -224,7 +226,8 @@ rule noDefaultAdminDelayChange(env e, method f, calldataarg args) { f(e, args); uint48 delayAfter = defaultAdminDelay(e); - assert delayBefore == delayAfter, "delay can't be changed atomically by any function"; + assert delayBefore == delayAfter, + "delay can't be changed atomically by any function"; } /* @@ -240,7 +243,8 @@ rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) { assert pendingDelayBefore != pendingDelayAfter => ( f.selector == changeDefaultAdminDelay(uint48).selector || f.selector == rollbackDefaultAdminDelay().selector - ), "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay"; + ), + "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay"; } /* @@ -263,10 +267,10 @@ rule noDefaultAdminDelayIncreaseWaitChange(env e, method f, calldataarg args) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule beginDefaultAdminTransfer(env e, address newAdmin) { - require nonpayable(e); require timeSanity(e); - requireInvariant defaultAdminConsistency(defaultAdmin()); - requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin()); + require nonpayable(e); + require nonzerosender(e); + requireInvariant defaultAdminConsistency(e.msg.sender); beginDefaultAdminTransfer@withrevert(e, newAdmin); bool success = !lastReverted; @@ -288,18 +292,24 @@ rule beginDefaultAdminTransfer(env e, address newAdmin) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args, address newAdmin) { - require e1.block.timestamp < e2.block.timestamp; + 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"; + // change can only happen towards the newAdmin, with the delay + assert adminAfter != adminBefore => ( + adminAfter == newAdmin && + e2.block.timestamp >= e1.block.timestamp + delayBefore + ), + "The admin can only change after the enforced delay and to the previously scheduled new admin"; } /* @@ -309,17 +319,19 @@ rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args */ rule acceptDefaultAdminTransfer(env e) { require nonpayable(e); - requireInvariant defaultAdminConsistency(defaultAdmin()); - requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin()); address pendingAdminBefore = pendingDefaultAdmin_(); - uint48 scheduleAfter = pendingDefaultAdminSchedule_(); + uint48 scheduleBefore = pendingDefaultAdminSchedule_(); acceptDefaultAdminTransfer@withrevert(e); bool success = !lastReverted; // liveness - assert success <=> e.msg.sender == pendingAdminBefore && isSet(scheduleAfter) && hasPassed(e, scheduleAfter), + 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 @@ -338,8 +350,8 @@ rule acceptDefaultAdminTransfer(env e) { */ rule cancelDefaultAdminTransfer(env e) { require nonpayable(e); - requireInvariant defaultAdminConsistency(defaultAdmin()); - requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin()); + require nonzerosender(e); + requireInvariant defaultAdminConsistency(e.msg.sender); cancelDefaultAdminTransfer@withrevert(e); bool success = !lastReverted; @@ -361,11 +373,11 @@ rule cancelDefaultAdminTransfer(env e) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule changeDefaultAdminDelay(env e, uint48 newDelay) { - require nonpayable(e); require timeSanity(e); + require nonpayable(e); + require nonzerosender(e); require delayChangeWaitSanity(e, newDelay); - requireInvariant defaultAdminConsistency(defaultAdmin()); - requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin()); + requireInvariant defaultAdminConsistency(e.msg.sender); uint48 delayBefore = defaultAdminDelay(e); @@ -377,7 +389,9 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) { "only the current default admin can begin a delay change"; // effect - assert success => pendingDelay_(e) == newDelay, "pending delay is set"; + assert success => pendingDelay_(e) == newDelay, + "pending delay is set"; + assert success => ( pendingDelaySchedule_(e) > e.block.timestamp || delayBefore == newDelay || // Interpreted as decreasing, x - x = 0 @@ -392,17 +406,22 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48 newDelay) { - require e1.block.timestamp < e2.block.timestamp; + 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"; + assert delayAfter != delayBefore => ( + delayAfter == newDelay && + e2.block.timestamp >= delayWait + ), + "A delay can only change after the applied schedule"; } /* @@ -427,8 +446,8 @@ rule pendingDelayWait(env e, uint48 newDelay) { */ rule rollbackDefaultAdminDelay(env e) { require nonpayable(e); - requireInvariant defaultAdminConsistency(defaultAdmin()); - requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin()); + require nonzerosender(e); + requireInvariant defaultAdminConsistency(e.msg.sender); rollbackDefaultAdminDelay@withrevert(e); bool success = !lastReverted; @@ -443,58 +462,3 @@ rule rollbackDefaultAdminDelay(env e) { 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"; -} diff --git a/certora/specs/helpers/helpers.spec b/certora/specs/helpers/helpers.spec index 24842d62f13..04e76df94ae 100644 --- a/certora/specs/helpers/helpers.spec +++ b/certora/specs/helpers/helpers.spec @@ -1 +1,10 @@ +// environment definition nonpayable(env e) returns bool = e.msg.value == 0; +definition nonzerosender(env e) returns bool = e.msg.sender != 0; + +// constants +definition max_uint48() returns mathint = (1 << 48) - 1; + +// 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; From 7e814a3074baa921db584c180ff6e300cdec8735 Mon Sep 17 00:00:00 2001 From: Francisco Date: Tue, 23 May 2023 22:21:17 +0100 Subject: [PATCH 3/3] Fix release merge script (#4273) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Ernesto García --- scripts/release/workflow/prepare-release-merge.sh | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/scripts/release/workflow/prepare-release-merge.sh b/scripts/release/workflow/prepare-release-merge.sh index 8be96922c39..4e6da5145dd 100644 --- a/scripts/release/workflow/prepare-release-merge.sh +++ b/scripts/release/workflow/prepare-release-merge.sh @@ -9,15 +9,18 @@ MERGE_BRANCH=merge/$GITHUB_REF_NAME git checkout -B "$MERGE_BRANCH" "$GITHUB_REF_NAME" # Get deleted changesets in this branch that might conflict with master -readarray -t DELETED_CHANGESETS < <(git diff origin/master --name-only -- '.changeset/*.md') +# --diff-filter=D - Only deleted files +readarray -t DELETED_CHANGESETS < <(git diff origin/master --diff-filter=D --name-only -- '.changeset/*.md') # Merge master, which will take those files cherry-picked. Auto-resolve conflicts favoring master. -git merge origin/master -m "Merge master to $GITHUB_REF_NAME" -X theirs +# Ignore conflicts that can't be resolved. +git merge origin/master -m "Merge master to $GITHUB_REF_NAME" -X theirs || true # Remove the originally deleted changesets to correctly sync with master rm -f "${DELETED_CHANGESETS[@]}" -git add .changeset/ +# Only git add deleted files +git ls-files --deleted .changeset/ | xargs git add # Allow empty here since there may be no changes if `rm -f` failed for all changesets git commit --allow-empty -m "Sync changesets with master"