Updated contract deposit_erc20

contracts/deposit_erc20/certora/always-depletable.spec

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
+
+rule always_depletable {
+    env e;
+
+    require(e.msg.sender != 0);
+    require(e.msg.sender != currentContract);
+    require(e.msg.value == 0);
+
+    uint amount = currentContract.token.balanceOf(e, currentContract);
+    require(max_uint >= amount + currentContract.token.balanceOf(e, e.msg.sender));
+    require(currentContract.sent + amount <= max_uint);
+
+    withdraw@withrevert(e, amount);
+
+    assert !lastReverted;
+    assert (currentContract.token.balanceOf(e, currentContract) == 0);
+}

contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf

@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/always-depletable.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}

contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf

@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/deposit-deposit-revert.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}

contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf

@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/no-deposit-twice.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}

contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf

@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-contract-bal.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}

contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf

@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-leq-init-bal.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}

contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf

@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-not-revert.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}

contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf

@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-sender-rcv.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}

contracts/deposit_erc20/certora/deposit-deposit-revert.spec

@@ -0,0 +1,15 @@
+import "helper/erc20.spec";
+
+rule deposit_deposit_revert {
+    env e1;
+    env e2;
+
+    method f;
+    calldataarg args;
+
+    deposit(e1);
+    f(e2, args);
+
+    assert f.selector != sig:deposit().selector;
+}
+

contracts/deposit_erc20/certora/getters.sol

@@ -1,15 +1 @@
-function getBalance() public view returns (uint) {
-    return token.balanceOf(address(this));
-}
 
-function getAddressBalance(address addr) public view returns (uint) {
-    return token.balanceOf(addr);
-}
-
-function getSent() public view returns (uint) {
-    return sent;
-}
-
-function getInitialDeposit() public view returns (uint) {
-    return initial_deposit;
-}

contracts/deposit_erc20/certora/helper/erc20.spec

@@ -0,0 +1,20 @@
+/***
+ * This spec file adds `DISPATCHER` summaries for the methods in the ERC20
+ * specification.  It is useful for writing specifications that work with
+ * arbitrary ERC20 contracts; if using it, you should add a variety of ERC20
+ * implementations to the scene.
+ *
+ * See [Using DISPATCHER for ERC20 contracts][guide] in the user guide for more
+ * information.
+ *
+ * [guide]: https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#using-dispatcher-for-erc20-contracts
+ */
+
+methods {
+    function _.totalSupply()                         external => DISPATCHER(true);
+    function _.balanceOf(address)                    external => DISPATCHER(true);
+    function _.allowance(address,address)            external => DISPATCHER(true);
+    function _.approve(address,uint256)              external => DISPATCHER(true);
+    function _.transfer(address,uint256)             external => DISPATCHER(true);
+    function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
+}

contracts/deposit_erc20/certora/methods.spec

@@ -1,7 +1 @@
-methods {
-    function withdraw(uint) external;
-    function getBalance() external returns (uint) envfree;
-    function getAddressBalance(address) external returns (uint) envfree;
-    function getInitialDeposit() external returns (uint) envfree;
-    function getSent() external returns (uint) envfree;
-}
+

contracts/deposit_erc20/certora/no-deposit-twice.spec

