diff --git a/examples/rounding/Pool.sol b/examples/rounding/Pool.sol new file mode 100644 index 00000000..4cac3f5f --- /dev/null +++ b/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); + } +} diff --git a/examples/rounding/pool.act.md b/examples/rounding/pool.act.md new file mode 100644 index 00000000..85ae9b5a --- /dev/null +++ b/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 +``` diff --git a/examples/rounding/readme.md b/examples/rounding/readme.md new file mode 100644 index 00000000..94fafd62 --- /dev/null +++ b/examples/rounding/readme.md @@ -0,0 +1,139 @@ +# Rounding Error + +Understanding the impact of rounding error in a smart contract is a critical task for secure smart +contract development. + +There are two properties of interest: + +- The direction of the rounding error (who loses out) +- The size of the rounding error (by how much do they lose) + +For example in the case of a smart contract that holds a pool of tokens, it is a critical property +that any rounding error is always in favour of the pool. If this property does not hold the pool +will slowly bleed tokens as it is used. + +The following procedure should allow us to automatically prove statements about the direction and +size of rounding error in an act behaviour: + +- For every calculation involving a division encode the calculation as a two forumlae in `smt2`: one + over the reals and one over the integers. +- assert some relation between the two forumlae (e.g. the expression over the integers is always + less than or equal to the expression over the reals) +- assert that the difference between the two expression is never greater than some user provided + constant. + +For a manual example of a very similar procedure, see the [uniswap v1 +model](https://github.com/runtimeverification/verified-smart-contracts/blob/uniswap/uniswap/x-y-k.pdf) +produced by Runtime Verification. + +## Rounding Annotations + +For a concrete syntax proposal, consider the following snippet from a smart contract implementing a +token pool (the full implementation can be seen [here](./Pool.sol), and it's act spec is +[here](./pool.act.md). + +`exit` allows the caller to exchange `shares` pool shares for the proportional amount of the +underlying tokens. + +```solidity +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); +} +``` + +`exit` can be represented in act as follows. Note the **rounding annotations** (`:: (...)`) on the +storage blocks for `token0` and `token1`. + +These annotations consist of two parts: + +1. a relation to `exact` +2. a constant integer bound + +They produce an `smt2` query encoding the following: + +1. The given relation between the integer and real forms of the expression holds +2. The difference between the integer and real forms does not exceed `bound` + +Additionally the act compiler can analyze all defined behaviours and throw a warning if there are +writes to storage involving division that do not have rounding annotations. + +The annotations in the act below can be read as: + +> The rounding error in `exit` is always in favour of the pool, and never exceeds 1 wei. + +```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 +``` + +## Potential Alternative Syntax + +The rounding behaviour is a high level property of the transition system, and it may therefore be +desirable to seperate it syntacticaly from the raw behaviours. + +It may also be possible to automatically derive the rounding annotations from some kind of high +level description, where the rounding properties on individual storage reads/writes can be computed +by the compiler. + +Such a procedure seems potentially incomplete and error prone, and may obscure important details +from the visibility of developers and auditors. + +The high level syntax could perhaps look something like the following: + +```act +rounding of Pool + +join + + for ACCT_ID, bound 1 + against CALLER, bound 1 + +exit + + for ACCT_ID, bound 1 + against CALLER, bound 1 +```