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

certora/harnesses/AccessControlHarness.sol

@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts (last updated v4.5.0) (access/AccessControl.sol)
+
+pragma solidity ^0.8.0;
+
+import "../munged/access/AccessControl.sol";
+
+contract AccessControlHarness is AccessControl {
+    
+}

certora/harnesses/ERC20FlashMintHarness.sol

@@ -0,0 +1,5 @@
+import "../munged/token/ERC20/extensions/ERC20FlashMint.sol";
+
+contract ERC20FlashMintHarness is ERC20FlashMint {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) {}
+}

certora/harnesses/ERC20WrapperHarness.sol

@@ -6,5 +6,12 @@ contract ERC20WrapperHarness is ERC20Wrapper {
         ERC20Wrapper(underlyingToken)
         ERC20(_name, _symbol)
     {}
-}
 
+    function underlyingTotalSupply() public view returns (uint256) {
+        return underlying.totalSupply();
+    }
+
+    function underlyingBalanceOf(address account) public view returns (uint256) {
+        return underlying.balanceOf(account);
+    }
+}

certora/harnesses/IERC3156FlashBorrowerHarness.sol

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.4.1 (interfaces/IERC3156FlashBorrower.sol)
+
+import "../munged/interfaces/IERC3156FlashBorrower.sol";
+
+pragma solidity ^0.8.0;
+
+contract IERC3156FlashBorrowerHarness is IERC3156FlashBorrower {
+    bytes32 somethingToReturn;
+
+    function onFlashLoan(
+        address initiator,
+        address token,
+        uint256 amount,
+        uint256 fee,
+        bytes calldata data
+    ) external override returns (bytes32){
+        return somethingToReturn;
+    }
+}

certora/helpers/DummyERC20A.sol

@@ -0,0 +1,5 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+import "./DummyERC20Impl.sol";
+
+contract DummyERC20A is DummyERC20Impl {}

certora/helpers/DummyERC20B.sol

@@ -0,0 +1,5 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+import "./DummyERC20Impl.sol";
+
+contract DummyERC20B is DummyERC20Impl {}

certora/helpers/DummyERC20Impl.sol

@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+// with mint
+contract DummyERC20Impl {
+    uint256 t;
+    mapping (address => uint256) b;
+    mapping (address => mapping (address => uint256)) a;
+
+    string public name;
+    string public symbol;
+    uint public decimals;
+
+    function myAddress() public returns (address) {
+        return address(this);
+    }
+
+    function add(uint a, uint b) internal pure returns (uint256) {
+        uint c = a +b;
+        require (c >= a);
+        return c;
+    }
+    function sub(uint a, uint b) internal pure returns (uint256) {
+        require (a>=b);
+        return a-b;
+    }
+
+    function totalSupply() external view returns (uint256) {
+        return t;
+    }
+    function balanceOf(address account) external view returns (uint256) {
+        return b[account];
+    }
+    function transfer(address recipient, uint256 amount) external returns (bool) {
+        b[msg.sender] = sub(b[msg.sender], amount);
+        b[recipient] = add(b[recipient], amount);
+        return true;
+    }
+    function allowance(address owner, address spender) external view returns (uint256) {
+        return a[owner][spender];
+    }
+    function approve(address spender, uint256 amount) external returns (bool) {
+        a[msg.sender][spender] = amount;
+        return true;
+    }
+
+    function transferFrom(
+        address sender,
+        address recipient,
+        uint256 amount
+    ) external returns (bool) {
+        b[sender] = sub(b[sender], amount);
+        b[recipient] = add(b[recipient], amount);
+        a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
+        return true;
+    }
+}

certora/munged/access/AccessControl.sol

