mint

behaviour mint of UniswapV2Exchange
interface mint(address to)

for all

    LockState : bool

    Token0 : address UniswapV2Exchange
    Token1 : address UniswapV2Exchange

    Balance0 : uint256
    Balance1 : uint256
    Reserve0 : uint112
    Reserve1 : uint112

    Price0Last : uint256
    Price1Last : uint256
    BlockTimestampLast : uint32

    Factory : address UniswapV2Factory
    FeeTo   : address
    KLast   : uint256

    DstBal : uint256
    Burned : uint256
    FeeBal : uint256
    TotalSupply : uint256

where

    // --- centralized fee switch ---

    FeeOn := FeeTo =/= 0

    // --- amounts paid into pool ---

    Amount0 := Balance0 - Reserve0
    Amount1 := Balance1 - Reserve1

    // --- LP share minting ---

    MINIMUM_LIQUIDITY := 1000

    EmptyLiquidity := #sqrt(Amount0 * Amount1) - MINIMUM_LIQUIDITY
    FundedLiquidity := #min((Amount0 * TotalSupply) / Reserve0, (Amount1 * TotalSupply) / Reserve1)

    SharesMinted := #if TotalSupply == 0 #then EmptyLiquidity #else FundedLiquidity #fi

    // --- fee minting ---

    RootK := #sqrt(Reserve0 * Reserve1)
    RootKLast := #sqrt(KLast)
    FeeLiquidity := (TotalSupply * (RootK - RootKLast)) / ((RootK * 4) + RootKLast)

    FeeMinted := #if FeeOn and KLast > 0  #then FeeLiquidity #else 0 #fi

    // --- time since last call ---

    TimeElapsed := ((TIME mod pow32) -Word BlockTimestampLast) mod pow32

storage Token0

    balanceOf[ACCT_ID] |-> Balance0

storage Token1

    balanceOf[ACCT_ID] |-> Balance1

storage Factory

    feeTo |-> FeeTo

storage

    token0  |-> Token0
    token1  |-> Token1
    factory |-> Factory

    // --- reentrancy guard ---

    lockState |-> LockState => LockState

    // --- cached invariant update ---

    kLast |-> KLast => #if FeeOn #then Reserve0 * Reserve1 #else KLast #fi

    // --- mint liquidity tokens ---

    balanceOf[FeeTo] |-> FeeBal => FeeBal + FeeMinted
    balanceOf[to]    |-> DstBal => DstBal + SharesMinted
    balanceOf[0]     |-> Burned => Burned + #if TotalSupply == 0 #then Burned + MINIMUM_LIQUIDITY #else Burned #fi
    totalSupply      |-> TotalSupply => TotalSupply + SharesMinted + FeeMinted

    // --- sync reserves to balances, update cached timestamp ---

    reserve0_reserve1_blockTimestampLast |-> #WordPackUInt112UInt112UInt32(Reserve0, Reserve1, BlockTimestampLast) \
      => #WordPackUInt112UInt112UInt32(Balance0, Balance1, (TIME mod pow32))

    // --- price accumulator updates ---

    price0CumulativeLast |-> PriceLast0 =>                                          \
      #if Reserve0 =/= 0 and Reserve1 =/= 0 and TimeElapsed > 0                     \
        #then chop(((((pow112 * Reserve1) / Reserve0) * TimeElapsed) + PriceLast0)) \
        #else PriceLast0                                                            \
      #fi

    price1CumulativeLast |-> PriceLast1 =>                                          \
      #if Reserve0 =/= 0 and Reserve1 =/= 0 and TimeElapsed > 0                     \
        #then chop(((((pow112 * Reserve0) / Reserve1) * TimeElapsed) + PriceLast1)) \
        #else PriceLast1                                                            \
      #fi

iff in range uint112

    Balance0
    Balance1

iff in range uint256

    // --- invariant calculation ---

    Reserve0 * Reserve1

    // --- LP share calculations ---

    Amount0
    Amount1

    Amount0 * Amount1
    EmptyLiquidity

    Amount0 * TotalSupply
    Amount1 * TotalSupply
    FundedLiquidity

    // --- fee calculations ---

    RootK - RootKLast
    TotalSupply * (RootK - RootKLast)
    RootK * 4
    (RootK * 4) + RootKLast
    (TotalSupply * (RootK - RootKLast)) / ((RootK * 4) + RootKLast)

    // --- token minting ---

    DstBal + FundedLiquidity
    DstBal + EmptyLiquidity

    FeeBal + FeeLiquidity

    Burned + MINIMUM_LIQUIDITY

    TotalSupply + EmptyLiquidity
    TotalSupply + EmptyLiquidity + FeeLiquidity

    TotalSupply + FundedLiquidity
    TotalSupply + FundedLiquidity + FeeLiquidity

iff

    // --- LP shares must be created ---

    ((TotalSupply == 0)         \
      and (Amount0 > 0)         \
      and (Amount1 > 0)         \
      and (EmptyLiquidity > 0)  \
    )                           \
    or ((TotalSupply > 0)       \
      and (Reserve0 > 0)        \
      and (Reserve1 > 0)        \
      and (FundedLiquidity > 0) \
    )

    // --- no reentrancy ---

    LockState == 1

    // --- not payable ---

    VCallValue == 0

    // --- max call stack depth ---

    VCallDepth < 1024

if

    // --- no storage collisions ---

    0 =/= to
    0 =/= FeeTo
    to =/= FeeTo

calls

    UniswapV2Exchange.balanceOf
    UniswapV2Exchange.getReserves
    UniswapV2Factory.feeTo

returns Liquidity