diff --git a/certora/scripts/verifyERC20Wrapper.sh b/certora/scripts/verifyERC20Wrapper.sh index c4aaef9ff..15654d84e 100644 --- a/certora/scripts/verifyERC20Wrapper.sh +++ b/certora/scripts/verifyERC20Wrapper.sh @@ -6,5 +6,5 @@ certoraRun \ --optimistic_loop \ --staging \ --rule_sanity \ - --msg "wrapper spec sanity check fixes" + --msg "ERC20wrapper spec" \ No newline at end of file diff --git a/certora/scripts/verifyTimelock.sh b/certora/scripts/verifyTimelock.sh index 93bb92f75..2876d5f92 100644 --- a/certora/scripts/verifyTimelock.sh +++ b/certora/scripts/verifyTimelock.sh @@ -6,6 +6,7 @@ certoraRun \ --loop_iter 3 \ --staging alex/new-dt-hashing-alpha \ --rule_sanity \ + --settings -byteMapHashingPrecision=32 \ --rule "$1" \ --msg "$1" \ No newline at end of file diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec index 83f925d86..b57ce3113 100644 --- a/certora/specs/AccessControl.spec +++ b/certora/specs/AccessControl.spec @@ -11,7 +11,7 @@ methods { // STATUS - verified -// check onlyRole modifier for grantRole() +// If `onlyRole` modifier reverts then `grantRole()` reverts rule onlyRoleModifierCheckGrant(env e){ bytes32 role; address account; @@ -58,7 +58,7 @@ rule grantRoleEffect(env e){ // STATUS - verified -// grantRole() does not affect another accounts +// revokeRole() does not affect another accounts rule revokeRoleEffect(env e){ bytes32 role; address account; bytes32 anotherRole; address nonEffectedAcc; diff --git a/certora/specs/ERC1155.spec b/certora/specs/ERC1155.spec index 3ecca54ca..9b5839031 100644 --- a/certora/specs/ERC1155.spec +++ b/certora/specs/ERC1155.spec @@ -52,7 +52,7 @@ rule onlyOwnerCanApprove(env e){ // STATUS - verified -// chech in which scenarios (if any) isApprovedForAll() revertes +// Chech that isApprovedForAll() revertes in planned scenarios and no more. rule approvalRevertCases(env e){ address account; address operator; isApprovedForAll@withrevert(account, operator); @@ -104,7 +104,7 @@ rule unexpectedBalanceChange(method f, env e) // STATUS - verified -// chech in which scenarios balanceOf() revertes +// Chech that `balanceOf()` revertes in planned scenarios and no more (only if `account` is 0) rule balanceOfRevertCases(env e){ address account; uint256 id; balanceOf@withrevert(account, id); @@ -113,7 +113,7 @@ rule balanceOfRevertCases(env e){ // STATUS - verified -// chech in which scenarios balanceOfBatch() revertes +// Chech that `balanceOfBatch()` revertes in planned scenarios and no more (only if at least one of `account`s is 0) rule balanceOfBatchRevertCases(env e){ address[] accounts; uint256[] ids; address account1; address account2; address account3; @@ -131,7 +131,7 @@ rule balanceOfBatchRevertCases(env e){ ///////////////////////////////////////////////// -// Transfer (14/14) +// Transfer (13/13) ///////////////////////////////////////////////// @@ -178,7 +178,7 @@ rule transferCorrectness(env e){ // STATUS - verified -// cannot transfer more than allowed (safeBatchTransferFrom version) +// safeBatchTransferFrom updates `from` and `to` balances) rule transferBatchCorrectness(env e){ address from; address to; uint256[] ids; uint256[] amounts; bytes data; uint256 idToCheck1; uint256 amountToCheck1; @@ -230,7 +230,6 @@ rule cannotTransferMoreSingle(env e){ safeTransferFrom@withrevert(e, from, to, id, amount, data); assert amount > balanceBefore => lastReverted, "Achtung! Scammer!"; - assert to == 0 => lastReverted, "Achtung! Scammer!"; } @@ -258,21 +257,6 @@ rule cannotTransferMoreBatch(env e){ } -// STATUS - verified -// safeBatchTransferFrom should revert if `to` is 0 address or if arrays length is different -rule revertOfTransferBatch(env e){ - address from; address to; uint256[] ids; uint256[] amounts; bytes data; - - require ids.length < 100000000; - require amounts.length < 100000000; - - safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data); - - assert ids.length != amounts.length => lastReverted, "Achtung! Scammer!"; - assert to == 0 => lastReverted, "Achtung! Scammer!"; -} - - // STATUS - verified // Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0 rule transferBalanceReduceEffect(env e){ @@ -293,7 +277,7 @@ rule transferBalanceReduceEffect(env e){ // STATUS - verified -// Sender calling safeTransferFrom should only reduce 'to' balance and not other's if sending amount is greater than 0 +// Sender calling safeTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0 rule transferBalanceIncreaseEffect(env e){ address from; address to; address other; uint256 id; uint256 amount; @@ -338,7 +322,7 @@ rule transferBatchBalanceFromEffect(env e){ // STATUS - verified -// Sender calling safeBatchTransferFrom should only reduce 'to' balance and not other's if sending amount is greater than 0 +// Sender calling safeBatchTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0 rule transferBatchBalanceToEffect(env e){ address from; address to; address other; uint256[] ids; uint256[] amounts; @@ -434,12 +418,12 @@ rule noTransferBatchEffectOnApproval(env e){ ///////////////////////////////////////////////// -// Mint (9/9) +// Mint (7/9) ///////////////////////////////////////////////// // STATUS - verified -// mint additivity +// Additivity of _mint: _mint(a); _mint(b) has same effect as _mint(a+b) rule mintAdditivity(env e){ address to; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; bytes data; require amount == amount1 + amount2; @@ -459,8 +443,8 @@ rule mintAdditivity(env e){ } -// STATUS - verified -// mint should revert if `from` is 0 +// STATUS - verified +// Chech that `_mint()` revertes in planned scenario(s) (only if `to` is 0) rule mintRevertCases(env e){ address to; uint256 id; uint256 amount; bytes data; @@ -471,28 +455,27 @@ rule mintRevertCases(env e){ // STATUS - verified -// mintBatch should revert if `from` is 0 or arrays have different length +// Chech that `_mintBatch()` revertes in planned scenario(s) (only if `to` is 0 or arrays have different length) rule mintBatchRevertCases(env e){ address to; uint256[] ids; uint256[] amounts; bytes data; - require ids.length < 100000000; - require amounts.length < 100000000; + require ids.length < 1000000000; + require amounts.length < 1000000000; _mintBatch@withrevert(e, to, ids, amounts, data); - assert to == 0 => lastReverted, "Should revert"; - assert ids.length != amounts.length => lastReverted, "Should revert"; + assert (ids.length != amounts.length || to == 0) => lastReverted, "Should revert"; } // STATUS - verified -// check that mint updates `to` balance correctly +// Check that mint updates `to` balance correctly rule mintCorrectWork(env e){ address to; uint256 id; uint256 amount; bytes data; uint256 otherBalanceBefore = balanceOf(to, id); - _mint(e, to, id, amount, data); + _mint(e, to, id, amount, data); uint256 otherBalanceAfter = balanceOf(to, id); @@ -534,7 +517,7 @@ rule mintBatchCorrectWork(env e){ // STATUS - verified -// the user cannot mint more than max_uint256 +// The user cannot mint more than max_uint256 rule cantMintMoreSingle(env e){ address to; uint256 id; uint256 amount; bytes data; @@ -571,7 +554,7 @@ rule cantMintMoreBatch(env e){ // STATUS - verified -// mint changes only `to` balance +// `_mint()` changes only `to` balance rule cantMintOtherBalances(env e){ address to; uint256 id; uint256 amount; bytes data; address other; @@ -618,7 +601,7 @@ rule cantMintBatchOtherBalances(env e){ // STATUS - verified -// burn additivity +// Additivity of _burn: _burn(a); _burn(b) has same effect as _burn(a+b) rule burnAdditivity(env e){ address from; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; require amount == amount1 + amount2; @@ -639,7 +622,7 @@ rule burnAdditivity(env e){ // STATUS - verified -// burn should revert if `from` is 0 +// Chech that `_burn()` revertes in planned scenario(s) (if `from` is 0) rule burnRevertCases(env e){ address from; uint256 id; uint256 amount; @@ -650,16 +633,16 @@ rule burnRevertCases(env e){ // STATUS - verified -// burnBatch should revert if `from` is 0 or arrays have different length +// Chech that `balanceOf()` revertes in planned scenario(s) (if `from` is 0 or arrays have different length) rule burnBatchRevertCases(env e){ address from; uint256[] ids; uint256[] amounts; - require ids.length < 100000000; + require ids.length < 1000000000; + require amounts.length < 1000000000; _burnBatch@withrevert(e, from, ids, amounts); - assert from == 0 => lastReverted, "Should revert"; - assert ids.length != amounts.length => lastReverted, "Should revert"; + assert (from == 0 || ids.length != amounts.length) => lastReverted, "Should revert"; } diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index 3ea288545..01c1b4295 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -40,7 +40,7 @@ invariant underTotalAndContractBalanceOfCorrelation(env e) // STATUS - verified -// check correct values update by depositFor() +// Check that values are updated correctly by `depositFor()` rule depositForSpecBasic(env e){ address account; uint256 amount; @@ -64,11 +64,10 @@ rule depositForSpecBasic(env e){ // STATUS - verified -// check correct values update by depositFor() +// Check that values are updated correctly by `depositFor()` rule depositForSpecWrapper(env e){ address account; uint256 amount; - // require e.msg.sender != currentContract; require underlying() != currentContract; uint256 wrapperUserBalanceBefore = balanceOf(e, account); @@ -88,7 +87,7 @@ rule depositForSpecWrapper(env e){ // STATUS - verified -// check correct values update by depositFor() +// Check that values are updated correctly by `depositFor()` rule depositForSpecUnderlying(env e){ address account; uint256 amount; @@ -116,7 +115,7 @@ rule depositForSpecUnderlying(env e){ // STATUS - verified -// check correct values update by withdrawTo() +// Check that values are updated correctly by `withdrawTo()` rule withdrawToSpecBasic(env e){ address account; uint256 amount; @@ -136,7 +135,7 @@ rule withdrawToSpecBasic(env e){ // STATUS - verified -// check correct values update by withdrawTo() +// Check that values are updated correctly by `withdrawTo()` rule withdrawToSpecWrapper(env e){ address account; uint256 amount; @@ -159,7 +158,7 @@ rule withdrawToSpecWrapper(env e){ // STATUS - verified -// check correct values update by withdrawTo() +// cCheck that values are updated correctly by `withdrawTo()` rule withdrawToSpecUnderlying(env e){ address account; uint256 amount; @@ -189,14 +188,13 @@ rule withdrawToSpecUnderlying(env e){ // STATUS - verified -// check correct values update by _recover() +// Check that values are updated correctly by `_recover()` rule recoverSpec(env e){ address account; uint256 amount; uint256 wrapperTotalBefore = totalSupply(e); uint256 wrapperUserBalanceBefore = balanceOf(e, account); uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); - uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); mathint value = underlyingThisBalanceBefore - wrapperTotalBefore; diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 9e08fcf98..fbce17bfd 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -5,7 +5,11 @@ methods { _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) @@ -13,23 +17,6 @@ methods { _checkRole(bytes32) => DISPATCHER(true) } -//////////////////////////////////////////////////////////////////////////// -// Definitions // -//////////////////////////////////////////////////////////////////////////// - - -definition unset(bytes32 id) returns bool = - getTimestamp(id) == 0; - -definition pending(bytes32 id) returns bool = - getTimestamp(id) > _DONE_TIMESTAMP(); - -definition ready(bytes32 id, env e) returns bool = - getTimestamp(id) > _DONE_TIMESTAMP() && getTimestamp(id) <= e.block.timestamp; - -definition done(bytes32 id) returns bool = - getTimestamp(id) == _DONE_TIMESTAMP(); - //////////////////////////////////////////////////////////////////////////// @@ -38,7 +25,7 @@ definition done(bytes32 id) returns bool = function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){ - require data.length < 7; + require data.length < 32; require hashOperation(target, value, data, predecessor, salt) == id; } @@ -56,40 +43,41 @@ function executionsCall(method f, env e, address target, uint256 value, bytes da } } -//////////////////////////////////////////////////////////////////////////// -// Ghosts // -//////////////////////////////////////////////////////////////////////////// - //////////////////////////////////////////////////////////////////////////// -// Invariants // +// Invariants // //////////////////////////////////////////////////////////////////////////// +// STATUS - verified +// `isOperation()` correctness check +invariant operationCheck(bytes32 id) + getTimestamp(id) > 0 <=> isOperation(id) + -//////////////////////////////////////////////////////////////////////////// -// Rules // -//////////////////////////////////////////////////////////////////////////// +// STATUS - verified +// `isOperationPending()` correctness check +invariant pendingCheck(bytes32 id) + getTimestamp(id) > _DONE_TIMESTAMP() <=> isOperationPending(id) -rule keccakCheck(method f, env e){ - address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; - address targetRand; uint256 valueRand; bytes dataRand; bytes32 predecessorRand; bytes32 saltRand; +// STATUS - verified +// `isOperationReady()` correctness check +invariant readyCheck(env e, bytes32 id) + (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id) - require data.length < 7; - // uint256 freshIndex; - // require freshIndex <= data.length - // require target != targetRand || value != valueRand || data[freshIndex] != dataRand[freshIndex] || predecessor != predecessorRand || salt != saltRand; +// STATUS - verified +// `isOperationDone()` correctness check +invariant doneCheck(bytes32 id) + getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id) - bytes32 a = hashOperation(target, value, data, predecessor, salt); - bytes32 b = hashOperation(target, value, data, predecessor, salt); - // bytes32 c = hashOperation(targetRand, valueRand, dataRand, predecessorRand, saltRand); - assert a == b, "hashes are different"; - // assert a != c, "hashes are the same"; -} + +//////////////////////////////////////////////////////////////////////////// +// Rules // +//////////////////////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////// @@ -98,77 +86,75 @@ rule keccakCheck(method f, env e){ // STATUS - verified -// unset() -> unset() || pending() only +// Possible transitions: form `!isOperation()` to `!isOperation()` or `isOperationPending()` only rule unsetPendingTransitionGeneral(method f, env e){ bytes32 id; - require unset(id); + require !isOperation(id); require e.block.timestamp > 1; calldataarg args; f(e, args); - assert pending(id) || unset(id); + assert isOperationPending(id) || !isOperation(id); } // STATUS - verified -// unset() -> pending() via schedule() and scheduleBatch() only +// Possible transitions: form `!isOperation()` to `isOperationPending()` via `schedule()` and `scheduleBatch()` only rule unsetPendingTransitionMethods(method f, env e){ bytes32 id; - require unset(id); + require !isOperation(id); calldataarg args; f(e, args); - bool tmp = pending(id); - - assert pending(id) => (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector + 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 -// ready() -> done() via execute() and executeBatch() only +// Possible transitions: form `ready()` to `isOperationDone()` via `execute()` and `executeBatch()` only rule readyDoneTransition(method f, env e){ bytes32 id; - require ready(id, e); + require isOperationReady(e, id); calldataarg args; f(e, args); - assert done(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector - || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not done yet!"; + 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 -// pending() -> cancelled() via cancel() only +// isOperationPending() -> cancelled() via cancel() only rule pendingCancelledTransition(method f, env e){ bytes32 id; - require pending(id); + require isOperationPending(id); calldataarg args; f(e, args); - assert unset(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?"; + assert !isOperation(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?"; } // STATUS - verified -// done() -> nowhere +// isOperationDone() -> nowhere rule doneToNothingTransition(method f, env e){ bytes32 id; - require done(id); + require isOperationDone(id); calldataarg args; f(e, args); - assert done(id), "Did you find a way to escape? There is no way! HA-HA-HA"; + assert isOperationDone(id), "Did you find a way to escape? There is no way! HA-HA-HA"; } @@ -192,26 +178,6 @@ rule minDelayOnlyChange(method f, env e){ } -// STATUS - in progress -// execute() is the only way to set timestamp to 1 -rule getTimestampOnlyChange(method f, env e){ - bytes32 id; - address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay; - address[] targets; uint256[] values; bytes[] datas; - - require (targets[0] == target && values[0] == value && datas[0] == data) - || (targets[1] == target && values[1] == value && datas[1] == data) - || (targets[2] == target && values[2] == value && datas[2] == data); - - hashIdCorrelation(id, target, value, data, predecessor, salt); - - executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas); - - assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector - || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?"; -} - - // STATUS - verified // scheduled operation timestamp == block.timestamp + delay (kind of unit test) rule scheduleCheck(method f, env e){ @@ -219,7 +185,6 @@ rule scheduleCheck(method f, env e){ address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; - require getTimestamp(id) < e.block.timestamp; hashIdCorrelation(id, target, value, data, predecessor, salt); schedule(e, target, value, data, predecessor, salt, delay); @@ -229,13 +194,13 @@ rule scheduleCheck(method f, env e){ // STATUS - verified -// Cannot call execute on a pending (not ready) operation +// 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 pending(id) && !ready(id, e); + require isOperationPending(id) && !isOperationReady(e, id); execute@withrevert(e, target, value, data, predecessor, salt); @@ -244,13 +209,13 @@ rule cannotCallExecute(method f, env e){ // STATUS - verified -// in unset() execute() reverts +// 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 unset(id); + require !isOperation(id); execute@withrevert(e, target, value, data, predecessor, salt); @@ -259,51 +224,47 @@ rule executeRevertsFromUnset(method f, env e, env e2){ // STATUS - verified -// Execute reverts => state returns to pending +// 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 pending(id) && !ready(id, e); + require isOperationPending(id) && !isOperationReady(e, id); execute@withrevert(e, target, value, data, predecessor, salt); bool reverted = lastReverted; - assert lastReverted => pending(id) && !ready(id, e), "you go against execution nature"; + 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 ready +// Canceled operations cannot be executed → can’t move from canceled to isOperationDone rule cancelledNotExecuted(method f, env e){ bytes32 id; - require unset(id); + require !isOperation(id); require e.block.timestamp > 1; calldataarg args; f(e, args); - assert !done(id), "The ship is not a creature of the air"; + assert !isOperationDone(id), "The ship is not a creature of the air"; } -// STATUS - broken -// Only proposers can schedule an operation -rule onlyProposerCertorafallbackFail(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes32, bytes32, bytes32, uint256).selector +// 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; - // hashIdCorrelation(id, target, value, data, predecessor, salt); - _checkRole@withrevert(e, PROPOSER_ROLE()); bool isCheckRoleReverted = lastReverted; - - // schedule@withrevert(e, target, value, data, predecessor, salt, delay); calldataarg args; f@withrevert(e, args); @@ -315,38 +276,86 @@ rule onlyProposerCertorafallbackFail(method f, env e) filtered { f -> f.selector // STATUS - verified -// Only proposers can schedule an operation -rule onlyProposer1(method f, env e){ +// if `ready` then has waited minimum period after isOperationPending() +rule cooldown(method f, env e, env e2){ bytes32 id; - bytes32 role; - // address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; - address[] targets; uint256[] values; bytes[] datas; bytes32 predecessor; bytes32 salt; uint256 delay; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + uint256 minDelay = getMinDelay(); + + hashIdCorrelation(id, target, value, data, predecessor, salt); - // hashIdCorrelation(id, target, value, data, predecessor, salt); + schedule(e, target, value, data, predecessor, salt, delay); - _checkRole@withrevert(e, PROPOSER_ROLE()); + calldataarg args; + f(e, args); - bool isCheckRoleReverted = lastReverted; - - // schedule@withrevert(e, target, value, data, predecessor, salt, delay); - scheduleBatch@withrevert(e, targets, values, datas, predecessor, salt, delay); + assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready"; +} - bool isScheduleReverted = lastReverted; - assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected"; +// 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"; } + + + + // STATUS - in progress -// Ready = has waited minimum period after pending -rule cooldown(method f, env e, env e2){ +// execute() is the only way to set timestamp to 1 +rule getTimestampOnlyChange(method f, env e){ bytes32 id; + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay; + address[] targets; uint256[] values; bytes[] datas; - require unset(id); + require (targets[0] == target && values[0] == value && datas[0] == data) + || (targets[1] == target && values[1] == value && datas[1] == data) + || (targets[2] == target && values[2] == value && datas[2] == data); - calldataarg args; - f(e, args); + hashIdCorrelation(id, target, value, data, predecessor, salt); + + executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas); - // e.block.timestamp - delay > time scheduled => ready() - assert e.block.timestamp >= getTimestamp(id) => ready(id, e), "No rush! When I'm ready, I'm ready"; -} \ No newline at end of file + assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?"; +}