FSM.py

# contract: ERC20
# code: https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/token/ERC20/ERC20.sol

uint x = balances[msg.sender]
uint y = balances[*]
uint m = allowance[*][msg.sender]
uint n = allowance[msg.sender][*]

init(uint k = totalSupply):
  (x = k) if k > 0
transfer(uint k = amount):
  (x, y) -> (x - k, y + k) if k > 0
approve(uint k = amount):
  (n) -> (n + k) if k > 0
transferFrom(uint k = amount):
  (m, y) -> (m - k, y + k) if k > 0


# contract: Auction
# code: https://www.microsoft.com/en-us/research/uploads/prod/2021/02/SmartPulse-Oakland21-preprint.pdf
uint x = balances[*]
uint y = refunds[*]
uint z = msg.sender == winner
uint m = closed

init:
  (x = 0, y = 0, z = 0, m = 0)
bid(uint k = msg.value):
  (x, y, 0, 0) -> (x + k, y + k, 1, 0) if k > 0
refund:
  (x, y, 0, 1) -> (x - y, 0, 1)

# contract: UniswapV1
# code: https://github.com/Uniswap/v1-contracts/blob/master/contracts/uniswap_exchange.vy

uint x = self.balance
uint y = self.token.balanceOf(self)
uint z = self.balances[msg.sender]
uint n = self.totalSupply

init:
  (x = 0, y = 0, z = 0, n = 0)
add_liquidity(uint k = msg.value, uint i = self.token.balanceOf(self)):
  (0,0,0,0) -> (k, i, k, k) if k, i > 0
  (x, y, z, n) -> (x + k, k * y / x, z + k * n / x, n + k * n / x) if k > 0
remove_liquidity(uint k = msg.value):
  (x, y, z, n) -> (x - k * x / n, y - k * y / n, z - k, n - k) if k > 0
token_to_eth(uint k = amount):
  (x, y, z, n) -> (x - k*x / (y + k), y + k, z, n) if k > 0
eth_to_token(uint k = msg.value):
  (x, y, z, n) -> (x + k, y - k*y / (x + k), z, n) if k > 0