324 lines
10 KiB
Ruby
324 lines
10 KiB
Ruby
methods {
|
||
getTimestamp(bytes32) returns(uint256) envfree
|
||
_DONE_TIMESTAMP() returns(uint256) envfree
|
||
PROPOSER_ROLE() returns(bytes32) envfree
|
||
_minDelay() returns(uint256) envfree
|
||
getMinDelay() returns(uint256) envfree
|
||
hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree
|
||
isOperation(bytes32) returns(bool) envfree
|
||
isOperationPending(bytes32) returns(bool) envfree
|
||
isOperationDone(bytes32) returns(bool) envfree
|
||
|
||
isOperationReady(bytes32) returns(bool)
|
||
cancel(bytes32)
|
||
schedule(address, uint256, bytes32, bytes32, bytes32, uint256)
|
||
execute(address, uint256, bytes, bytes32, bytes32)
|
||
executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
|
||
_checkRole(bytes32) => DISPATCHER(true)
|
||
}
|
||
|
||
|
||
|
||
////////////////////////////////////////////////////////////////////////////
|
||
// Functions //
|
||
////////////////////////////////////////////////////////////////////////////
|
||
|
||
|
||
function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){
|
||
require data.length < 32;
|
||
require hashOperation(target, value, data, predecessor, salt) == id;
|
||
}
|
||
|
||
|
||
|
||
////////////////////////////////////////////////////////////////////////////
|
||
// Invariants //
|
||
////////////////////////////////////////////////////////////////////////////
|
||
|
||
|
||
// STATUS - verified
|
||
// `isOperation()` correctness check
|
||
invariant operationCheck(bytes32 id)
|
||
getTimestamp(id) > 0 <=> isOperation(id)
|
||
|
||
|
||
// STATUS - verified
|
||
// `isOperationPending()` correctness check
|
||
invariant pendingCheck(bytes32 id)
|
||
getTimestamp(id) > _DONE_TIMESTAMP() <=> isOperationPending(id)
|
||
|
||
|
||
// STATUS - verified
|
||
// `isOperationReady()` correctness check
|
||
invariant readyCheck(env e, bytes32 id)
|
||
(e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id)
|
||
|
||
|
||
// STATUS - verified
|
||
// `isOperationDone()` correctness check
|
||
invariant doneCheck(bytes32 id)
|
||
getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id)
|
||
|
||
|
||
|
||
////////////////////////////////////////////////////////////////////////////
|
||
// Rules //
|
||
////////////////////////////////////////////////////////////////////////////
|
||
|
||
|
||
/////////////////////////////////////////////////////////////
|
||
// STATE TRANSITIONS
|
||
/////////////////////////////////////////////////////////////
|
||
|
||
|
||
// STATUS - verified
|
||
// Possible transitions: form `!isOperation()` to `!isOperation()` or `isOperationPending()` only
|
||
rule unsetPendingTransitionGeneral(method f, env e){
|
||
bytes32 id;
|
||
|
||
require !isOperation(id);
|
||
require e.block.timestamp > 1;
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
assert isOperationPending(id) || !isOperation(id);
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// Possible transitions: form `!isOperation()` to `isOperationPending()` via `schedule()` and `scheduleBatch()` only
|
||
rule unsetPendingTransitionMethods(method f, env e){
|
||
bytes32 id;
|
||
|
||
require !isOperation(id);
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
assert isOperationPending(id) => (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector
|
||
|| f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector), "Why do we need to follow the schedule?";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// Possible transitions: form `ready()` to `isOperationDone()` via `execute()` and `executeBatch()` only
|
||
rule readyDoneTransition(method f, env e){
|
||
bytes32 id;
|
||
|
||
require isOperationReady(e, id);
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
assert isOperationDone(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector
|
||
|| f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not isOperationDone yet!";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// isOperationPending() -> cancelled() via cancel() only
|
||
rule pendingCancelledTransition(method f, env e){
|
||
bytes32 id;
|
||
|
||
require isOperationPending(id);
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
assert !isOperation(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// isOperationDone() -> nowhere
|
||
rule doneToNothingTransition(method f, env e){
|
||
bytes32 id;
|
||
|
||
require isOperationDone(id);
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
assert isOperationDone(id), "Did you find a way to escape? There is no way! HA-HA-HA";
|
||
}
|
||
|
||
|
||
|
||
/////////////////////////////////////////////////////////////
|
||
// THE REST
|
||
/////////////////////////////////////////////////////////////
|
||
|
||
|
||
// STATUS - verified
|
||
// only TimelockController contract can change minDelay
|
||
rule minDelayOnlyChange(method f, env e){
|
||
uint256 delayBefore = _minDelay();
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
uint256 delayAfter = _minDelay();
|
||
|
||
assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// scheduled operation timestamp == block.timestamp + delay (kind of unit test)
|
||
rule scheduleCheck(method f, env e){
|
||
bytes32 id;
|
||
|
||
address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
|
||
|
||
hashIdCorrelation(id, target, value, data, predecessor, salt);
|
||
|
||
schedule(e, target, value, data, predecessor, salt, delay);
|
||
|
||
assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// Cannot call `execute()` on a isOperationPending (not ready) operation
|
||
rule cannotCallExecute(method f, env e){
|
||
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
|
||
bytes32 id;
|
||
|
||
hashIdCorrelation(id, target, value, data, predecessor, salt);
|
||
require isOperationPending(id) && !isOperationReady(e, id);
|
||
|
||
execute@withrevert(e, target, value, data, predecessor, salt);
|
||
|
||
assert lastReverted, "you go against execution nature";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// Cannot call `execute()` on a !isOperation operation
|
||
rule executeRevertsFromUnset(method f, env e, env e2){
|
||
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
|
||
bytes32 id;
|
||
|
||
hashIdCorrelation(id, target, value, data, predecessor, salt);
|
||
require !isOperation(id);
|
||
|
||
execute@withrevert(e, target, value, data, predecessor, salt);
|
||
|
||
assert lastReverted, "you go against execution nature";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// Execute reverts => state returns to isOperationPending
|
||
rule executeRevertsEffectCheck(method f, env e){
|
||
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
|
||
bytes32 id;
|
||
|
||
hashIdCorrelation(id, target, value, data, predecessor, salt);
|
||
require isOperationPending(id) && !isOperationReady(e, id);
|
||
|
||
execute@withrevert(e, target, value, data, predecessor, salt);
|
||
bool reverted = lastReverted;
|
||
|
||
assert lastReverted => isOperationPending(id) && !isOperationReady(e, id), "you go against execution nature";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// Canceled operations cannot be executed → can’t move from canceled to isOperationDone
|
||
rule cancelledNotExecuted(method f, env e){
|
||
bytes32 id;
|
||
|
||
require !isOperation(id);
|
||
require e.block.timestamp > 1;
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
assert !isOperationDone(id), "The ship is not a creature of the air";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// Only proposers can schedule
|
||
rule onlyProposer(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector
|
||
|| f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector } {
|
||
bytes32 id;
|
||
bytes32 role;
|
||
address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
|
||
|
||
_checkRole@withrevert(e, PROPOSER_ROLE());
|
||
|
||
bool isCheckRoleReverted = lastReverted;
|
||
|
||
calldataarg args;
|
||
f@withrevert(e, args);
|
||
|
||
bool isScheduleReverted = lastReverted;
|
||
|
||
assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// if `ready` then has waited minimum period after isOperationPending()
|
||
rule cooldown(method f, env e, env e2){
|
||
bytes32 id;
|
||
address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
|
||
uint256 minDelay = getMinDelay();
|
||
|
||
hashIdCorrelation(id, target, value, data, predecessor, salt);
|
||
|
||
schedule(e, target, value, data, predecessor, salt, delay);
|
||
|
||
calldataarg args;
|
||
f(e, args);
|
||
|
||
assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// `schedule()` should change only one id's timestamp
|
||
rule scheduleChange(env e){
|
||
bytes32 id; bytes32 otherId;
|
||
address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
|
||
|
||
uint256 otherIdTimestampBefore = getTimestamp(otherId);
|
||
|
||
hashIdCorrelation(id, target, value, data, predecessor, salt);
|
||
|
||
schedule(e, target, value, data, predecessor, salt, delay);
|
||
|
||
assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// `execute()` should change only one id's timestamp
|
||
rule executeChange(env e){
|
||
bytes32 id; bytes32 otherId;
|
||
address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt;
|
||
uint256 otherIdTimestampBefore = getTimestamp(otherId);
|
||
|
||
hashIdCorrelation(id, target, value, data, predecessor, salt);
|
||
|
||
execute(e, target, value, data, predecessor, salt);
|
||
|
||
assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
|
||
}
|
||
|
||
|
||
// STATUS - verified
|
||
// `cancel()` should change only one id's timestamp
|
||
rule cancelChange(env e){
|
||
bytes32 id; bytes32 otherId;
|
||
|
||
uint256 otherIdTimestampBefore = getTimestamp(otherId);
|
||
|
||
cancel(e, id);
|
||
|
||
assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
|
||
}
|