Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into remotes/origin/certora/erc20

certora/scripts/verifyAccessControl.sh

@@ -3,7 +3,6 @@ certoraRun \
     --verify AccessControlHarness:certora/specs/AccessControl.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --staging \
-    --rule_sanity \
-    --msg "modifier check"
+    --cloud \
+    --msg "AccessControl verification"
     

certora/scripts/verifyAllSasha.sh

@@ -0,0 +1,5 @@
+sh certora/scripts/verifyTimelock.sh
+sh certora/scripts/verifyERC1155.sh
+sh certora/scripts/verifyERC20FlashMint.sh
+sh certora/scripts/verifyERC20Wrapper.sh
+sh certora/scripts/verifyAccessControl.sh

certora/scripts/verifyERC1155.sh

@@ -4,8 +4,6 @@ certoraRun \
     --solc solc8.2 \
     --optimistic_loop \
     --loop_iter 3 \
-    --staging \
-    --rule_sanity \
-    --rule "$1" \
-    --msg "$1 check"
+    --cloud \
+    --msg "ERC1155 verification"
     

certora/scripts/verifyERC20FlashMint.sh

@@ -4,7 +4,6 @@ certoraRun \
     --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --staging \
-    --rule_sanity \
-    --msg "flashMint"
+    --cloud \
+    --msg "ERC20FlashMint verification"
     

certora/scripts/verifyERC20Wrapper.sh

@@ -4,7 +4,6 @@ certoraRun \
     --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --staging \
-    --rule_sanity \
-    --msg "wrapper spec sanity check fixes"
+    --cloud \
+    --msg "ERC20Wrapper verification"
     

certora/scripts/verifyTimelock.sh

@@ -5,7 +5,6 @@ certoraRun \
     --optimistic_loop \
     --loop_iter 3 \
     --staging alex/new-dt-hashing-alpha \
-    --rule_sanity \
-    --rule "$1" \
-    --msg "$1"
+    --settings -byteMapHashingPrecision=32 \
+    --msg "TimelockController verification"
       

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;

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

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,14 @@ 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);   
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
 
     mathint value = underlyingThisBalanceBefore - wrapperTotalBefore;
 

certora/specs/RulesInProgress.spec

@@ -136,4 +136,41 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
     uint256 ps = proposalSnapshot(pId);
 
     assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
-}
+}
+
+
+
+/////////////////// 2nd iteration with OZ ////////////////////////// 
+
+function executionsCall(method f, env e, address target, uint256 value, bytes data, 
+                                    bytes32 predecessor, bytes32 salt, uint256 delay, 
+                                    address[] targets, uint256[] values, bytes[] datas) {
+    if  (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) {
+        execute(e, target, value, data, predecessor, salt);
+	} else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
+        executeBatch(e, targets, values, datas, predecessor, salt);
+	} else {
+        calldataarg args;
+        f(e, args);
+    }
+}
+
+// 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?";
+}
+

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,58 +25,45 @@ 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;
 }
 
 
-function executionsCall(method f, env e, address target, uint256 value, bytes data, 
-                                    bytes32 predecessor, bytes32 salt, uint256 delay, 
-                                    address[] targets, uint256[] values, bytes[] datas) {
-    if  (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) {
-        execute(e, target, value, data, predecessor, salt);
-	} else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
-        executeBatch(e, targets, values, datas, predecessor, salt);
-	} else {
-        calldataarg args;
-        f(e, args);
-    }
-}
 
 ////////////////////////////////////////////////////////////////////////////
-//                           Ghosts                                       //
+//                         Invariants                                     //
 ////////////////////////////////////////////////////////////////////////////
 
 
-
-////////////////////////////////////////////////////////////////////////////
-//                            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)
 
-////////////////////////////////////////////////////////////////////////////
-//                            Rules                                       //
-////////////////////////////////////////////////////////////////////////////
 
+// STATUS - verified
+// `isOperationReady()` correctness check
+invariant readyCheck(env e, bytes32 id)
+    (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, 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;
 
-    require data.length < 7;
-    // uint256 freshIndex;
-    // require freshIndex <= data.length
+// STATUS - verified
+// `isOperationDone()` correctness check
+invariant doneCheck(bytes32 id)
+    getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id)
 
-    // require target != targetRand || value != valueRand || data[freshIndex] != dataRand[freshIndex] || predecessor != predecessorRand || salt != saltRand;
 
-    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 +72,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 +164,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 +171,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 +180,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 +195,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 +210,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 +262,62 @@ 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);
 
-    _checkRole@withrevert(e, PROPOSER_ROLE());
+    schedule(e, target, value, data, predecessor, salt, delay);
 
-    bool isCheckRoleReverted = lastReverted;
-    
-    // schedule@withrevert(e, target, value, data, predecessor, salt, delay);
-    scheduleBatch@withrevert(e, targets, values, datas, predecessor, salt, delay);
+    calldataarg args;
+    f(e, args);
 
-    bool isScheduleReverted = lastReverted;
+    assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready";
+}
 
-    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 - in progress
-// Ready = has waited minimum period after pending 
-rule cooldown(method f, env e, env e2){
-    bytes32 id;
+// 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);
 
-    require unset(id);
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
 
-    calldataarg args;
-    f(e, args);
+    execute(e, target, value, data, predecessor, salt);
+
+    assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
+}
 
-    // 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";
-}
+
+// 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";
+}