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

certora/munged/governance/TimelockController.sol

@@ -353,11 +353,4 @@ contract TimelockController is AccessControl {
         emit MinDelayChange(_minDelay, newDelay);
         _minDelay = newDelay;
     }
-
-
-
-    function scheduleCheck1(bytes32 id) public virtual onlyRole(PROPOSER_ROLE) {
-        bool tmp = false;
-        require(tmp);
-    }
 } 

certora/munged/token/ERC1155/ERC1155.sol

@@ -268,7 +268,7 @@ contract ERC1155 is Context, ERC165, IERC1155, IERC1155MetadataURI {
         uint256 id,
         uint256 amount,
         bytes memory data
-    ) internal virtual {
+    ) public virtual {              // HARNESS: internal -> public
         require(to != address(0), "ERC1155: mint to the zero address");
 
         address operator = _msgSender();
@@ -299,7 +299,7 @@ contract ERC1155 is Context, ERC165, IERC1155, IERC1155MetadataURI {
         uint256[] memory ids,
         uint256[] memory amounts,
         bytes memory data
-    ) internal virtual {
+    ) public virtual {                    // HARNESS: internal -> public
         require(to != address(0), "ERC1155: mint to the zero address");
         require(ids.length == amounts.length, "ERC1155: ids and amounts length mismatch");
 
@@ -330,7 +330,7 @@ contract ERC1155 is Context, ERC165, IERC1155, IERC1155MetadataURI {
         address from,
         uint256 id,
         uint256 amount
-    ) internal virtual {
+    ) public virtual {                // HARNESS: internal -> public
         require(from != address(0), "ERC1155: burn from the zero address");
 
         address operator = _msgSender();
@@ -361,7 +361,7 @@ contract ERC1155 is Context, ERC165, IERC1155, IERC1155MetadataURI {
         address from,
         uint256[] memory ids,
         uint256[] memory amounts
-    ) internal virtual {
+    ) public virtual {                    // HARNESS: internal -> public
         require(from != address(0), "ERC1155: burn from the zero address");
         require(ids.length == amounts.length, "ERC1155: ids and amounts length mismatch");
 
@@ -465,7 +465,7 @@ contract ERC1155 is Context, ERC165, IERC1155, IERC1155MetadataURI {
         uint256 id,
         uint256 amount,
         bytes memory data
-    ) private {
+    ) public {                     // HARNESS: private -> public
         if (to.isContract()) {
             try IERC1155Receiver(to).onERC1155Received(operator, from, id, amount, data) returns (bytes4 response) {
                 if (response != IERC1155Receiver.onERC1155Received.selector) {
@@ -486,7 +486,7 @@ contract ERC1155 is Context, ERC165, IERC1155, IERC1155MetadataURI {
         uint256[] memory ids,
         uint256[] memory amounts,
         bytes memory data
-    ) private {
+    ) public {                      // HARNESS: private -> public
         if (to.isContract()) {
             try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns (
                 bytes4 response

certora/scripts/verifyAccessControl.sh

@@ -0,0 +1,9 @@
+certoraRun \
+    certora/harnesses/AccessControlHarness.sol \
+    --verify AccessControlHarness:certora/specs/AccessControl.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --staging \
+    --rule_sanity \
+    --msg "modifier check"
+    

certora/scripts/verifyERC1155.sh

@@ -0,0 +1,11 @@
+certoraRun \
+    certora/munged/token/ERC1155/ERC1155.sol \
+    --verify ERC1155:certora/specs/ERC1155.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --staging \
+    --rule_sanity \
+    --rule "$1" \
+    --msg "$1 check"
+    

certora/scripts/verifyTimelock.sh

@@ -3,8 +3,9 @@ certoraRun \
     --verify TimelockControllerHarness:certora/specs/TimelockController.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --staging alex/unify-hash-functions \
+    --loop_iter 3 \
+    --staging alex/new-dt-hashing-alpha \
     --rule_sanity \
     --rule "$1" \
-    --msg "$1 false check with hash"
-    
+    --msg "$1"
+      

certora/specs/AccessControl.spec

@@ -0,0 +1,85 @@
+methods {
+    grantRole(bytes32, address)
+    revokeRole(bytes32, address)
+    _checkRole(bytes32)
+    safeTransferFrom(address, address, uint256, uint256, bytes)
+    safeBatchTransferFrom(address, address, uint256[], uint256[], bytes)
+
+    getRoleAdmin(bytes32) returns(bytes32) envfree
+    hasRole(bytes32, address) returns(bool) envfree
+} 
+
+
+// STATUS - verified
+// check onlyRole modifier for grantRole()
+rule onlyRoleModifierCheckGrant(env e){
+    bytes32 role; address account;
+
+    _checkRole@withrevert(e, getRoleAdmin(role));
+    bool checkRevert = lastReverted;
+
+    grantRole@withrevert(e, role, account);
+    bool grantRevert = lastReverted;
+
+    assert checkRevert => grantRevert, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// check onlyRole modifier for revokeRole()
+rule onlyRoleModifierCheckRevoke(env e){
+    bytes32 role; address account;
+
+    _checkRole@withrevert(e, getRoleAdmin(role));
+    bool checkRevert = lastReverted;
+
+    revokeRole@withrevert(e, role, account);
+    bool revokeRevert = lastReverted;
+
+    assert checkRevert => revokeRevert, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// grantRole() does not affect another accounts 
+rule grantRoleEffect(env e){
+    bytes32 role; address account; 
+    bytes32 anotherRole; address nonEffectedAcc;
+    require account != nonEffectedAcc;
+
+    bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
+
+    grantRole(e, role, account);
+
+    bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
+
+    assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// grantRole() does not affect another accounts 
+rule revokeRoleEffect(env e){
+    bytes32 role; address account; 
+    bytes32 anotherRole; address nonEffectedAcc;
+    require account != nonEffectedAcc;
+
+    bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
+
+    revokeRole(e, role, account);
+
+    bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
+
+    assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
+}
+
+
+
+
+
+
+
+
+
+
+

certora/specs/ERC1155.spec

@@ -0,0 +1,563 @@
+methods {
+    isApprovedForAll(address, address) returns(bool) envfree
+    balanceOf(address, uint256) returns(uint256) envfree
+    balanceOfBatch(address[], uint256[]) returns(uint256[]) envfree
+    _doSafeBatchTransferAcceptanceCheck(address, address, address, uint256[], uint256[], bytes) envfree
+    _doSafeTransferAcceptanceCheck(address, address, address, uint256, uint256, bytes) envfree
+
+    setApprovalForAll(address, bool)
+    safeTransferFrom(address, address, uint256, uint256, bytes)
+    safeBatchTransferFrom(address, address, uint256[], uint256[], bytes)
+    _mint(address, uint256, uint256, bytes)
+    _mintBatch(address, uint256[], uint256[], bytes)
+    _burn(address, uint256, uint256)
+    _burnBatch(address, uint256[], uint256[])
+}
+
+
+
+/////////////////////////////////////////////////
+// Approval
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// Function $f, which is not setApprovalForAll, should not change approval
+rule unexpectedAllowanceChange(method f, env e) filtered { f -> f.selector != setApprovalForAll(address, bool).selector } {
+    address account; address operator;
+    bool approveBefore = isApprovedForAll(account, operator); 
+
+    calldataarg args;
+    f(e, args);
+
+    bool approveAfter = isApprovedForAll(account, operator);
+
+    assert approveBefore == approveAfter, "You couldn't get king's approval this way!";
+}   
+
+
+// STATUS - verified
+// approval can be changed only by owner
+rule onlyOwnerCanApprove(env e){
+    address owner; address operator; bool approved;
+
+    bool aprovalBefore = isApprovedForAll(owner, operator);
+
+    setApprovalForAll(e, operator, approved);
+
+    bool aprovalAfter = isApprovedForAll(owner, operator);
+
+    assert aprovalBefore != aprovalAfter => owner == e.msg.sender, "There should be only one owner";
+}
+
+
+// STATUS - verified
+// chech in which scenarios (if any) isApprovedForAll() revertes
+rule approvalRevertCases(env e){
+    address account; address operator;
+    isApprovedForAll@withrevert(account, operator);
+    assert !lastReverted, "Houston, we have a problem";
+}
+
+
+// STATUS - verified 
+// Set approval changes only one approval
+rule onlyOneAllowanceChange(method f, env e) {
+    address owner; address operator; address user; 
+    bool approved;
+
+    bool userApproveBefore = isApprovedForAll(owner, user);
+
+    setApprovalForAll(e, operator, approved);
+
+    bool userApproveAfter = isApprovedForAll(owner, user);
+
+    assert userApproveBefore != userApproveAfter => (e.msg.sender == owner && operator == user), "Imposter!";
+}   
+
+
+
+/////////////////////////////////////////////////
+// Balance
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// Function $f, which is not one of transfers, mints and burns, should not change balanceOf of a user
+rule unexpectedBalanceChange(method f, env e) 
+    filtered { f -> f.selector != safeTransferFrom(address, address, uint256, uint256, bytes).selector
+                        && f.selector != safeBatchTransferFrom(address, address, uint256[], uint256[], bytes).selector 
+                        && f.selector != _mint(address, uint256, uint256, bytes).selector 
+                        && f.selector != _mintBatch(address, uint256[], uint256[], bytes).selector  
+                        && f.selector != _burn(address, uint256, uint256).selector 
+                        && f.selector != _burnBatch(address, uint256[], uint256[]).selector } {
+    address from; uint256 id;
+    uint256 balanceBefore = balanceOf(from, id);
+
+    calldataarg args;
+    f(e, args);
+
+    uint256 balanceAfter = balanceOf(from, id);
+
+    assert balanceBefore == balanceAfter, "How you dare to take my money?";
+}   
+
+
+// STATUS - verified
+// chech in which scenarios balanceOf() revertes
+rule balanceOfRevertCases(env e){
+    address account; uint256 id;
+    balanceOf@withrevert(account, id);
+    assert lastReverted => account == 0, "Houston, we have a problem";
+}
+
+
+// STATUS - verified
+// chech in which scenarios balanceOfBatch() revertes
+rule balanceOfBatchRevertCases(env e){
+    address[] accounts; uint256[] ids;
+    address account1; address account2; address account3;
+    uint256 id1; uint256 id2; uint256 id3;
+
+    require accounts.length == 3; 
+    require ids.length == 3; 
+
+    require accounts[0] == account1; require accounts[1] == account2; require accounts[2] == account3;
+
+    balanceOfBatch@withrevert(accounts, ids);
+    assert lastReverted => (account1 == 0 || account2 == 0 || account3 == 0), "Houston, we have a problem";
+}
+
+
+
+/////////////////////////////////////////////////
+// Transfer
+/////////////////////////////////////////////////
+
+
+// STATUS - 
+// cannot transfer more than `from` balance (safeTransferFrom version)
+rule cannotTransferMoreSingle(env e){
+    address from; address to; uint256 id; uint256 amount; bytes data;
+    uint256 balanceBefore = balanceOf(from, id);
+
+    safeTransferFrom@withrevert(e, from, to, id, amount, data);
+
+    assert amount > balanceBefore => lastReverted, "Achtung! Scammer!";
+    assert to == 0 => lastReverted, "Achtung! Scammer!";
+}
+
+
+// STATUS - 
+// cannot transfer more than allowed (safeBatchTransferFrom version)
+rule cannotTransferMoreBatch(env e){
+    address from; address to; uint256[] ids; uint256[] amounts; bytes data;
+    uint256 idToCheck1; uint256 amountToCheck1;
+    uint256 idToCheck2; uint256 amountToCheck2;
+    uint256 idToCheck3; uint256 amountToCheck3;
+
+    uint256 balanceBefore1 = balanceOf(from, idToCheck1);
+    uint256 balanceBefore2 = balanceOf(from, idToCheck2);
+    uint256 balanceBefore3 = balanceOf(from, 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;
+
+    safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);
+
+    assert (amountToCheck1 > balanceBefore1 || amountToCheck2 > balanceBefore2 || amountToCheck2 > balanceBefore2) => lastReverted, "Achtung! Scammer!";
+}
+
+
+// STATUS - (added debug vars)
+// 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;
+
+    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){
+    address from; address to; address other;
+    uint256 id; uint256 amount; 
+    bytes data;
+
+    require other != to;
+    require amount > 0;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 otherBalanceAfter = balanceOf(other, id);
+
+    assert from != other => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!";
+}
+
+
+// STATUS - 
+// 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;
+    uint256 id; uint256 amount; 
+    bytes data;
+
+    require from != other;
+
+    uint256 otherBalanceBefore = balanceOf(other, id);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    uint256 otherBalanceAfter = balanceOf(other, id);
+
+    assert other != to => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!";
+}
+
+
+// STATUS - 
+// 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;
+    uint256[] ids; uint256[] amounts;
+    uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3;
+    bytes data;
+
+    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);
+
+    safeBatchTransferFrom(e, from, to, ids, amounts, data);
+
+    uint256 otherBalanceAfter1 = balanceOf(other, id1);
+    uint256 otherBalanceAfter2 = balanceOf(other, id2);
+    uint256 otherBalanceAfter3 = balanceOf(other, id3);
+
+    assert from != other => (otherBalanceBefore1 == otherBalanceAfter1 
+                                && otherBalanceBefore2 == otherBalanceAfter2 
+                                && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!";
+}
+
+
+// STATUS - 
+// 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;
+    uint256[] ids; uint256[] amounts;
+    uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3;
+    bytes data;
+
+    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);
+
+    safeBatchTransferFrom(e, from, 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), "Don't touch my money!";
+}
+
+
+// STATUS - verified
+// cannot transfer without approval (safeTransferFrom version)
+rule noTransferForNotApproved(env e) {
+    address from; address operator;
+    address to; uint256 id; uint256 amount; bytes data;
+
+    require from != e.msg.sender;
+
+    bool approve = isApprovedForAll(from, e.msg.sender);
+
+    safeTransferFrom@withrevert(e, from, to, id, amount, data);
+
+    assert !approve => lastReverted, "You don't have king's approval!";
+}   
+
+
+// STATUS - 
+// cannot transfer without approval (safeBatchTransferFrom version)
+rule noTransferBatchForNotApproved(env e) {
+    address from; address operator; address to; 
+    bytes data;
+    uint256[] ids; uint256[] amounts;
+
+    require from != e.msg.sender;
+
+    bool approve = isApprovedForAll(from, e.msg.sender);
+
+    safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);
+
+    assert !approve => lastReverted, "You don't have king's approval!";
+}   
+
+
+// STATUS - 
+// safeTransferFrom doesn't affect any approval
+rule noTransferEffectOnApproval(env e){
+    address from; address to;
+    address owner; address operator;
+    uint256 id; uint256 amount; 
+    bytes data;
+
+    bool approveBefore = isApprovedForAll(owner, operator);
+
+    safeTransferFrom(e, from, to, id, amount, data);
+
+    bool approveAfter = isApprovedForAll(owner, operator);
+
+    assert approveBefore == approveAfter, "Something was effected";
+}
+
+
+// STATUS - 
+// safeTransferFrom doesn't affect any approval
+rule noTransferBatchEffectOnApproval(env e){
+    address from; address to;
+    address owner; address operator;
+    uint256[] ids; uint256[] amounts;
+    bytes data;
+
+    bool approveBefore = isApprovedForAll(owner, operator);
+
+    safeBatchTransferFrom(e, from, to, ids, amounts, data);
+
+    bool approveAfter = isApprovedForAll(owner, operator);
+
+    assert approveBefore == approveAfter, "Something was effected";
+}
+
+
+/////////////////////////////////////////////////
+// Mint
+/////////////////////////////////////////////////
+
+
+// STATUS - verified
+// the user cannot mint more than max_uint256
+rule cantMintMoreSingle(env e){
+    address to; uint256 id; uint256 amount; bytes data;
+
+    require to_mathint(balanceOf(to, id) + amount) > max_uint256;
+
+    _mint@withrevert(e, to, id, amount, data);
+    
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// STATUS - verified
+// the user cannot mint more than max_uint256 (batch version)
+rule cantMintMoreBatch(env e){
+    address to; bytes data;
+    uint256 id1; uint256 id2; uint256 id3; 
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+
+    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 to_mathint(balanceOf(to, id1) + amount1) > max_uint256 
+                || to_mathint(balanceOf(to, id2) + amount2) > max_uint256
+                || to_mathint(balanceOf(to, id3) + amount3) > max_uint256;
+
+    _mintBatch@withrevert(e, to, ids, amounts, data);
+    
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// 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";
+// }
+
+
+
+/////////////////////////////////////////////////
+// Burn
+/////////////////////////////////////////////////
+
+
+// STATUS - 
+// check that burn updates `from` balance correctly
+rule burnCorrectWork(env e){
+    address from; uint256 id; uint256 amount;
+
+    uint256 otherBalanceBefore = balanceOf(from, id);
+
+    _burn(e, from, id, amount);
+
+    uint256 otherBalanceAfter = balanceOf(from, id);
+    
+    assert otherBalanceBefore == otherBalanceAfter + amount, "Something is wrong";
+}
+
+
+// STATUS - 
+// check that burnBatch updates `from` balance correctly
+rule burnBatchCorrectWork(env e){
+    address from;
+    uint256 id1; uint256 id2; uint256 id3; 
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    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;
+    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;
+
+    uint256 otherBalanceBefore1 = balanceOf(from, id1);
+    uint256 otherBalanceBefore2 = balanceOf(from, id2);
+    uint256 otherBalanceBefore3 = balanceOf(from, id3);
+
+    _burnBatch(e, from, ids, amounts);
+
+    uint256 otherBalanceAfter1 = balanceOf(from, id1);
+    uint256 otherBalanceAfter2 = balanceOf(from, id2);
+    uint256 otherBalanceAfter3 = balanceOf(from, 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 cantBurnMoreSingle(env e){
+    address from; uint256 id; uint256 amount;
+
+    require to_mathint(balanceOf(from, id) - amount) < 0;
+
+    _burn@withrevert(e, from, id, amount);
+    
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// 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)
+rule cantBurnMoreBatch(env e){
+    address from;
+    uint256 id1; uint256 id2; uint256 id3; 
+    uint256 amount1; uint256 amount2; uint256 amount3;
+    uint256[] ids; uint256[] amounts;
+
+    require ids.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 to_mathint(balanceOf(from, id1) - amount1) < 0 
+                || to_mathint(balanceOf(from, id2) - amount2) < 0 
+                || to_mathint(balanceOf(from, id3) - amount3) < 0 ;
+
+    _burnBatch@withrevert(e, from, ids, amounts);
+    
+    assert lastReverted, "Don't be too greedy!";
+}
+
+
+// STATUS - 
+// burnBatch changes only `from` balance
+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);
+
+    _burnBatch(e, from, ids, amounts);
+
+    uint256 otherBalanceAfter1 = balanceOf(other, id1);
+    uint256 otherBalanceAfter2 = balanceOf(other, id2);
+    uint256 otherBalanceAfter3 = balanceOf(other, id3);
+    
+    assert other != from => (otherBalanceBefore1 == otherBalanceAfter1 
+                                || otherBalanceBefore2 == otherBalanceAfter2 
+                                || otherBalanceBefore3 == otherBalanceAfter3)
+                                , "I like to see your money disappearing";
+}

certora/specs/TimelockController.spec

@@ -5,16 +5,13 @@ methods {
     _DONE_TIMESTAMP() returns(uint256) envfree
     _minDelay() returns(uint256) envfree
     getMinDelay() returns(uint256) envfree
+    hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree
     
     cancel(bytes32)
-    schedule(address, uint256, bytes, bytes32, bytes32, uint256)
+    schedule(address, uint256, bytes32, bytes32, bytes32, uint256)
     execute(address, uint256, bytes, bytes32, bytes32)
-
-    hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree // => uniqueHashGhost(target, value, data, predecessor, salt)
 }
 
-
-
 ////////////////////////////////////////////////////////////////////////////
 //                       Definitions                                      //
 ////////////////////////////////////////////////////////////////////////////
@@ -45,6 +42,19 @@ function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data
 }
 
 
+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                                       //
 ////////////////////////////////////////////////////////////////////////////
@@ -63,22 +73,24 @@ function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data
 
 
 rule keccakCheck(method f, env e){
-    address target;
-    uint256 value;
-    bytes data;
-    bytes32 predecessor;
-    bytes32 salt;
+    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
+    address targetRand; uint256 valueRand; bytes dataRand; bytes32 predecessorRand; bytes32 saltRand;
+
+    require data.length < 4;
+    // uint256 freshIndex;
+    // require freshIndex <= data.length
 
-    require data.length < 3;
+    // 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";
 }
 
 
-
 /////////////////////////////////////////////////////////////
 // STATE TRANSITIONS
 /////////////////////////////////////////////////////////////
@@ -99,7 +111,7 @@ rule unsetPendingTransitionGeneral(method f, env e){
 }
 
 
-// STATUS - verified
+// STATUS - 
 // unset() -> pending() via schedule() and scheduleBatch() only
 rule unsetPendingTransitionMethods(method f, env e){
     bytes32 id;
@@ -109,8 +121,10 @@ rule unsetPendingTransitionMethods(method f, env e){
     calldataarg args;
     f(e, args);
 
-    assert pending(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?";
+    bool tmp = pending(id);
+
+    assert pending(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?";
 }
 
 
@@ -181,17 +195,19 @@ rule minDealyOnlyChange(method f, env e){
 // 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 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);
 
-    require getTimestamp(id) != 1;
     hashIdCorrelation(id, target, value, data, predecessor, salt);
 
-    calldataarg args;
-    // write helper function with values from hashOperation() call;
-    f(e, args);
+    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?";
+                                        || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?";
 }
 
 
@@ -233,20 +249,16 @@ rule executeRevertFromUnset(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 data.length < 4;
-    // require hashOperation(target, value, data, predecessor, salt) == id;
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
     require unset(id);
 
-    scheduleCheck1@withrevert(e, id);
-
-    // execute@withrevert(e, target, value, data, predecessor, salt);
+    execute@withrevert(e, target, value, data, predecessor, salt);
 
     assert lastReverted, "you go against execution nature";
 }
 
 
-// STATUS - verified
+// STATUS - 
 // Execute reverts => state returns to pending
 rule executeRevertEffectCheck(method f, env e){
     address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;