You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
501 lines
31 KiB
501 lines
31 KiB
2 years ago
|
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";
|
||
|
}
|