|
@@ -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";
|
|
|
-}
|