mirror of
https://github.com/th30d4y/OpenLearnX.git
synced 2026-05-26 19:26:33 +00:00
Fix .gitignore: stop tracking ignored files
This commit is contained in:
5t4l1n
@@ -0,0 +1,126 @@
|
||||
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, method f, bytes32 role, address account) {
|
||||
calldataarg args;
|
||||
|
||||
bool hasRoleBefore = hasRole(role, account);
|
||||
f(e, args);
|
||||
bool hasRoleAfter = hasRole(role, account);
|
||||
|
||||
assert (
|
||||
!hasRoleBefore &&
|
||||
hasRoleAfter
|
||||
) => (
|
||||
f.selector == grantRole(bytes32, address).selector
|
||||
);
|
||||
|
||||
assert (
|
||||
hasRoleBefore &&
|
||||
!hasRoleAfter
|
||||
) => (
|
||||
f.selector == revokeRole(bytes32, address).selector ||
|
||||
f.selector == renounceRole(bytes32, address).selector
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: grantRole only affects the specified user/role combo │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule grantRoleEffect(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);
|
||||
|
||||
grantRole@withrevert(e, role, account);
|
||||
bool success = !lastReverted;
|
||||
|
||||
bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
|
||||
|
||||
// liveness
|
||||
assert success <=> isCallerAdmin;
|
||||
|
||||
// effect
|
||||
assert success => hasRole(role, account);
|
||||
|
||||
// no side effect
|
||||
assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ 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;
|
||||
|
||||
// effect
|
||||
assert success => !hasRole(role, account);
|
||||
|
||||
// no side effect
|
||||
assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ 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);
|
||||
|
||||
renounceRole@withrevert(e, role, account);
|
||||
bool success = !lastReverted;
|
||||
|
||||
bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
|
||||
|
||||
// liveness
|
||||
assert success <=> account == e.msg.sender;
|
||||
|
||||
// effect
|
||||
assert success => !hasRole(role, account);
|
||||
|
||||
// no side effect
|
||||
assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
|
||||
}
|
||||
@@ -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";
|
||||
}
|
||||
@@ -0,0 +1,366 @@
|
||||
import "helpers/helpers.spec"
|
||||
|
||||
methods {
|
||||
pushFront(bytes32) envfree
|
||||
pushBack(bytes32) envfree
|
||||
popFront() returns (bytes32) envfree
|
||||
popBack() returns (bytes32) envfree
|
||||
clear() envfree
|
||||
|
||||
// exposed for FV
|
||||
begin() returns (int128) envfree
|
||||
end() returns (int128) envfree
|
||||
|
||||
// view
|
||||
length() returns (uint256) envfree
|
||||
empty() returns (bool) envfree
|
||||
front() returns (bytes32) envfree
|
||||
back() returns (bytes32) envfree
|
||||
at_(uint256) returns (bytes32) envfree // at is a reserved word
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Helpers │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
|
||||
function min_int128() returns mathint {
|
||||
return -(1 << 127);
|
||||
}
|
||||
|
||||
function max_int128() returns mathint {
|
||||
return (1 << 127) - 1;
|
||||
}
|
||||
|
||||
// Could be broken in theory, but not in practice
|
||||
function boundedQueue() returns bool {
|
||||
return
|
||||
max_int128() > to_mathint(end()) &&
|
||||
min_int128() < to_mathint(begin());
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: end is larger or equal than begin │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant boundariesConsistency()
|
||||
end() >= begin()
|
||||
filtered { f -> !f.isView }
|
||||
{ preserved { require boundedQueue(); } }
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: length is end minus begin │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant lengthConsistency()
|
||||
length() == to_mathint(end()) - to_mathint(begin())
|
||||
filtered { f -> !f.isView }
|
||||
{ preserved { require boundedQueue(); } }
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: empty() is length 0 and no element exists │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant emptiness()
|
||||
empty() <=> length() == 0
|
||||
filtered { f -> !f.isView }
|
||||
{ preserved { require boundedQueue(); } }
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: front points to the first index and back points to the last one │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant queueEndings()
|
||||
at_(length() - 1) == back() && at_(0) == front()
|
||||
filtered { f -> !f.isView }
|
||||
{
|
||||
preserved {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: pushFront adds an element at the beginning of the queue │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule pushFront(bytes32 value) {
|
||||
require boundedQueue();
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
|
||||
pushFront@withrevert(value);
|
||||
|
||||
// liveness
|
||||
assert !lastReverted, "never reverts";
|
||||
|
||||
// effect
|
||||
assert front() == value, "front set to value";
|
||||
assert length() == lengthBefore + 1, "queue extended";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: pushFront preserves the previous values in the queue with a +1 offset │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule pushFrontConsistency(uint256 index) {
|
||||
require boundedQueue();
|
||||
|
||||
bytes32 beforeAt = at_(index);
|
||||
|
||||
bytes32 value;
|
||||
pushFront(value);
|
||||
|
||||
// try to read value
|
||||
bytes32 afterAt = at_@withrevert(index + 1);
|
||||
|
||||
assert !lastReverted, "value still there";
|
||||
assert afterAt == beforeAt, "data is preserved";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: pushBack adds an element at the end of the queue │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule pushBack(bytes32 value) {
|
||||
require boundedQueue();
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
|
||||
pushBack@withrevert(value);
|
||||
|
||||
// liveness
|
||||
assert !lastReverted, "never reverts";
|
||||
|
||||
// effect
|
||||
assert back() == value, "back set to value";
|
||||
assert length() == lengthBefore + 1, "queue increased";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: pushBack preserves the previous values in the queue │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule pushBackConsistency(uint256 index) {
|
||||
require boundedQueue();
|
||||
|
||||
bytes32 beforeAt = at_(index);
|
||||
|
||||
bytes32 value;
|
||||
pushBack(value);
|
||||
|
||||
// try to read value
|
||||
bytes32 afterAt = at_@withrevert(index);
|
||||
|
||||
assert !lastReverted, "value still there";
|
||||
assert afterAt == beforeAt, "data is preserved";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: popFront removes an element from the beginning of the queue │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule popFront {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bytes32 frontBefore = front@withrevert();
|
||||
|
||||
bytes32 popped = popFront@withrevert();
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> lengthBefore != 0, "never reverts if not previously empty";
|
||||
|
||||
// effect
|
||||
assert success => frontBefore == popped, "previous front is returned";
|
||||
assert success => length() == lengthBefore - 1, "queue decreased";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: at(x) is preserved and offset to at(x - 1) after calling popFront |
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule popFrontConsistency(uint256 index) {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
// Read (any) value that is not the front (this asserts the value exists / the queue is long enough)
|
||||
require index > 1;
|
||||
bytes32 before = at_(index);
|
||||
|
||||
popFront();
|
||||
|
||||
// try to read value
|
||||
bytes32 after = at_@withrevert(index - 1);
|
||||
|
||||
assert !lastReverted, "value still exists in the queue";
|
||||
assert before == after, "values are offset and not modified";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: popBack removes an element from the end of the queue │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule popBack {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bytes32 backBefore = back@withrevert();
|
||||
|
||||
bytes32 popped = popBack@withrevert();
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> lengthBefore != 0, "never reverts if not previously empty";
|
||||
|
||||
// effect
|
||||
assert success => backBefore == popped, "previous back is returned";
|
||||
assert success => length() == lengthBefore - 1, "queue decreased";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: at(x) is preserved after calling popBack |
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule popBackConsistency(uint256 index) {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
// Read (any) value that is not the back (this asserts the value exists / the queue is long enough)
|
||||
require index < length() - 1;
|
||||
bytes32 before = at_(index);
|
||||
|
||||
popBack();
|
||||
|
||||
// try to read value
|
||||
bytes32 after = at_@withrevert(index);
|
||||
|
||||
assert !lastReverted, "value still exists in the queue";
|
||||
assert before == after, "values are offset and not modified";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: clear sets length to 0 │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule clear {
|
||||
clear@withrevert();
|
||||
|
||||
// liveness
|
||||
assert !lastReverted, "never reverts";
|
||||
|
||||
// effect
|
||||
assert length() == 0, "sets length to 0";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: front/back access reverts only if the queue is empty or querying out of bounds │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule onlyEmptyRevert(env e) {
|
||||
require nonpayable(e);
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
|
||||
bool emptyBefore = empty();
|
||||
|
||||
f@withrevert(e, args);
|
||||
|
||||
assert lastReverted => (
|
||||
(f.selector == front().selector && emptyBefore) ||
|
||||
(f.selector == back().selector && emptyBefore) ||
|
||||
(f.selector == popFront().selector && emptyBefore) ||
|
||||
(f.selector == popBack().selector && emptyBefore) ||
|
||||
f.selector == at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert
|
||||
), "only revert if empty or out of bounds";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: at(index) only reverts if index is out of bounds |
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule onlyOutOfBoundsRevert(uint256 index) {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
at_@withrevert(index);
|
||||
|
||||
assert lastReverted <=> index >= length(), "only reverts if index is out of bounds";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: only clear/push/pop operations can change the length of the queue │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule noLengthChange(env e) {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
f(e, args);
|
||||
uint256 lengthAfter = length();
|
||||
|
||||
assert lengthAfter != lengthBefore => (
|
||||
(f.selector == pushFront(bytes32).selector && lengthAfter == lengthBefore + 1) ||
|
||||
(f.selector == pushBack(bytes32).selector && lengthAfter == lengthBefore + 1) ||
|
||||
(f.selector == popBack().selector && lengthAfter == lengthBefore - 1) ||
|
||||
(f.selector == popFront().selector && lengthAfter == lengthBefore - 1) ||
|
||||
(f.selector == clear().selector && lengthAfter == 0)
|
||||
), "length is only affected by clear/pop/push operations";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: only push/pop can change values bounded in the queue (outside values aren't cleared) │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule noDataChange(env e) {
|
||||
requireInvariant boundariesConsistency();
|
||||
require boundedQueue();
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
|
||||
uint256 index;
|
||||
bytes32 atBefore = at_(index);
|
||||
f(e, args);
|
||||
bytes32 atAfter = at_@withrevert(index);
|
||||
bool atAfterSuccess = !lastReverted;
|
||||
|
||||
assert !atAfterSuccess <=> (
|
||||
f.selector == clear().selector ||
|
||||
(f.selector == popBack().selector && index == length()) ||
|
||||
(f.selector == popFront().selector && index == length())
|
||||
), "indexes of the queue are only removed by clear or pop";
|
||||
|
||||
assert atAfterSuccess && atAfter != atBefore => (
|
||||
f.selector == popFront().selector ||
|
||||
f.selector == pushFront(bytes32).selector
|
||||
), "values of the queue are only changed by popFront or pushFront";
|
||||
}
|
||||
@@ -0,0 +1,414 @@
|
||||
import "helpers/helpers.spec"
|
||||
import "methods/IERC20.spec"
|
||||
import "methods/IERC2612.spec"
|
||||
|
||||
methods {
|
||||
// non standard ERC20 functions
|
||||
increaseAllowance(address,uint256) returns (bool)
|
||||
decreaseAllowance(address,uint256) returns (bool)
|
||||
|
||||
// exposed for FV
|
||||
mint(address,uint256)
|
||||
burn(address,uint256)
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Ghost & hooks: sum of all balances │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
ghost sumOfBalances() returns uint256 {
|
||||
init_state axiom sumOfBalances() == 0;
|
||||
}
|
||||
|
||||
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
|
||||
havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: totalSupply is the sum of all balances │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant totalSupplyIsSumOfBalances()
|
||||
totalSupply() == sumOfBalances()
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: balance of address(0) is 0 │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant zeroAddressNoBalance()
|
||||
balanceOf(0) == 0
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: only mint and burn can change total supply │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule noChangeTotalSupply(env e) {
|
||||
requireInvariant totalSupplyIsSumOfBalances();
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
|
||||
uint256 totalSupplyBefore = totalSupply();
|
||||
f(e, args);
|
||||
uint256 totalSupplyAfter = totalSupply();
|
||||
|
||||
assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector;
|
||||
assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: only the token holder or an approved third party can reduce an account's balance │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule onlyAuthorizedCanTransfer(env e) {
|
||||
requireInvariant totalSupplyIsSumOfBalances();
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
address account;
|
||||
|
||||
uint256 allowanceBefore = allowance(account, e.msg.sender);
|
||||
uint256 balanceBefore = balanceOf(account);
|
||||
f(e, args);
|
||||
uint256 balanceAfter = balanceOf(account);
|
||||
|
||||
assert (
|
||||
balanceAfter < balanceBefore
|
||||
) => (
|
||||
f.selector == burn(address,uint256).selector ||
|
||||
e.msg.sender == account ||
|
||||
balanceBefore - balanceAfter <= allowanceBefore
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: only the token holder (or a permit) can increase allowance. The spender can decrease it by using it │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule onlyHolderOfSpenderCanChangeAllowance(env e) {
|
||||
requireInvariant totalSupplyIsSumOfBalances();
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
address holder;
|
||||
address spender;
|
||||
|
||||
uint256 allowanceBefore = allowance(holder, spender);
|
||||
f(e, args);
|
||||
uint256 allowanceAfter = allowance(holder, spender);
|
||||
|
||||
assert (
|
||||
allowanceAfter > allowanceBefore
|
||||
) => (
|
||||
(f.selector == approve(address,uint256).selector && e.msg.sender == holder) ||
|
||||
(f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
|
||||
(f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
|
||||
);
|
||||
|
||||
assert (
|
||||
allowanceAfter < allowanceBefore
|
||||
) => (
|
||||
(f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
|
||||
(f.selector == approve(address,uint256).selector && e.msg.sender == holder ) ||
|
||||
(f.selector == decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) ||
|
||||
(f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: mint behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule mint(env e) {
|
||||
requireInvariant totalSupplyIsSumOfBalances();
|
||||
require nonpayable(e);
|
||||
|
||||
address to;
|
||||
address other;
|
||||
uint256 amount;
|
||||
|
||||
// cache state
|
||||
uint256 toBalanceBefore = balanceOf(to);
|
||||
uint256 otherBalanceBefore = balanceOf(other);
|
||||
uint256 totalSupplyBefore = totalSupply();
|
||||
|
||||
// run transaction
|
||||
mint@withrevert(e, to, amount);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
assert to == 0 || totalSupplyBefore + amount > max_uint256;
|
||||
} else {
|
||||
// updates balance and totalSupply
|
||||
assert balanceOf(to) == toBalanceBefore + amount;
|
||||
assert totalSupply() == totalSupplyBefore + amount;
|
||||
|
||||
// no other balance is modified
|
||||
assert balanceOf(other) != otherBalanceBefore => other == to;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: burn behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule burn(env e) {
|
||||
requireInvariant totalSupplyIsSumOfBalances();
|
||||
require nonpayable(e);
|
||||
|
||||
address from;
|
||||
address other;
|
||||
uint256 amount;
|
||||
|
||||
// cache state
|
||||
uint256 fromBalanceBefore = balanceOf(from);
|
||||
uint256 otherBalanceBefore = balanceOf(other);
|
||||
uint256 totalSupplyBefore = totalSupply();
|
||||
|
||||
// run transaction
|
||||
burn@withrevert(e, from, amount);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
assert from == 0 || fromBalanceBefore < amount;
|
||||
} else {
|
||||
// updates balance and totalSupply
|
||||
assert balanceOf(from) == fromBalanceBefore - amount;
|
||||
assert totalSupply() == totalSupplyBefore - amount;
|
||||
|
||||
// no other balance is modified
|
||||
assert balanceOf(other) != otherBalanceBefore => other == from;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: transfer behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule transfer(env e) {
|
||||
requireInvariant totalSupplyIsSumOfBalances();
|
||||
require nonpayable(e);
|
||||
|
||||
address holder = e.msg.sender;
|
||||
address recipient;
|
||||
address other;
|
||||
uint256 amount;
|
||||
|
||||
// cache state
|
||||
uint256 holderBalanceBefore = balanceOf(holder);
|
||||
uint256 recipientBalanceBefore = balanceOf(recipient);
|
||||
uint256 otherBalanceBefore = balanceOf(other);
|
||||
|
||||
// run transaction
|
||||
transfer@withrevert(e, recipient, amount);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
assert holder == 0 || recipient == 0 || amount > holderBalanceBefore;
|
||||
} else {
|
||||
// balances of holder and recipient are updated
|
||||
assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount);
|
||||
assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
|
||||
|
||||
// no other balance is modified
|
||||
assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: transferFrom behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule transferFrom(env e) {
|
||||
requireInvariant totalSupplyIsSumOfBalances();
|
||||
require nonpayable(e);
|
||||
|
||||
address spender = e.msg.sender;
|
||||
address holder;
|
||||
address recipient;
|
||||
address other;
|
||||
uint256 amount;
|
||||
|
||||
// cache state
|
||||
uint256 allowanceBefore = allowance(holder, spender);
|
||||
uint256 holderBalanceBefore = balanceOf(holder);
|
||||
uint256 recipientBalanceBefore = balanceOf(recipient);
|
||||
uint256 otherBalanceBefore = balanceOf(other);
|
||||
|
||||
// run transaction
|
||||
transferFrom@withrevert(e, holder, recipient, amount);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore;
|
||||
} else {
|
||||
// allowance is valid & updated
|
||||
assert allowanceBefore >= amount;
|
||||
assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
|
||||
|
||||
// balances of holder and recipient are updated
|
||||
assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount);
|
||||
assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
|
||||
|
||||
// no other balance is modified
|
||||
assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: approve behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule approve(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address holder = e.msg.sender;
|
||||
address spender;
|
||||
address otherHolder;
|
||||
address otherSpender;
|
||||
uint256 amount;
|
||||
|
||||
// cache state
|
||||
uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
|
||||
|
||||
// run transaction
|
||||
approve@withrevert(e, spender, amount);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
assert holder == 0 || spender == 0;
|
||||
} else {
|
||||
// allowance is updated
|
||||
assert allowance(holder, spender) == amount;
|
||||
|
||||
// other allowances are untouched
|
||||
assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: increaseAllowance behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule increaseAllowance(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address holder = e.msg.sender;
|
||||
address spender;
|
||||
address otherHolder;
|
||||
address otherSpender;
|
||||
uint256 amount;
|
||||
|
||||
// cache state
|
||||
uint256 allowanceBefore = allowance(holder, spender);
|
||||
uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
|
||||
|
||||
// run transaction
|
||||
increaseAllowance@withrevert(e, spender, amount);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256;
|
||||
} else {
|
||||
// allowance is updated
|
||||
assert allowance(holder, spender) == allowanceBefore + amount;
|
||||
|
||||
// other allowances are untouched
|
||||
assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: decreaseAllowance behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule decreaseAllowance(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address holder = e.msg.sender;
|
||||
address spender;
|
||||
address otherHolder;
|
||||
address otherSpender;
|
||||
uint256 amount;
|
||||
|
||||
// cache state
|
||||
uint256 allowanceBefore = allowance(holder, spender);
|
||||
uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
|
||||
|
||||
// run transaction
|
||||
decreaseAllowance@withrevert(e, spender, amount);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
assert holder == 0 || spender == 0 || allowanceBefore < amount;
|
||||
} else {
|
||||
// allowance is updated
|
||||
assert allowance(holder, spender) == allowanceBefore - amount;
|
||||
|
||||
// other allowances are untouched
|
||||
assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: permit behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule permit(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address holder;
|
||||
address spender;
|
||||
uint256 amount;
|
||||
uint256 deadline;
|
||||
uint8 v;
|
||||
bytes32 r;
|
||||
bytes32 s;
|
||||
|
||||
address account1;
|
||||
address account2;
|
||||
address account3;
|
||||
|
||||
// cache state
|
||||
uint256 nonceBefore = nonces(holder);
|
||||
uint256 otherNonceBefore = nonces(account1);
|
||||
uint256 otherAllowanceBefore = allowance(account2, account3);
|
||||
|
||||
// sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice
|
||||
require nonceBefore < max_uint256;
|
||||
require otherNonceBefore < max_uint256;
|
||||
|
||||
// run transaction
|
||||
permit@withrevert(e, holder, spender, amount, deadline, v, r, s);
|
||||
|
||||
// check outcome
|
||||
if (lastReverted) {
|
||||
// Without formally checking the signature, we can't verify exactly the revert causes
|
||||
assert true;
|
||||
} else {
|
||||
// allowance and nonce are updated
|
||||
assert allowance(holder, spender) == amount;
|
||||
assert nonces(holder) == nonceBefore + 1;
|
||||
|
||||
// deadline was respected
|
||||
assert deadline >= e.block.timestamp;
|
||||
|
||||
// no other allowance or nonce is modified
|
||||
assert nonces(account1) != otherNonceBefore => account1 == holder;
|
||||
assert allowance(account2, account3) != otherAllowanceBefore => (account2 == holder && account3 == spender);
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,48 @@
|
||||
import "helpers/helpers.spec"
|
||||
import "methods/IERC20.spec"
|
||||
import "methods/IERC3156.spec"
|
||||
|
||||
methods {
|
||||
// non standard ERC3156 functions
|
||||
flashFeeReceiver() returns (address) envfree
|
||||
|
||||
// function summaries below
|
||||
_mint(address account, uint256 amount) => specMint(account, amount)
|
||||
_burn(address account, uint256 amount) => specBurn(account, amount)
|
||||
_transfer(address from, address to, uint256 amount) => specTransfer(from, to, amount)
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Ghost: track mint and burns in the CVL │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
ghost mapping(address => uint256) trackedMintAmount;
|
||||
ghost mapping(address => uint256) trackedBurnAmount;
|
||||
ghost mapping(address => mapping(address => uint256)) trackedTransferedAmount;
|
||||
|
||||
function specMint(address account, uint256 amount) returns bool { trackedMintAmount[account] = amount; return true; }
|
||||
function specBurn(address account, uint256 amount) returns bool { trackedBurnAmount[account] = amount; return true; }
|
||||
function specTransfer(address from, address to, uint256 amount) returns bool { trackedTransferedAmount[from][to] = amount; return true; }
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: When doing a flashLoan, "amount" is minted and burnt, additionally, the fee is either burnt │
|
||||
│ (if the fee recipient is 0) or transferred (if the fee recipient is not 0) │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule checkMintAndBurn(env e) {
|
||||
address receiver;
|
||||
address token;
|
||||
uint256 amount;
|
||||
bytes data;
|
||||
|
||||
uint256 fees = flashFee(token, amount);
|
||||
address recipient = flashFeeReceiver();
|
||||
|
||||
flashLoan(e, receiver, token, amount, data);
|
||||
|
||||
assert trackedMintAmount[receiver] == amount;
|
||||
assert trackedBurnAmount[receiver] == amount + (recipient == 0 ? fees : 0);
|
||||
assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == fees;
|
||||
}
|
||||
@@ -0,0 +1,198 @@
|
||||
import "helpers/helpers.spec"
|
||||
import "ERC20.spec"
|
||||
|
||||
methods {
|
||||
underlying() returns(address) envfree
|
||||
underlyingTotalSupply() returns(uint256) envfree
|
||||
underlyingBalanceOf(address) returns(uint256) envfree
|
||||
underlyingAllowanceToThis(address) returns(uint256) envfree
|
||||
|
||||
depositFor(address, uint256) returns(bool)
|
||||
withdrawTo(address, uint256) returns(bool)
|
||||
recover(address) returns(uint256)
|
||||
}
|
||||
|
||||
use invariant totalSupplyIsSumOfBalances
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool {
|
||||
return underlyingBalanceOf(a) <= underlyingTotalSupply();
|
||||
}
|
||||
|
||||
function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool {
|
||||
return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply();
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: wrapped token can't be undercollateralized (solvency of the wrapper) │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant totalSupplyIsSmallerThanUnderlyingBalance()
|
||||
totalSupply() <= underlyingBalanceOf(currentContract) &&
|
||||
underlyingBalanceOf(currentContract) <= underlyingTotalSupply() &&
|
||||
underlyingTotalSupply() <= max_uint256
|
||||
{
|
||||
preserved {
|
||||
requireInvariant totalSupplyIsSumOfBalances;
|
||||
require underlyingBalancesLowerThanUnderlyingSupply(currentContract);
|
||||
}
|
||||
preserved depositFor(address account, uint256 amount) with (env e) {
|
||||
require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract);
|
||||
}
|
||||
}
|
||||
|
||||
invariant noSelfWrap()
|
||||
currentContract != underlying()
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: depositFor liveness and effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule depositFor(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address sender = e.msg.sender;
|
||||
address receiver;
|
||||
address other;
|
||||
uint256 amount;
|
||||
|
||||
// sanity
|
||||
requireInvariant noSelfWrap;
|
||||
requireInvariant totalSupplyIsSumOfBalances;
|
||||
requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
|
||||
require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, sender);
|
||||
|
||||
uint256 balanceBefore = balanceOf(receiver);
|
||||
uint256 supplyBefore = totalSupply();
|
||||
uint256 senderUnderlyingBalanceBefore = underlyingBalanceOf(sender);
|
||||
uint256 senderUnderlyingAllowanceBefore = underlyingAllowanceToThis(sender);
|
||||
uint256 wrapperUnderlyingBalanceBefore = underlyingBalanceOf(currentContract);
|
||||
uint256 underlyingSupplyBefore = underlyingTotalSupply();
|
||||
|
||||
uint256 otherBalanceBefore = balanceOf(other);
|
||||
uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other);
|
||||
|
||||
depositFor@withrevert(e, receiver, amount);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
sender != currentContract && // invalid sender
|
||||
sender != 0 && // invalid sender
|
||||
receiver != 0 && // invalid receiver
|
||||
amount <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
|
||||
amount <= senderUnderlyingAllowanceBefore // deposit doesn't exceed allowance
|
||||
);
|
||||
|
||||
// effects
|
||||
assert success => (
|
||||
balanceOf(receiver) == balanceBefore + amount &&
|
||||
totalSupply() == supplyBefore + amount &&
|
||||
underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount &&
|
||||
underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert underlyingTotalSupply() == underlyingSupplyBefore;
|
||||
assert balanceOf(other) != otherBalanceBefore => other == receiver;
|
||||
assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: withdrawTo liveness and effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule withdrawTo(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address sender = e.msg.sender;
|
||||
address receiver;
|
||||
address other;
|
||||
uint256 amount;
|
||||
|
||||
// sanity
|
||||
requireInvariant noSelfWrap;
|
||||
requireInvariant totalSupplyIsSumOfBalances;
|
||||
requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
|
||||
require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, receiver);
|
||||
|
||||
uint256 balanceBefore = balanceOf(sender);
|
||||
uint256 supplyBefore = totalSupply();
|
||||
uint256 receiverUnderlyingBalanceBefore = underlyingBalanceOf(receiver);
|
||||
uint256 wrapperUnderlyingBalanceBefore = underlyingBalanceOf(currentContract);
|
||||
uint256 underlyingSupplyBefore = underlyingTotalSupply();
|
||||
|
||||
uint256 otherBalanceBefore = balanceOf(other);
|
||||
uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other);
|
||||
|
||||
withdrawTo@withrevert(e, receiver, amount);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
sender != 0 && // invalid sender
|
||||
receiver != 0 && // invalid receiver
|
||||
amount <= balanceBefore // withdraw doesn't exceed balance
|
||||
);
|
||||
|
||||
// effects
|
||||
assert success => (
|
||||
balanceOf(sender) == balanceBefore - amount &&
|
||||
totalSupply() == supplyBefore - amount &&
|
||||
underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
|
||||
underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert underlyingTotalSupply() == underlyingSupplyBefore;
|
||||
assert balanceOf(other) != otherBalanceBefore => other == sender;
|
||||
assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: recover liveness and effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule recover(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address receiver;
|
||||
address other;
|
||||
|
||||
// sanity
|
||||
requireInvariant noSelfWrap;
|
||||
requireInvariant totalSupplyIsSumOfBalances;
|
||||
requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
|
||||
|
||||
uint256 value = underlyingBalanceOf(currentContract) - totalSupply();
|
||||
uint256 supplyBefore = totalSupply();
|
||||
uint256 balanceBefore = balanceOf(receiver);
|
||||
|
||||
uint256 otherBalanceBefore = balanceOf(other);
|
||||
uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other);
|
||||
|
||||
recover@withrevert(e, receiver);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> receiver != 0;
|
||||
|
||||
// effect
|
||||
assert success => (
|
||||
balanceOf(receiver) == balanceBefore + value &&
|
||||
totalSupply() == supplyBefore + value &&
|
||||
totalSupply() == underlyingBalanceOf(currentContract)
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore;
|
||||
assert balanceOf(other) != otherBalanceBefore => other == receiver;
|
||||
}
|
||||
@@ -0,0 +1,589 @@
|
||||
import "helpers/helpers.spec"
|
||||
import "methods/IERC721.spec"
|
||||
|
||||
methods {
|
||||
// exposed for FV
|
||||
mint(address,uint256)
|
||||
safeMint(address,uint256)
|
||||
safeMint(address,uint256,bytes)
|
||||
burn(uint256)
|
||||
|
||||
tokenExists(uint256) returns (bool) envfree
|
||||
unsafeOwnerOf(uint256) returns (address) envfree
|
||||
unsafeGetApproved(uint256) returns (address) envfree
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Helpers │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
|
||||
// Could be broken in theory, but not in practice
|
||||
function balanceLimited(address account) returns bool {
|
||||
return balanceOf(account) < max_uint256;
|
||||
}
|
||||
|
||||
function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
|
||||
if (f.selector == transferFrom(address,address,uint256).selector) {
|
||||
transferFrom@withrevert(e, from, to, tokenId);
|
||||
} else if (f.selector == safeTransferFrom(address,address,uint256).selector) {
|
||||
safeTransferFrom@withrevert(e, from, to, tokenId);
|
||||
} else if (f.selector == safeTransferFrom(address,address,uint256,bytes).selector) {
|
||||
bytes params;
|
||||
require params.length < 0xffff;
|
||||
safeTransferFrom@withrevert(e, from, to, tokenId, params);
|
||||
} else {
|
||||
calldataarg args;
|
||||
f@withrevert(e, args);
|
||||
}
|
||||
}
|
||||
|
||||
function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
|
||||
if (f.selector == mint(address,uint256).selector) {
|
||||
mint@withrevert(e, to, tokenId);
|
||||
} else if (f.selector == safeMint(address,uint256).selector) {
|
||||
safeMint@withrevert(e, to, tokenId);
|
||||
} else if (f.selector == safeMint(address,uint256,bytes).selector) {
|
||||
bytes params;
|
||||
require params.length < 0xffff;
|
||||
safeMint@withrevert(e, to, tokenId, params);
|
||||
} else {
|
||||
require false;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Ghost & hooks: ownership count │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
ghost ownedTotal() returns uint256 {
|
||||
init_state axiom ownedTotal() == 0;
|
||||
}
|
||||
|
||||
ghost mapping(address => uint256) ownedByUser {
|
||||
init_state axiom forall address a. ownedByUser[a] == 0;
|
||||
}
|
||||
|
||||
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE {
|
||||
ownedByUser[newOwner] = ownedByUser[newOwner] + to_uint256(newOwner != 0 ? 1 : 0);
|
||||
ownedByUser[oldOwner] = ownedByUser[oldOwner] - to_uint256(oldOwner != 0 ? 1 : 0);
|
||||
|
||||
havoc ownedTotal assuming ownedTotal@new() == ownedTotal@old()
|
||||
+ to_uint256(newOwner != 0 ? 1 : 0)
|
||||
- to_uint256(oldOwner != 0 ? 1 : 0);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Ghost & hooks: sum of all balances │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
ghost sumOfBalances() returns uint256 {
|
||||
init_state axiom sumOfBalances() == 0;
|
||||
}
|
||||
|
||||
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
|
||||
havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
|
||||
}
|
||||
|
||||
ghost mapping(address => uint256) ghostBalanceOf {
|
||||
init_state axiom forall address a. ghostBalanceOf[a] == 0;
|
||||
}
|
||||
|
||||
hook Sload uint256 value _balances[KEY address user] STORAGE {
|
||||
require ghostBalanceOf[user] == value;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: ownedTotal is the sum of all balances │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant ownedTotalIsSumOfBalances()
|
||||
ownedTotal() == sumOfBalances()
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: balanceOf is the number of tokens owned │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant balanceOfConsistency(address user)
|
||||
balanceOf(user) == ownedByUser[user] &&
|
||||
balanceOf(user) == ghostBalanceOf[user]
|
||||
{
|
||||
preserved {
|
||||
require balanceLimited(user);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: owner of a token must have some balance │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant ownerHasBalance(uint256 tokenId)
|
||||
balanceOf(ownerOf(tokenId)) > 0
|
||||
{
|
||||
preserved {
|
||||
requireInvariant balanceOfConsistency(ownerOf(tokenId));
|
||||
require balanceLimited(ownerOf(tokenId));
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: tokens that do not exist are not owned and not approved │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant notMintedUnset(uint256 tokenId)
|
||||
(!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) &&
|
||||
(!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0)
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: ownerOf and getApproved revert if token does not exist │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule notMintedRevert(uint256 tokenId) {
|
||||
requireInvariant notMintedUnset(tokenId);
|
||||
|
||||
bool e = tokenExists(tokenId);
|
||||
|
||||
address owner = ownerOf@withrevert(tokenId);
|
||||
assert e <=> !lastReverted;
|
||||
assert e => owner == unsafeOwnerOf(tokenId); // notMintedUnset tells us this is non-zero
|
||||
|
||||
address approved = getApproved@withrevert(tokenId);
|
||||
assert e <=> !lastReverted;
|
||||
assert e => approved == unsafeGetApproved(tokenId);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule unsafeDontRevert(uint256 tokenId) {
|
||||
unsafeOwnerOf@withrevert(tokenId);
|
||||
assert !lastReverted;
|
||||
|
||||
unsafeGetApproved@withrevert(tokenId);
|
||||
assert !lastReverted;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: balance of address(0) is 0 │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule zeroAddressBalanceRevert() {
|
||||
balanceOf@withrevert(0);
|
||||
assert lastReverted;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: total supply can only change through mint and burn │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule supplyChange(env e) {
|
||||
uint256 supplyBefore = ownedTotal();
|
||||
method f; calldataarg args; f(e, args);
|
||||
uint256 supplyAfter = ownedTotal();
|
||||
|
||||
assert supplyAfter > supplyBefore => (
|
||||
supplyAfter == supplyBefore + 1 &&
|
||||
(
|
||||
f.selector == mint(address,uint256).selector ||
|
||||
f.selector == safeMint(address,uint256).selector ||
|
||||
f.selector == safeMint(address,uint256,bytes).selector
|
||||
)
|
||||
);
|
||||
assert supplyAfter < supplyBefore => (
|
||||
supplyAfter == supplyBefore - 1 &&
|
||||
f.selector == burn(uint256).selector
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule balanceChange(env e, address account) {
|
||||
requireInvariant balanceOfConsistency(account);
|
||||
require balanceLimited(account);
|
||||
|
||||
uint256 balanceBefore = balanceOf(account);
|
||||
method f; calldataarg args; f(e, args);
|
||||
uint256 balanceAfter = balanceOf(account);
|
||||
|
||||
// balance can change by at most 1
|
||||
assert balanceBefore != balanceAfter => (
|
||||
balanceAfter == balanceBefore - 1 ||
|
||||
balanceAfter == balanceBefore + 1
|
||||
);
|
||||
|
||||
// only selected function can change balances
|
||||
assert balanceBefore != balanceAfter => (
|
||||
f.selector == transferFrom(address,address,uint256).selector ||
|
||||
f.selector == safeTransferFrom(address,address,uint256).selector ||
|
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector ||
|
||||
f.selector == mint(address,uint256).selector ||
|
||||
f.selector == safeMint(address,uint256).selector ||
|
||||
f.selector == safeMint(address,uint256,bytes).selector ||
|
||||
f.selector == burn(uint256).selector
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: ownership can only change through mint, burn or transfers. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule ownershipChange(env e, uint256 tokenId) {
|
||||
address ownerBefore = unsafeOwnerOf(tokenId);
|
||||
method f; calldataarg args; f(e, args);
|
||||
address ownerAfter = unsafeOwnerOf(tokenId);
|
||||
|
||||
assert ownerBefore == 0 && ownerAfter != 0 => (
|
||||
f.selector == mint(address,uint256).selector ||
|
||||
f.selector == safeMint(address,uint256).selector ||
|
||||
f.selector == safeMint(address,uint256,bytes).selector
|
||||
);
|
||||
|
||||
assert ownerBefore != 0 && ownerAfter == 0 => (
|
||||
f.selector == burn(uint256).selector
|
||||
);
|
||||
|
||||
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
|
||||
f.selector == transferFrom(address,address,uint256).selector ||
|
||||
f.selector == safeTransferFrom(address,address,uint256).selector ||
|
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: token approval can only change through approve or transfers (implicitly). │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule approvalChange(env e, uint256 tokenId) {
|
||||
address approvalBefore = unsafeGetApproved(tokenId);
|
||||
method f; calldataarg args; f(e, args);
|
||||
address approvalAfter = unsafeGetApproved(tokenId);
|
||||
|
||||
// approve can set any value, other functions reset
|
||||
assert approvalBefore != approvalAfter => (
|
||||
f.selector == approve(address,uint256).selector ||
|
||||
(
|
||||
(
|
||||
f.selector == transferFrom(address,address,uint256).selector ||
|
||||
f.selector == safeTransferFrom(address,address,uint256).selector ||
|
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector ||
|
||||
f.selector == burn(uint256).selector
|
||||
) && approvalAfter == 0
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: approval for all tokens can only change through isApprovedForAll. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule approvedForAllChange(env e, address owner, address spender) {
|
||||
bool approvedForAllBefore = isApprovedForAll(owner, spender);
|
||||
method f; calldataarg args; f(e, args);
|
||||
bool approvedForAllAfter = isApprovedForAll(owner, spender);
|
||||
|
||||
assert approvedForAllBefore != approvedForAllAfter => f.selector == setApprovalForAll(address,bool).selector;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: transferFrom behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule transferFrom(env e, address from, address to, uint256 tokenId) {
|
||||
require nonpayable(e);
|
||||
|
||||
address operator = e.msg.sender;
|
||||
uint256 otherTokenId;
|
||||
address otherAccount;
|
||||
|
||||
requireInvariant ownerHasBalance(tokenId);
|
||||
require balanceLimited(to);
|
||||
|
||||
uint256 balanceOfFromBefore = balanceOf(from);
|
||||
uint256 balanceOfToBefore = balanceOf(to);
|
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
|
||||
address ownerBefore = unsafeOwnerOf(tokenId);
|
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
|
||||
address approvalBefore = unsafeGetApproved(tokenId);
|
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId);
|
||||
|
||||
transferFrom@withrevert(e, from, to, tokenId);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
from == ownerBefore &&
|
||||
from != 0 &&
|
||||
to != 0 &&
|
||||
(operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => (
|
||||
balanceOf(from) == balanceOfFromBefore - to_uint256(from != to ? 1 : 0) &&
|
||||
balanceOf(to) == balanceOfToBefore + to_uint256(from != to ? 1 : 0) &&
|
||||
unsafeOwnerOf(tokenId) == to &&
|
||||
unsafeGetApproved(tokenId) == 0
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
|
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
|
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: safeTransferFrom behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
|
||||
f.selector == safeTransferFrom(address,address,uint256).selector ||
|
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector
|
||||
} {
|
||||
require nonpayable(e);
|
||||
|
||||
address operator = e.msg.sender;
|
||||
uint256 otherTokenId;
|
||||
address otherAccount;
|
||||
|
||||
requireInvariant ownerHasBalance(tokenId);
|
||||
require balanceLimited(to);
|
||||
|
||||
uint256 balanceOfFromBefore = balanceOf(from);
|
||||
uint256 balanceOfToBefore = balanceOf(to);
|
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
|
||||
address ownerBefore = unsafeOwnerOf(tokenId);
|
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
|
||||
address approvalBefore = unsafeGetApproved(tokenId);
|
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId);
|
||||
|
||||
helperTransferWithRevert(e, f, from, to, tokenId);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> (
|
||||
from == ownerBefore &&
|
||||
from != 0 &&
|
||||
to != 0 &&
|
||||
(operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => (
|
||||
balanceOf(from) == balanceOfFromBefore - to_uint256(from != to ? 1: 0) &&
|
||||
balanceOf(to) == balanceOfToBefore + to_uint256(from != to ? 1: 0) &&
|
||||
unsafeOwnerOf(tokenId) == to &&
|
||||
unsafeGetApproved(tokenId) == 0
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
|
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
|
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: mint behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule mint(env e, address to, uint256 tokenId) {
|
||||
require nonpayable(e);
|
||||
requireInvariant notMintedUnset(tokenId);
|
||||
|
||||
uint256 otherTokenId;
|
||||
address otherAccount;
|
||||
|
||||
require balanceLimited(to);
|
||||
|
||||
uint256 supplyBefore = ownedTotal();
|
||||
uint256 balanceOfToBefore = balanceOf(to);
|
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
|
||||
address ownerBefore = unsafeOwnerOf(tokenId);
|
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
|
||||
|
||||
mint@withrevert(e, to, tokenId);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
ownerBefore == 0 &&
|
||||
to != 0
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => (
|
||||
ownedTotal() == supplyBefore + 1 &&
|
||||
balanceOf(to) == balanceOfToBefore + 1 &&
|
||||
unsafeOwnerOf(tokenId) == to
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to;
|
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: safeMint behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
|
||||
f.selector == safeMint(address,uint256).selector ||
|
||||
f.selector == safeMint(address,uint256,bytes).selector
|
||||
} {
|
||||
require nonpayable(e);
|
||||
requireInvariant notMintedUnset(tokenId);
|
||||
|
||||
uint256 otherTokenId;
|
||||
address otherAccount;
|
||||
|
||||
require balanceLimited(to);
|
||||
|
||||
uint256 supplyBefore = ownedTotal();
|
||||
uint256 balanceOfToBefore = balanceOf(to);
|
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
|
||||
address ownerBefore = unsafeOwnerOf(tokenId);
|
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
|
||||
|
||||
helperMintWithRevert(e, f, to, tokenId);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> (
|
||||
ownerBefore == 0 &&
|
||||
to != 0
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => (
|
||||
ownedTotal() == supplyBefore + 1 &&
|
||||
balanceOf(to) == balanceOfToBefore + 1 &&
|
||||
unsafeOwnerOf(tokenId) == to
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to;
|
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: burn behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule burn(env e, uint256 tokenId) {
|
||||
require nonpayable(e);
|
||||
|
||||
address from = unsafeOwnerOf(tokenId);
|
||||
uint256 otherTokenId;
|
||||
address otherAccount;
|
||||
|
||||
requireInvariant ownerHasBalance(tokenId);
|
||||
|
||||
uint256 supplyBefore = ownedTotal();
|
||||
uint256 balanceOfFromBefore = balanceOf(from);
|
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
|
||||
address ownerBefore = unsafeOwnerOf(tokenId);
|
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
|
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId);
|
||||
|
||||
burn@withrevert(e, tokenId);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
ownerBefore != 0
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => (
|
||||
ownedTotal() == supplyBefore - 1 &&
|
||||
balanceOf(from) == balanceOfFromBefore - 1 &&
|
||||
unsafeOwnerOf(tokenId) == 0 &&
|
||||
unsafeGetApproved(tokenId) == 0
|
||||
);
|
||||
|
||||
// no side effect
|
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == from;
|
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
|
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: approve behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule approve(env e, address spender, uint256 tokenId) {
|
||||
require nonpayable(e);
|
||||
|
||||
address caller = e.msg.sender;
|
||||
address owner = unsafeOwnerOf(tokenId);
|
||||
uint256 otherTokenId;
|
||||
|
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId);
|
||||
|
||||
approve@withrevert(e, spender, tokenId);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
owner != 0 &&
|
||||
owner != spender &&
|
||||
(owner == caller || isApprovedForAll(owner, caller))
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => unsafeGetApproved(tokenId) == spender;
|
||||
|
||||
// no side effect
|
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: setApprovalForAll behavior and side effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule setApprovalForAll(env e, address operator, bool approved) {
|
||||
require nonpayable(e);
|
||||
|
||||
address owner = e.msg.sender;
|
||||
address otherOwner;
|
||||
address otherOperator;
|
||||
|
||||
bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);
|
||||
|
||||
setApprovalForAll@withrevert(e, operator, approved);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> owner != operator;
|
||||
|
||||
// effect
|
||||
assert success => isApprovedForAll(owner, operator) == approved;
|
||||
|
||||
// no side effect
|
||||
assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
|
||||
otherOwner == owner &&
|
||||
otherOperator == operator
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,334 @@
|
||||
import "helpers/helpers.spec"
|
||||
|
||||
methods {
|
||||
// library
|
||||
set(bytes32,bytes32) returns (bool) envfree
|
||||
remove(bytes32) returns (bool) envfree
|
||||
contains(bytes32) returns (bool) envfree
|
||||
length() returns (uint256) envfree
|
||||
key_at(uint256) returns (bytes32) envfree
|
||||
value_at(uint256) returns (bytes32) envfree
|
||||
tryGet_contains(bytes32) returns (bool) envfree
|
||||
tryGet_value(bytes32) returns (bytes32) envfree
|
||||
get(bytes32) returns (bytes32) envfree
|
||||
|
||||
// FV
|
||||
_indexOf(bytes32) returns (uint256) envfree
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Helpers │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
function sanity() returns bool {
|
||||
return length() < max_uint256;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: the value mapping is empty for keys that are not in the EnumerableMap. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant noValueIfNotContained(bytes32 key)
|
||||
!contains(key) => tryGet_value(key) == 0
|
||||
{
|
||||
preserved set(bytes32 otherKey, bytes32 someValue) {
|
||||
require sanity();
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: All indexed keys are contained │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant indexedContained(uint256 index)
|
||||
index < length() => contains(key_at(index))
|
||||
{
|
||||
preserved {
|
||||
requireInvariant consistencyIndex(index);
|
||||
requireInvariant consistencyIndex(to_uint256(length() - 1));
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: A value can only be stored at a single location │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant atUniqueness(uint256 index1, uint256 index2)
|
||||
index1 == index2 <=> key_at(index1) == key_at(index2)
|
||||
{
|
||||
preserved remove(bytes32 key) {
|
||||
requireInvariant atUniqueness(index1, to_uint256(length() - 1));
|
||||
requireInvariant atUniqueness(index2, to_uint256(length() - 1));
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: index <> value relationship is consistent │
|
||||
│ │
|
||||
│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another. │
|
||||
│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are set │
|
||||
│ and removed from the EnumerableMap). │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant consistencyIndex(uint256 index)
|
||||
index < length() => _indexOf(key_at(index)) == index + 1
|
||||
{
|
||||
preserved remove(bytes32 key) {
|
||||
requireInvariant consistencyIndex(to_uint256(length() - 1));
|
||||
}
|
||||
}
|
||||
|
||||
invariant consistencyKey(bytes32 key)
|
||||
contains(key) => (
|
||||
_indexOf(key) > 0 &&
|
||||
_indexOf(key) <= length() &&
|
||||
key_at(to_uint256(_indexOf(key) - 1)) == key
|
||||
)
|
||||
{
|
||||
preserved remove(bytes32 otherKey) {
|
||||
requireInvariant consistencyKey(otherKey);
|
||||
requireInvariant atUniqueness(
|
||||
to_uint256(_indexOf(key) - 1),
|
||||
to_uint256(_indexOf(otherKey) - 1)
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: state only changes by setting or removing elements │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule stateChange(env e, bytes32 key) {
|
||||
require sanity();
|
||||
requireInvariant consistencyKey(key);
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bool containsBefore = contains(key);
|
||||
bytes32 valueBefore = tryGet_value(key);
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
f(e, args);
|
||||
|
||||
uint256 lengthAfter = length();
|
||||
bool containsAfter = contains(key);
|
||||
bytes32 valueAfter = tryGet_value(key);
|
||||
|
||||
assert lengthBefore != lengthAfter => (
|
||||
(f.selector == set(bytes32,bytes32).selector && lengthAfter == lengthBefore + 1) ||
|
||||
(f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1)
|
||||
);
|
||||
|
||||
assert containsBefore != containsAfter => (
|
||||
(f.selector == set(bytes32,bytes32).selector && containsAfter) ||
|
||||
(f.selector == remove(bytes32).selector && !containsAfter)
|
||||
);
|
||||
|
||||
assert valueBefore != valueAfter => (
|
||||
(f.selector == set(bytes32,bytes32).selector && containsAfter) ||
|
||||
(f.selector == remove(bytes32).selector && !containsAfter && valueAfter == 0)
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: check liveness of view functions. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule liveness_1(bytes32 key) {
|
||||
requireInvariant consistencyKey(key);
|
||||
|
||||
// contains never revert
|
||||
bool contains = contains@withrevert(key);
|
||||
assert !lastReverted;
|
||||
|
||||
// tryGet never reverts (key)
|
||||
tryGet_contains@withrevert(key);
|
||||
assert !lastReverted;
|
||||
|
||||
// tryGet never reverts (value)
|
||||
tryGet_value@withrevert(key);
|
||||
assert !lastReverted;
|
||||
|
||||
// get reverts iff the key is not in the map
|
||||
get@withrevert(key);
|
||||
assert !lastReverted <=> contains;
|
||||
}
|
||||
|
||||
rule liveness_2(uint256 index) {
|
||||
requireInvariant consistencyIndex(index);
|
||||
|
||||
// length never revert
|
||||
uint256 length = length@withrevert();
|
||||
assert !lastReverted;
|
||||
|
||||
// key_at reverts iff the index is out of bound
|
||||
key_at@withrevert(index);
|
||||
assert !lastReverted <=> index < length;
|
||||
|
||||
// value_at reverts iff the index is out of bound
|
||||
value_at@withrevert(index);
|
||||
assert !lastReverted <=> index < length;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: get and tryGet return the expected values. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule getAndTryGet(bytes32 key) {
|
||||
requireInvariant noValueIfNotContained(key);
|
||||
|
||||
bool contained = contains(key);
|
||||
bool tryContained = tryGet_contains(key);
|
||||
bytes32 tryValue = tryGet_value(key);
|
||||
bytes32 value = get@withrevert(key); // revert is not contained
|
||||
|
||||
assert contained == tryContained;
|
||||
assert contained => tryValue == value;
|
||||
assert !contained => tryValue == 0;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: set key-value in EnumerableMap │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule set(bytes32 key, bytes32 value, bytes32 otherKey) {
|
||||
require sanity();
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bool containsBefore = contains(key);
|
||||
bool containsOtherBefore = contains(otherKey);
|
||||
bytes32 otherValueBefore = tryGet_value(otherKey);
|
||||
|
||||
bool added = set@withrevert(key, value);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success && contains(key) && get(key) == value,
|
||||
"liveness & immediate effect";
|
||||
|
||||
assert added <=> !containsBefore,
|
||||
"return value: added iff not contained";
|
||||
|
||||
assert length() == lengthBefore + to_mathint(added ? 1 : 0),
|
||||
"effect: length increases iff added";
|
||||
|
||||
assert added => (key_at(lengthBefore) == key && value_at(lengthBefore) == value),
|
||||
"effect: add at the end";
|
||||
|
||||
assert containsOtherBefore != contains(otherKey) => (added && key == otherKey),
|
||||
"side effect: other keys are not affected";
|
||||
|
||||
assert otherValueBefore != tryGet_value(otherKey) => key == otherKey,
|
||||
"side effect: values attached to other keys are not affected";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: remove key from EnumerableMap │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule remove(bytes32 key, bytes32 otherKey) {
|
||||
requireInvariant consistencyKey(key);
|
||||
requireInvariant consistencyKey(otherKey);
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bool containsBefore = contains(key);
|
||||
bool containsOtherBefore = contains(otherKey);
|
||||
bytes32 otherValueBefore = tryGet_value(otherKey);
|
||||
|
||||
bool removed = remove@withrevert(key);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success && !contains(key),
|
||||
"liveness & immediate effect";
|
||||
|
||||
assert removed <=> containsBefore,
|
||||
"return value: removed iff contained";
|
||||
|
||||
assert length() == lengthBefore - to_mathint(removed ? 1 : 0),
|
||||
"effect: length decreases iff removed";
|
||||
|
||||
assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey),
|
||||
"side effect: other keys are not affected";
|
||||
|
||||
assert otherValueBefore != tryGet_value(otherKey) => key == otherKey,
|
||||
"side effect: values attached to other keys are not affected";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: when adding a new key, the other keys remain in set, at the same index. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule setEnumerability(bytes32 key, bytes32 value, uint256 index) {
|
||||
require sanity();
|
||||
|
||||
bytes32 atKeyBefore = key_at(index);
|
||||
bytes32 atValueBefore = value_at(index);
|
||||
|
||||
set(key, value);
|
||||
|
||||
bytes32 atKeyAfter = key_at@withrevert(index);
|
||||
assert !lastReverted;
|
||||
|
||||
bytes32 atValueAfter = value_at@withrevert(index);
|
||||
assert !lastReverted;
|
||||
|
||||
assert atKeyAfter == atKeyBefore;
|
||||
assert atValueAfter != atValueBefore => (
|
||||
key == atKeyBefore &&
|
||||
value == atValueAfter
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: when removing a existing key, the other keys remain in set, at the same index (except for the last one). │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule removeEnumerability(bytes32 key, uint256 index) {
|
||||
uint256 last = length() - 1;
|
||||
|
||||
requireInvariant consistencyKey(key);
|
||||
requireInvariant consistencyIndex(index);
|
||||
requireInvariant consistencyIndex(last);
|
||||
|
||||
bytes32 atKeyBefore = key_at(index);
|
||||
bytes32 atValueBefore = value_at(index);
|
||||
bytes32 lastKeyBefore = key_at(last);
|
||||
bytes32 lastValueBefore = value_at(last);
|
||||
|
||||
remove(key);
|
||||
|
||||
// can't read last value & keys (length decreased)
|
||||
bytes32 atKeyAfter = key_at@withrevert(index);
|
||||
assert lastReverted <=> index == last;
|
||||
|
||||
bytes32 atValueAfter = value_at@withrevert(index);
|
||||
assert lastReverted <=> index == last;
|
||||
|
||||
// One value that is allowed to change is if previous value was removed,
|
||||
// in that case the last value before took its place.
|
||||
assert (
|
||||
index != last &&
|
||||
atKeyBefore != atKeyAfter
|
||||
) => (
|
||||
atKeyBefore == key &&
|
||||
atKeyAfter == lastKeyBefore
|
||||
);
|
||||
|
||||
assert (
|
||||
index != last &&
|
||||
atValueBefore != atValueAfter
|
||||
) => (
|
||||
atValueAfter == lastValueBefore
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,247 @@
|
||||
import "helpers/helpers.spec"
|
||||
|
||||
methods {
|
||||
// library
|
||||
add(bytes32) returns (bool) envfree
|
||||
remove(bytes32) returns (bool) envfree
|
||||
contains(bytes32) returns (bool) envfree
|
||||
length() returns (uint256) envfree
|
||||
at_(uint256) returns (bytes32) envfree
|
||||
|
||||
// FV
|
||||
_indexOf(bytes32) returns (uint256) envfree
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Helpers │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
function sanity() returns bool {
|
||||
return length() < max_uint256;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: All indexed keys are contained │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant indexedContained(uint256 index)
|
||||
index < length() => contains(at_(index))
|
||||
{
|
||||
preserved {
|
||||
requireInvariant consistencyIndex(index);
|
||||
requireInvariant consistencyIndex(to_uint256(length() - 1));
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: A value can only be stored at a single location │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant atUniqueness(uint256 index1, uint256 index2)
|
||||
index1 == index2 <=> at_(index1) == at_(index2)
|
||||
{
|
||||
preserved remove(bytes32 key) {
|
||||
requireInvariant atUniqueness(index1, to_uint256(length() - 1));
|
||||
requireInvariant atUniqueness(index2, to_uint256(length() - 1));
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: index <> key relationship is consistent │
|
||||
│ │
|
||||
│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another. │
|
||||
│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are added │
|
||||
│ and removed from the EnumerableSet). │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant consistencyIndex(uint256 index)
|
||||
index < length() => _indexOf(at_(index)) == index + 1
|
||||
{
|
||||
preserved remove(bytes32 key) {
|
||||
requireInvariant consistencyIndex(to_uint256(length() - 1));
|
||||
}
|
||||
}
|
||||
|
||||
invariant consistencyKey(bytes32 key)
|
||||
contains(key) => (
|
||||
_indexOf(key) > 0 &&
|
||||
_indexOf(key) <= length() &&
|
||||
at_(to_uint256(_indexOf(key) - 1)) == key
|
||||
)
|
||||
{
|
||||
preserved remove(bytes32 otherKey) {
|
||||
requireInvariant consistencyKey(otherKey);
|
||||
requireInvariant atUniqueness(
|
||||
to_uint256(_indexOf(key) - 1),
|
||||
to_uint256(_indexOf(otherKey) - 1)
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: state only changes by adding or removing elements │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule stateChange(env e, bytes32 key) {
|
||||
require sanity();
|
||||
requireInvariant consistencyKey(key);
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bool containsBefore = contains(key);
|
||||
|
||||
method f;
|
||||
calldataarg args;
|
||||
f(e, args);
|
||||
|
||||
uint256 lengthAfter = length();
|
||||
bool containsAfter = contains(key);
|
||||
|
||||
assert lengthBefore != lengthAfter => (
|
||||
(f.selector == add(bytes32).selector && lengthAfter == lengthBefore + 1) ||
|
||||
(f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1)
|
||||
);
|
||||
|
||||
assert containsBefore != containsAfter => (
|
||||
(f.selector == add(bytes32).selector && containsAfter) ||
|
||||
(f.selector == remove(bytes32).selector && containsBefore)
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: check liveness of view functions. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule liveness_1(bytes32 key) {
|
||||
requireInvariant consistencyKey(key);
|
||||
|
||||
// contains never revert
|
||||
contains@withrevert(key);
|
||||
assert !lastReverted;
|
||||
}
|
||||
|
||||
rule liveness_2(uint256 index) {
|
||||
requireInvariant consistencyIndex(index);
|
||||
|
||||
// length never revert
|
||||
uint256 length = length@withrevert();
|
||||
assert !lastReverted;
|
||||
|
||||
// at reverts iff the index is out of bound
|
||||
at_@withrevert(index);
|
||||
assert !lastReverted <=> index < length;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: add key to EnumerableSet if not already contained │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule add(bytes32 key, bytes32 otherKey) {
|
||||
require sanity();
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bool containsBefore = contains(key);
|
||||
bool containsOtherBefore = contains(otherKey);
|
||||
|
||||
bool added = add@withrevert(key);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success && contains(key),
|
||||
"liveness & immediate effect";
|
||||
|
||||
assert added <=> !containsBefore,
|
||||
"return value: added iff not contained";
|
||||
|
||||
assert length() == lengthBefore + to_mathint(added ? 1 : 0),
|
||||
"effect: length increases iff added";
|
||||
|
||||
assert added => at_(lengthBefore) == key,
|
||||
"effect: add at the end";
|
||||
|
||||
assert containsOtherBefore != contains(otherKey) => (added && key == otherKey),
|
||||
"side effect: other keys are not affected";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: remove key from EnumerableSet if already contained │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule remove(bytes32 key, bytes32 otherKey) {
|
||||
requireInvariant consistencyKey(key);
|
||||
requireInvariant consistencyKey(otherKey);
|
||||
|
||||
uint256 lengthBefore = length();
|
||||
bool containsBefore = contains(key);
|
||||
bool containsOtherBefore = contains(otherKey);
|
||||
|
||||
bool removed = remove@withrevert(key);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success && !contains(key),
|
||||
"liveness & immediate effect";
|
||||
|
||||
assert removed <=> containsBefore,
|
||||
"return value: removed iff contained";
|
||||
|
||||
assert length() == lengthBefore - to_mathint(removed ? 1 : 0),
|
||||
"effect: length decreases iff removed";
|
||||
|
||||
assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey),
|
||||
"side effect: other keys are not affected";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: when adding a new key, the other keys remain in set, at the same index. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule addEnumerability(bytes32 key, uint256 index) {
|
||||
require sanity();
|
||||
|
||||
bytes32 atBefore = at_(index);
|
||||
add(key);
|
||||
bytes32 atAfter = at_@withrevert(index);
|
||||
bool atAfterSuccess = !lastReverted;
|
||||
|
||||
assert atAfterSuccess;
|
||||
assert atBefore == atAfter;
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: when removing a existing key, the other keys remain in set, at the same index (except for the last one). │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule removeEnumerability(bytes32 key, uint256 index) {
|
||||
uint256 last = length() - 1;
|
||||
|
||||
requireInvariant consistencyKey(key);
|
||||
requireInvariant consistencyIndex(index);
|
||||
requireInvariant consistencyIndex(last);
|
||||
|
||||
bytes32 atBefore = at_(index);
|
||||
bytes32 lastBefore = at_(last);
|
||||
|
||||
remove(key);
|
||||
|
||||
// can't read last value (length decreased)
|
||||
bytes32 atAfter = at_@withrevert(index);
|
||||
assert lastReverted <=> index == last;
|
||||
|
||||
// One value that is allowed to change is if previous value was removed,
|
||||
// in that case the last value before took its place.
|
||||
assert (
|
||||
index != last &&
|
||||
atBefore != atAfter
|
||||
) => (
|
||||
atBefore == key &&
|
||||
atAfter == lastBefore
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,165 @@
|
||||
import "helpers/helpers.spec"
|
||||
|
||||
methods {
|
||||
// initialize, reinitialize, disable
|
||||
initialize() envfree
|
||||
reinitialize(uint8) envfree
|
||||
disable() envfree
|
||||
|
||||
nested_init_init() envfree
|
||||
nested_init_reinit(uint8) envfree
|
||||
nested_reinit_init(uint8) envfree
|
||||
nested_reinit_reinit(uint8,uint8) envfree
|
||||
|
||||
// view
|
||||
version() returns uint8 envfree
|
||||
initializing() returns bool envfree
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Definitions │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
definition isUninitialized() returns bool = version() == 0;
|
||||
definition isInitialized() returns bool = version() > 0;
|
||||
definition isDisabled() returns bool = version() == 255;
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: A contract must only ever be in an initializing state while in the middle of a transaction execution. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant notInitializing()
|
||||
!initializing()
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: The version cannot decrease & disable state is irrevocable. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule increasingVersion(env e) {
|
||||
uint8 versionBefore = version();
|
||||
bool disabledBefore = isDisabled();
|
||||
|
||||
method f; calldataarg args;
|
||||
f(e, args);
|
||||
|
||||
assert versionBefore <= version(), "_initialized must only increase";
|
||||
assert disabledBefore => isDisabled(), "a disabled initializer must stay disabled";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: Cannot initialize a contract that is already initialized. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule cannotInitializeTwice() {
|
||||
require isInitialized();
|
||||
|
||||
initialize@withrevert();
|
||||
|
||||
assert lastReverted, "contract must only be initialized once";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: Cannot initialize once disabled. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule cannotInitializeOnceDisabled() {
|
||||
require isDisabled();
|
||||
|
||||
initialize@withrevert();
|
||||
|
||||
assert lastReverted, "contract is disabled";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: Cannot reinitialize once disabled. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule cannotReinitializeOnceDisabled() {
|
||||
require isDisabled();
|
||||
|
||||
uint8 n;
|
||||
reinitialize@withrevert(n);
|
||||
|
||||
assert lastReverted, "contract is disabled";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: Cannot nest initializers (after construction). │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule cannotNestInitializers_init_init() {
|
||||
nested_init_init@withrevert();
|
||||
assert lastReverted, "nested initializers";
|
||||
}
|
||||
|
||||
rule cannotNestInitializers_init_reinit(uint8 m) {
|
||||
nested_init_reinit@withrevert(m);
|
||||
assert lastReverted, "nested initializers";
|
||||
}
|
||||
|
||||
rule cannotNestInitializers_reinit_init(uint8 n) {
|
||||
nested_reinit_init@withrevert(n);
|
||||
assert lastReverted, "nested initializers";
|
||||
}
|
||||
|
||||
rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) {
|
||||
nested_reinit_reinit@withrevert(n, m);
|
||||
assert lastReverted, "nested initializers";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: Initialize correctly sets the version. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule initializeEffects() {
|
||||
requireInvariant notInitializing();
|
||||
|
||||
bool isUninitializedBefore = isUninitialized();
|
||||
|
||||
initialize@withrevert();
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts";
|
||||
assert success => version() == 1, "initialize must set version() to 1";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: Reinitialize correctly sets the version. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule reinitializeEffects() {
|
||||
requireInvariant notInitializing();
|
||||
|
||||
uint8 versionBefore = version();
|
||||
|
||||
uint8 n;
|
||||
reinitialize@withrevert(n);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> versionBefore < n, "can only reinitialize to a latter versions";
|
||||
assert success => version() == n, "reinitialize must set version() to n";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: Can disable. │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule disableEffect() {
|
||||
requireInvariant notInitializing();
|
||||
|
||||
disable@withrevert();
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success, "call to _disableInitializers failed";
|
||||
assert isDisabled(), "disable state not set";
|
||||
}
|
||||
@@ -0,0 +1,78 @@
|
||||
import "helpers/helpers.spec"
|
||||
import "methods/IOwnable.spec"
|
||||
|
||||
methods {
|
||||
restricted()
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: transferOwnership changes ownership │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule transferOwnership(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address newOwner;
|
||||
address current = owner();
|
||||
|
||||
transferOwnership@withrevert(e, newOwner);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
|
||||
assert success => owner() == newOwner, "current owner changed";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: renounceOwnership removes the owner │
|
||||
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule renounceOwnership(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address current = owner();
|
||||
|
||||
renounceOwnership@withrevert(e);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> e.msg.sender == current, "unauthorized caller";
|
||||
assert success => owner() == 0, "owner not cleared";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Access control: only current owner can call restricted functions │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address current = owner();
|
||||
|
||||
calldataarg args;
|
||||
restricted@withrevert(e, args);
|
||||
|
||||
assert !lastReverted <=> e.msg.sender == current, "access control failed";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: ownership can only change in specific ways │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
|
||||
address oldCurrent = owner();
|
||||
|
||||
method f; calldataarg args;
|
||||
f(e, args);
|
||||
|
||||
address newCurrent = owner();
|
||||
|
||||
// If owner changes, must be either transferOwnership or renounceOwnership
|
||||
assert oldCurrent != newCurrent => (
|
||||
(e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == transferOwnership(address).selector) ||
|
||||
(e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == renounceOwnership().selector)
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,108 @@
|
||||
import "helpers/helpers.spec"
|
||||
import "methods/IOwnable2Step.spec"
|
||||
|
||||
methods {
|
||||
restricted()
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: transferOwnership sets the pending owner │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule transferOwnership(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address newOwner;
|
||||
address current = owner();
|
||||
|
||||
transferOwnership@withrevert(e, newOwner);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> e.msg.sender == current, "unauthorized caller";
|
||||
assert success => pendingOwner() == newOwner, "pending owner not set";
|
||||
assert success => owner() == current, "current owner changed";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: renounceOwnership removes the owner and the pendingOwner │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule renounceOwnership(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address current = owner();
|
||||
|
||||
renounceOwnership@withrevert(e);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> e.msg.sender == current, "unauthorized caller";
|
||||
assert success => pendingOwner() == 0, "pending owner not cleared";
|
||||
assert success => owner() == 0, "owner not cleared";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: acceptOwnership changes owner and reset pending owner │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule acceptOwnership(env e) {
|
||||
|
||||
require nonpayable(e);
|
||||
|
||||
address current = owner();
|
||||
address pending = pendingOwner();
|
||||
|
||||
acceptOwnership@withrevert(e);
|
||||
bool success = !lastReverted;
|
||||
|
||||
assert success <=> e.msg.sender == pending, "unauthorized caller";
|
||||
assert success => pendingOwner() == 0, "pending owner not cleared";
|
||||
assert success => owner() == pending, "owner not transferred";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Access control: only current owner can call restricted functions │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
address current = owner();
|
||||
|
||||
calldataarg args;
|
||||
restricted@withrevert(e, args);
|
||||
|
||||
assert !lastReverted <=> e.msg.sender == current, "access control failed";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: ownership and pending ownership can only change in specific ways │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule ownerOrPendingOwnerChange(env e, method f) {
|
||||
address oldCurrent = owner();
|
||||
address oldPending = pendingOwner();
|
||||
|
||||
calldataarg args;
|
||||
f(e, args);
|
||||
|
||||
address newCurrent = owner();
|
||||
address newPending = pendingOwner();
|
||||
|
||||
// If owner changes, must be either acceptOwnership or renounceOwnership
|
||||
assert oldCurrent != newCurrent => (
|
||||
(e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
|
||||
(e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == renounceOwnership().selector)
|
||||
);
|
||||
|
||||
// If pending changes, must be either acceptance or reset
|
||||
assert oldPending != newPending => (
|
||||
(e.msg.sender == oldCurrent && newCurrent == oldCurrent && f.selector == transferOwnership(address).selector) ||
|
||||
(e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
|
||||
(e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == renounceOwnership().selector)
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,96 @@
|
||||
import "helpers/helpers.spec"
|
||||
|
||||
methods {
|
||||
paused() returns (bool) envfree
|
||||
pause()
|
||||
unpause()
|
||||
onlyWhenPaused()
|
||||
onlyWhenNotPaused()
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: _pause pauses the contract │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule pause(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
bool pausedBefore = paused();
|
||||
|
||||
pause@withrevert(e);
|
||||
bool success = !lastReverted;
|
||||
|
||||
bool pausedAfter = paused();
|
||||
|
||||
// liveness
|
||||
assert success <=> !pausedBefore, "works if and only if the contract was not paused before";
|
||||
|
||||
// effect
|
||||
assert success => pausedAfter, "contract must be paused after a successful call";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: _unpause unpauses the contract │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule unpause(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
bool pausedBefore = paused();
|
||||
|
||||
unpause@withrevert(e);
|
||||
bool success = !lastReverted;
|
||||
|
||||
bool pausedAfter = paused();
|
||||
|
||||
// liveness
|
||||
assert success <=> pausedBefore, "works if and only if the contract was paused before";
|
||||
|
||||
// effect
|
||||
assert success => !pausedAfter, "contract must be unpaused after a successful call";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: whenPaused modifier can only be called if the contract is paused │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule whenPaused(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
onlyWhenPaused@withrevert(e);
|
||||
assert !lastReverted <=> paused(), "works if and only if the contract is paused";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule whenNotPaused(env e) {
|
||||
require nonpayable(e);
|
||||
|
||||
onlyWhenNotPaused@withrevert(e);
|
||||
assert !lastReverted <=> !paused(), "works if and only if the contract is not paused";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rules: only _pause and _unpause can change paused status │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule noPauseChange(env e) {
|
||||
method f;
|
||||
calldataarg args;
|
||||
|
||||
bool pausedBefore = paused();
|
||||
f(e, args);
|
||||
bool pausedAfter = paused();
|
||||
|
||||
assert pausedBefore != pausedAfter => (
|
||||
(!pausedAfter && f.selector == unpause().selector) ||
|
||||
(pausedAfter && f.selector == pause().selector)
|
||||
), "contract's paused status can only be changed by _pause() or _unpause()";
|
||||
}
|
||||
@@ -0,0 +1,275 @@
|
||||
import "helpers/helpers.spec"
|
||||
import "methods/IAccessControl.spec"
|
||||
|
||||
methods {
|
||||
TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree
|
||||
PROPOSER_ROLE() returns (bytes32) envfree
|
||||
EXECUTOR_ROLE() returns (bytes32) envfree
|
||||
CANCELLER_ROLE() returns (bytes32) envfree
|
||||
isOperation(bytes32) returns (bool) envfree
|
||||
isOperationPending(bytes32) returns (bool) envfree
|
||||
isOperationReady(bytes32) returns (bool)
|
||||
isOperationDone(bytes32) returns (bool) envfree
|
||||
getTimestamp(bytes32) returns (uint256) envfree
|
||||
getMinDelay() returns (uint256) envfree
|
||||
|
||||
hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree
|
||||
hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree
|
||||
|
||||
schedule(address, uint256, bytes, bytes32, bytes32, uint256)
|
||||
scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256)
|
||||
execute(address, uint256, bytes, bytes32, bytes32)
|
||||
executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
|
||||
cancel(bytes32)
|
||||
|
||||
updateDelay(uint256)
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Helpers │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
// Uniformly handle scheduling of batched and non-batched operations.
|
||||
function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
|
||||
if (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) {
|
||||
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
|
||||
require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
|
||||
schedule@withrevert(e, target, value, data, predecessor, salt, delay);
|
||||
} else if (f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) {
|
||||
address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt;
|
||||
require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
|
||||
scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay);
|
||||
} else {
|
||||
calldataarg args;
|
||||
f@withrevert(e, args);
|
||||
}
|
||||
}
|
||||
|
||||
// Uniformly handle execution of batched and non-batched operations.
|
||||
function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) {
|
||||
if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) {
|
||||
address target; uint256 value; bytes data; bytes32 salt;
|
||||
require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
|
||||
execute@withrevert(e, target, value, data, predecessor, salt);
|
||||
} else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
|
||||
address[] targets; uint256[] values; bytes[] payloads; bytes32 salt;
|
||||
require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
|
||||
executeBatch@withrevert(e, targets, values, payloads, predecessor, salt);
|
||||
} else {
|
||||
calldataarg args;
|
||||
f@withrevert(e, args);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Definitions │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
definition DONE_TIMESTAMP() returns uint256 = 1;
|
||||
definition UNSET() returns uint8 = 0x1;
|
||||
definition PENDING() returns uint8 = 0x2;
|
||||
definition DONE() returns uint8 = 0x4;
|
||||
|
||||
definition isUnset(bytes32 id) returns bool = !isOperation(id);
|
||||
definition isPending(bytes32 id) returns bool = isOperationPending(id);
|
||||
definition isDone(bytes32 id) returns bool = isOperationDone(id);
|
||||
definition state(bytes32 id) returns uint8 = (isUnset(id) ? UNSET() : 0) | (isPending(id) ? PENDING() : 0) | (isDone(id) ? DONE() : 0);
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariants: consistency of accessors │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant isOperationCheck(bytes32 id)
|
||||
isOperation(id) <=> getTimestamp(id) > 0
|
||||
filtered { f -> !f.isView }
|
||||
|
||||
invariant isOperationPendingCheck(bytes32 id)
|
||||
isOperationPending(id) <=> getTimestamp(id) > DONE_TIMESTAMP()
|
||||
filtered { f -> !f.isView }
|
||||
|
||||
invariant isOperationDoneCheck(bytes32 id)
|
||||
isOperationDone(id) <=> getTimestamp(id) == DONE_TIMESTAMP()
|
||||
filtered { f -> !f.isView }
|
||||
|
||||
invariant isOperationReadyCheck(env e, bytes32 id)
|
||||
isOperationReady(e, id) <=> (isOperationPending(id) && getTimestamp(id) <= e.block.timestamp)
|
||||
filtered { f -> !f.isView }
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Invariant: a proposal id is either unset, pending or done │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
invariant stateConsistency(bytes32 id, env e)
|
||||
// Check states are mutually exclusive
|
||||
(isUnset(id) <=> (!isPending(id) && !isDone(id) )) &&
|
||||
(isPending(id) <=> (!isUnset(id) && !isDone(id) )) &&
|
||||
(isDone(id) <=> (!isUnset(id) && !isPending(id))) &&
|
||||
// Check that the state helper behaves as expected:
|
||||
(isUnset(id) <=> state(id) == UNSET() ) &&
|
||||
(isPending(id) <=> state(id) == PENDING() ) &&
|
||||
(isDone(id) <=> state(id) == DONE() ) &&
|
||||
// Check substate
|
||||
isOperationReady(e, id) => isPending(id)
|
||||
filtered { f -> !f.isView }
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: state transition rules │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule stateTransition(bytes32 id, env e, method f, calldataarg args) {
|
||||
require e.block.timestamp > 1; // Sanity
|
||||
|
||||
uint8 stateBefore = state(id);
|
||||
f(e, args);
|
||||
uint8 stateAfter = state(id);
|
||||
|
||||
// Cannot jump from UNSET to DONE
|
||||
assert stateBefore == UNSET() => stateAfter != DONE();
|
||||
|
||||
// UNSET → PENDING: schedule or scheduleBatch
|
||||
assert stateBefore == UNSET() && stateAfter == PENDING() => (
|
||||
f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
|
||||
f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
|
||||
);
|
||||
|
||||
// PENDING → UNSET: cancel
|
||||
assert stateBefore == PENDING() && stateAfter == UNSET() => (
|
||||
f.selector == cancel(bytes32).selector
|
||||
);
|
||||
|
||||
// PENDING → DONE: execute or executeBatch
|
||||
assert stateBefore == PENDING() && stateAfter == DONE() => (
|
||||
f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector ||
|
||||
f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
|
||||
);
|
||||
|
||||
// DONE is final
|
||||
assert stateBefore == DONE() => stateAfter == DONE();
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: minimum delay can only be updated through a timelock execution │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule minDelayOnlyChange(env e) {
|
||||
uint256 delayBefore = getMinDelay();
|
||||
|
||||
method f; calldataarg args;
|
||||
f(e, args);
|
||||
|
||||
assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == updateDelay(uint256).selector), "Unauthorized delay update";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: schedule liveness and effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
|
||||
f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
|
||||
f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
|
||||
} {
|
||||
require nonpayable(e);
|
||||
|
||||
// Basic timestamp assumptions
|
||||
require e.block.timestamp > 1;
|
||||
require e.block.timestamp + delay < max_uint256;
|
||||
require e.block.timestamp + getMinDelay() < max_uint256;
|
||||
|
||||
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
|
||||
|
||||
uint8 stateBefore = state(id);
|
||||
bool isDelaySufficient = delay >= getMinDelay();
|
||||
bool isProposerBefore = hasRole(PROPOSER_ROLE(), e.msg.sender);
|
||||
|
||||
helperScheduleWithRevert(e, f, id, delay);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
stateBefore == UNSET() &&
|
||||
isDelaySufficient &&
|
||||
isProposerBefore
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => state(id) == PENDING(), "State transition violation";
|
||||
assert success => getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set";
|
||||
|
||||
// no side effect
|
||||
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: execute liveness and effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
|
||||
f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector ||
|
||||
f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
|
||||
} {
|
||||
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
|
||||
|
||||
uint8 stateBefore = state(id);
|
||||
bool isOperationReadyBefore = isOperationReady(e, id);
|
||||
bool isExecutorOrOpen = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0);
|
||||
bool predecessorDependency = predecessor == 0 || isDone(predecessor);
|
||||
|
||||
helperExecuteWithRevert(e, f, id, predecessor);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// The underlying transaction can revert, and that would cause the execution to revert. We can check that all non
|
||||
// reverting calls meet the requirements in terms of proposal readiness, access control and predecessor dependency.
|
||||
// We can't however guarantee that these requirements being meet ensure liveness of the proposal, because the
|
||||
// proposal can revert for reasons beyond our control.
|
||||
|
||||
// liveness, should be `<=>` but can only check `=>` (see comment above)
|
||||
assert success => (
|
||||
stateBefore == PENDING() &&
|
||||
isOperationReadyBefore &&
|
||||
predecessorDependency &&
|
||||
isExecutorOrOpen
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => state(id) == DONE(), "State transition violation";
|
||||
|
||||
// no side effect
|
||||
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
|
||||
}
|
||||
|
||||
/*
|
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
||||
│ Rule: cancel liveness and effects │
|
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
||||
*/
|
||||
rule cancel(env e, bytes32 id) {
|
||||
require nonpayable(e);
|
||||
|
||||
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
|
||||
|
||||
uint8 stateBefore = state(id);
|
||||
bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender);
|
||||
|
||||
cancel@withrevert(e, id);
|
||||
bool success = !lastReverted;
|
||||
|
||||
// liveness
|
||||
assert success <=> (
|
||||
stateBefore == PENDING() &&
|
||||
isCanceller
|
||||
);
|
||||
|
||||
// effect
|
||||
assert success => state(id) == UNSET(), "State transition violation";
|
||||
|
||||
// no side effect
|
||||
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";
|
||||
}
|
||||
@@ -0,0 +1 @@
|
||||
definition nonpayable(env e) returns bool = e.msg.value == 0;
|
||||
@@ -0,0 +1,7 @@
|
||||
methods {
|
||||
hasRole(bytes32, address) returns(bool) envfree
|
||||
getRoleAdmin(bytes32) returns(bytes32) envfree
|
||||
grantRole(bytes32, address)
|
||||
revokeRole(bytes32, address)
|
||||
renounceRole(bytes32, address)
|
||||
}
|
||||
+36
@@ -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)
|
||||
}
|
||||
@@ -0,0 +1,11 @@
|
||||
methods {
|
||||
name() returns (string) envfree => DISPATCHER(true)
|
||||
symbol() returns (string) envfree => DISPATCHER(true)
|
||||
decimals() returns (uint8) envfree => DISPATCHER(true)
|
||||
totalSupply() returns (uint256) envfree => DISPATCHER(true)
|
||||
balanceOf(address) returns (uint256) envfree => DISPATCHER(true)
|
||||
allowance(address,address) returns (uint256) envfree => DISPATCHER(true)
|
||||
approve(address,uint256) returns (bool) => DISPATCHER(true)
|
||||
transfer(address,uint256) returns (bool) => DISPATCHER(true)
|
||||
transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true)
|
||||
}
|
||||
@@ -0,0 +1,5 @@
|
||||
methods {
|
||||
permit(address,address,uint256,uint256,uint8,bytes32,bytes32) => DISPATCHER(true)
|
||||
nonces(address) returns (uint256) envfree => DISPATCHER(true)
|
||||
DOMAIN_SEPARATOR() returns (bytes32) envfree => DISPATCHER(true)
|
||||
}
|
||||
@@ -0,0 +1,5 @@
|
||||
methods {
|
||||
maxFlashLoan(address) returns (uint256) envfree => DISPATCHER(true)
|
||||
flashFee(address,uint256) returns (uint256) envfree => DISPATCHER(true)
|
||||
flashLoan(address,address,uint256,bytes) returns (bool) => DISPATCHER(true)
|
||||
}
|
||||
@@ -0,0 +1,3 @@
|
||||
methods {
|
||||
owner() returns (address) envfree
|
||||
}
|
||||
@@ -0,0 +1,20 @@
|
||||
methods {
|
||||
// IERC721
|
||||
balanceOf(address) returns (uint256) envfree => DISPATCHER(true)
|
||||
ownerOf(uint256) returns (address) envfree => DISPATCHER(true)
|
||||
getApproved(uint256) returns (address) envfree => DISPATCHER(true)
|
||||
isApprovedForAll(address,address) returns (bool) envfree => DISPATCHER(true)
|
||||
safeTransferFrom(address,address,uint256,bytes) => DISPATCHER(true)
|
||||
safeTransferFrom(address,address,uint256) => DISPATCHER(true)
|
||||
transferFrom(address,address,uint256) => DISPATCHER(true)
|
||||
approve(address,uint256) => DISPATCHER(true)
|
||||
setApprovalForAll(address,bool) => DISPATCHER(true)
|
||||
|
||||
// IERC721Metadata
|
||||
name() returns (string) => DISPATCHER(true)
|
||||
symbol() returns (string) => DISPATCHER(true)
|
||||
tokenURI(uint256) returns (string) => DISPATCHER(true)
|
||||
|
||||
// IERC721Receiver
|
||||
onERC721Received(address,address,uint256,bytes) returns (bytes4) => DISPATCHER(true)
|
||||
}
|
||||
@@ -0,0 +1,5 @@
|
||||
methods {
|
||||
owner() returns (address) envfree
|
||||
transferOwnership(address)
|
||||
renounceOwnership()
|
||||
}
|
||||
@@ -0,0 +1,7 @@
|
||||
methods {
|
||||
owner() returns (address) envfree
|
||||
pendingOwner() returns (address) envfree
|
||||
transferOwnership(address)
|
||||
acceptOwnership()
|
||||
renounceOwnership()
|
||||
}
|
||||
Reference in New Issue
Block a user