Auction.rs

// Code: https://www.microsoft.com/en-us/research/uploads/prod/2021/02/SmartPulse-Oakland21-preprint.pdf

impl Bidding for Auction {
  uint eth_amount = address(this).balance;
  uint refund_amount = refunds[*];

  init {
    dist(eth_amount) + dist(refund_amount) == 0;
  }

  init -- bid {
    diff(eth_amount - refund_amount) == 0;
    diff(eth_amout) > 0;
  }

  bid -- refund {
    diff(eth_amount - refund_amount) == 0;
    diff(eth_amount) < 0;
  }

  loop {
    dist(eth_amount) + dist(refund_amount) == 0;
  }
}

ERC20.rs

//Contract: https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/token/ERC20/ERC20.sol

impl Cashflow for ERC20 {
  uint sending_amount = balances[*];
  uint receiving_amount = balances[*];
  uint owner_amount = balances[*];
  uint total_supply = totalSupply;
    
  init {
    diff(owner_amount) + diff(total_supply) == 0;
  }
  
  init -- exchange {
    diff(sending_amount) + diff(receiving_amount) == 0;
  }

  loop {
    dist(sending_amount) + dist(receiving_amount) == 0;
  }
}

oUSD.rs

// contract: https://peckshield.medium.com/origin-dollar-incident-root-cause-analysis-f27e11988c90

impl DaiVault for oUSD {
    address DAI_ADDRESS = "0x....";
    address PRICE_PROVIDER = "0x....";
    uint dai_price = IOracle(PRICE_PROVIDER).price(DAI_ADDRESS);
    uint dai_amount = IERC20(TOKEN_ADDRESS).balanceOf(address(this)); // VAULT dai balance
    uint usd_amount oUSD.balanceOf(msg.sender); // user usd balance

    init {
        dist(dai_amount) + dist(usd_amount) == 0;
    }

    init -- mint {
        diff(dai_amount) * new(dai_price) == diff(usd_amount);
    }
    
    loop {
        dist(dai_amount) + dist(usd_amount) == 0;
    }
}

UniswapV1.rs

// Contract: https://github.com/Uniswap/v1-contracts/blob/master/contracts/uniswap_exchange.vy

impl AMM for Exchange {
  uint eth_amount = address(this).balance;
  uint token_amount = this.balanceOf(address(this));

  init {
    new(eth_amount) + new(token_amount) == 0;
  }

  init, exchange -- liquid {
    diff(eth_amount) * diff(token_amount) > 0; // both assets increase/decrease
    diff(eth_amount) * old(token_amount) == diff(token_amount) * old(eth_amount); // must maintain this ratio
  }
  
  init, liquid -- exchange {
    diff(eth_amount) * diff(token_amount) < 0;
    if diff(eth_amount) < 0 {
      diff(eth_amount * token_amount) == 3 * diff(token_amount) * new(eth_amount) / 1000; // 0.3% fee
    } else {
      diff(eth_amount * token_amount) == 3 * diff(eth_amount) * new(token_amount) / 1000; // 0.3% fee
    }
  }

  loop {
    dist(eth_amount) + dist(token_amount) == 0;
  }
}

1. built-in functions:

• old(x) : old value of x
• new(x) : new value of x
• diff(x) : new(x) - old(x)
• dist(x) : |new(x) - old(x)|
• min(x, y) : if x > y return y else return x
• max(x, y) : if x > y return x else return y

2. reversed states:

• init: is executed when the contract is deployed
• loop: is executed before other state transitions (except init). If the condition is satisfied then state is unchanged, otherwise execute other state transitions

3. syntax

• use <type> <expression> as <variable_name>; : in the state transitions, the <variable_name> is used as an alias of <expression> where the <expression> is imported from the contract
• a variable is always wrapped with a function call. For example, new(cur_bid) is valid, but cur_bid is invalid