examples: rounding: init

examples/rounding/Pool.sol

@@ -0,0 +1,90 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+pragma solidity ^0.6.12;
+
+interface ERC20 {
+    function balanceOf(address usr) external view returns (uint256);
+    function transfer(address usr, uint256 amt) external returns (bool);
+    function transferFrom(address src, address dst, uint256 amt) external returns (bool);
+}
+
+
+contract Pool {
+    // --- Data ---
+    string  public constant name = "Token";
+    string  public constant symbol = "TKN";
+    uint8   public constant decimals = 18;
+
+    ERC20 immutable public token0;
+    ERC20 immutable public token1;
+
+    uint256 public totalSupply;
+    mapping (address => uint) public balanceOf;
+
+    event Transfer(address indexed src, address indexed dst, uint wad);
+
+    // --- Math ---
+    function add(uint x, uint y) internal pure returns (uint z) {
+        require((z = x + y) >= x);
+    }
+    function sub(uint x, uint y) internal pure returns (uint z) {
+        require((z = x - y) <= x);
+    }
+    function mul(uint x, uint y) internal pure returns (uint z) {
+        require(y == 0 || (z = x * y) / y == x);
+    }
+    function min(uint x, uint y) internal pure returns (uint z) {
+        z = x < y ? x : y;
+    }
+
+    // --- Init ---
+    constructor(address _token0, address _token1) public {
+        token0 = ERC20(_token0);
+        token1 = ERC20(_token1);
+    }
+
+    // --- Token ---
+    function transfer(address dst, uint wad) external returns (bool) {
+        balanceOf[msg.sender] = sub(balanceOf[msg.sender], wad);
+        balanceOf[dst] = add(balanceOf[dst], wad);
+        emit Transfer(msg.sender, dst, wad);
+        return true;
+    }
+
+    function mint(address usr, uint wad) internal {
+        balanceOf[usr] = add(balanceOf[usr], wad);
+        totalSupply = add(totalSupply, wad);
+        emit Transfer(address(0), usr, wad);
+    }
+    function burn(address usr, uint wad) internal {
+        balanceOf[usr] = sub(balanceOf[usr], wad);
+        totalSupply = sub(totalSupply, wad);
+        emit Transfer(usr, address(0), wad);
+    }
+
+    // --- Join / Exit ---
+    function join(uint amt0, uint amt1) external returns (uint shares) {
+        token0.transferFrom(msg.sender, address(this), amt0);
+        token1.transferFrom(msg.sender, address(this), amt1);
+
+        if (totalSupply == 0) {
+            shares = min(amt0, amt1);
+        } else {
+            shares = min(
+                mul(totalSupply, amt0) / token0.balanceOf(address(this)),
+                mul(totalSupply, amt1) / token1.balanceOf(address(this))
+            );
+        }
+
+        mint(msg.sender, shares);
+    }
+    function exit(uint shares) external returns (uint amt0, uint amt1) {
+        require(totalSupply > 0);
+
+        amt0 = mul(token0.balanceOf(address(this)), shares) / totalSupply;
+        amt1 = mul(token1.balanceOf(address(this)), shares) / totalSupply;
+
+        burn(msg.sender, shares);
+        token0.transfer(msg.sender, amt0);
+        token1.transfer(msg.sender, amt1);
+    }
+}

examples/rounding/pool.act.md

