Merge pull request #195 from lefterislazar/hevm-erc20

Hevm ERC20

Author: zoep

tests/hevm/pass/erc20/erc20.act

@@ -0,0 +1,214 @@
+constructor of Token
+interface constructor(uint256 _totalSupply)
+
+iff CALLVALUE == 0
+
+creates
+
+  uint256 totalSupply := _totalSupply
+  mapping(address => uint) balanceOf :=  [CALLER := _totalSupply]
+  mapping(address=>mapping(address=>uint)) allowance := []
+
+
+behaviour transfer of Token
+interface transfer(uint256 value, address to)
+
+iff
+
+  CALLVALUE == 0
+  inRange(uint256, balanceOf[CALLER] - value)
+  CALLER =/= to => inRange(uint256, balanceOf[to] + value)
+
+case CALLER =/= to:
+
+  storage
+
+     balanceOf[CALLER] => balanceOf[CALLER] - value
+     balanceOf[to]     => balanceOf[to] + value
+
+  returns 1
+
+case CALLER == to:
+
+  returns 1
+
+
+behaviour transferFrom of Token
+interface transferFrom(address src, address dst, uint amount)
+
+iff
+
+  amount <= balanceOf[src]
+  src    =/= dst => inRange(uint256, balanceOf[dst] + amount)
+  CALLER =/= src => inRange(uint256, allowance[src][CALLER] - amount)
+  CALLVALUE == 0
+
+case src =/= dst and CALLER == src:
+
+  storage
+
+     balanceOf[src] => balanceOf[src] - amount
+     balanceOf[dst] => balanceOf[dst] + amount
+
+  returns 1
+
+case src =/= dst and CALLER =/= src and allowance[src][CALLER] == 2^256 - 1:
+
+  storage
+
+     balanceOf[src] => balanceOf[src] - amount
+     balanceOf[dst] => balanceOf[dst] + amount
+
+  returns 1
+
+case src =/= dst and CALLER =/= src and allowance[src][CALLER] < 2^256 - 1:
+
+  storage
+
+    allowance[src][CALLER] => allowance[src][CALLER] - amount
+    balanceOf[src]         => balanceOf[src] - amount
+    balanceOf[dst]         => balanceOf[dst] + amount
+
+  returns 1
+
+case src == dst and CALLER =/= src and allowance[src][CALLER] < 2^256 - 1:
+
+  storage
+
+    allowance[src][CALLER] => allowance[src][CALLER] - amount
+
+  returns 1
+
+case src == dst and (CALLER == src or allowance[src][CALLER] == 2^256 - 1):
+
+  returns 1
+
+
+behaviour approve of Token
+interface approve(address spender, uint amount)
+
+iff
+
+  inRange(uint256, amount)
+  CALLVALUE == 0
+
+case CALLER =/= spender:
+
+  storage
+
+    allowance[CALLER][spender] => amount
+
+  returns 1
+
+case CALLER == spender:
+
+  returns 1
+
+
+behaviour burn of Token
+interface burn(uint256 amount)
+
+iff
+
+  CALLVALUE == 0
+  inRange(uint256, totalSupply - amount)
+  inRange(uint256, balanceOf[CALLER] - amount)
+
+storage
+
+  totalSupply => totalSupply - amount
+  balanceOf[CALLER] => balanceOf[CALLER] - amount
+
+returns 1
+
+
+behaviour burnFrom of Token
+interface burnFrom(address src, uint256 amount)
+
+iff
+  amount <= totalSupply
+  amount <= balanceOf[src]
+  CALLER =/= src => amount <= allowance[src][CALLER]
+  CALLVALUE == 0
+
+case CALLER =/= src and allowance[src][CALLER] == 2^256 - 1:
+
+  storage
+
+    totalSupply => totalSupply - amount
+    balanceOf[src] => balanceOf[src] - amount
+
+  returns 1
+
+case CALLER =/= src and allowance[src][CALLER] < 2^256 - 1:
+
+  storage
+
+    totalSupply => totalSupply - amount
+    allowance[src][CALLER] => allowance[src][CALLER] - amount
+    balanceOf[src]         => balanceOf[src] - amount
+
+  returns 1
+
+case CALLER == src:
+
+  storage
+
+    totalSupply => totalSupply - amount
+    balanceOf[src] => balanceOf[src] - amount
+
+  returns 1
+
+ensures
+
+  pre(balanceOf[src]) - post(balanceOf[src]) == pre(totalSupply) - post(totalSupply)
+
+
+behaviour mint of Token
+interface mint(address dst, uint256 amount)
+
+iff in range uint256
+
+  totalSupply + amount
+  balanceOf[dst] + amount
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  totalSupply => totalSupply + amount
+  balanceOf[dst] => balanceOf[dst] + amount
+
+returns 1
+
+
+// View functions:
+
+behaviour totalSupply of Token
+interface totalSupply()
+
+iff 
+
+  CALLVALUE == 0
+
+returns pre(totalSupply)
+
+behaviour balanceOf of Token
+interface balanceOf(address idx)
+
+iff 
+
+  CALLVALUE == 0
+
+returns pre(balanceOf[idx])
+
+behaviour allowance of Token
+interface allowance(address idx1, address idx2)
+
+iff 
+
+  CALLVALUE == 0
+
+returns pre(allowance[idx1][idx2])

tests/hevm/pass/erc20/erc20.sol

@@ -0,0 +1,56 @@
+pragma solidity >=0.8.0;
+
+contract Token {
+    uint256 public totalSupply;
+    mapping (address => uint256) public balanceOf;
+    mapping (address => mapping (address => uint256)) public allowance;
+
+    constructor(uint256 _totalSupply) {
+        totalSupply = _totalSupply;
+        balanceOf[msg.sender] = _totalSupply;
+    }
+
+
+    function approve(address spender, uint256 value) public returns (bool) {
+        if(spender != msg.sender) {
+            allowance[msg.sender][spender] = value;
+        }
+        return true;
+    }
+
+    function transfer(uint256 value, address to) public returns (bool) {
+        balanceOf[msg.sender] = balanceOf[msg.sender] - value;
+        balanceOf[to] = balanceOf[to] + value;
+        return true;
+    }
+
+    function transferFrom(address from, address to, uint256 value) public returns (bool) {
+        if(from != msg.sender && allowance[from][msg.sender] != type(uint256).max) {
+            allowance[from][msg.sender] = allowance[from][msg.sender] - value;
+        }
+        balanceOf[from] = balanceOf[from] - value;
+        balanceOf[to] = balanceOf[to] + value;
+        return true;
+    }
+
+    function burn(uint256 value) public returns (bool) {
+        totalSupply = totalSupply - value;
+        balanceOf[msg.sender] = balanceOf[msg.sender] - value;
+        return true;
+    }
+
+    function burnFrom(address account, uint256 value) public returns (bool) {
+        if(account != msg.sender && allowance[account][msg.sender] != type(uint256).max) {
+            allowance[account][msg.sender] = allowance[account][msg.sender] - value;
+        }
+        totalSupply = totalSupply - value;
+        balanceOf[account] = balanceOf[account] - value;
+        return true;
+    }
+
+    function mint(address account, uint256 value) public returns (bool) {
+        totalSupply = totalSupply + value;
+        balanceOf[account] = balanceOf[account] + value;
+        return true;
+    }
+}