@@ -1,13 +1,11 @@
-rule no_deposit_twice {
-    env e1;
-    env e2;
-
-    method f;
-    calldataarg args;
+persistent ghost bool multiple_deposit {
+    init_state axiom multiple_deposit == false;
+}
 
-    deposit(e1);
-    f(e2, args);
-
-    assert f.selector != sig:deposit().selector;
+hook Sstore ever_deposited bool value (bool old_value) { 
+    if(old_value && value)
+        multiple_deposit = true;
 }
 
+invariant no_deposit_twice()
+    !multiple_deposit;

contracts/deposit_erc20/certora/wd-contract-bal.spec

@@ -1,15 +1,20 @@
 // SPDX-License-Identifier: GPL-3.0-only
+import "./helper/erc20.spec";
 
 rule wd_contract_bal {
     env e;
     uint amount;
     mathint mi_amount = amount;
-
-    mathint before = getBalance();
+    mathint before = currentContract.token.balanceOf(e, currentContract);
     require before >= mi_amount;
 
     withdraw(e, amount);
 
-    mathint after = getBalance();
-    assert before == after + mi_amount;
+    mathint after = currentContract.token.balanceOf(e, currentContract);
+    if(e.msg.sender == currentContract) {
+        assert before == after;
+    }
+    else {
+        assert before == after + mi_amount;
+    }
 }

contracts/deposit_erc20/certora/wd-leq-init-bal.spec

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
 
 invariant wd_leq_init_bal()
-    getSent() <= getInitialDeposit();
+    currentContract.sent <= currentContract.initial_deposit;

contracts/deposit_erc20/certora/wd-not-revert.spec

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
+
+rule wd_not_revert {
+    env e;
+    uint amount;
+    uint before = currentContract.token.balanceOf(e, currentContract);
+
+    require(e.msg.sender != 0);
+    require(e.msg.value == 0);
+
+    require(max_uint >= amount + currentContract.token.balanceOf(e, e.msg.sender));
+    require(currentContract.sent + amount + before <= max_uint);
+    require(amount <= before);
+
+    withdraw@withrevert(e, amount);
+
+    assert !lastReverted;
+}

contracts/deposit_erc20/certora/wd-sender-rcv.spec

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
+
+rule wd_sender_rcv {
+    env e;
+    uint amount;
+    address sender = e.msg.sender;
+
+    mathint before = currentContract.token.balanceOf(e, sender);
+    withdraw(e, amount);
+    mathint after = currentContract.token.balanceOf(e, sender);
+
+    if(e.msg.sender != currentContract)
+        assert after == before + amount;
+    else
+        assert after == before;
+}

contracts/deposit_erc20/ground-truth.csv

@@ -1,7 +1,8 @@
 property,version,truth,footnote-md
+always-depletable,v1,1,
+deposit-deposit-revert,v1,1,
 no-deposit-twice,v1,1,
-no-deposit-twice,v2,1,
 wd-leq-init-bal,v1,0,"This property should not hold for ERC20 tokens, since one can easily increase the contract balance without the contract being able to notice or prevent it. Since this is also possible with ETH (via coinbase or `selfdestruct` transactions), the behavior is comparable for the purposes of these tests."
-wd-leq-init-bal,v2,0,
 wd-contract-bal,v1,1,
-wd-contract-bal,v2,1,
+wd-not-revert,v1,1
+wd-sender-rcv,v1,1

contracts/deposit_erc20/hardhat/DepositERC20.sol

@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity >= 0.8.2;
+
+import "./ERC20v1.sol";
+
+/// @custom:version conformant to specification.
+contract TokenTransfer {
+    ERC20 token;
+    bool ever_deposited;
+
+    uint private sent;
+    uint initial_deposit;
+
+    // ghost variables
+    uint _count_deposit;
+
+    constructor(ERC20 token_) {
+        token = token_;
+    }
+
+    function deposit() public {
+        require(!ever_deposited);
+
+        ever_deposited = true;
+        uint allowance = token.allowance(msg.sender, address(this));
+        token.transferFrom(msg.sender, address(this), allowance);
+
+        initial_deposit = token.totalSupply();
+
+        _count_deposit += 1;	
+    }
+
+    function withdraw(uint amount) public {
+        sent += amount;
+        token.transfer(msg.sender, amount);
+    }
+
+    function getBalance() public view returns (uint) {
+        return token.balanceOf(address(this));
+    }
+
+    function getAddressBalance(address addr) public view returns (uint) {
+        return token.balanceOf(addr);
+    }
+
+    function getSent() public view returns (uint) {
+        return sent;
+    }
+
+    function getInitialDeposit() public view returns (uint) {
+        return initial_deposit;
+    }
+
+}