@@ -0,0 +1,182 @@
+# Pool
+
+## Constructor
+
+```act
+behaviour init of Pool
+interface constructor(address _token0, address _token1)
+
+creates
+
+    address token0 := _token0
+    address token1 := _token1
+
+    uint256 public totalSupply := 0
+    mapping (address => uint) balanceOf := []
+```
+
+## Transfer
+
+`transfer` allows the caller to transfer `wad` pool shares to `dst`.
+
+`transfer` fails if:
+
+  - any of the calculations overflow
+  - ether is provided in the call
+
+Self transfers are allowed, provided the caller has more than `wad` pool shares.
+
+```act
+behaviour transfer of Pool
+interface transfer(address dst, uint wad)
+
+iff
+
+   CALLVALUE == 0
+   wad <= balanceOf[CALLER]
+   CALLER =/= to => balanceOf[dst] + wad < 2^256
+
+case CALLER =/= to:
+
+   storage
+
+       balanceOf[CALLER] => balanceOf[CALLER] - wad
+       balanceOf[dst]    => balanceOf[dst]    + wad
+
+   returns 1
+
+case CALLER == to:
+
+   returns 1
+```
+
+## Join
+
+`join` allows the caller to exchange `amt0` and `amt1` tokens for some amount of pool shares. The
+exact amount of pool shares minted depends on the state of the pool at the time of the call.
+
+`join` fails if:
+
+- any calculation overflows
+- ether is provided in the call
+
+```act
+behaviour join of Pool
+interface join(uint amt0, uint amt1)
+
+iff
+
+    CALLVALUE == 0
+
+iff in range uint256
+
+    token0.balanceOf[CALLER] - amt0
+    token0.balanceOf[ACCT_ID] + amt0
+
+    token1.balanceOf[CALLER] - amt1
+    token1.balanceOf[ACCT_ID] + amt1
+
+storage token0
+
+    balanceOf[CALLER]  => balanceOf[CALLER]  - amt0
+    balanceOf[ACCT_ID] => balanceOf[ACCT_ID] + amt0
+
+storage token1
+
+    balanceOf[CALLER]  => balanceOf[CALLER]  - amt0
+    balanceOf[ACCT_ID] => balanceOf[ACCT_ID] + amt0
+
+case totalSupply == 0:
+
+    iff in range uint256
+
+        balanceOf[CALLER] + min(amt0, amt1)
+        totalSupply + min(amt0, amt1)
+
+    storage
+
+        balanceOf[CALLER] => balanceOf[CALLER] + min(amt0, amt1)
+
+    returns min(amt0, amt1)
+
+case totalSupply =/= 0:
+
+    iff in range uint256
+
+        totalSupply * amt0
+        totalSupply * amt1
+
+        balanceOf[CALLER] + sharesSubsq
+        totalSupply + sharesSubsq
+
+    storage
+
+        balanceOf[CALLER] => balanceOf[CALLER] + sharesSubsq :: (<= exact, bound 1)
+
+    returns sharesSubsq
+
+where
+
+    sharesSubsq := min(
+        (totalSupply * amt0) / token0.balanceOf[ACCT_ID],
+        (totalSupply * amt1) / token1.balanceOf[ACCT_ID],
+    )
+```
+
+## Exit
+
+`exit` allows the callers to exchange `shares` pool shares for the proportional amount of the
+underlying tokens.
+
+`exit` fails if:
+
+- any calculations overflow
+- totalSupply is 0
+- ether is provided in the call
+
+```act
+behaviour exit of Pool
+interface exit(uint shares)
+
+iff
+
+    CALLVALUE == 0
+    totalSupply > 0
+
+iff in range uint256
+
+    token0.balanceOf[ACCT_ID] - amt0
+    token0.balanceOf[CALLER]  + amt0
+
+    token1.balanceOf[ACCT_ID] - amt1
+    token1.balanceOf[CALLER]  + amt1
+
+    token0.balanceOf[ACCT_ID] * shares
+    token1.balanceOf[ACCT_ID] * shares
+
+    balanceOf[CALLER] - shares
+
+storage token0
+
+    balanceOf[ACCT_ID] => balanceOf[ACCT_ID] - amt0 :: (>= exact, bound 1)
+    balanceOf[CALLER]  => balanceOf[CALLER]  + amt0 :: (<= exact, bound 1)
+
+storage token1
+
+    balanceOf[ACCT_ID] => balanceOf[ACCT_ID] - amt1 :: (>= exact, bound 1)
+    balanceOf[CALLER]  => balanceOf[CALLER]  + amt1 :: (<= exact, bound 1)
+
+storage
+
+    balanceOf[CALLER] => balanceOf[CALLER] - shares
+
+where
+
+    amt0 := (token0.balanceOf[ACCT_ID] * shares) / totalSupply
+    amt1 := (token1.balanceOf[ACCT_ID] * shares) / totalSupply
+
+rounding
+
+    for ACCT_ID, bound 1
+    against CALLER, bound 1
+```