@@ -93,7 +93,7 @@ abstract contract AccessControl is Context, IAccessControl, ERC165 {
      *
      * _Available since v4.6._
      */
-    function _checkRole(bytes32 role) internal view virtual {
+    function _checkRole(bytes32 role) public view virtual {         // HARNESS: internal -> public
         _checkRole(role, _msgSender());
     }
 

certora/munged/governance/TimelockController.sol

@@ -24,10 +24,10 @@ contract TimelockController is AccessControl {
     bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE");
     bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
     bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
-    uint256 internal constant _DONE_TIMESTAMP = uint256(1);
+    uint256 public constant _DONE_TIMESTAMP = uint256(1);                           // HARNESS: internal -> public
 
     mapping(bytes32 => uint256) private _timestamps;
-    uint256 private _minDelay;
+    uint256 public _minDelay;                                                       // HARNESS: private -> public
 
     /**
      * @dev Emitted when a call is scheduled as part of operation `id`.
@@ -353,4 +353,11 @@ 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/ERC20/ERC20.sol

@@ -277,7 +277,7 @@ contract ERC20 is Context, IERC20, IERC20Metadata {
      * - `account` cannot be the zero address.
      * - `account` must have at least `amount` tokens.
      */
-    function _burn(address account, uint256 amount) internal virtual {
+    function _burn(address account, uint256 amount) public virtual returns (bool) {          // HARNESS: internal -> public
         require(account != address(0), "ERC20: burn from the zero address");
 
         _beforeTokenTransfer(account, address(0), amount);
@@ -292,6 +292,8 @@ contract ERC20 is Context, IERC20, IERC20Metadata {
         emit Transfer(account, address(0), amount);
 
         _afterTokenTransfer(account, address(0), amount);
+
+        return true;
     }
 
     /**

certora/munged/token/ERC20/extensions/ERC20FlashMint.sol

@@ -40,9 +40,11 @@ abstract contract ERC20FlashMint is ERC20, IERC3156FlashLender {
         require(token == address(this), "ERC20FlashMint: wrong token");
         // silence warning about unused variable without the addition of bytecode.
         amount;
-        return 0;
+        return fee;                 // HARNESS: made "return" nonzero
     }
 
+    uint256 public fee;             // HARNESS: added it to simulate random fee amount
+
     /**
      * @dev Performs a flash loan. New tokens are minted and sent to the
      * `receiver`, who is required to implement the {IERC3156FlashBorrower}
@@ -70,7 +72,7 @@ abstract contract ERC20FlashMint is ERC20, IERC3156FlashLender {
         uint256 fee = flashFee(token, amount);
         _mint(address(receiver), amount);
         require(
-            receiver.onFlashLoan(msg.sender, token, amount, fee, data) == _RETURN_VALUE,
+            receiver.onFlashLoan(msg.sender, token, amount, fee, data) == _RETURN_VALUE,        // HAVOC_ALL
             "ERC20FlashMint: invalid return value"
         );
         uint256 currentAllowance = allowance(address(receiver), address(this));

certora/munged/token/ERC20/extensions/ERC20Wrapper.sol

@@ -44,7 +44,7 @@ abstract contract ERC20Wrapper is ERC20 {
      * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
      * function that can be exposed with access control if desired.
      */
-    function _recover(address account) internal virtual returns (uint256) {
+    function _recover(address account) public virtual returns (uint256) {           // HARNESS: internal -> public
         uint256 value = underlying.balanceOf(address(this)) - totalSupply();
         _mint(account, value);
         return value;

certora/scripts/verifyERC20FlashMint.sh

@@ -0,0 +1,10 @@
+certoraRun \
+    certora/harnesses/ERC20FlashMintHarness.sol certora/harnesses/IERC3156FlashBorrowerHarness.sol \
+    certora/munged/token/ERC20/ERC20.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \
+    --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --staging \
+    --rule_sanity \
+    --msg "letsWatchItBurns"
+    

certora/scripts/verifyERC20Wrapper.sh

@@ -0,0 +1,10 @@
+certoraRun \
+    certora/harnesses/ERC20WrapperHarness.sol \
+    certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \
+    --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --staging \
+    --rule_sanity \
+    --msg "all check"
+    

certora/scripts/verifyTimelock.sh

@@ -1,7 +1,10 @@
 certoraRun \
-    certora/harnesses/TimelockControllerHarness.sol \
+    certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \
     --verify TimelockControllerHarness:certora/specs/TimelockController.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --cloud \
+    --staging alex/unify-hash-functions \
-    --msg "sanity"
+    --rule_sanity \
+    --rule "$1" \
+    --msg "$1 false check with hash"
+    

certora/specs/ERC20FlashMint.spec

@@ -0,0 +1,37 @@
+import "erc20.spec"
+
+methods {
+    onFlashLoan(address, address, uint256, uint256, bytes) => HAVOC_ALL // HAVOC_ECF
+
+    _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount);
+}
+
+ghost mapping(address => uint256) trackedBurnAmount;
+
+function specBurn(address account, uint256 amount) returns bool {   // retuns needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'"
+    trackedBurnAmount[account] = amount;
+    return true;
+}
+
+// ghost to save args that were passed to burn function
+// summarize burn
+// assert ghost == amount + fee
+
+
+// STATUS - in progress
+// HAVOC_ALL - everything is havoced => violation
+// HAVOC_ECF - verified
+// https://vaas-stg.certora.com/output/3106/8795450b626f2ca53a2b/?anonymousKey=dd774da10cc595e4e38357af9e4f50bf2c0cb02a
+// fee + flashLoan amount is burned
+rule letsWatchItBurns(env e){
+    address receiver; address token; uint256 amount; bytes data;
+    require amount > 0;
+
+    uint256 feeBefore = flashFee(e, token, amount);
+
+    flashLoan(e, receiver, token, amount, data);
+
+    uint256 burned = trackedBurnAmount[receiver];
+
+    assert to_mathint(amount + feeBefore) == burned, "cheater";
+}

certora/specs/ERC20Wrapper.spec

@@ -0,0 +1,203 @@
+import "erc20.spec"
+
+methods {
+    underlying() returns(address) envfree
+    underlyingTotalSupply() returns(uint256) envfree
+    underlyingBalanceOf(address) returns(uint256) envfree
+
+    depositFor(address, uint256) returns(bool)
+    withdrawTo(address, uint256) returns(bool)
+    _recover(address) returns(uint256)
+}
+
+
+// STATUS - verified
+// totalsupply of wrapped should be less than or equal to underlying (assuming no transfer they should be equal) - solvency
+invariant whatAboutTotal(env e)
+    totalSupply(e) <= underlyingTotalSupply()
+    filtered { f -> f.selector != certorafallback_0().selector }
+    {
+        preserved {
+            require underlyingBalanceOf(currentContract) <= underlyingTotalSupply();
+            require underlying() != currentContract;
+        }
+        preserved depositFor(address account, uint256 amount) with (env e2){
+            require underlyingBalanceOf(currentContract) <= underlyingTotalSupply();
+            require totalSupply(e) + amount <= underlyingTotalSupply();
+            require underlying() != currentContract;
+        }
+    }
+
+
+// STATUS - verified
+// check correct values update by depositFor()
+rule depositForSpecBasic(env e){
+    address account; uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 wrapperTotalBefore = totalSupply(e);
+    uint256 underlyingTotalBefore = underlyingTotalSupply();
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
+
+    depositFor(e, account, amount);
+
+    uint256 wrapperTotalAfter = totalSupply(e);
+    uint256 underlyingTotalAfter = underlyingTotalSupply();
+    uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract);
+
+    assert wrapperTotalBefore == wrapperTotalAfter - amount, "wrapper total wrong update";
+    assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated";
+    assert underlyingThisBalanceBefore == underlyingThisBalanceAfter - amount, "underlying this balance wrong update";
+}
+
+
+rule depositForSpecWrapper(env e){
+    address account; uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 wrapperUserBalanceBefore = balanceOf(e, account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
+
+    depositFor(e, account, amount);
+
+    uint256 wrapperUserBalanceAfter = balanceOf(e, account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
+
+    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore 
+                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter 
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount, "wrapper balances wrong update";
+    assert account != e.msg.sender => wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount
+                && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update";
+}
+
+
+rule depositForSpecUnderlying(env e){
+    address account; uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account);
+
+    depositFor(e, account, amount);
+
+    uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account);
+
+    assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore
+                && underlyingSenderBalanceAfter == underlyingUserBalanceAfter
+                && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount, "underlying balances wrong update";
+    
+    assert account != e.msg.sender && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
+                && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update";
+    
+    assert account != e.msg.sender && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
+                && underlyingUserBalanceBefore == underlyingUserBalanceAfter, "underlying balances wrong update";
+}
+
+
+// STATUS - verified
+// check correct values update by withdrawTo()
+rule withdrawToSpecBasic(env e){
+    address account; uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 wrapperTotalBefore = totalSupply(e);
+    uint256 underlyingTotalBefore = underlyingTotalSupply();
+
+    withdrawTo(e, account, amount);
+
+    uint256 wrapperTotalAfter = totalSupply(e);
+    uint256 underlyingTotalAfter = underlyingTotalSupply();
+
+    assert wrapperTotalBefore == wrapperTotalAfter + amount, "wrapper total wrong update";
+    assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated";
+}
+
+
+rule withdrawToSpecWrapper(env e){
+    address account; uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 wrapperUserBalanceBefore = balanceOf(e, account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
+
+    withdrawTo(e, account, amount);
+
+    uint256 wrapperUserBalanceAfter = balanceOf(e, account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
+    
+    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount, "wrapper user balance wrong update";
+    assert account != e.msg.sender => wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + amount
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter, "wrapper user balance wrong update";
+}
+
+
+rule withdrawToSpecUnderlying(env e){
+    address account; uint256 amount;
+
+    require e.msg.sender != currentContract;
+    require underlying() != currentContract;
+
+    uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account);
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
+
+    withdrawTo(e, account, amount);
+
+    uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender);
+    uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account);
+    uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract);
+
+    assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore 
+                && underlyingSenderBalanceAfter == underlyingUserBalanceAfter 
+                && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update (acc == sender)";
+    
+    assert account != e.msg.sender && account == currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter
+                && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter, "underlying balances wrong update (acc == contract)"; 
+    assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount
+                && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter
+                && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount, "underlying balances wrong update (acc != contract)";   
+}
+
+
+// STATUS - verified
+// check correct values update by _recover()
+rule recoverSpec(env e){
+    address account; uint256 amount; // e.msg.sender
+    require underlying() != currentContract;
+
+    require e.msg.sender != currentContract;
+
+    uint256 wrapperTotalBefore = totalSupply(e);
+    uint256 wrapperUserBalanceBefore = balanceOf(e, account);
+    uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
+
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);   
+
+    mathint value = underlyingThisBalanceBefore - wrapperTotalBefore;
+
+    _recover(e, account);
+
+    uint256 wrapperTotalAfter = totalSupply(e);
+    uint256 wrapperUserBalanceAfter = balanceOf(e, account);
+    uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
+    
+    assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update";
+    assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+                && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value, "wrapper balances wrong update";
+    assert e.msg.sender != account => wrapperUserBalanceBefore == wrapperUserBalanceAfter - value
+                && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update";
+}

certora/specs/TimelockController.spec

@@ -1,36 +1,328 @@
+using AccessControlHarness as AC
+
 methods {
-    // hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) => uniqueHashGhost(target, value, data, predecessor, salt)
+    getTimestamp(bytes32) returns(uint256) envfree
+    _DONE_TIMESTAMP() returns(uint256) envfree
+    _minDelay() returns(uint256) envfree
+    getMinDelay() returns(uint256) envfree
+    
+    cancel(bytes32)
+    schedule(address, uint256, bytes, 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)
 }
 
-// ghost uniqueHashGhost(address, uint256, bytes, bytes32, bytes32) returns bytes32;
-//
-// Assuming the hash is deterministic, and correlates the trio properly
-// function hashUniquness(address target1, uint256 value1, bytes data1, bytes32 predecessor1, bytes32 salt1, 
-//                             address target2, uint256 value2, bytes data2, bytes32 predecessor2, bytes32 salt2){
-//     require ((target1 != target2) || (value1 != value2) || (data1 != data2) || (predecessor1 != predecessor2) || (salt1 != salt2)) <=> 
-//     (uniqueHashGhost(target1, value1, data1, predecessor1, salt1) != uniqueHashGhost(target2, value2, data2, predecessor2, salt2));
-// }
-// 
-// 
-// rule keccakCheck(method f, env e){
-//     address target;
-//     uint256 value;
-//     bytes data;
-//     bytes32 predecessor;
-//     bytes32 salt;
-// 
-//     hashUniquness(target, value, data, predecessor, salt, 
-//                          target, value, data, predecessor, salt);
-// 
-//     bytes32 a = hashOperation(e, target, value, data, predecessor, salt);
-//     bytes32 b = hashOperation(e, target, value, data, predecessor, salt);
-// 
-//     assert a == b, "hashes are different";
-// }
 
-rule sanity(method f) {
+
-    env e;
+////////////////////////////////////////////////////////////////////////////
-    calldataarg arg;
+//                       Definitions                                      //
-    f(e, arg);
+////////////////////////////////////////////////////////////////////////////
-    assert false;
+
+
+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();
+
+
+
+////////////////////////////////////////////////////////////////////////////
+//                         Functions                                      //
+////////////////////////////////////////////////////////////////////////////
+
+
+function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){
+    require data.length < 7;
+    require hashOperation(target, value, data, predecessor, salt) == id;
+}
+
+
+////////////////////////////////////////////////////////////////////////////
+//                           Ghosts                                       //
+////////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////////
+//                            Invariants                                  //
+////////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////////
+//                            Rules                                       //
+////////////////////////////////////////////////////////////////////////////
+
+
+rule keccakCheck(method f, env e){
+    address target;
+    uint256 value;
+    bytes data;
+    bytes32 predecessor;
+    bytes32 salt;
+
+    require data.length < 3;
+
+    bytes32 a = hashOperation(target, value, data, predecessor, salt);
+    bytes32 b = hashOperation(target, value, data, predecessor, salt);
+
+    assert a == b, "hashes are different";
+}
+
+
+
+/////////////////////////////////////////////////////////////
+// STATE TRANSITIONS
+/////////////////////////////////////////////////////////////
+
+
+// STATUS - verified
+// unset() -> unset() || pending() only
+rule unsetPendingTransitionGeneral(method f, env e){
+    bytes32 id;
+
+    require unset(id);
+    require e.block.timestamp > 1;
+
+    calldataarg args;
+    f(e, args);
+
+    assert pending(id) || unset(id);
+}
+
+
+// STATUS - verified
+// unset() -> pending() via schedule() and scheduleBatch() only
+rule unsetPendingTransitionMethods(method f, env e){
+    bytes32 id;
+
+    require unset(id);
+
+    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?";
+}
+
+
+// STATUS - verified
+// ready() -> done() via execute() and executeBatch() only
+rule readyDoneTransition(method f, env e){
+    bytes32 id;
+
+    require ready(id, e);
+
+    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!";
+}
+
+
+// STATUS - verified
+// pending() -> cancelled() via cancel() only
+rule pendingCancelledTransition(method f, env e){
+    bytes32 id;
+
+    require pending(id);
+
+    calldataarg args;
+    f(e, args);
+
+    assert unset(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?";
+}
+
+
+// STATUS - verified
+// done() -> nowhere
+rule doneToNothingTransition(method f, env e){
+    bytes32 id;
+
+    require done(id);
+
+    calldataarg args;
+    f(e, args);
+
+    assert done(id), "Did you find a way to escape? There is no way! HA-HA-HA";
+}
+
+
+
+/////////////////////////////////////////////////////////////
+// THE REST
+/////////////////////////////////////////////////////////////
+
+
+// STATUS - verified
+// only TimelockController contract can change minDealy
+rule minDealyOnlyChange(method f, env e){
+    uint256 delayBefore = _minDelay();    
+
+    calldataarg args;
+    f(e, args);
+
+    uint256 delayAfter = _minDelay();
+
+    assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!";
+}
+
+
+// STATUS - verified
+// Only proposers can schedule an operation
+rule scheduleOnlyWay(method f, env e){
+    uint256 delayBefore = _minDelay();    
+
+    calldataarg args;
+    f(e, args);
+
+    uint256 delayAfter = _minDelay();
+
+    assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!";
+}
+
+
+// STATUS - in progress (need working hash)
+// 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;
+
+    require getTimestamp(id) != 1;
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    calldataarg args;
+    // write helper function with values from hashOperation() call;
+    f(e, args);
+
+    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 - in progress (need working hash)
+// scheduled operation timestamp == block.timestamp + delay (kind of unit test)
+rule scheduleCheck(method f, env e){
+    bytes32 id;
+
+    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
+
+    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";
+}
+
+
+// STATUS - in progress (need working hash)
+// 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;
+    bytes32 id;
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+    require pending(id) && !ready(id, e);
+
+    execute@withrevert(e, target, value, data, predecessor, salt);
+
+    assert lastReverted, "you go against execution nature";
+}
+
+
+// STATUS - in progress
+// in unset() execute() reverts
+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;
+    require unset(id);
+
+    scheduleCheck1@withrevert(e, id);
+
+    // execute@withrevert(e, target, value, data, predecessor, salt);
+
+    assert lastReverted, "you go against execution nature";
+}
+
+
+// STATUS - verified
+// Execute reverts => state returns to pending
+rule executeRevertEffectCheck(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);
+
+    execute@withrevert(e, target, value, data, predecessor, salt);
+    bool reverted = lastReverted;
+
+    assert lastReverted => pending(id) && !ready(id, e), "you go against execution nature";
+}
+
+
+// STATUS - verified
+// Canceled operations cannot be executed → can’t move from canceled to ready
+rule cancelledNotExecuted(method f, env e){
+    bytes32 id;
+
+    require unset(id);
+    require e.block.timestamp > 1;
+
+    calldataarg args;
+    f(e, args);
+
+    assert !done(id), "The ship is not a creature of the air";
+}
+
+
+// STATUS - in progress
+// Only proposers can schedule an operation
+rule onlyProposer(method f, env e){
+    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);
+
+    AC._checkRole@withrevert(e, role);
+
+    bool isCheckRoleReverted = lastReverted;
+    
+    schedule@withrevert(e, target, value, data, predecessor, salt, delay);
+
+    bool isScheduleReverted = lastReverted;
+
+    assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected";
+}
+
+
+// STATUS - in progress
+// Ready = has waited minimum period after pending 
+rule cooldown(method f, env e, env e2){
+    bytes32 id;
+
+    require unset(id);
+
+    calldataarg args;
+    f(e, args);
+
+    // 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";
 }

certora/specs/erc20.spec

@@ -0,0 +1,12 @@
+// erc20 methods
+methods {
+    name()                                returns (string)  => DISPATCHER(true)
+    symbol()                              returns (string)  => DISPATCHER(true)
+    decimals()                            returns (string)  => DISPATCHER(true)
+    totalSupply()                         returns (uint256) => DISPATCHER(true)
+    balanceOf(address)                    returns (uint256) => DISPATCHER(true)
+    allowance(address,address)            returns (uint)    => DISPATCHER(true)
+    approve(address,uint256)              returns (bool)    => DISPATCHER(true)
+    transfer(address,uint256)             returns (bool)    => DISPATCHER(true)
+    transferFrom(address,address,uint256) returns (bool)    => DISPATCHER(true)
+}