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

certora/specs/ERC1155.spec

@@ -17,7 +17,7 @@ methods {
 
 
 /////////////////////////////////////////////////
-// Approval
+// Approval (4/4)
 /////////////////////////////////////////////////
 
 
@@ -60,8 +60,8 @@ rule approvalRevertCases(env e){
 }
 
 
-// STATUS - verified 
-// Set approval changes only one approval
+// STATUS - verified
+// setApproval changes only one approval
 rule onlyOneAllowanceChange(method f, env e) {
     address owner; address operator; address user; 
     bool approved;
@@ -78,7 +78,7 @@ rule onlyOneAllowanceChange(method f, env e) {
 
 
 /////////////////////////////////////////////////
-// Balance
+// Balance (3/3)
 /////////////////////////////////////////////////
 
 
@@ -131,11 +131,97 @@ rule balanceOfBatchRevertCases(env e){
 
 
 /////////////////////////////////////////////////
-// Transfer
+// Transfer (14/14)
 /////////////////////////////////////////////////
 
 
-// STATUS - 
+// STATUS - verified
+// transfer additivity
+rule transferAdditivity(env e){
+    address from; address to; uint256 id; bytes data;
+    uint256 amount; uint256 amount1; uint256 amount2;
+    require amount == amount1 + amount2;
+
+    storage initialStorage = lastStorage;
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 balanceAfterSingleTransaction = balanceOf(to, id);
+
+    safeTransferFrom(e, from, to, id, amount1, data) at initialStorage;
+    safeTransferFrom(e, from, to, id, amount2, data);
+
+    uint256 balanceAfterDoubleTransaction = balanceOf(to, id);
+
+    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
+}
+
+
+// STATUS - verified
+// safeTransferFrom updates `from` and `to` balances
+rule transferCorrectness(env e){
+    address from; address to; uint256 id; uint256 amount; bytes data;
+
+    require to != from;
+
+    uint256 fromBalanceBefore = balanceOf(from, id);
+    uint256 toBalanceBefore = balanceOf(to, id);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 fromBalanceAfter = balanceOf(from, id);
+    uint256 toBalanceAfter = balanceOf(to, id);
+
+    assert fromBalanceBefore == fromBalanceAfter + amount, "Something wet wrong";
+    assert toBalanceBefore == toBalanceAfter - amount, "Something wet wrong";
+}
+
+
+// STATUS - verified
+// cannot transfer more than allowed (safeBatchTransferFrom version)
+rule transferBatchCorrectness(env e){
+    address from; address to; uint256[] ids; uint256[] amounts; bytes data;
+    uint256 idToCheck1; uint256 amountToCheck1;
+    uint256 idToCheck2; uint256 amountToCheck2;
+    uint256 idToCheck3; uint256 amountToCheck3;
+
+    require to != from;
+    require idToCheck1 != idToCheck2 && idToCheck3 != idToCheck2 && idToCheck1 != idToCheck3;
+    
+    require ids.length == 3;        
+    require amounts.length == 3;    
+    require ids[0] == idToCheck1; require amounts[0] == amountToCheck1;
+    require ids[1] == idToCheck2; require amounts[1] == amountToCheck2;
+    require ids[2] == idToCheck3; require amounts[2] == amountToCheck3;
+
+    uint256 fromBalanceBefore1 = balanceOf(from, idToCheck1);
+    uint256 fromBalanceBefore2 = balanceOf(from, idToCheck2);
+    uint256 fromBalanceBefore3 = balanceOf(from, idToCheck3);
+
+    uint256 toBalanceBefore1 = balanceOf(to, idToCheck1);
+    uint256 toBalanceBefore2 = balanceOf(to, idToCheck2);
+    uint256 toBalanceBefore3 = balanceOf(to, idToCheck3);
+
+    safeBatchTransferFrom(e, from, to, ids, amounts, data);
+
+    uint256 fromBalanceAfter1 = balanceOf(from, idToCheck1);
+    uint256 fromBalanceAfter2 = balanceOf(from, idToCheck2);
+    uint256 fromBalanceAfter3 = balanceOf(from, idToCheck3);
+
+    uint256 toBalanceAfter1 = balanceOf(to, idToCheck1);
+    uint256 toBalanceAfter2 = balanceOf(to, idToCheck2);
+    uint256 toBalanceAfter3 = balanceOf(to, idToCheck3);
+
+    assert (fromBalanceBefore1 == fromBalanceAfter1 + amountToCheck1)
+                && (fromBalanceBefore2 == fromBalanceAfter2 + amountToCheck2)
+                && (fromBalanceBefore3 == fromBalanceAfter3 + amountToCheck3), "Something wet wrong";
+    assert (toBalanceBefore1 == toBalanceAfter1 - amountToCheck1)
+                && (toBalanceBefore2 == toBalanceAfter2 - amountToCheck2)
+                && (toBalanceBefore3 == toBalanceAfter3 - amountToCheck3), "Something wet wrong";
+}
+
+
+// STATUS - verified
 // cannot transfer more than `from` balance (safeTransferFrom version)
 rule cannotTransferMoreSingle(env e){
     address from; address to; uint256 id; uint256 amount; bytes data;
@@ -148,7 +234,7 @@ rule cannotTransferMoreSingle(env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // cannot transfer more than allowed (safeBatchTransferFrom version)
 rule cannotTransferMoreBatch(env e){
     address from; address to; uint256[] ids; uint256[] amounts; bytes data;
@@ -168,17 +254,17 @@ rule cannotTransferMoreBatch(env e){
 
     safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);
 
-    assert (amountToCheck1 > balanceBefore1 || amountToCheck2 > balanceBefore2 || amountToCheck2 > balanceBefore2) => lastReverted, "Achtung! Scammer!";
+    assert (amountToCheck1 > balanceBefore1 || amountToCheck2 > balanceBefore2 || amountToCheck3 > balanceBefore3) => lastReverted, "Achtung! Scammer!";
 }
 
 
-// STATUS - (added debug vars)
+// 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;
 
-    uint256 idTMP = ids.length;
-    uint256 amountsTMP = amounts.length;
+    require ids.length < 100000000;
+    require amounts.length < 100000000;
 
     safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);
 
@@ -195,7 +281,6 @@ rule transferBalanceReduceEffect(env e){
     bytes data;
 
     require other != to;
-    require amount > 0;
 
     uint256 otherBalanceBefore = balanceOf(other, id);
 
@@ -207,7 +292,7 @@ rule transferBalanceReduceEffect(env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // Sender calling safeTransferFrom should only reduce 'to' balance and not other's if sending amount is greater than 0
 rule transferBalanceIncreaseEffect(env e){
     address from; address to; address other;
@@ -226,7 +311,7 @@ rule transferBalanceIncreaseEffect(env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0
 rule transferBatchBalanceFromEffect(env e){
     address from; address to; address other;
@@ -236,13 +321,6 @@ rule transferBatchBalanceFromEffect(env e){
 
     require other != to;
 
-    // require ids.length == 3; 
-    // require amounts.length == 3;
- 
-    // require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
-    // require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
-    // require amount1 > 0; require amount2 > 0; require amount3 > 0;
-
     uint256 otherBalanceBefore1 = balanceOf(other, id1);
     uint256 otherBalanceBefore2 = balanceOf(other, id2);
     uint256 otherBalanceBefore3 = balanceOf(other, id3);
@@ -259,7 +337,7 @@ rule transferBatchBalanceFromEffect(env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // Sender calling safeBatchTransferFrom should only reduce 'to' balance and not other's if sending amount is greater than 0
 rule transferBatchBalanceToEffect(env e){
     address from; address to; address other;
@@ -269,13 +347,6 @@ rule transferBatchBalanceToEffect(env e){
 
     require other != from;
 
-    // require ids.length == 3; 
-    // require amounts.length == 3;
- 
-    // require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
-    // require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
-    // require amount1 > 0; require amount2 > 0; require amount3 > 0;
-
     uint256 otherBalanceBefore1 = balanceOf(other, id1);
     uint256 otherBalanceBefore2 = balanceOf(other, id2);
     uint256 otherBalanceBefore3 = balanceOf(other, id3);
@@ -308,7 +379,7 @@ rule noTransferForNotApproved(env e) {
 }   
 
 
-// STATUS - 
+// STATUS - verified
 // cannot transfer without approval (safeBatchTransferFrom version)
 rule noTransferBatchForNotApproved(env e) {
     address from; address operator; address to; 
@@ -325,7 +396,7 @@ rule noTransferBatchForNotApproved(env e) {
 }   
 
 
-// STATUS - 
+// STATUS - verified
 // safeTransferFrom doesn't affect any approval
 rule noTransferEffectOnApproval(env e){
     address from; address to;
@@ -343,7 +414,7 @@ rule noTransferEffectOnApproval(env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // safeTransferFrom doesn't affect any approval
 rule noTransferBatchEffectOnApproval(env e){
     address from; address to;
@@ -361,11 +432,107 @@ rule noTransferBatchEffectOnApproval(env e){
 }
 
 
+
 /////////////////////////////////////////////////
-// Mint
+// Mint (9/9)
 /////////////////////////////////////////////////
 
 
+// STATUS - verified
+// mint additivity
+rule mintAdditivity(env e){
+    address to; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; bytes data;
+    require amount == amount1 + amount2;
+
+    storage initialStorage = lastStorage;
+
+    _mint(e, to, id, amount, data);
+
+    uint256 balanceAfterSingleTransaction = balanceOf(to, id);
+
+    _mint(e, to, id, amount1, data) at initialStorage;
+    _mint(e, to, id, amount2, data);
+
+    uint256 balanceAfterDoubleTransaction = balanceOf(to, id);
+
+    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
+}
+
+
+// STATUS - verified
+// mint should revert if `from` is 0
+rule mintRevertCases(env e){
+    address to; uint256 id; uint256 amount; bytes data;
+
+    _mint@withrevert(e, to, id, amount, data);
+
+    assert to == 0 => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
+// mintBatch should revert if `from` 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;
+
+    _mintBatch@withrevert(e, to, ids, amounts, data);
+
+    assert to == 0 => lastReverted, "Should revert";
+    assert ids.length != amounts.length => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
+// 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);
+
+    uint256 otherBalanceAfter = balanceOf(to, id);
+    
+    assert otherBalanceBefore == otherBalanceAfter - amount, "Something is wrong";
+}
+
+
+// STATUS - verified
+// check that mintBatch updates `bootcamp participantsfrom` balance correctly
+rule mintBatchCorrectWork(env e){
+    address to;
+    uint256 id1; uint256 id2; uint256 id3; 
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+    bytes data;
+
+    require ids.length == 3; 
+    require amounts.length == 3; 
+
+    require id1 != id2 && id2 != id3 && id3 != id1;
+    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
+    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
+
+    uint256 otherBalanceBefore1 = balanceOf(to, id1);
+    uint256 otherBalanceBefore2 = balanceOf(to, id2);
+    uint256 otherBalanceBefore3 = balanceOf(to, id3);
+
+    _mintBatch(e, to, ids, amounts, data);
+
+    uint256 otherBalanceAfter1 = balanceOf(to, id1);
+    uint256 otherBalanceAfter2 = balanceOf(to, id2);
+    uint256 otherBalanceAfter3 = balanceOf(to, id3);
+    
+    assert otherBalanceBefore1 == otherBalanceAfter1 - amount1
+            && otherBalanceBefore2 == otherBalanceAfter2 - amount2
+            && otherBalanceBefore3 == otherBalanceAfter3 - amount3
+            , "Something is wrong";
+}
+
+
 // STATUS - verified
 // the user cannot mint more than max_uint256
 rule cantMintMoreSingle(env e){
@@ -403,36 +570,100 @@ rule cantMintMoreBatch(env e){
 }
 
 
-// rule mintRevert(env e){
-//     address operator;
-//     address from;
-//     address to;
-//     uint256 id;
-//     uint256 amount;
-//     bytes data;
-// 
-//     require operator == e.msg.sender;
-//     require from == 0;
-// 
-//     _doSafeTransferAcceptanceCheck@withrevert(operator, from, to, id, amount, data);
-// 
-//     bool acceptanceCheck = lastReverted;
-// 
-//     _mint@withrevert(e, to, id, amount, data);
-// 
-//     bool mintRevert = lastReverted;
-// 
-//     assert acceptanceCheck => mintRevert, "reverts are wrong";
-// }
+// STATUS - verified
+// mint changes only `to` balance
+rule cantMintOtherBalances(env e){
+    address to; uint256 id; uint256 amount; bytes data;
+    address other;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    _mint(e, to, id, amount, data);
 
+    uint256 otherBalanceAfter = balanceOf(other, id);
+    
+    assert other != to => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing";
+}
+
+
+// STATUS - verified
+// mintBatch changes only `to` balance
+rule cantMintBatchOtherBalances(env e){
+    address to;
+    uint256 id1; uint256 id2; uint256 id3; 
+    uint256[] ids; uint256[] amounts;
+    address other;
+    bytes data;
+
+    uint256 otherBalanceBefore1 = balanceOf(other, id1);
+    uint256 otherBalanceBefore2 = balanceOf(other, id2);
+    uint256 otherBalanceBefore3 = balanceOf(other, id3);
+
+    _mintBatch(e, to, ids, amounts, data);
+
+    uint256 otherBalanceAfter1 = balanceOf(other, id1);
+    uint256 otherBalanceAfter2 = balanceOf(other, id2);
+    uint256 otherBalanceAfter3 = balanceOf(other, id3);
+    
+    assert other != to => (otherBalanceBefore1 == otherBalanceAfter1 
+                                && otherBalanceBefore2 == otherBalanceAfter2 
+                                && otherBalanceBefore3 == otherBalanceAfter3)
+                                , "I like to see your money disappearing";
+}
 
 
 /////////////////////////////////////////////////
-// Burn
+// Burn (9/9)
 /////////////////////////////////////////////////
 
 
-// STATUS - 
+// STATUS - verified
+// burn additivity
+rule burnAdditivity(env e){
+    address from; uint256 id; uint256 amount; uint256 amount1; uint256 amount2;
+    require amount == amount1 + amount2;
+
+    storage initialStorage = lastStorage;
+
+    _burn(e, from, id, amount);
+
+    uint256 balanceAfterSingleTransaction = balanceOf(from, id);
+
+    _burn(e, from, id, amount1) at initialStorage;
+    _burn(e, from, id, amount2);
+
+    uint256 balanceAfterDoubleTransaction = balanceOf(from, id);
+
+    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
+}
+
+
+// STATUS - verified
+// burn should revert if `from` is 0
+rule burnRevertCases(env e){
+    address from; uint256 id; uint256 amount;
+
+    _burn@withrevert(e, from, id, amount);
+
+    assert from == 0 => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
+// burnBatch should revert if `from` is 0 or arrays have different length
+rule burnBatchRevertCases(env e){
+    address from; uint256[] ids; uint256[] amounts;
+
+    require ids.length < 100000000;
+
+    _burnBatch@withrevert(e, from, ids, amounts);
+
+    assert from == 0 => lastReverted, "Should revert";
+    assert ids.length != amounts.length => lastReverted, "Should revert";
+}
+
+
+// STATUS - verified
 // check that burn updates `from` balance correctly
 rule burnCorrectWork(env e){
     address from; uint256 id; uint256 amount;
@@ -447,7 +678,7 @@ rule burnCorrectWork(env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // check that burnBatch updates `from` balance correctly
 rule burnBatchCorrectWork(env e){
     address from;
@@ -456,7 +687,6 @@ rule burnBatchCorrectWork(env e){
     uint256[] ids; uint256[] amounts;
 
     require ids.length == 3; 
-    require amounts.length == 3;
 
     require id1 != id2 && id2 != id3 && id3 != id1;
     require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
@@ -480,7 +710,7 @@ rule burnBatchCorrectWork(env e){
 
 
 // STATUS - verified
-// the user cannot mint more than max_uint256
+// the user cannot burn more than they have
 rule cantBurnMoreSingle(env e){
     address from; uint256 id; uint256 amount;
 
@@ -492,24 +722,8 @@ rule cantBurnMoreSingle(env e){
 }
 
 
-// STATUS - 
-// burn changes only `from` balance
-rule cantBurnOtherBalances(env e){
-    address from; uint256 id; uint256 amount;
-    address other;
-
-    uint256 otherBalanceBefore = balanceOf(other, id);
-
-    _burn(e, from, id, amount);
-
-    uint256 otherBalanceAfter = balanceOf(other, id);
-    
-    assert other != from => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing";
-}
-
-
 // STATUS - verified
-// the user cannot mint more than max_uint256 (batch version)
+// the user cannot burn more than they have (batch version)
 rule cantBurnMoreBatch(env e){
     address from;
     uint256 id1; uint256 id2; uint256 id3; 
@@ -531,21 +745,31 @@ rule cantBurnMoreBatch(env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
+// burn changes only `from` balance
+rule cantBurnOtherBalances(env e){
+    address from; uint256 id; uint256 amount;
+    address other;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    _burn(e, from, id, amount);
+
+    uint256 otherBalanceAfter = balanceOf(other, id);
+    
+    assert other != from => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing";
+}
+
+
+// STATUS - verified
 // burnBatch changes only `from` balance
-rule cantBurnbatchOtherBalances(env e){
+rule cantBurnBatchOtherBalances(env e){
     address from;
     uint256 id1; uint256 id2; uint256 id3; 
     uint256 amount1; uint256 amount2; uint256 amount3;
     uint256[] ids; uint256[] amounts;
     address other;
 
-    require ids.length == 3; 
-    require amounts.length == 3;
-
-    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
-    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
-
     uint256 otherBalanceBefore1 = balanceOf(other, id1);
     uint256 otherBalanceBefore2 = balanceOf(other, id2);
     uint256 otherBalanceBefore3 = balanceOf(other, id3);
@@ -557,7 +781,7 @@ rule cantBurnbatchOtherBalances(env e){
     uint256 otherBalanceAfter3 = balanceOf(other, id3);
     
     assert other != from => (otherBalanceBefore1 == otherBalanceAfter1 
-                                || otherBalanceBefore2 == otherBalanceAfter2 
-                                || otherBalanceBefore3 == otherBalanceAfter3)
+                                && otherBalanceBefore2 == otherBalanceAfter2 
+                                && otherBalanceBefore3 == otherBalanceAfter3)
                                 , "I like to see your money disappearing";
 }

certora/specs/ERC20FlashMint.spec

@@ -1,9 +1,8 @@
 import "erc20.spec"
 
 methods {
-    onFlashLoan(address, address, uint256, uint256, bytes) => HAVOC_ALL
-
-    _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount);
+    maxFlashLoan(address) returns(uint256) envfree
+    _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount)
 }
 
 ghost mapping(address => uint256) trackedBurnAmount;
@@ -15,7 +14,7 @@ function specBurn(address account, uint256 amount) returns bool {   // retuns ne
 
 
 // STATUS - verified
-// fee + flashLoan amount is burned
+// Check that if flashLoan() call is successful, then proper amount of tokens was burnt(fee + flashLoan amount)
 rule letsWatchItBurns(env e){
     address receiver; address token; uint256 amount; bytes data;
 
@@ -26,4 +25,4 @@ rule letsWatchItBurns(env e){
     uint256 burned = trackedBurnAmount[receiver];
 
     assert to_mathint(amount + feeBefore) == burned, "cheater";
-}
+}

certora/specs/TimelockController.spec

@@ -1,8 +1,7 @@
-using AccessControlHarness as AC
-
 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
@@ -10,6 +9,8 @@ methods {
     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)
 }
 
 ////////////////////////////////////////////////////////////////////////////
@@ -76,7 +77,7 @@ 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 < 4;
+    require data.length < 7;
     // uint256 freshIndex;
     // require freshIndex <= data.length
 
@@ -111,7 +112,7 @@ rule unsetPendingTransitionGeneral(method f, env e){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // unset() -> pending() via schedule() and scheduleBatch() only
 rule unsetPendingTransitionMethods(method f, env e){
     bytes32 id;
@@ -178,8 +179,8 @@ rule doneToNothingTransition(method f, env e){
 
 
 // STATUS - verified
-// only TimelockController contract can change minDealy
-rule minDealyOnlyChange(method f, env e){
+// only TimelockController contract can change minDelay
+rule minDelayOnlyChange(method f, env e){
     uint256 delayBefore = _minDelay();    
 
     calldataarg args;
@@ -191,7 +192,7 @@ rule minDealyOnlyChange(method f, env e){
 }
 
 
-// STATUS - in progress (need working hash)
+// STATUS - in progress 
 // execute() is the only way to set timestamp to 1
 rule getTimestampOnlyChange(method f, env e){
     bytes32 id;
@@ -211,7 +212,7 @@ rule getTimestampOnlyChange(method f, env e){
 }
 
 
-// STATUS - in progress (need working hash)
+// STATUS - verified
 // scheduled operation timestamp == block.timestamp + delay (kind of unit test)
 rule scheduleCheck(method f, env e){
     bytes32 id;
@@ -219,16 +220,15 @@ rule scheduleCheck(method f, env e){
     address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
 
     require getTimestamp(id) < e.block.timestamp;
-    // require getMinDelay() > 0;  
     hashIdCorrelation(id, target, value, data, predecessor, salt);
 
     schedule(e, target, value, data, predecessor, salt, delay);
 
-    assert getTimestamp(id) == to_uint256(e.block.timestamp + getMinDelay()), "Time doesn't obey to mortal souls";
+    assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls";
 }
 
 
-// STATUS - in progress (need working hash)
+// STATUS - verified
 // Cannot call execute on a pending (not ready) operation
 rule cannotCallExecute(method f, env e){
     address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
@@ -243,9 +243,9 @@ rule cannotCallExecute(method f, env e){
 }
 
 
-// STATUS - in progress
+// STATUS - verified
 // in unset() execute() reverts
-rule executeRevertFromUnset(method f, env e, env e2){
+rule executeRevertsFromUnset(method f, env e, env e2){
     address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
     bytes32 id;
 
@@ -258,9 +258,9 @@ rule executeRevertFromUnset(method f, env e, env e2){
 }
 
 
-// STATUS - 
+// STATUS - verified
 // Execute reverts => state returns to pending
-rule executeRevertEffectCheck(method f, env e){
+rule executeRevertsEffectCheck(method f, env e){
     address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
     bytes32 id;
 
@@ -289,21 +289,47 @@ rule cancelledNotExecuted(method f, env e){
 }
 
 
-// STATUS - in progress (add schedule batch)
+// STATUS - broken
 // Only proposers can schedule an operation
-rule onlyProposer(method f, env e){
+rule onlyProposerCertorafallbackFail(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes32, 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;
 
-    require unset(id);
-    hashIdCorrelation(id, target, value, data, predecessor, salt);
+    // 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);
+
+    bool isScheduleReverted = lastReverted;
+
+    assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected";
+}
+
+
+// STATUS - verified
+// Only proposers can schedule an operation
+rule onlyProposer1(method f, env e){
+    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;
+
+    // hashIdCorrelation(id, target, value, data, predecessor, salt);
 
-    AC._checkRole@withrevert(e, role);
+    _checkRole@withrevert(e, PROPOSER_ROLE());
 
     bool isCheckRoleReverted = lastReverted;
     
-    schedule@withrevert(e, target, value, data, predecessor, salt, delay);
+    // schedule@withrevert(e, target, value, data, predecessor, salt, delay);
+    scheduleBatch@withrevert(e, targets, values, datas, predecessor, salt, delay);
 
     bool isScheduleReverted = lastReverted;