From bdc33a2337c71365cd8be145ea7437e15a197482 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Mon, 9 Sep 2024 17:17:46 -0500 Subject: [PATCH 1/9] Added summary of initial state after pasring contracts. Used configuration variable. --- src/solidity.md | 2396 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 2395 insertions(+), 1 deletion(-) diff --git a/src/solidity.md b/src/solidity.md index 3afce94..ba794b9 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -17,6 +17,7 @@ module SOLIDITY-CONFIGURATION configuration $PGM:Program ~> $TXN:Transactions + $ISUNISWAP:Bool Id @@ -83,6 +84,2397 @@ module SOLIDITY-CONFIGURATION endmodule ``` +```k +module SOLIDITY-UNISWAP-INIT-SUMMARY + imports SOLIDITY-CONFIGURATION + + syntax Id ::= "account" [token] + | "act" [token] + | "allowance" [token] + | "allowed" [token] + | "amountIn" [token] + | "amountInMax" [token] + | "amountInWithFee" [token] + | "amountOut" [token] + | "amountOutDesired" [token] + | "amountOutMin" [token] + | "amounts" [token] + | "amount0In" [token] + | "amount1In" [token] + | "amount0Out" [token] + | "amount1Out" [token] + | "approvalEvent" [token] + | "approve" [token] + | "balance" [token] + | "balanceOf" [token] + | "balance0" [token] + | "balance0Adjusted" [token] + | "balance1" [token] + | "balance1Adjusted" [token] + | "block" [token] + | "blockTimestamp" [token] + | "blockTimestampLast" [token] + | "burn" [token] + | "call" [token] + | "constMINIMUMLIQUIDITY" [token] + | "constUINTMAX" [token] + | "constUINT112MAX" [token] + | "constUINT256MAX" [token] + | "currentAllowance" [token] + | "dai" [token] + | "daiact" [token] + | "daiAmountDesired" [token] + | "daiAmountIn" [token] + | "daiAmountMin" [token] + | "daiAmountOut" [token] + | "dAIMock" [token] + | "daiownr" [token] + | "daispdr" [token] + | "decimals" [token] + | "denominator" [token] + | "deposit" [token] + | "dst" [token] + | "emitEvent" [token] + | "from" [token] + | "fromBalance" [token] + | "getLocalPair" [token] + | "getReserves" [token] + | "guy" [token] + | "i" [token] + | "iERC20" [token] + | "input" [token] + | "kLast" [token] + | "length" [token] + | "localPairs" [token] + | "mint" [token] + | "mintOnDeposit" [token] + | "msg" [token] + | "numerator" [token] + | "output" [token] + | "owner" [token] + | "pair" [token] + | "pairEl1" [token] + | "pairEl2" [token] + | "pairReserves" [token] + | "path" [token] + | "price0CumulativeLast" [token] + | "price1CumulativeLast" [token] + | "reduced" [token] + | "reserveIn" [token] + | "reserveOut" [token] + | "reserves" [token] + | "reserve0" [token] + | "reserve1" [token] + | "router" [token] + | "safeTransferFrom" [token] + | "sender" [token] + | "setLocalPair" [token] + | "setUp" [token] + | "spender" [token] + | "src" [token] + | "success" [token] + | "swap" [token] + | "swapExactTokensForTokens" [token] + | "swapEvent" [token] + | "swapMultiHopExactAmountIn" [token] + | "swapMultiHopExactAmountOut" [token] + | "swapSingleHopExactAmountIn" [token] + | "swapSingleHopExactAmountOut" [token] + | "swapTokensForExactTokens" [token] + | "sync" [token] + | "syncEvent" [token] + | "syncLocalPair" [token] + | "testSwapMultiHopExactAmountIn" [token] + | "testSwapMultiHopExactAmountOut" [token] + | "testSwapSingleHopExactAmountIn" [token] + | "testSwapSingleHopExactAmountOut" [token] + | "this" [token] + | "timeElapsed" [token] + | "timestamp" [token] + | "to" [token] + | "tokenA" [token] + | "tokenB" [token] + | "tokens" [token] + | "token0" [token] + | "token1" [token] + | "totalSupply" [token] + | "transfer" [token] + | "transferEvent" [token] + | "transferFrom" [token] + | "uniswapV2LibraryGetAmountIn" [token] + | "uniswapV2LibraryGetAmountOut" [token] + | "uniswapV2LibraryGetAmountsIn" [token] + | "uniswapV2LibraryGetAmountsOut" [token] + | "uniswapV2LibraryGetReserves" [token] + | "uniswapV2LibraryPairFor" [token] + | "uniswapV2LibrarySortTokens" [token] + | "uniswapV2Pair" [token] + | "uniswapV2Router02" [token] + | "uniswapV2Swap" [token] + | "uniswapV2SwapTest" [token] + | "usdc" [token] + | "usdcAmountOut" [token] + | "usdcAmountOutMin" [token] + | "uSDCMock" [token] + | "usr" [token] + | "value" [token] + | "wad" [token] + | "weth" [token] + | "wethact" [token] + | "wethAmount" [token] + | "wETHMock" [token] + | "wethownr" [token] + | "wethspdr" [token] + + syntax Id ::= "vidAllowances" [token] + | "vidBalances" [token] + | "vidDai" [token] + | "vidReserve0" [token] + | "vidReserve1" [token] + | "vidTo" [token] + | "vidToken0" [token] + | "vidToken1" [token] + | "vidTotalSupply" [token] + | "vidUni" [token] + | "vidUsdc" [token] + | "vidWeth" [token] + | "fidApprove" [token] + | "fidSpendAllowance" [token] + | "fidSwap" [token] + | "fidTransfer" [token] + | "fidUpdate" [token] + + syntax Id ::= "require" [token] | "assert" [token] + + syntax Decimal ::= "1e18" [token] + | "1e6" [token] + + rule _:Program => .K ... + true + (_:CompileCell => + + + uniswapV2SwapTest + + + + + iERC20 + + + + + approve + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( bool ) + + + + balanceOf + + + ListItem ( address ) + + + ListItem ( uint256 ) + + + + transfer + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( bool ) + + + + transferFrom + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( bool ) + + + + + + + + + dAIMock + + + (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) + (balanceOf |-> mapping ( address daiact => uint256 )) + (constUINTMAX |-> uint256) + (totalSupply |-> uint256) + + + ListItem ( constUINTMAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) + + + + + allowance + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( daiownr ) + ListItem ( daispdr ) + + + ListItem ( mapping ( address daiownr => mapping ( address daispdr => uint256 ) ) ) + + + ListItem ( noId ) + + + false + + + return allowance [ daiownr ] [ daispdr ] ; .Statements + + + + approve + + + external + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + allowance [ msg . sender ] [ usr ] = wad ; emit approvalEvent ( msg . sender , usr , wad , .TypedVals ) ; return true ; .Statements + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( daiact ) + + + ListItem ( mapping ( address daiact => uint256 ) ) + + + ListItem ( noId ) + + + false + + + return balanceOf [ daiact ] ; .Statements + + + + burn + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + .List + + + .List + + + false + + + if ( balanceOf [ usr ] >= wad ) { balanceOf [ usr ] = balanceOf [ usr ] - wad ; totalSupply = totalSupply - wad ; .Statements } .Statements + + + + decimals + + + external + + + .List + + + .List + + + ListItem ( uint8 ) + + + ListItem ( noId ) + + + false + + + return 18 ; .Statements + + + + mint + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + .List + + + .List + + + false + + + balanceOf [ usr ] = balanceOf [ usr ] + wad ; totalSupply = totalSupply + wad ; emit transferEvent ( address ( 0 , .TypedVals ) , usr , wad , .TypedVals ) ; .Statements + + + + mintOnDeposit + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + .List + + + .List + + + false + + + mint ( usr , wad , .TypedVals ) ; .Statements + + + + safeTransferFrom + + + external + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + transferFrom ( from , to , value , .TypedVals ) ; .Statements + + + + totalSupply + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return totalSupply ; .Statements + + + + transfer + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( dst ) + ListItem ( wad ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + return transferFrom ( msg . sender , dst , wad , .TypedVals ) ; .Statements + + + + transferFrom + + + public + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( src ) + ListItem ( dst ) + ListItem ( wad ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + require ( balanceOf [ src ] >= wad , "Dai/insufficient-balance" , .TypedVals ) ; if ( src != msg . sender && allowance [ src ] [ msg . sender ] != constUINTMAX ) { require ( allowance [ src ] [ msg . sender ] >= wad , "Dai/insufficient-allowance" , .TypedVals ) ; allowance [ src ] [ msg . sender ] = allowance [ src ] [ msg . sender ] - wad ; .Statements } balanceOf [ src ] = balanceOf [ src ] - wad ; balanceOf [ dst ] = balanceOf [ dst ] + wad ; emit transferEvent ( src , dst , wad , .TypedVals ) ; return true ; .Statements + + + + + + + approvalEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( src ) + ListItem ( guy ) + ListItem ( wad ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + transferEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( src ) + ListItem ( dst ) + ListItem ( wad ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + + + uSDCMock + + + (constUINT256MAX |-> uint256) + (vidAllowances |-> mapping ( address account => mapping ( address spender => uint256 ) )) + (vidBalances |-> mapping ( address account => uint256 )) + (vidTotalSupply |-> uint256) + + + ListItem ( constUINT256MAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) + + + + + allowance + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( owner ) + ListItem ( spender ) + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return vidAllowances [ owner ] [ spender ] ; .Statements + + + + approve + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( spender ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address owner = msg . sender ; fidApprove ( owner , spender , value , true , .TypedVals ) ; return true ; .Statements + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( account ) + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return vidBalances [ account ] ; .Statements + + + + decimals + + + external + + + .List + + + .List + + + ListItem ( uint8 ) + + + ListItem ( noId ) + + + false + + + return 18 ; .Statements + + + + fidApprove + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + ListItem ( bool ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + ListItem ( emitEvent ) + + + .List + + + .List + + + false + + + require ( owner != address ( 0 , .TypedVals ) , "USDC: invalid approver" , .TypedVals ) ; require ( spender != address ( 0 , .TypedVals ) , "USDC: invalid spender" , .TypedVals ) ; vidAllowances [ owner ] [ spender ] = value ; if ( emitEvent ) { emit approvalEvent ( owner , spender , value , .TypedVals ) ; .Statements } .Statements + + + + fidSpendAllowance + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + .List + + + .List + + + false + + + uint256 currentAllowance = allowance ( owner , spender , .TypedVals ) ; if ( currentAllowance != constUINT256MAX ) { require ( currentAllowance >= value , "USDC: insufficient allowance" , .TypedVals ) ; fidApprove ( owner , spender , currentAllowance - value , false , .TypedVals ) ; .Statements } .Statements + + + + fidTransfer + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + require ( from != address ( 0 , .TypedVals ) , "USDC: invalid sender" , .TypedVals ) ; require ( to != address ( 0 , .TypedVals ) , "USDC: invalid receiver" , .TypedVals ) ; fidUpdate ( from , to , value , .TypedVals ) ; .Statements + + + + fidUpdate + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + if ( from == address ( 0 , .TypedVals ) ) { vidTotalSupply = vidTotalSupply + value ; .Statements } else { uint256 fromBalance = vidBalances [ from ] ; require ( fromBalance >= value , "USDC: insufficient balance" , .TypedVals ) ; vidBalances [ from ] = fromBalance - value ; .Statements } if ( to == address ( 0 , .TypedVals ) ) { vidTotalSupply = vidTotalSupply - value ; .Statements } else { vidBalances [ to ] = vidBalances [ to ] + value ; .Statements } emit transferEvent ( from , to , value , .TypedVals ) ; .Statements + + + + mint + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( account ) + ListItem ( value ) + + + .List + + + .List + + + false + + + require ( account != address ( 0 , .TypedVals ) , "USDC: invalid receiver" , .TypedVals ) ; fidUpdate ( address ( 0 , .TypedVals ) , account , value , .TypedVals ) ; .Statements + + + + transfer + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address owner = msg . sender ; fidTransfer ( owner , to , value , .TypedVals ) ; return true ; .Statements + + + + transferFrom + + + public + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address spender = msg . sender ; fidSpendAllowance ( from , spender , value , .TypedVals ) ; fidTransfer ( from , to , value , .TypedVals ) ; return true ; .Statements + + + + + + + approvalEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + transferEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + + + uniswapV2Pair + + + (balanceOf |-> mapping ( address act => uint256 )) + (blockTimestampLast |-> uint32) + (constMINIMUMLIQUIDITY |-> uint256) + (constUINT112MAX |-> uint256) + (kLast |-> uint256) + (price0CumulativeLast |-> uint256) + (price1CumulativeLast |-> uint256) + (reserve0 |-> uint112) + (reserve1 |-> uint112) + (token0 |-> address) + (token1 |-> address) + (totalSupply |-> uint256) + + + ListItem ( constUINT112MAX = 0xffffffffffffffffffffffffffff ; ) + ListItem ( constMINIMUMLIQUIDITY = 10 ** 3 ; ) + + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( act ) + + + ListItem ( mapping ( address act => uint256 ) ) + + + ListItem ( noId ) + + + false + + + return balanceOf [ act ] ; .Statements + + + + constMINIMUMLIQUIDITY + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return constMINIMUMLIQUIDITY ; .Statements + + + + constructor + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( vidToken0 ) + ListItem ( vidToken1 ) + + + .List + + + .List + + + false + + + token0 = vidToken0 ; token1 = vidToken1 ; .Statements + + + + fidUpdate + + + private + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint112 ) + ListItem ( uint112 ) + + + ListItem ( balance0 ) + ListItem ( balance1 ) + ListItem ( vidReserve0 ) + ListItem ( vidReserve1 ) + + + .List + + + .List + + + false + + + require ( balance0 <= constUINT112MAX && balance1 <= constUINT112MAX , "UniswapV2: OVERFLOW" , .TypedVals ) ; uint32 blockTimestamp = uint32 ( block . timestamp % 2 ** 32 , .TypedVals ) ; uint32 timeElapsed = blockTimestamp - blockTimestampLast ; if ( timeElapsed > 0 && vidReserve0 != 0 && vidReserve1 != 0 ) { price0CumulativeLast = price0CumulativeLast + vidReserve1 / vidReserve0 * timeElapsed ; price1CumulativeLast = price1CumulativeLast + vidReserve0 / vidReserve1 * timeElapsed ; .Statements } reserve0 = uint112 ( balance0 , .TypedVals ) ; reserve1 = uint112 ( balance1 , .TypedVals ) ; blockTimestampLast = blockTimestamp ; emit syncEvent ( reserve0 , reserve1 , .TypedVals ) ; .Statements + + + + getReserves + + + public + + + .List + + + .List + + + ListItem ( uint112 [ ]::TypeName ) + + + ListItem ( reserves ) + + + false + + + reserves = new uint112 [ ] ( 3 , .TypedVals ) ; reserves [ 0 ] = reserve0 ; reserves [ 1 ] = reserve1 ; reserves [ 2 ] = blockTimestampLast ; .Statements + + + + kLast + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return kLast ; .Statements + + + + price0CumulativeLast + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return price0CumulativeLast ; .Statements + + + + price1CumulativeLast + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return price1CumulativeLast ; .Statements + + + + swap + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address ) + + + ListItem ( amount0Out ) + ListItem ( amount1Out ) + ListItem ( to ) + + + .List + + + .List + + + false + + + require ( amount0Out > 0 || amount1Out > 0 , "UniswapV2: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; uint112 [ ] memory reserves = getReserves ( .TypedVals ) ; require ( amount0Out < reserves [ 0 ] && amount1Out < reserves [ 1 ] , "UniswapV2: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 balance0 ; uint256 balance1 ; { address vidToken0 = token0 ; address vidToken1 = token1 ; require ( to != vidToken0 && to != vidToken1 , "UniswapV2: INVALID_TO" , .TypedVals ) ; if ( amount0Out > 0 ) iERC20 ( vidToken0 , .TypedVals ) . transfer ( to , amount0Out , .TypedVals ) ; if ( amount1Out > 0 ) iERC20 ( vidToken1 , .TypedVals ) . transfer ( to , amount1Out , .TypedVals ) ; balance0 = iERC20 ( vidToken0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; balance1 = iERC20 ( vidToken1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; .Statements } uint256 amount0In = balance0 > reserves [ 0 ] - amount0Out ? balance0 - ( reserves [ 0 ] - amount0Out ) : 0 ; uint256 amount1In = balance1 > reserves [ 1 ] - amount1Out ? balance1 - ( reserves [ 1 ] - amount1Out ) : 0 ; require ( amount0In > 0 || amount1In > 0 , "UniswapV2: INSUFFICIENT_INPUT_AMOUNT" , .TypedVals ) ; { uint256 balance0Adjusted = balance0 * 1000 - amount0In * 3 ; uint256 balance1Adjusted = balance1 * 1000 - amount1In * 3 ; require ( balance0Adjusted * balance1Adjusted >= uint256 ( reserves [ 0 ] , .TypedVals ) * reserves [ 1 ] * 1000 ** 2 , "UniswapV2: K" , .TypedVals ) ; .Statements } fidUpdate ( balance0 , balance1 , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; emit swapEvent ( msg . sender , amount0In , amount1In , amount0Out , amount1Out , to , .TypedVals ) ; .Statements + + + + sync + + + external + + + .List + + + .List + + + .List + + + .List + + + false + + + fidUpdate ( iERC20 ( token0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , iERC20 ( token1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , reserve0 , reserve1 , .TypedVals ) ; .Statements + + + + token0 + + + public + + + .List + + + .List + + + ListItem ( address ) + + + ListItem ( noId ) + + + false + + + return token0 ; .Statements + + + + token1 + + + public + + + .List + + + .List + + + ListItem ( address ) + + + ListItem ( noId ) + + + false + + + return token1 ; .Statements + + + + totalSupply + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return totalSupply ; .Statements + + + + + + + swapEvent + + + ListItem ( address ) + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address ) + + + ListItem ( sender ) + ListItem ( amount0In ) + ListItem ( amount1In ) + ListItem ( amount0Out ) + ListItem ( amount1Out ) + ListItem ( to ) + + + SetItem ( 0 ) + SetItem ( 5 ) + + + + syncEvent + + + ListItem ( uint112 ) + ListItem ( uint112 ) + + + ListItem ( reserve0 ) + ListItem ( reserve1 ) + + + .Set + + + + + + uniswapV2Router02 + + + localPairs |-> mapping ( address pairEl1 => mapping ( address pairEl2 => address ) ) + + + .List + + + + + fidSwap + + + private + + + ListItem ( uint256 [ ]::TypeName ) + ListItem ( address [ ]::TypeName ) + ListItem ( address ) + + + ListItem ( amounts ) + ListItem ( path ) + ListItem ( vidTo ) + + + .List + + + .List + + + false + + + { uint256 i ; while ( i < path . length - 1 ) { { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2LibrarySortTokens ( input , output , .TypedVals ) ; uint256 amountOut = amounts [ i + 1 ] ; uint256 amount0Out = input == tokens [ 0 ] ? uint256 ( 0 , .TypedVals ) : amountOut ; uint256 amount1Out = input == tokens [ 0 ] ? amountOut : uint256 ( 0 , .TypedVals ) ; address to = i < path . length - 2 ? uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) : vidTo ; uniswapV2Pair ( uniswapV2LibraryPairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements + + + + getLocalPair + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( address ) + + + ListItem ( pair ) + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; pair = localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] ; .Statements + + + + localPairs + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( pairEl1 ) + ListItem ( pairEl2 ) + + + ListItem ( mapping ( address pairEl1 => mapping ( address pairEl2 => address ) ) ) + + + ListItem ( noId ) + + + false + + + return localPairs [ pairEl1 ] [ pairEl2 ] ; .Statements + + + + setLocalPair + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + .List + + + .List + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] = address ( new uniswapV2Pair ( address ( tokens [ 0 ] , .TypedVals ) , address ( tokens [ 1 ] , .TypedVals ) , .TypedVals ) , .TypedVals ) ; .Statements + + + + swapExactTokensForTokens + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + ListItem ( address ) + + + ListItem ( amountIn ) + ListItem ( amountOutMin ) + ListItem ( path ) + ListItem ( to ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + amounts = uniswapV2LibraryGetAmountsOut ( amountIn , path , .TypedVals ) ; require ( amounts [ amounts . length - 1 ] >= amountOutMin , "UniswapV2Router: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; iERC20 ( path [ 0 ] , .TypedVals ) . transferFrom ( msg . sender , uniswapV2LibraryPairFor ( path [ 0 ] , path [ 1 ] , .TypedVals ) , amounts [ 0 ] , .TypedVals ) ; fidSwap ( amounts , path , to , .TypedVals ) ; .Statements + + + + swapTokensForExactTokens + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + ListItem ( address ) + + + ListItem ( amountOut ) + ListItem ( amountInMax ) + ListItem ( path ) + ListItem ( to ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + amounts = uniswapV2LibraryGetAmountsIn ( amountOut , path , .TypedVals ) ; require ( amounts [ 0 ] <= amountInMax , "UniswapV2Router: EXCESSIVE_INPUT_AMOUNT" , .TypedVals ) ; iERC20 ( path [ 0 ] , .TypedVals ) . transferFrom ( msg . sender , uniswapV2LibraryPairFor ( path [ 0 ] , path [ 1 ] , .TypedVals ) , amounts [ 0 ] , .TypedVals ) ; fidSwap ( amounts , path , to , .TypedVals ) ; .Statements + + + + syncLocalPair + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + .List + + + .List + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; uniswapV2Pair ( localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] , .TypedVals ) . sync ( .TypedVals ) ; .Statements + + + + uniswapV2LibraryGetAmountIn + + + private + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountOut ) + ListItem ( reserveIn ) + ListItem ( reserveOut ) + + + ListItem ( uint256 ) + + + ListItem ( amountIn ) + + + false + + + require ( amountOut > 0 , "UniswapV2Library: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; require ( reserveIn > 0 && reserveOut > 0 , "UniswapV2Library: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 numerator = reserveIn * amountOut * 1000 ; uint256 denominator = ( reserveOut - amountOut ) * 997 ; amountIn = denominator != 0 ? numerator / denominator + 1 : 1 ; .Statements + + + + uniswapV2LibraryGetAmountOut + + + private + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountIn ) + ListItem ( reserveIn ) + ListItem ( reserveOut ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + require ( amountIn > 0 , "UniswapV2Library: INSUFFICIENT_INPUT_AMOUNT" , .TypedVals ) ; require ( reserveIn > 0 && reserveOut > 0 , "UniswapV2Library: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 amountInWithFee = amountIn * 997 ; uint256 numerator = amountInWithFee * reserveOut ; uint256 denominator = reserveIn * 1000 + amountInWithFee ; amountOut = numerator / denominator ; .Statements + + + + uniswapV2LibraryGetAmountsIn + + + private + + + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + + + ListItem ( amountOut ) + ListItem ( path ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ amounts . length - 1 ] = amountOut ; { uint256 i = path . length - 1 ; while ( i > 0 ) { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i - 1 ] , path [ i ] , .TypedVals ) ; amounts [ i - 1 ] = uniswapV2LibraryGetAmountIn ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i -- ; .Statements } .Statements } .Statements + + + + uniswapV2LibraryGetAmountsOut + + + private + + + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + + + ListItem ( amountIn ) + ListItem ( path ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; { uint256 i ; while ( i < path . length - 1 ) { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; amounts [ i + 1 ] = uniswapV2LibraryGetAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements + + + + uniswapV2LibraryGetReserves + + + private + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( reserves ) + + + false + + + reserves = new uint256 [ ] ( 2 , .TypedVals ) ; address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; uint112 [ ] memory pairReserves = uniswapV2Pair ( uniswapV2LibraryPairFor ( tokenA , tokenB , .TypedVals ) , .TypedVals ) . getReserves ( .TypedVals ) ; reserves [ 0 ] = tokenA == tokens [ 0 ] ? pairReserves [ 0 ] : pairReserves [ 1 ] ; reserves [ 1 ] = tokenA == tokens [ 0 ] ? pairReserves [ 1 ] : pairReserves [ 0 ] ; .Statements + + + + uniswapV2LibraryPairFor + + + private + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( address ) + + + ListItem ( pair ) + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; pair = localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] ; .Statements + + + + uniswapV2LibrarySortTokens + + + private + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( address [ ]::TypeName ) + + + ListItem ( tokens ) + + + false + + + tokens = new address [ ] ( 2 , .TypedVals ) ; require ( tokenA != tokenB , "UniswapV2Library: IDENTICAL_ADDRESSES" , .TypedVals ) ; tokens [ 0 ] = tokenA < tokenB ? tokenA : tokenB ; tokens [ 1 ] = tokenA < tokenB ? tokenB : tokenA ; require ( tokens [ 0 ] != address ( 0 , .TypedVals ) , "UniswapV2Library: ZERO_ADDRESS" , .TypedVals ) ; .Statements + + + + ... + + + uniswapV2Swap + + + (dai |-> iERC20) + (router |-> uniswapV2Router02) + (usdc |-> iERC20) + (weth |-> iERC20) + + + .List + + + + + constructor + + + public + + + ListItem ( address ) + ListItem ( address ) + ListItem ( address ) + + + ListItem ( vidWeth ) + ListItem ( vidDai ) + ListItem ( vidUsdc ) + + + .List + + + .List + + + false + + + weth = iERC20 ( vidWeth , .TypedVals ) ; dai = iERC20 ( vidDai , .TypedVals ) ; usdc = iERC20 ( vidUsdc , .TypedVals ) ; router = new uniswapV2Router02 ( .TypedVals ) ; router . setLocalPair ( vidWeth , vidDai , .TypedVals ) ; router . setLocalPair ( vidWeth , vidUsdc , .TypedVals ) ; router . setLocalPair ( vidUsdc , vidDai , .TypedVals ) ; .Statements + + + + dai + + + public + + + .List + + + .List + + + ListItem ( iERC20 ) + + + ListItem ( noId ) + + + false + + + return dai ; .Statements + + + + router + + + public + + + .List + + + .List + + + ListItem ( uniswapV2Router02 ) + + + ListItem ( noId ) + + + false + + + return router ; .Statements + + + + swapMultiHopExactAmountIn + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountIn ) + ListItem ( amountOutMin ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + dai . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountIn , .TypedVals ) ; dai . approve ( address ( router , .TypedVals ) , amountIn , .TypedVals ) ; address [ ] memory path = new address [ ] ( 3 , .TypedVals ) ; path [ 0 ] = address ( dai , .TypedVals ) ; path [ 1 ] = address ( weth , .TypedVals ) ; path [ 2 ] = address ( usdc , .TypedVals ) ; uint256 [ ] memory amounts = router . swapExactTokensForTokens ( amountIn , amountOutMin , path , msg . sender , .TypedVals ) ; return amounts [ 2 ] ; .Statements + + + + swapMultiHopExactAmountOut + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountOutDesired ) + ListItem ( amountInMax ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + dai . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountInMax , .TypedVals ) ; dai . approve ( address ( router , .TypedVals ) , amountInMax , .TypedVals ) ; address [ ] memory path = new address [ ] ( 3 , .TypedVals ) ; path [ 0 ] = address ( dai , .TypedVals ) ; path [ 1 ] = address ( weth , .TypedVals ) ; path [ 2 ] = address ( usdc , .TypedVals ) ; uint256 [ ] memory amounts = router . swapTokensForExactTokens ( amountOutDesired , amountInMax , path , msg . sender , .TypedVals ) ; if ( amounts [ 0 ] < amountInMax ) { dai . transfer ( msg . sender , amountInMax - amounts [ 0 ] , .TypedVals ) ; .Statements } return amounts [ 2 ] ; .Statements + + + + swapSingleHopExactAmountIn + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountIn ) + ListItem ( amountOutMin ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + weth . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountIn , .TypedVals ) ; weth . approve ( address ( router , .TypedVals ) , amountIn , .TypedVals ) ; address [ ] memory path = new address [ ] ( 2 , .TypedVals ) ; path [ 0 ] = address ( weth , .TypedVals ) ; path [ 1 ] = address ( dai , .TypedVals ) ; uint256 [ ] memory amounts = router . swapExactTokensForTokens ( amountIn , amountOutMin , path , msg . sender , .TypedVals ) ; return amounts [ 1 ] ; .Statements + + + + swapSingleHopExactAmountOut + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountOutDesired ) + ListItem ( amountInMax ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + weth . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountInMax , .TypedVals ) ; weth . approve ( address ( router , .TypedVals ) , amountInMax , .TypedVals ) ; address [ ] memory path = new address [ ] ( 2 , .TypedVals ) ; path [ 0 ] = address ( weth , .TypedVals ) ; path [ 1 ] = address ( dai , .TypedVals ) ; uint256 [ ] memory amounts = router . swapTokensForExactTokens ( amountOutDesired , amountInMax , path , msg . sender , .TypedVals ) ; if ( amounts [ 0 ] < amountInMax ) { weth . transfer ( msg . sender , amountInMax - amounts [ 0 ] , .TypedVals ) ; .Statements } return amounts [ 1 ] ; .Statements + + + + usdc + + + public + + + .List + + + .List + + + ListItem ( iERC20 ) + + + ListItem ( noId ) + + + false + + + return usdc ; .Statements + + + + weth + + + public + + + .List + + + .List + + + ListItem ( iERC20 ) + + + ListItem ( noId ) + + + false + + + return weth ; .Statements + + + + ... + + + uniswapV2SwapTest + + + (vidDai |-> dAIMock) + (vidUni |-> uniswapV2Swap) + (vidUsdc |-> uSDCMock) + (vidWeth |-> wETHMock) + + + .List + + + + + setUp + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + vidWeth = new wETHMock ( .TypedVals ) ; vidDai = new dAIMock ( .TypedVals ) ; vidUsdc = new uSDCMock ( .TypedVals ) ; vidUni = new uniswapV2Swap ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; .Statements + + + + testSwapMultiHopExactAmountIn + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 4 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 3 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 3 * wethAmount , .TypedVals ) ; vidUsdc . mint ( address ( this , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidUsdc . approve ( address ( vidUni , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountMin = 1 ; vidUni . swapSingleHopExactAmountIn ( wethAmount , daiAmountMin , .TypedVals ) ; uint256 daiAmountIn = 1e18 ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidUsdc . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; uint256 usdcAmountOutMin = 1 ; uint256 usdcAmountOut = vidUni . swapMultiHopExactAmountIn ( daiAmountIn , usdcAmountOutMin , .TypedVals ) ; assert ( usdcAmountOut >= usdcAmountOutMin , .TypedVals ) ; .Statements + + + + testSwapMultiHopExactAmountOut + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 20 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidUsdc . mint ( address ( this , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidUsdc . approve ( address ( vidUni , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountOut = 2 * 1e18 ; vidUni . swapSingleHopExactAmountOut ( daiAmountOut , 4 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidUsdc . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; uint256 amountOutDesired = 1e6 ; uint256 amountOut = vidUni . swapMultiHopExactAmountOut ( amountOutDesired , daiAmountOut , .TypedVals ) ; assert ( amountOut == amountOutDesired , .TypedVals ) ; .Statements + + + + testSwapSingleHopExactAmountIn + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 2 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountMin = 1 ; uint256 daiAmountOut = vidUni . swapSingleHopExactAmountIn ( wethAmount , daiAmountMin , .TypedVals ) ; assert ( daiAmountOut >= daiAmountMin , .TypedVals ) ; .Statements + + + + testSwapSingleHopExactAmountOut + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 10 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 6 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountDesired = 1e18 ; uint256 daiAmountOut = vidUni . swapSingleHopExactAmountOut ( daiAmountDesired , 2 * wethAmount , .TypedVals ) ; assert ( daiAmountOut == daiAmountDesired , .TypedVals ) ; .Statements + + + + ... + + + wETHMock + + + (allowance |-> mapping ( address wethownr => mapping ( address wethspdr => uint256 ) )) + (balanceOf |-> mapping ( address wethact => uint256 )) + (constUINT256MAX |-> uint256) + + + ListItem ( constUINT256MAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) + + + + + allowance + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( wethownr ) + ListItem ( wethspdr ) + + + ListItem ( mapping ( address wethownr => mapping ( address wethspdr => uint256 ) ) ) + + + ListItem ( noId ) + + + false + + + return allowance [ wethownr ] [ wethspdr ] ; .Statements + + + + approve + + + external + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( spender ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + allowance [ msg . sender ] [ spender ] = value ; emit approvalEvent ( msg . sender , spender , value , .TypedVals ) ; return true ; .Statements + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( wethact ) + + + ListItem ( mapping ( address wethact => uint256 ) ) + + + ListItem ( noId ) + + + false + + + return balanceOf [ wethact ] ; .Statements + + + + decimals + + + external + + + .List + + + .List + + + ListItem ( uint8 ) + + + ListItem ( noId ) + + + false + + + return 18 ; .Statements + + + + deposit + + + external + + + .List + + + .List + + + .List + + + .List + + + true + + + balanceOf [ msg . sender ] = balanceOf [ msg . sender ] + msg . value ; emit transferEvent ( address ( 0 , .TypedVals ) , msg . sender , msg . value , .TypedVals ) ; .Statements + + + + transfer + + + external + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + if ( to != address ( 0 , .TypedVals ) && to != address ( this , .TypedVals ) ) { uint256 balance = balanceOf [ msg . sender ] ; require ( balance >= value , "WETH: transfer amount exceeds balance" , .TypedVals ) ; balanceOf [ msg . sender ] = balance - value ; balanceOf [ to ] = balanceOf [ to ] + value ; emit transferEvent ( msg . sender , to , value , .TypedVals ) ; .Statements } else { uint256 balance = balanceOf [ msg . sender ] ; require ( balance >= value , "WETH: burn amount exceeds balance" , .TypedVals ) ; balanceOf [ msg . sender ] = balance - value ; emit transferEvent ( msg . sender , address ( 0 , .TypedVals ) , value , .TypedVals ) ; ( bool success , ) = msg . sender . call { value : value , .KeyValues } ( "" , .TypedVals ) ; require ( success , "WETH: ETH transfer failed" , .TypedVals ) ; .Statements } return true ; .Statements + + + + transferFrom + + + external + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + if ( from != msg . sender ) { uint256 allowed = allowance [ from ] [ msg . sender ] ; if ( allowed != constUINT256MAX ) { require ( allowed >= value , "WETH: request exceeds allowance" , .TypedVals ) ; uint256 reduced = allowed - value ; allowance [ from ] [ msg . sender ] = reduced ; emit approvalEvent ( from , msg . sender , reduced , .TypedVals ) ; .Statements } .Statements } if ( to != address ( 0 , .TypedVals ) && to != address ( this , .TypedVals ) ) { uint256 balance = balanceOf [ from ] ; require ( balance >= value , "WETH: transfer amount exceeds balance" , .TypedVals ) ; balanceOf [ from ] = balance - value ; balanceOf [ to ] = balanceOf [ to ] + value ; emit transferEvent ( from , to , value , .TypedVals ) ; .Statements } else { uint256 balance = balanceOf [ from ] ; require ( balance >= value , "WETH: burn amount exceeds balance" , .TypedVals ) ; balanceOf [ from ] = balance - value ; emit transferEvent ( from , address ( 0 , .TypedVals ) , value , .TypedVals ) ; ( bool success , ) = msg . sender . call { value : value , .KeyValues } ( "" , .TypedVals ) ; require ( success , "WETH: ETH transfer failed" , .TypedVals ) ; .Statements } return true ; .Statements + + + + + + + approvalEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + transferEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + + + + ) + [priority(40)] + +endmodule +``` + ```k module SOLIDITY-DATA-SYNTAX imports MINT-SYNTAX @@ -178,8 +2570,10 @@ module SOLIDITY imports SOLIDITY-TRANSACTION imports SOLIDITY-EXPRESSION imports SOLIDITY-STATEMENT + imports SOLIDITY-UNISWAP-INIT-SUMMARY - rule _:PragmaDefinition Ss:SourceUnits => Ss + rule _:PragmaDefinition Ss:SourceUnits => Ss ... + false rule S:SourceUnit Ss:SourceUnits => S ~> Ss rule .SourceUnits => .K rule C:ContractBodyElement Cc:ContractBodyElements => C ~> Cc From 327a656f29b1aebdc2c6487c25828c2e661ee0ce Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Mon, 9 Sep 2024 17:23:01 -0500 Subject: [PATCH 2/9] Update krun-sol to pass new configuration variable. --- bin/kparse-bool | 2 ++ bin/krun-sol | 5 +++-- 2 files changed, 5 insertions(+), 2 deletions(-) create mode 100755 bin/kparse-bool diff --git a/bin/kparse-bool b/bin/kparse-bool new file mode 100755 index 0000000..0a0f9b3 --- /dev/null +++ b/bin/kparse-bool @@ -0,0 +1,2 @@ +#!/bin/bash +kparse -d "$(dirname "$0")/../solidity-kompiled" -s Bool -m SOLIDITY-DATA-SYNTAX "$(cat "$1")" diff --git a/bin/krun-sol b/bin/krun-sol index 928509a..d8bb832 100755 --- a/bin/krun-sol +++ b/bin/krun-sol @@ -1,5 +1,6 @@ #!/bin/bash contract="$1" txn="$2" -shift; shift -krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" --no-expand-macros "$@" +isuniswap="$3" +shift; shift; shift +krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" -cISUNISWAP="$isuniswap" -pISUNISWAP="$(dirname "$0")/kparse-bool" --no-expand-macros "$@" From 2cee49f37ad717a20d15398cc6a5e620d946951c Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 11 Sep 2024 11:22:53 -0500 Subject: [PATCH 3/9] Edited Makefile according to the modification to krun-sol. --- Makefile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 1ef218f..58f8321 100644 --- a/Makefile +++ b/Makefile @@ -75,13 +75,13 @@ test-aave: test-regression: ${REGRESSION_TESTS} -$(REGRESSION_TESTS): %.out: %.sol %.txn %.ref $(SEMANTICS_FILE_NAME)-kompiled/timestamp - ulimit -s 65536 && bin/krun-sol $*.sol $*.txn > $*.out 2>&1 +$(REGRESSION_TESTS): %.out: %.sol %.txn %.ref %.smr $(SEMANTICS_FILE_NAME)-kompiled/timestamp + ulimit -s 65536 && bin/krun-sol $*.sol $*.txn $*.smr > $*.out 2>&1 diff -U3 -w $*.ref $*.out test-examples: ${EXAMPLE_TESTS} .SECONDEXPANSION: -$(EXAMPLE_TESTS): %.out: $$(subst $(TRANSACTIONS_DIR), $(EXAMPLES_DIR), $$(@D)).sol %.txn %.ref $(SEMANTICS_FILE_NAME)-kompiled/timestamp - ulimit -s 65536 && bin/krun-sol $< $*.txn > $*.out 2>&1 +$(EXAMPLE_TESTS): %.out: $$(subst $(TRANSACTIONS_DIR), $(EXAMPLES_DIR), $$(@D)).sol %.txn %.ref %.smr $(SEMANTICS_FILE_NAME)-kompiled/timestamp + ulimit -s 65536 && bin/krun-sol $< $*.txn $*.smr > $*.out 2>&1 diff -U3 -w $*.ref $*.out From b6122ecff3f06e12a7ce29a7c80f999c0ee92479 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Mon, 9 Sep 2024 17:44:49 -0500 Subject: [PATCH 4/9] Added new input files to read the configuration variable from. --- test/regression/arithmetic.smr | 1 + test/regression/arraystestcontract.smr | 1 + test/regression/block.smr | 1 + test/regression/boolean.smr | 1 + test/regression/contract.smr | 1 + test/regression/emit.smr | 1 + test/regression/eventtestcontract.smr | 1 + test/regression/for.smr | 1 + test/regression/function.smr | 1 + test/regression/if.smr | 1 + test/regression/increment.smr | 1 + test/regression/mapstestcontract.smr | 1 + test/regression/swaps.smr | 1 + test/transactions/swaps/UniswapV2Swap/UniswapTest.smr | 1 + .../swaps/UniswapV2SwapRenamed/UniswapTestRenamed.smr | 1 + 15 files changed, 15 insertions(+) create mode 100644 test/regression/arithmetic.smr create mode 100644 test/regression/arraystestcontract.smr create mode 100644 test/regression/block.smr create mode 100644 test/regression/boolean.smr create mode 100644 test/regression/contract.smr create mode 100644 test/regression/emit.smr create mode 100644 test/regression/eventtestcontract.smr create mode 100644 test/regression/for.smr create mode 100644 test/regression/function.smr create mode 100644 test/regression/if.smr create mode 100644 test/regression/increment.smr create mode 100644 test/regression/mapstestcontract.smr create mode 100644 test/regression/swaps.smr create mode 100644 test/transactions/swaps/UniswapV2Swap/UniswapTest.smr create mode 100644 test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.smr diff --git a/test/regression/arithmetic.smr b/test/regression/arithmetic.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/arithmetic.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/arraystestcontract.smr b/test/regression/arraystestcontract.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/arraystestcontract.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/block.smr b/test/regression/block.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/block.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/boolean.smr b/test/regression/boolean.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/boolean.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/contract.smr b/test/regression/contract.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/contract.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/emit.smr b/test/regression/emit.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/emit.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/eventtestcontract.smr b/test/regression/eventtestcontract.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/eventtestcontract.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/for.smr b/test/regression/for.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/for.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/function.smr b/test/regression/function.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/function.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/if.smr b/test/regression/if.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/if.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/increment.smr b/test/regression/increment.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/increment.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/mapstestcontract.smr b/test/regression/mapstestcontract.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/mapstestcontract.smr @@ -0,0 +1 @@ +false diff --git a/test/regression/swaps.smr b/test/regression/swaps.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/regression/swaps.smr @@ -0,0 +1 @@ +false diff --git a/test/transactions/swaps/UniswapV2Swap/UniswapTest.smr b/test/transactions/swaps/UniswapV2Swap/UniswapTest.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/transactions/swaps/UniswapV2Swap/UniswapTest.smr @@ -0,0 +1 @@ +false diff --git a/test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.smr b/test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.smr new file mode 100644 index 0000000..27ba77d --- /dev/null +++ b/test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.smr @@ -0,0 +1 @@ +true From aa9c170fe2322671cafed7a2c12daab67137d207 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Mon, 9 Sep 2024 17:45:50 -0500 Subject: [PATCH 5/9] Updated reference outputs, adding the new cell. --- test/regression/arithmetic.ref | 3 +++ test/regression/arraystestcontract.ref | 3 +++ test/regression/block.ref | 3 +++ test/regression/boolean.ref | 3 +++ test/regression/contract.ref | 3 +++ test/regression/emit.ref | 3 +++ test/regression/eventtestcontract.ref | 3 +++ test/regression/for.ref | 3 +++ test/regression/function.ref | 3 +++ test/regression/if.ref | 3 +++ test/regression/increment.ref | 3 +++ test/regression/mapstestcontract.ref | 3 +++ test/regression/swaps.ref | 3 +++ test/transactions/swaps/UniswapV2Swap/UniswapTest.ref | 3 +++ .../swaps/UniswapV2SwapRenamed/UniswapTestRenamed.ref | 3 +++ 15 files changed, 45 insertions(+) diff --git a/test/regression/arithmetic.ref b/test/regression/arithmetic.ref index 9c1b9e1..8f0b8dc 100644 --- a/test/regression/arithmetic.ref +++ b/test/regression/arithmetic.ref @@ -2,6 +2,9 @@ .K + + false + TestArithmetic diff --git a/test/regression/arraystestcontract.ref b/test/regression/arraystestcontract.ref index 903d105..9f931fc 100644 --- a/test/regression/arraystestcontract.ref +++ b/test/regression/arraystestcontract.ref @@ -2,6 +2,9 @@ .K + + false + TestArraysContract diff --git a/test/regression/block.ref b/test/regression/block.ref index 85c35ab..c391753 100644 --- a/test/regression/block.ref +++ b/test/regression/block.ref @@ -2,6 +2,9 @@ .K + + false + BlockTest diff --git a/test/regression/boolean.ref b/test/regression/boolean.ref index e8ea87d..1782854 100644 --- a/test/regression/boolean.ref +++ b/test/regression/boolean.ref @@ -2,6 +2,9 @@ .K + + false + BoolTest diff --git a/test/regression/contract.ref b/test/regression/contract.ref index 530568b..05e5b9c 100644 --- a/test/regression/contract.ref +++ b/test/regression/contract.ref @@ -2,6 +2,9 @@ .K + + false + UniswapV2Swap diff --git a/test/regression/emit.ref b/test/regression/emit.ref index 9c8f959..adcf165 100644 --- a/test/regression/emit.ref +++ b/test/regression/emit.ref @@ -3,6 +3,9 @@ Approval(1, 0, 2) .K + + false + EmitTest diff --git a/test/regression/eventtestcontract.ref b/test/regression/eventtestcontract.ref index 075bdd6..4168afa 100644 --- a/test/regression/eventtestcontract.ref +++ b/test/regression/eventtestcontract.ref @@ -2,6 +2,9 @@ .K + + false + TestEventsContract diff --git a/test/regression/for.ref b/test/regression/for.ref index 2c2ce0f..6eb4154 100644 --- a/test/regression/for.ref +++ b/test/regression/for.ref @@ -2,6 +2,9 @@ .K + + false + ForTest diff --git a/test/regression/function.ref b/test/regression/function.ref index 28f5615..9665508 100644 --- a/test/regression/function.ref +++ b/test/regression/function.ref @@ -2,6 +2,9 @@ .K + + false + UniswapV2SwapTest diff --git a/test/regression/if.ref b/test/regression/if.ref index eefe65e..3ef42b9 100644 --- a/test/regression/if.ref +++ b/test/regression/if.ref @@ -2,6 +2,9 @@ .K + + false + IfTest diff --git a/test/regression/increment.ref b/test/regression/increment.ref index c7a13af..393b888 100644 --- a/test/regression/increment.ref +++ b/test/regression/increment.ref @@ -2,6 +2,9 @@ .K + + false + IncTest diff --git a/test/regression/mapstestcontract.ref b/test/regression/mapstestcontract.ref index 9912701..8cb4997 100644 --- a/test/regression/mapstestcontract.ref +++ b/test/regression/mapstestcontract.ref @@ -2,6 +2,9 @@ .K + + false + TestMapsContract diff --git a/test/regression/swaps.ref b/test/regression/swaps.ref index cb7fd58..4d725fa 100644 --- a/test/regression/swaps.ref +++ b/test/regression/swaps.ref @@ -15002,6 +15002,9 @@ Swap(7, 1000000000000000000, 0, 0, 332669001559828603, 2) .K + + false + UniswapV2SwapTest diff --git a/test/transactions/swaps/UniswapV2Swap/UniswapTest.ref b/test/transactions/swaps/UniswapV2Swap/UniswapTest.ref index 11f14e9..bf7f885 100644 --- a/test/transactions/swaps/UniswapV2Swap/UniswapTest.ref +++ b/test/transactions/swaps/UniswapV2Swap/UniswapTest.ref @@ -99,6 +99,9 @@ Transfer(6, 2, 1999999999998955749) .K + + false + UniswapV2SwapTest diff --git a/test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.ref b/test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.ref index 9fbfa25..05bdf82 100644 --- a/test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.ref +++ b/test/transactions/swaps/UniswapV2SwapRenamed/UniswapTestRenamed.ref @@ -99,6 +99,9 @@ transferEvent(6, 2, 1999999999998955749) .K + + true + uniswapV2SwapTest From e6cf62bc2aaf5696b7f0dbc4f46f66d6e76337fa Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 11 Sep 2024 11:51:33 -0500 Subject: [PATCH 6/9] Moved tokens of Uniswap in separate module. --- src/solidity.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/solidity.md b/src/solidity.md index ba794b9..9cb05c7 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -85,8 +85,7 @@ endmodule ``` ```k -module SOLIDITY-UNISWAP-INIT-SUMMARY - imports SOLIDITY-CONFIGURATION +module SOLIDITY-UNISWAP-TOKENS syntax Id ::= "account" [token] | "act" [token] @@ -249,6 +248,14 @@ module SOLIDITY-UNISWAP-INIT-SUMMARY syntax Decimal ::= "1e18" [token] | "1e6" [token] +endmodule +``` + +```k +module SOLIDITY-UNISWAP-INIT-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-UNISWAP-TOKENS + rule _:Program => .K ... true (_:CompileCell => From 36474262b482caa592b4f3c6788e75525086525d Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 11 Sep 2024 12:18:38 -0500 Subject: [PATCH 7/9] Moved modules related to uniswap summarization to separate file --- src/solidity.md | 2399 +------------------------------------- src/uniswap-summaries.md | 2399 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 2400 insertions(+), 2398 deletions(-) create mode 100644 src/uniswap-summaries.md diff --git a/src/solidity.md b/src/solidity.md index 9cb05c7..3db1edc 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -7,6 +7,7 @@ requires "contract.md" requires "transaction.md" requires "expression.md" requires "statement.md" +requires "uniswap-summaries.md" module SOLIDITY-CONFIGURATION imports SOLIDITY-DATA @@ -84,2404 +85,6 @@ module SOLIDITY-CONFIGURATION endmodule ``` -```k -module SOLIDITY-UNISWAP-TOKENS - - syntax Id ::= "account" [token] - | "act" [token] - | "allowance" [token] - | "allowed" [token] - | "amountIn" [token] - | "amountInMax" [token] - | "amountInWithFee" [token] - | "amountOut" [token] - | "amountOutDesired" [token] - | "amountOutMin" [token] - | "amounts" [token] - | "amount0In" [token] - | "amount1In" [token] - | "amount0Out" [token] - | "amount1Out" [token] - | "approvalEvent" [token] - | "approve" [token] - | "balance" [token] - | "balanceOf" [token] - | "balance0" [token] - | "balance0Adjusted" [token] - | "balance1" [token] - | "balance1Adjusted" [token] - | "block" [token] - | "blockTimestamp" [token] - | "blockTimestampLast" [token] - | "burn" [token] - | "call" [token] - | "constMINIMUMLIQUIDITY" [token] - | "constUINTMAX" [token] - | "constUINT112MAX" [token] - | "constUINT256MAX" [token] - | "currentAllowance" [token] - | "dai" [token] - | "daiact" [token] - | "daiAmountDesired" [token] - | "daiAmountIn" [token] - | "daiAmountMin" [token] - | "daiAmountOut" [token] - | "dAIMock" [token] - | "daiownr" [token] - | "daispdr" [token] - | "decimals" [token] - | "denominator" [token] - | "deposit" [token] - | "dst" [token] - | "emitEvent" [token] - | "from" [token] - | "fromBalance" [token] - | "getLocalPair" [token] - | "getReserves" [token] - | "guy" [token] - | "i" [token] - | "iERC20" [token] - | "input" [token] - | "kLast" [token] - | "length" [token] - | "localPairs" [token] - | "mint" [token] - | "mintOnDeposit" [token] - | "msg" [token] - | "numerator" [token] - | "output" [token] - | "owner" [token] - | "pair" [token] - | "pairEl1" [token] - | "pairEl2" [token] - | "pairReserves" [token] - | "path" [token] - | "price0CumulativeLast" [token] - | "price1CumulativeLast" [token] - | "reduced" [token] - | "reserveIn" [token] - | "reserveOut" [token] - | "reserves" [token] - | "reserve0" [token] - | "reserve1" [token] - | "router" [token] - | "safeTransferFrom" [token] - | "sender" [token] - | "setLocalPair" [token] - | "setUp" [token] - | "spender" [token] - | "src" [token] - | "success" [token] - | "swap" [token] - | "swapExactTokensForTokens" [token] - | "swapEvent" [token] - | "swapMultiHopExactAmountIn" [token] - | "swapMultiHopExactAmountOut" [token] - | "swapSingleHopExactAmountIn" [token] - | "swapSingleHopExactAmountOut" [token] - | "swapTokensForExactTokens" [token] - | "sync" [token] - | "syncEvent" [token] - | "syncLocalPair" [token] - | "testSwapMultiHopExactAmountIn" [token] - | "testSwapMultiHopExactAmountOut" [token] - | "testSwapSingleHopExactAmountIn" [token] - | "testSwapSingleHopExactAmountOut" [token] - | "this" [token] - | "timeElapsed" [token] - | "timestamp" [token] - | "to" [token] - | "tokenA" [token] - | "tokenB" [token] - | "tokens" [token] - | "token0" [token] - | "token1" [token] - | "totalSupply" [token] - | "transfer" [token] - | "transferEvent" [token] - | "transferFrom" [token] - | "uniswapV2LibraryGetAmountIn" [token] - | "uniswapV2LibraryGetAmountOut" [token] - | "uniswapV2LibraryGetAmountsIn" [token] - | "uniswapV2LibraryGetAmountsOut" [token] - | "uniswapV2LibraryGetReserves" [token] - | "uniswapV2LibraryPairFor" [token] - | "uniswapV2LibrarySortTokens" [token] - | "uniswapV2Pair" [token] - | "uniswapV2Router02" [token] - | "uniswapV2Swap" [token] - | "uniswapV2SwapTest" [token] - | "usdc" [token] - | "usdcAmountOut" [token] - | "usdcAmountOutMin" [token] - | "uSDCMock" [token] - | "usr" [token] - | "value" [token] - | "wad" [token] - | "weth" [token] - | "wethact" [token] - | "wethAmount" [token] - | "wETHMock" [token] - | "wethownr" [token] - | "wethspdr" [token] - - syntax Id ::= "vidAllowances" [token] - | "vidBalances" [token] - | "vidDai" [token] - | "vidReserve0" [token] - | "vidReserve1" [token] - | "vidTo" [token] - | "vidToken0" [token] - | "vidToken1" [token] - | "vidTotalSupply" [token] - | "vidUni" [token] - | "vidUsdc" [token] - | "vidWeth" [token] - | "fidApprove" [token] - | "fidSpendAllowance" [token] - | "fidSwap" [token] - | "fidTransfer" [token] - | "fidUpdate" [token] - - syntax Id ::= "require" [token] | "assert" [token] - - syntax Decimal ::= "1e18" [token] - | "1e6" [token] - -endmodule -``` - -```k -module SOLIDITY-UNISWAP-INIT-SUMMARY - imports SOLIDITY-CONFIGURATION - imports SOLIDITY-UNISWAP-TOKENS - - rule _:Program => .K ... - true - (_:CompileCell => - - - uniswapV2SwapTest - - - - - iERC20 - - - - - approve - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( bool ) - - - - balanceOf - - - ListItem ( address ) - - - ListItem ( uint256 ) - - - - transfer - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( bool ) - - - - transferFrom - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( bool ) - - - - - - - - - dAIMock - - - (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) - (balanceOf |-> mapping ( address daiact => uint256 )) - (constUINTMAX |-> uint256) - (totalSupply |-> uint256) - - - ListItem ( constUINTMAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) - - - - - allowance - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( daiownr ) - ListItem ( daispdr ) - - - ListItem ( mapping ( address daiownr => mapping ( address daispdr => uint256 ) ) ) - - - ListItem ( noId ) - - - false - - - return allowance [ daiownr ] [ daispdr ] ; .Statements - - - - approve - - - external - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( usr ) - ListItem ( wad ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - allowance [ msg . sender ] [ usr ] = wad ; emit approvalEvent ( msg . sender , usr , wad , .TypedVals ) ; return true ; .Statements - - - - balanceOf - - - public - - - ListItem ( address ) - - - ListItem ( daiact ) - - - ListItem ( mapping ( address daiact => uint256 ) ) - - - ListItem ( noId ) - - - false - - - return balanceOf [ daiact ] ; .Statements - - - - burn - - - public - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( usr ) - ListItem ( wad ) - - - .List - - - .List - - - false - - - if ( balanceOf [ usr ] >= wad ) { balanceOf [ usr ] = balanceOf [ usr ] - wad ; totalSupply = totalSupply - wad ; .Statements } .Statements - - - - decimals - - - external - - - .List - - - .List - - - ListItem ( uint8 ) - - - ListItem ( noId ) - - - false - - - return 18 ; .Statements - - - - mint - - - public - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( usr ) - ListItem ( wad ) - - - .List - - - .List - - - false - - - balanceOf [ usr ] = balanceOf [ usr ] + wad ; totalSupply = totalSupply + wad ; emit transferEvent ( address ( 0 , .TypedVals ) , usr , wad , .TypedVals ) ; .Statements - - - - mintOnDeposit - - - public - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( usr ) - ListItem ( wad ) - - - .List - - - .List - - - false - - - mint ( usr , wad , .TypedVals ) ; .Statements - - - - safeTransferFrom - - - external - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( from ) - ListItem ( to ) - ListItem ( value ) - - - .List - - - .List - - - false - - - transferFrom ( from , to , value , .TypedVals ) ; .Statements - - - - totalSupply - - - public - - - .List - - - .List - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return totalSupply ; .Statements - - - - transfer - - - public - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( dst ) - ListItem ( wad ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - return transferFrom ( msg . sender , dst , wad , .TypedVals ) ; .Statements - - - - transferFrom - - - public - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( src ) - ListItem ( dst ) - ListItem ( wad ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - require ( balanceOf [ src ] >= wad , "Dai/insufficient-balance" , .TypedVals ) ; if ( src != msg . sender && allowance [ src ] [ msg . sender ] != constUINTMAX ) { require ( allowance [ src ] [ msg . sender ] >= wad , "Dai/insufficient-allowance" , .TypedVals ) ; allowance [ src ] [ msg . sender ] = allowance [ src ] [ msg . sender ] - wad ; .Statements } balanceOf [ src ] = balanceOf [ src ] - wad ; balanceOf [ dst ] = balanceOf [ dst ] + wad ; emit transferEvent ( src , dst , wad , .TypedVals ) ; return true ; .Statements - - - - - - - approvalEvent - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( src ) - ListItem ( guy ) - ListItem ( wad ) - - - SetItem ( 0 ) - SetItem ( 1 ) - - - - transferEvent - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( src ) - ListItem ( dst ) - ListItem ( wad ) - - - SetItem ( 0 ) - SetItem ( 1 ) - - - - - - uSDCMock - - - (constUINT256MAX |-> uint256) - (vidAllowances |-> mapping ( address account => mapping ( address spender => uint256 ) )) - (vidBalances |-> mapping ( address account => uint256 )) - (vidTotalSupply |-> uint256) - - - ListItem ( constUINT256MAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) - - - - - allowance - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( owner ) - ListItem ( spender ) - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return vidAllowances [ owner ] [ spender ] ; .Statements - - - - approve - - - public - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( spender ) - ListItem ( value ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - address owner = msg . sender ; fidApprove ( owner , spender , value , true , .TypedVals ) ; return true ; .Statements - - - - balanceOf - - - public - - - ListItem ( address ) - - - ListItem ( account ) - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return vidBalances [ account ] ; .Statements - - - - decimals - - - external - - - .List - - - .List - - - ListItem ( uint8 ) - - - ListItem ( noId ) - - - false - - - return 18 ; .Statements - - - - fidApprove - - - private - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - ListItem ( bool ) - - - ListItem ( owner ) - ListItem ( spender ) - ListItem ( value ) - ListItem ( emitEvent ) - - - .List - - - .List - - - false - - - require ( owner != address ( 0 , .TypedVals ) , "USDC: invalid approver" , .TypedVals ) ; require ( spender != address ( 0 , .TypedVals ) , "USDC: invalid spender" , .TypedVals ) ; vidAllowances [ owner ] [ spender ] = value ; if ( emitEvent ) { emit approvalEvent ( owner , spender , value , .TypedVals ) ; .Statements } .Statements - - - - fidSpendAllowance - - - private - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( owner ) - ListItem ( spender ) - ListItem ( value ) - - - .List - - - .List - - - false - - - uint256 currentAllowance = allowance ( owner , spender , .TypedVals ) ; if ( currentAllowance != constUINT256MAX ) { require ( currentAllowance >= value , "USDC: insufficient allowance" , .TypedVals ) ; fidApprove ( owner , spender , currentAllowance - value , false , .TypedVals ) ; .Statements } .Statements - - - - fidTransfer - - - private - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( from ) - ListItem ( to ) - ListItem ( value ) - - - .List - - - .List - - - false - - - require ( from != address ( 0 , .TypedVals ) , "USDC: invalid sender" , .TypedVals ) ; require ( to != address ( 0 , .TypedVals ) , "USDC: invalid receiver" , .TypedVals ) ; fidUpdate ( from , to , value , .TypedVals ) ; .Statements - - - - fidUpdate - - - private - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( from ) - ListItem ( to ) - ListItem ( value ) - - - .List - - - .List - - - false - - - if ( from == address ( 0 , .TypedVals ) ) { vidTotalSupply = vidTotalSupply + value ; .Statements } else { uint256 fromBalance = vidBalances [ from ] ; require ( fromBalance >= value , "USDC: insufficient balance" , .TypedVals ) ; vidBalances [ from ] = fromBalance - value ; .Statements } if ( to == address ( 0 , .TypedVals ) ) { vidTotalSupply = vidTotalSupply - value ; .Statements } else { vidBalances [ to ] = vidBalances [ to ] + value ; .Statements } emit transferEvent ( from , to , value , .TypedVals ) ; .Statements - - - - mint - - - public - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( account ) - ListItem ( value ) - - - .List - - - .List - - - false - - - require ( account != address ( 0 , .TypedVals ) , "USDC: invalid receiver" , .TypedVals ) ; fidUpdate ( address ( 0 , .TypedVals ) , account , value , .TypedVals ) ; .Statements - - - - transfer - - - public - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( to ) - ListItem ( value ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - address owner = msg . sender ; fidTransfer ( owner , to , value , .TypedVals ) ; return true ; .Statements - - - - transferFrom - - - public - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( from ) - ListItem ( to ) - ListItem ( value ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - address spender = msg . sender ; fidSpendAllowance ( from , spender , value , .TypedVals ) ; fidTransfer ( from , to , value , .TypedVals ) ; return true ; .Statements - - - - - - - approvalEvent - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( owner ) - ListItem ( spender ) - ListItem ( value ) - - - SetItem ( 0 ) - SetItem ( 1 ) - - - - transferEvent - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( from ) - ListItem ( to ) - ListItem ( value ) - - - SetItem ( 0 ) - SetItem ( 1 ) - - - - - - uniswapV2Pair - - - (balanceOf |-> mapping ( address act => uint256 )) - (blockTimestampLast |-> uint32) - (constMINIMUMLIQUIDITY |-> uint256) - (constUINT112MAX |-> uint256) - (kLast |-> uint256) - (price0CumulativeLast |-> uint256) - (price1CumulativeLast |-> uint256) - (reserve0 |-> uint112) - (reserve1 |-> uint112) - (token0 |-> address) - (token1 |-> address) - (totalSupply |-> uint256) - - - ListItem ( constUINT112MAX = 0xffffffffffffffffffffffffffff ; ) - ListItem ( constMINIMUMLIQUIDITY = 10 ** 3 ; ) - - - - - balanceOf - - - public - - - ListItem ( address ) - - - ListItem ( act ) - - - ListItem ( mapping ( address act => uint256 ) ) - - - ListItem ( noId ) - - - false - - - return balanceOf [ act ] ; .Statements - - - - constMINIMUMLIQUIDITY - - - public - - - .List - - - .List - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return constMINIMUMLIQUIDITY ; .Statements - - - - constructor - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( vidToken0 ) - ListItem ( vidToken1 ) - - - .List - - - .List - - - false - - - token0 = vidToken0 ; token1 = vidToken1 ; .Statements - - - - fidUpdate - - - private - - - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( uint112 ) - ListItem ( uint112 ) - - - ListItem ( balance0 ) - ListItem ( balance1 ) - ListItem ( vidReserve0 ) - ListItem ( vidReserve1 ) - - - .List - - - .List - - - false - - - require ( balance0 <= constUINT112MAX && balance1 <= constUINT112MAX , "UniswapV2: OVERFLOW" , .TypedVals ) ; uint32 blockTimestamp = uint32 ( block . timestamp % 2 ** 32 , .TypedVals ) ; uint32 timeElapsed = blockTimestamp - blockTimestampLast ; if ( timeElapsed > 0 && vidReserve0 != 0 && vidReserve1 != 0 ) { price0CumulativeLast = price0CumulativeLast + vidReserve1 / vidReserve0 * timeElapsed ; price1CumulativeLast = price1CumulativeLast + vidReserve0 / vidReserve1 * timeElapsed ; .Statements } reserve0 = uint112 ( balance0 , .TypedVals ) ; reserve1 = uint112 ( balance1 , .TypedVals ) ; blockTimestampLast = blockTimestamp ; emit syncEvent ( reserve0 , reserve1 , .TypedVals ) ; .Statements - - - - getReserves - - - public - - - .List - - - .List - - - ListItem ( uint112 [ ]::TypeName ) - - - ListItem ( reserves ) - - - false - - - reserves = new uint112 [ ] ( 3 , .TypedVals ) ; reserves [ 0 ] = reserve0 ; reserves [ 1 ] = reserve1 ; reserves [ 2 ] = blockTimestampLast ; .Statements - - - - kLast - - - public - - - .List - - - .List - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return kLast ; .Statements - - - - price0CumulativeLast - - - public - - - .List - - - .List - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return price0CumulativeLast ; .Statements - - - - price1CumulativeLast - - - public - - - .List - - - .List - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return price1CumulativeLast ; .Statements - - - - swap - - - external - - - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( address ) - - - ListItem ( amount0Out ) - ListItem ( amount1Out ) - ListItem ( to ) - - - .List - - - .List - - - false - - - require ( amount0Out > 0 || amount1Out > 0 , "UniswapV2: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; uint112 [ ] memory reserves = getReserves ( .TypedVals ) ; require ( amount0Out < reserves [ 0 ] && amount1Out < reserves [ 1 ] , "UniswapV2: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 balance0 ; uint256 balance1 ; { address vidToken0 = token0 ; address vidToken1 = token1 ; require ( to != vidToken0 && to != vidToken1 , "UniswapV2: INVALID_TO" , .TypedVals ) ; if ( amount0Out > 0 ) iERC20 ( vidToken0 , .TypedVals ) . transfer ( to , amount0Out , .TypedVals ) ; if ( amount1Out > 0 ) iERC20 ( vidToken1 , .TypedVals ) . transfer ( to , amount1Out , .TypedVals ) ; balance0 = iERC20 ( vidToken0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; balance1 = iERC20 ( vidToken1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; .Statements } uint256 amount0In = balance0 > reserves [ 0 ] - amount0Out ? balance0 - ( reserves [ 0 ] - amount0Out ) : 0 ; uint256 amount1In = balance1 > reserves [ 1 ] - amount1Out ? balance1 - ( reserves [ 1 ] - amount1Out ) : 0 ; require ( amount0In > 0 || amount1In > 0 , "UniswapV2: INSUFFICIENT_INPUT_AMOUNT" , .TypedVals ) ; { uint256 balance0Adjusted = balance0 * 1000 - amount0In * 3 ; uint256 balance1Adjusted = balance1 * 1000 - amount1In * 3 ; require ( balance0Adjusted * balance1Adjusted >= uint256 ( reserves [ 0 ] , .TypedVals ) * reserves [ 1 ] * 1000 ** 2 , "UniswapV2: K" , .TypedVals ) ; .Statements } fidUpdate ( balance0 , balance1 , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; emit swapEvent ( msg . sender , amount0In , amount1In , amount0Out , amount1Out , to , .TypedVals ) ; .Statements - - - - sync - - - external - - - .List - - - .List - - - .List - - - .List - - - false - - - fidUpdate ( iERC20 ( token0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , iERC20 ( token1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , reserve0 , reserve1 , .TypedVals ) ; .Statements - - - - token0 - - - public - - - .List - - - .List - - - ListItem ( address ) - - - ListItem ( noId ) - - - false - - - return token0 ; .Statements - - - - token1 - - - public - - - .List - - - .List - - - ListItem ( address ) - - - ListItem ( noId ) - - - false - - - return token1 ; .Statements - - - - totalSupply - - - public - - - .List - - - .List - - - ListItem ( uint256 ) - - - ListItem ( noId ) - - - false - - - return totalSupply ; .Statements - - - - - - - swapEvent - - - ListItem ( address ) - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( address ) - - - ListItem ( sender ) - ListItem ( amount0In ) - ListItem ( amount1In ) - ListItem ( amount0Out ) - ListItem ( amount1Out ) - ListItem ( to ) - - - SetItem ( 0 ) - SetItem ( 5 ) - - - - syncEvent - - - ListItem ( uint112 ) - ListItem ( uint112 ) - - - ListItem ( reserve0 ) - ListItem ( reserve1 ) - - - .Set - - - - - - uniswapV2Router02 - - - localPairs |-> mapping ( address pairEl1 => mapping ( address pairEl2 => address ) ) - - - .List - - - - - fidSwap - - - private - - - ListItem ( uint256 [ ]::TypeName ) - ListItem ( address [ ]::TypeName ) - ListItem ( address ) - - - ListItem ( amounts ) - ListItem ( path ) - ListItem ( vidTo ) - - - .List - - - .List - - - false - - - { uint256 i ; while ( i < path . length - 1 ) { { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2LibrarySortTokens ( input , output , .TypedVals ) ; uint256 amountOut = amounts [ i + 1 ] ; uint256 amount0Out = input == tokens [ 0 ] ? uint256 ( 0 , .TypedVals ) : amountOut ; uint256 amount1Out = input == tokens [ 0 ] ? amountOut : uint256 ( 0 , .TypedVals ) ; address to = i < path . length - 2 ? uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) : vidTo ; uniswapV2Pair ( uniswapV2LibraryPairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements - - - - getLocalPair - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( tokenA ) - ListItem ( tokenB ) - - - ListItem ( address ) - - - ListItem ( pair ) - - - false - - - address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; pair = localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] ; .Statements - - - - localPairs - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( pairEl1 ) - ListItem ( pairEl2 ) - - - ListItem ( mapping ( address pairEl1 => mapping ( address pairEl2 => address ) ) ) - - - ListItem ( noId ) - - - false - - - return localPairs [ pairEl1 ] [ pairEl2 ] ; .Statements - - - - setLocalPair - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( tokenA ) - ListItem ( tokenB ) - - - .List - - - .List - - - false - - - address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] = address ( new uniswapV2Pair ( address ( tokens [ 0 ] , .TypedVals ) , address ( tokens [ 1 ] , .TypedVals ) , .TypedVals ) , .TypedVals ) ; .Statements - - - - swapExactTokensForTokens - - - external - - - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( address [ ]::TypeName ) - ListItem ( address ) - - - ListItem ( amountIn ) - ListItem ( amountOutMin ) - ListItem ( path ) - ListItem ( to ) - - - ListItem ( uint256 [ ]::TypeName ) - - - ListItem ( amounts ) - - - false - - - amounts = uniswapV2LibraryGetAmountsOut ( amountIn , path , .TypedVals ) ; require ( amounts [ amounts . length - 1 ] >= amountOutMin , "UniswapV2Router: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; iERC20 ( path [ 0 ] , .TypedVals ) . transferFrom ( msg . sender , uniswapV2LibraryPairFor ( path [ 0 ] , path [ 1 ] , .TypedVals ) , amounts [ 0 ] , .TypedVals ) ; fidSwap ( amounts , path , to , .TypedVals ) ; .Statements - - - - swapTokensForExactTokens - - - external - - - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( address [ ]::TypeName ) - ListItem ( address ) - - - ListItem ( amountOut ) - ListItem ( amountInMax ) - ListItem ( path ) - ListItem ( to ) - - - ListItem ( uint256 [ ]::TypeName ) - - - ListItem ( amounts ) - - - false - - - amounts = uniswapV2LibraryGetAmountsIn ( amountOut , path , .TypedVals ) ; require ( amounts [ 0 ] <= amountInMax , "UniswapV2Router: EXCESSIVE_INPUT_AMOUNT" , .TypedVals ) ; iERC20 ( path [ 0 ] , .TypedVals ) . transferFrom ( msg . sender , uniswapV2LibraryPairFor ( path [ 0 ] , path [ 1 ] , .TypedVals ) , amounts [ 0 ] , .TypedVals ) ; fidSwap ( amounts , path , to , .TypedVals ) ; .Statements - - - - syncLocalPair - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( tokenA ) - ListItem ( tokenB ) - - - .List - - - .List - - - false - - - address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; uniswapV2Pair ( localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] , .TypedVals ) . sync ( .TypedVals ) ; .Statements - - - - uniswapV2LibraryGetAmountIn - - - private - - - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( uint256 ) - - - ListItem ( amountOut ) - ListItem ( reserveIn ) - ListItem ( reserveOut ) - - - ListItem ( uint256 ) - - - ListItem ( amountIn ) - - - false - - - require ( amountOut > 0 , "UniswapV2Library: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; require ( reserveIn > 0 && reserveOut > 0 , "UniswapV2Library: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 numerator = reserveIn * amountOut * 1000 ; uint256 denominator = ( reserveOut - amountOut ) * 997 ; amountIn = denominator != 0 ? numerator / denominator + 1 : 1 ; .Statements - - - - uniswapV2LibraryGetAmountOut - - - private - - - ListItem ( uint256 ) - ListItem ( uint256 ) - ListItem ( uint256 ) - - - ListItem ( amountIn ) - ListItem ( reserveIn ) - ListItem ( reserveOut ) - - - ListItem ( uint256 ) - - - ListItem ( amountOut ) - - - false - - - require ( amountIn > 0 , "UniswapV2Library: INSUFFICIENT_INPUT_AMOUNT" , .TypedVals ) ; require ( reserveIn > 0 && reserveOut > 0 , "UniswapV2Library: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 amountInWithFee = amountIn * 997 ; uint256 numerator = amountInWithFee * reserveOut ; uint256 denominator = reserveIn * 1000 + amountInWithFee ; amountOut = numerator / denominator ; .Statements - - - - uniswapV2LibraryGetAmountsIn - - - private - - - ListItem ( uint256 ) - ListItem ( address [ ]::TypeName ) - - - ListItem ( amountOut ) - ListItem ( path ) - - - ListItem ( uint256 [ ]::TypeName ) - - - ListItem ( amounts ) - - - false - - - require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ amounts . length - 1 ] = amountOut ; { uint256 i = path . length - 1 ; while ( i > 0 ) { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i - 1 ] , path [ i ] , .TypedVals ) ; amounts [ i - 1 ] = uniswapV2LibraryGetAmountIn ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i -- ; .Statements } .Statements } .Statements - - - - uniswapV2LibraryGetAmountsOut - - - private - - - ListItem ( uint256 ) - ListItem ( address [ ]::TypeName ) - - - ListItem ( amountIn ) - ListItem ( path ) - - - ListItem ( uint256 [ ]::TypeName ) - - - ListItem ( amounts ) - - - false - - - require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; { uint256 i ; while ( i < path . length - 1 ) { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; amounts [ i + 1 ] = uniswapV2LibraryGetAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements - - - - uniswapV2LibraryGetReserves - - - private - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( tokenA ) - ListItem ( tokenB ) - - - ListItem ( uint256 [ ]::TypeName ) - - - ListItem ( reserves ) - - - false - - - reserves = new uint256 [ ] ( 2 , .TypedVals ) ; address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; uint112 [ ] memory pairReserves = uniswapV2Pair ( uniswapV2LibraryPairFor ( tokenA , tokenB , .TypedVals ) , .TypedVals ) . getReserves ( .TypedVals ) ; reserves [ 0 ] = tokenA == tokens [ 0 ] ? pairReserves [ 0 ] : pairReserves [ 1 ] ; reserves [ 1 ] = tokenA == tokens [ 0 ] ? pairReserves [ 1 ] : pairReserves [ 0 ] ; .Statements - - - - uniswapV2LibraryPairFor - - - private - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( tokenA ) - ListItem ( tokenB ) - - - ListItem ( address ) - - - ListItem ( pair ) - - - false - - - address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; pair = localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] ; .Statements - - - - uniswapV2LibrarySortTokens - - - private - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( tokenA ) - ListItem ( tokenB ) - - - ListItem ( address [ ]::TypeName ) - - - ListItem ( tokens ) - - - false - - - tokens = new address [ ] ( 2 , .TypedVals ) ; require ( tokenA != tokenB , "UniswapV2Library: IDENTICAL_ADDRESSES" , .TypedVals ) ; tokens [ 0 ] = tokenA < tokenB ? tokenA : tokenB ; tokens [ 1 ] = tokenA < tokenB ? tokenB : tokenA ; require ( tokens [ 0 ] != address ( 0 , .TypedVals ) , "UniswapV2Library: ZERO_ADDRESS" , .TypedVals ) ; .Statements - - - - ... - - - uniswapV2Swap - - - (dai |-> iERC20) - (router |-> uniswapV2Router02) - (usdc |-> iERC20) - (weth |-> iERC20) - - - .List - - - - - constructor - - - public - - - ListItem ( address ) - ListItem ( address ) - ListItem ( address ) - - - ListItem ( vidWeth ) - ListItem ( vidDai ) - ListItem ( vidUsdc ) - - - .List - - - .List - - - false - - - weth = iERC20 ( vidWeth , .TypedVals ) ; dai = iERC20 ( vidDai , .TypedVals ) ; usdc = iERC20 ( vidUsdc , .TypedVals ) ; router = new uniswapV2Router02 ( .TypedVals ) ; router . setLocalPair ( vidWeth , vidDai , .TypedVals ) ; router . setLocalPair ( vidWeth , vidUsdc , .TypedVals ) ; router . setLocalPair ( vidUsdc , vidDai , .TypedVals ) ; .Statements - - - - dai - - - public - - - .List - - - .List - - - ListItem ( iERC20 ) - - - ListItem ( noId ) - - - false - - - return dai ; .Statements - - - - router - - - public - - - .List - - - .List - - - ListItem ( uniswapV2Router02 ) - - - ListItem ( noId ) - - - false - - - return router ; .Statements - - - - swapMultiHopExactAmountIn - - - external - - - ListItem ( uint256 ) - ListItem ( uint256 ) - - - ListItem ( amountIn ) - ListItem ( amountOutMin ) - - - ListItem ( uint256 ) - - - ListItem ( amountOut ) - - - false - - - dai . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountIn , .TypedVals ) ; dai . approve ( address ( router , .TypedVals ) , amountIn , .TypedVals ) ; address [ ] memory path = new address [ ] ( 3 , .TypedVals ) ; path [ 0 ] = address ( dai , .TypedVals ) ; path [ 1 ] = address ( weth , .TypedVals ) ; path [ 2 ] = address ( usdc , .TypedVals ) ; uint256 [ ] memory amounts = router . swapExactTokensForTokens ( amountIn , amountOutMin , path , msg . sender , .TypedVals ) ; return amounts [ 2 ] ; .Statements - - - - swapMultiHopExactAmountOut - - - external - - - ListItem ( uint256 ) - ListItem ( uint256 ) - - - ListItem ( amountOutDesired ) - ListItem ( amountInMax ) - - - ListItem ( uint256 ) - - - ListItem ( amountOut ) - - - false - - - dai . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountInMax , .TypedVals ) ; dai . approve ( address ( router , .TypedVals ) , amountInMax , .TypedVals ) ; address [ ] memory path = new address [ ] ( 3 , .TypedVals ) ; path [ 0 ] = address ( dai , .TypedVals ) ; path [ 1 ] = address ( weth , .TypedVals ) ; path [ 2 ] = address ( usdc , .TypedVals ) ; uint256 [ ] memory amounts = router . swapTokensForExactTokens ( amountOutDesired , amountInMax , path , msg . sender , .TypedVals ) ; if ( amounts [ 0 ] < amountInMax ) { dai . transfer ( msg . sender , amountInMax - amounts [ 0 ] , .TypedVals ) ; .Statements } return amounts [ 2 ] ; .Statements - - - - swapSingleHopExactAmountIn - - - external - - - ListItem ( uint256 ) - ListItem ( uint256 ) - - - ListItem ( amountIn ) - ListItem ( amountOutMin ) - - - ListItem ( uint256 ) - - - ListItem ( amountOut ) - - - false - - - weth . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountIn , .TypedVals ) ; weth . approve ( address ( router , .TypedVals ) , amountIn , .TypedVals ) ; address [ ] memory path = new address [ ] ( 2 , .TypedVals ) ; path [ 0 ] = address ( weth , .TypedVals ) ; path [ 1 ] = address ( dai , .TypedVals ) ; uint256 [ ] memory amounts = router . swapExactTokensForTokens ( amountIn , amountOutMin , path , msg . sender , .TypedVals ) ; return amounts [ 1 ] ; .Statements - - - - swapSingleHopExactAmountOut - - - external - - - ListItem ( uint256 ) - ListItem ( uint256 ) - - - ListItem ( amountOutDesired ) - ListItem ( amountInMax ) - - - ListItem ( uint256 ) - - - ListItem ( amountOut ) - - - false - - - weth . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountInMax , .TypedVals ) ; weth . approve ( address ( router , .TypedVals ) , amountInMax , .TypedVals ) ; address [ ] memory path = new address [ ] ( 2 , .TypedVals ) ; path [ 0 ] = address ( weth , .TypedVals ) ; path [ 1 ] = address ( dai , .TypedVals ) ; uint256 [ ] memory amounts = router . swapTokensForExactTokens ( amountOutDesired , amountInMax , path , msg . sender , .TypedVals ) ; if ( amounts [ 0 ] < amountInMax ) { weth . transfer ( msg . sender , amountInMax - amounts [ 0 ] , .TypedVals ) ; .Statements } return amounts [ 1 ] ; .Statements - - - - usdc - - - public - - - .List - - - .List - - - ListItem ( iERC20 ) - - - ListItem ( noId ) - - - false - - - return usdc ; .Statements - - - - weth - - - public - - - .List - - - .List - - - ListItem ( iERC20 ) - - - ListItem ( noId ) - - - false - - - return weth ; .Statements - - - - ... - - - uniswapV2SwapTest - - - (vidDai |-> dAIMock) - (vidUni |-> uniswapV2Swap) - (vidUsdc |-> uSDCMock) - (vidWeth |-> wETHMock) - - - .List - - - - - setUp - - - public - - - .List - - - .List - - - .List - - - .List - - - false - - - vidWeth = new wETHMock ( .TypedVals ) ; vidDai = new dAIMock ( .TypedVals ) ; vidUsdc = new uSDCMock ( .TypedVals ) ; vidUni = new uniswapV2Swap ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; .Statements - - - - testSwapMultiHopExactAmountIn - - - public - - - .List - - - .List - - - .List - - - .List - - - false - - - uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 4 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 3 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 3 * wethAmount , .TypedVals ) ; vidUsdc . mint ( address ( this , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidUsdc . approve ( address ( vidUni , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountMin = 1 ; vidUni . swapSingleHopExactAmountIn ( wethAmount , daiAmountMin , .TypedVals ) ; uint256 daiAmountIn = 1e18 ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidUsdc . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; uint256 usdcAmountOutMin = 1 ; uint256 usdcAmountOut = vidUni . swapMultiHopExactAmountIn ( daiAmountIn , usdcAmountOutMin , .TypedVals ) ; assert ( usdcAmountOut >= usdcAmountOutMin , .TypedVals ) ; .Statements - - - - testSwapMultiHopExactAmountOut - - - public - - - .List - - - .List - - - .List - - - .List - - - false - - - uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 20 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidUsdc . mint ( address ( this , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidUsdc . approve ( address ( vidUni , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountOut = 2 * 1e18 ; vidUni . swapSingleHopExactAmountOut ( daiAmountOut , 4 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidUsdc . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; uint256 amountOutDesired = 1e6 ; uint256 amountOut = vidUni . swapMultiHopExactAmountOut ( amountOutDesired , daiAmountOut , .TypedVals ) ; assert ( amountOut == amountOutDesired , .TypedVals ) ; .Statements - - - - testSwapSingleHopExactAmountIn - - - public - - - .List - - - .List - - - .List - - - .List - - - false - - - uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 2 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountMin = 1 ; uint256 daiAmountOut = vidUni . swapSingleHopExactAmountIn ( wethAmount , daiAmountMin , .TypedVals ) ; assert ( daiAmountOut >= daiAmountMin , .TypedVals ) ; .Statements - - - - testSwapSingleHopExactAmountOut - - - public - - - .List - - - .List - - - .List - - - .List - - - false - - - uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 10 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 6 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountDesired = 1e18 ; uint256 daiAmountOut = vidUni . swapSingleHopExactAmountOut ( daiAmountDesired , 2 * wethAmount , .TypedVals ) ; assert ( daiAmountOut == daiAmountDesired , .TypedVals ) ; .Statements - - - - ... - - - wETHMock - - - (allowance |-> mapping ( address wethownr => mapping ( address wethspdr => uint256 ) )) - (balanceOf |-> mapping ( address wethact => uint256 )) - (constUINT256MAX |-> uint256) - - - ListItem ( constUINT256MAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) - - - - - allowance - - - public - - - ListItem ( address ) - ListItem ( address ) - - - ListItem ( wethownr ) - ListItem ( wethspdr ) - - - ListItem ( mapping ( address wethownr => mapping ( address wethspdr => uint256 ) ) ) - - - ListItem ( noId ) - - - false - - - return allowance [ wethownr ] [ wethspdr ] ; .Statements - - - - approve - - - external - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( spender ) - ListItem ( value ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - allowance [ msg . sender ] [ spender ] = value ; emit approvalEvent ( msg . sender , spender , value , .TypedVals ) ; return true ; .Statements - - - - balanceOf - - - public - - - ListItem ( address ) - - - ListItem ( wethact ) - - - ListItem ( mapping ( address wethact => uint256 ) ) - - - ListItem ( noId ) - - - false - - - return balanceOf [ wethact ] ; .Statements - - - - decimals - - - external - - - .List - - - .List - - - ListItem ( uint8 ) - - - ListItem ( noId ) - - - false - - - return 18 ; .Statements - - - - deposit - - - external - - - .List - - - .List - - - .List - - - .List - - - true - - - balanceOf [ msg . sender ] = balanceOf [ msg . sender ] + msg . value ; emit transferEvent ( address ( 0 , .TypedVals ) , msg . sender , msg . value , .TypedVals ) ; .Statements - - - - transfer - - - external - - - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( to ) - ListItem ( value ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - if ( to != address ( 0 , .TypedVals ) && to != address ( this , .TypedVals ) ) { uint256 balance = balanceOf [ msg . sender ] ; require ( balance >= value , "WETH: transfer amount exceeds balance" , .TypedVals ) ; balanceOf [ msg . sender ] = balance - value ; balanceOf [ to ] = balanceOf [ to ] + value ; emit transferEvent ( msg . sender , to , value , .TypedVals ) ; .Statements } else { uint256 balance = balanceOf [ msg . sender ] ; require ( balance >= value , "WETH: burn amount exceeds balance" , .TypedVals ) ; balanceOf [ msg . sender ] = balance - value ; emit transferEvent ( msg . sender , address ( 0 , .TypedVals ) , value , .TypedVals ) ; ( bool success , ) = msg . sender . call { value : value , .KeyValues } ( "" , .TypedVals ) ; require ( success , "WETH: ETH transfer failed" , .TypedVals ) ; .Statements } return true ; .Statements - - - - transferFrom - - - external - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( from ) - ListItem ( to ) - ListItem ( value ) - - - ListItem ( bool ) - - - ListItem ( noId ) - - - false - - - if ( from != msg . sender ) { uint256 allowed = allowance [ from ] [ msg . sender ] ; if ( allowed != constUINT256MAX ) { require ( allowed >= value , "WETH: request exceeds allowance" , .TypedVals ) ; uint256 reduced = allowed - value ; allowance [ from ] [ msg . sender ] = reduced ; emit approvalEvent ( from , msg . sender , reduced , .TypedVals ) ; .Statements } .Statements } if ( to != address ( 0 , .TypedVals ) && to != address ( this , .TypedVals ) ) { uint256 balance = balanceOf [ from ] ; require ( balance >= value , "WETH: transfer amount exceeds balance" , .TypedVals ) ; balanceOf [ from ] = balance - value ; balanceOf [ to ] = balanceOf [ to ] + value ; emit transferEvent ( from , to , value , .TypedVals ) ; .Statements } else { uint256 balance = balanceOf [ from ] ; require ( balance >= value , "WETH: burn amount exceeds balance" , .TypedVals ) ; balanceOf [ from ] = balance - value ; emit transferEvent ( from , address ( 0 , .TypedVals ) , value , .TypedVals ) ; ( bool success , ) = msg . sender . call { value : value , .KeyValues } ( "" , .TypedVals ) ; require ( success , "WETH: ETH transfer failed" , .TypedVals ) ; .Statements } return true ; .Statements - - - - - - - approvalEvent - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( owner ) - ListItem ( spender ) - ListItem ( value ) - - - SetItem ( 0 ) - SetItem ( 1 ) - - - - transferEvent - - - ListItem ( address ) - ListItem ( address ) - ListItem ( uint256 ) - - - ListItem ( from ) - ListItem ( to ) - ListItem ( value ) - - - SetItem ( 0 ) - SetItem ( 1 ) - - - - - - - ) - [priority(40)] - -endmodule -``` - ```k module SOLIDITY-DATA-SYNTAX imports MINT-SYNTAX diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md new file mode 100644 index 0000000..e6e11eb --- /dev/null +++ b/src/uniswap-summaries.md @@ -0,0 +1,2399 @@ +# Summarized rules for the UniswapV2Swap test + +```k +module SOLIDITY-UNISWAP-TOKENS + + syntax Id ::= "account" [token] + | "act" [token] + | "allowance" [token] + | "allowed" [token] + | "amountIn" [token] + | "amountInMax" [token] + | "amountInWithFee" [token] + | "amountOut" [token] + | "amountOutDesired" [token] + | "amountOutMin" [token] + | "amounts" [token] + | "amount0In" [token] + | "amount1In" [token] + | "amount0Out" [token] + | "amount1Out" [token] + | "approvalEvent" [token] + | "approve" [token] + | "balance" [token] + | "balanceOf" [token] + | "balance0" [token] + | "balance0Adjusted" [token] + | "balance1" [token] + | "balance1Adjusted" [token] + | "block" [token] + | "blockTimestamp" [token] + | "blockTimestampLast" [token] + | "burn" [token] + | "call" [token] + | "constMINIMUMLIQUIDITY" [token] + | "constUINTMAX" [token] + | "constUINT112MAX" [token] + | "constUINT256MAX" [token] + | "currentAllowance" [token] + | "dai" [token] + | "daiact" [token] + | "daiAmountDesired" [token] + | "daiAmountIn" [token] + | "daiAmountMin" [token] + | "daiAmountOut" [token] + | "dAIMock" [token] + | "daiownr" [token] + | "daispdr" [token] + | "decimals" [token] + | "denominator" [token] + | "deposit" [token] + | "dst" [token] + | "emitEvent" [token] + | "from" [token] + | "fromBalance" [token] + | "getLocalPair" [token] + | "getReserves" [token] + | "guy" [token] + | "i" [token] + | "iERC20" [token] + | "input" [token] + | "kLast" [token] + | "length" [token] + | "localPairs" [token] + | "mint" [token] + | "mintOnDeposit" [token] + | "msg" [token] + | "numerator" [token] + | "output" [token] + | "owner" [token] + | "pair" [token] + | "pairEl1" [token] + | "pairEl2" [token] + | "pairReserves" [token] + | "path" [token] + | "price0CumulativeLast" [token] + | "price1CumulativeLast" [token] + | "reduced" [token] + | "reserveIn" [token] + | "reserveOut" [token] + | "reserves" [token] + | "reserve0" [token] + | "reserve1" [token] + | "router" [token] + | "safeTransferFrom" [token] + | "sender" [token] + | "setLocalPair" [token] + | "setUp" [token] + | "spender" [token] + | "src" [token] + | "success" [token] + | "swap" [token] + | "swapExactTokensForTokens" [token] + | "swapEvent" [token] + | "swapMultiHopExactAmountIn" [token] + | "swapMultiHopExactAmountOut" [token] + | "swapSingleHopExactAmountIn" [token] + | "swapSingleHopExactAmountOut" [token] + | "swapTokensForExactTokens" [token] + | "sync" [token] + | "syncEvent" [token] + | "syncLocalPair" [token] + | "testSwapMultiHopExactAmountIn" [token] + | "testSwapMultiHopExactAmountOut" [token] + | "testSwapSingleHopExactAmountIn" [token] + | "testSwapSingleHopExactAmountOut" [token] + | "this" [token] + | "timeElapsed" [token] + | "timestamp" [token] + | "to" [token] + | "tokenA" [token] + | "tokenB" [token] + | "tokens" [token] + | "token0" [token] + | "token1" [token] + | "totalSupply" [token] + | "transfer" [token] + | "transferEvent" [token] + | "transferFrom" [token] + | "uniswapV2LibraryGetAmountIn" [token] + | "uniswapV2LibraryGetAmountOut" [token] + | "uniswapV2LibraryGetAmountsIn" [token] + | "uniswapV2LibraryGetAmountsOut" [token] + | "uniswapV2LibraryGetReserves" [token] + | "uniswapV2LibraryPairFor" [token] + | "uniswapV2LibrarySortTokens" [token] + | "uniswapV2Pair" [token] + | "uniswapV2Router02" [token] + | "uniswapV2Swap" [token] + | "uniswapV2SwapTest" [token] + | "usdc" [token] + | "usdcAmountOut" [token] + | "usdcAmountOutMin" [token] + | "uSDCMock" [token] + | "usr" [token] + | "value" [token] + | "wad" [token] + | "weth" [token] + | "wethact" [token] + | "wethAmount" [token] + | "wETHMock" [token] + | "wethownr" [token] + | "wethspdr" [token] + + syntax Id ::= "vidAllowances" [token] + | "vidBalances" [token] + | "vidDai" [token] + | "vidReserve0" [token] + | "vidReserve1" [token] + | "vidTo" [token] + | "vidToken0" [token] + | "vidToken1" [token] + | "vidTotalSupply" [token] + | "vidUni" [token] + | "vidUsdc" [token] + | "vidWeth" [token] + | "fidApprove" [token] + | "fidSpendAllowance" [token] + | "fidSwap" [token] + | "fidTransfer" [token] + | "fidUpdate" [token] + + syntax Id ::= "require" [token] | "assert" [token] + + syntax Decimal ::= "1e18" [token] + | "1e6" [token] + +endmodule +``` + +```k +module SOLIDITY-UNISWAP-INIT-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-UNISWAP-TOKENS + + rule _:Program => .K ... + true + (_:CompileCell => + + + uniswapV2SwapTest + + + + + iERC20 + + + + + approve + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( bool ) + + + + balanceOf + + + ListItem ( address ) + + + ListItem ( uint256 ) + + + + transfer + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( bool ) + + + + transferFrom + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( bool ) + + + + + + + + + dAIMock + + + (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) + (balanceOf |-> mapping ( address daiact => uint256 )) + (constUINTMAX |-> uint256) + (totalSupply |-> uint256) + + + ListItem ( constUINTMAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) + + + + + allowance + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( daiownr ) + ListItem ( daispdr ) + + + ListItem ( mapping ( address daiownr => mapping ( address daispdr => uint256 ) ) ) + + + ListItem ( noId ) + + + false + + + return allowance [ daiownr ] [ daispdr ] ; .Statements + + + + approve + + + external + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + allowance [ msg . sender ] [ usr ] = wad ; emit approvalEvent ( msg . sender , usr , wad , .TypedVals ) ; return true ; .Statements + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( daiact ) + + + ListItem ( mapping ( address daiact => uint256 ) ) + + + ListItem ( noId ) + + + false + + + return balanceOf [ daiact ] ; .Statements + + + + burn + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + .List + + + .List + + + false + + + if ( balanceOf [ usr ] >= wad ) { balanceOf [ usr ] = balanceOf [ usr ] - wad ; totalSupply = totalSupply - wad ; .Statements } .Statements + + + + decimals + + + external + + + .List + + + .List + + + ListItem ( uint8 ) + + + ListItem ( noId ) + + + false + + + return 18 ; .Statements + + + + mint + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + .List + + + .List + + + false + + + balanceOf [ usr ] = balanceOf [ usr ] + wad ; totalSupply = totalSupply + wad ; emit transferEvent ( address ( 0 , .TypedVals ) , usr , wad , .TypedVals ) ; .Statements + + + + mintOnDeposit + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( usr ) + ListItem ( wad ) + + + .List + + + .List + + + false + + + mint ( usr , wad , .TypedVals ) ; .Statements + + + + safeTransferFrom + + + external + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + transferFrom ( from , to , value , .TypedVals ) ; .Statements + + + + totalSupply + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return totalSupply ; .Statements + + + + transfer + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( dst ) + ListItem ( wad ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + return transferFrom ( msg . sender , dst , wad , .TypedVals ) ; .Statements + + + + transferFrom + + + public + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( src ) + ListItem ( dst ) + ListItem ( wad ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + require ( balanceOf [ src ] >= wad , "Dai/insufficient-balance" , .TypedVals ) ; if ( src != msg . sender && allowance [ src ] [ msg . sender ] != constUINTMAX ) { require ( allowance [ src ] [ msg . sender ] >= wad , "Dai/insufficient-allowance" , .TypedVals ) ; allowance [ src ] [ msg . sender ] = allowance [ src ] [ msg . sender ] - wad ; .Statements } balanceOf [ src ] = balanceOf [ src ] - wad ; balanceOf [ dst ] = balanceOf [ dst ] + wad ; emit transferEvent ( src , dst , wad , .TypedVals ) ; return true ; .Statements + + + + + + + approvalEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( src ) + ListItem ( guy ) + ListItem ( wad ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + transferEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( src ) + ListItem ( dst ) + ListItem ( wad ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + + + uSDCMock + + + (constUINT256MAX |-> uint256) + (vidAllowances |-> mapping ( address account => mapping ( address spender => uint256 ) )) + (vidBalances |-> mapping ( address account => uint256 )) + (vidTotalSupply |-> uint256) + + + ListItem ( constUINT256MAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) + + + + + allowance + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( owner ) + ListItem ( spender ) + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return vidAllowances [ owner ] [ spender ] ; .Statements + + + + approve + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( spender ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address owner = msg . sender ; fidApprove ( owner , spender , value , true , .TypedVals ) ; return true ; .Statements + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( account ) + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return vidBalances [ account ] ; .Statements + + + + decimals + + + external + + + .List + + + .List + + + ListItem ( uint8 ) + + + ListItem ( noId ) + + + false + + + return 18 ; .Statements + + + + fidApprove + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + ListItem ( bool ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + ListItem ( emitEvent ) + + + .List + + + .List + + + false + + + require ( owner != address ( 0 , .TypedVals ) , "USDC: invalid approver" , .TypedVals ) ; require ( spender != address ( 0 , .TypedVals ) , "USDC: invalid spender" , .TypedVals ) ; vidAllowances [ owner ] [ spender ] = value ; if ( emitEvent ) { emit approvalEvent ( owner , spender , value , .TypedVals ) ; .Statements } .Statements + + + + fidSpendAllowance + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + .List + + + .List + + + false + + + uint256 currentAllowance = allowance ( owner , spender , .TypedVals ) ; if ( currentAllowance != constUINT256MAX ) { require ( currentAllowance >= value , "USDC: insufficient allowance" , .TypedVals ) ; fidApprove ( owner , spender , currentAllowance - value , false , .TypedVals ) ; .Statements } .Statements + + + + fidTransfer + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + require ( from != address ( 0 , .TypedVals ) , "USDC: invalid sender" , .TypedVals ) ; require ( to != address ( 0 , .TypedVals ) , "USDC: invalid receiver" , .TypedVals ) ; fidUpdate ( from , to , value , .TypedVals ) ; .Statements + + + + fidUpdate + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + if ( from == address ( 0 , .TypedVals ) ) { vidTotalSupply = vidTotalSupply + value ; .Statements } else { uint256 fromBalance = vidBalances [ from ] ; require ( fromBalance >= value , "USDC: insufficient balance" , .TypedVals ) ; vidBalances [ from ] = fromBalance - value ; .Statements } if ( to == address ( 0 , .TypedVals ) ) { vidTotalSupply = vidTotalSupply - value ; .Statements } else { vidBalances [ to ] = vidBalances [ to ] + value ; .Statements } emit transferEvent ( from , to , value , .TypedVals ) ; .Statements + + + + mint + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( account ) + ListItem ( value ) + + + .List + + + .List + + + false + + + require ( account != address ( 0 , .TypedVals ) , "USDC: invalid receiver" , .TypedVals ) ; fidUpdate ( address ( 0 , .TypedVals ) , account , value , .TypedVals ) ; .Statements + + + + transfer + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address owner = msg . sender ; fidTransfer ( owner , to , value , .TypedVals ) ; return true ; .Statements + + + + transferFrom + + + public + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address spender = msg . sender ; fidSpendAllowance ( from , spender , value , .TypedVals ) ; fidTransfer ( from , to , value , .TypedVals ) ; return true ; .Statements + + + + + + + approvalEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + transferEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + + + uniswapV2Pair + + + (balanceOf |-> mapping ( address act => uint256 )) + (blockTimestampLast |-> uint32) + (constMINIMUMLIQUIDITY |-> uint256) + (constUINT112MAX |-> uint256) + (kLast |-> uint256) + (price0CumulativeLast |-> uint256) + (price1CumulativeLast |-> uint256) + (reserve0 |-> uint112) + (reserve1 |-> uint112) + (token0 |-> address) + (token1 |-> address) + (totalSupply |-> uint256) + + + ListItem ( constUINT112MAX = 0xffffffffffffffffffffffffffff ; ) + ListItem ( constMINIMUMLIQUIDITY = 10 ** 3 ; ) + + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( act ) + + + ListItem ( mapping ( address act => uint256 ) ) + + + ListItem ( noId ) + + + false + + + return balanceOf [ act ] ; .Statements + + + + constMINIMUMLIQUIDITY + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return constMINIMUMLIQUIDITY ; .Statements + + + + constructor + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( vidToken0 ) + ListItem ( vidToken1 ) + + + .List + + + .List + + + false + + + token0 = vidToken0 ; token1 = vidToken1 ; .Statements + + + + fidUpdate + + + private + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint112 ) + ListItem ( uint112 ) + + + ListItem ( balance0 ) + ListItem ( balance1 ) + ListItem ( vidReserve0 ) + ListItem ( vidReserve1 ) + + + .List + + + .List + + + false + + + require ( balance0 <= constUINT112MAX && balance1 <= constUINT112MAX , "UniswapV2: OVERFLOW" , .TypedVals ) ; uint32 blockTimestamp = uint32 ( block . timestamp % 2 ** 32 , .TypedVals ) ; uint32 timeElapsed = blockTimestamp - blockTimestampLast ; if ( timeElapsed > 0 && vidReserve0 != 0 && vidReserve1 != 0 ) { price0CumulativeLast = price0CumulativeLast + vidReserve1 / vidReserve0 * timeElapsed ; price1CumulativeLast = price1CumulativeLast + vidReserve0 / vidReserve1 * timeElapsed ; .Statements } reserve0 = uint112 ( balance0 , .TypedVals ) ; reserve1 = uint112 ( balance1 , .TypedVals ) ; blockTimestampLast = blockTimestamp ; emit syncEvent ( reserve0 , reserve1 , .TypedVals ) ; .Statements + + + + getReserves + + + public + + + .List + + + .List + + + ListItem ( uint112 [ ]::TypeName ) + + + ListItem ( reserves ) + + + false + + + reserves = new uint112 [ ] ( 3 , .TypedVals ) ; reserves [ 0 ] = reserve0 ; reserves [ 1 ] = reserve1 ; reserves [ 2 ] = blockTimestampLast ; .Statements + + + + kLast + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return kLast ; .Statements + + + + price0CumulativeLast + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return price0CumulativeLast ; .Statements + + + + price1CumulativeLast + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return price1CumulativeLast ; .Statements + + + + swap + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address ) + + + ListItem ( amount0Out ) + ListItem ( amount1Out ) + ListItem ( to ) + + + .List + + + .List + + + false + + + require ( amount0Out > 0 || amount1Out > 0 , "UniswapV2: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; uint112 [ ] memory reserves = getReserves ( .TypedVals ) ; require ( amount0Out < reserves [ 0 ] && amount1Out < reserves [ 1 ] , "UniswapV2: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 balance0 ; uint256 balance1 ; { address vidToken0 = token0 ; address vidToken1 = token1 ; require ( to != vidToken0 && to != vidToken1 , "UniswapV2: INVALID_TO" , .TypedVals ) ; if ( amount0Out > 0 ) iERC20 ( vidToken0 , .TypedVals ) . transfer ( to , amount0Out , .TypedVals ) ; if ( amount1Out > 0 ) iERC20 ( vidToken1 , .TypedVals ) . transfer ( to , amount1Out , .TypedVals ) ; balance0 = iERC20 ( vidToken0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; balance1 = iERC20 ( vidToken1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; .Statements } uint256 amount0In = balance0 > reserves [ 0 ] - amount0Out ? balance0 - ( reserves [ 0 ] - amount0Out ) : 0 ; uint256 amount1In = balance1 > reserves [ 1 ] - amount1Out ? balance1 - ( reserves [ 1 ] - amount1Out ) : 0 ; require ( amount0In > 0 || amount1In > 0 , "UniswapV2: INSUFFICIENT_INPUT_AMOUNT" , .TypedVals ) ; { uint256 balance0Adjusted = balance0 * 1000 - amount0In * 3 ; uint256 balance1Adjusted = balance1 * 1000 - amount1In * 3 ; require ( balance0Adjusted * balance1Adjusted >= uint256 ( reserves [ 0 ] , .TypedVals ) * reserves [ 1 ] * 1000 ** 2 , "UniswapV2: K" , .TypedVals ) ; .Statements } fidUpdate ( balance0 , balance1 , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; emit swapEvent ( msg . sender , amount0In , amount1In , amount0Out , amount1Out , to , .TypedVals ) ; .Statements + + + + sync + + + external + + + .List + + + .List + + + .List + + + .List + + + false + + + fidUpdate ( iERC20 ( token0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , iERC20 ( token1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , reserve0 , reserve1 , .TypedVals ) ; .Statements + + + + token0 + + + public + + + .List + + + .List + + + ListItem ( address ) + + + ListItem ( noId ) + + + false + + + return token0 ; .Statements + + + + token1 + + + public + + + .List + + + .List + + + ListItem ( address ) + + + ListItem ( noId ) + + + false + + + return token1 ; .Statements + + + + totalSupply + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return totalSupply ; .Statements + + + + + + + swapEvent + + + ListItem ( address ) + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address ) + + + ListItem ( sender ) + ListItem ( amount0In ) + ListItem ( amount1In ) + ListItem ( amount0Out ) + ListItem ( amount1Out ) + ListItem ( to ) + + + SetItem ( 0 ) + SetItem ( 5 ) + + + + syncEvent + + + ListItem ( uint112 ) + ListItem ( uint112 ) + + + ListItem ( reserve0 ) + ListItem ( reserve1 ) + + + .Set + + + + + + uniswapV2Router02 + + + localPairs |-> mapping ( address pairEl1 => mapping ( address pairEl2 => address ) ) + + + .List + + + + + fidSwap + + + private + + + ListItem ( uint256 [ ]::TypeName ) + ListItem ( address [ ]::TypeName ) + ListItem ( address ) + + + ListItem ( amounts ) + ListItem ( path ) + ListItem ( vidTo ) + + + .List + + + .List + + + false + + + { uint256 i ; while ( i < path . length - 1 ) { { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2LibrarySortTokens ( input , output , .TypedVals ) ; uint256 amountOut = amounts [ i + 1 ] ; uint256 amount0Out = input == tokens [ 0 ] ? uint256 ( 0 , .TypedVals ) : amountOut ; uint256 amount1Out = input == tokens [ 0 ] ? amountOut : uint256 ( 0 , .TypedVals ) ; address to = i < path . length - 2 ? uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) : vidTo ; uniswapV2Pair ( uniswapV2LibraryPairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements + + + + getLocalPair + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( address ) + + + ListItem ( pair ) + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; pair = localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] ; .Statements + + + + localPairs + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( pairEl1 ) + ListItem ( pairEl2 ) + + + ListItem ( mapping ( address pairEl1 => mapping ( address pairEl2 => address ) ) ) + + + ListItem ( noId ) + + + false + + + return localPairs [ pairEl1 ] [ pairEl2 ] ; .Statements + + + + setLocalPair + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + .List + + + .List + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] = address ( new uniswapV2Pair ( address ( tokens [ 0 ] , .TypedVals ) , address ( tokens [ 1 ] , .TypedVals ) , .TypedVals ) , .TypedVals ) ; .Statements + + + + swapExactTokensForTokens + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + ListItem ( address ) + + + ListItem ( amountIn ) + ListItem ( amountOutMin ) + ListItem ( path ) + ListItem ( to ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + amounts = uniswapV2LibraryGetAmountsOut ( amountIn , path , .TypedVals ) ; require ( amounts [ amounts . length - 1 ] >= amountOutMin , "UniswapV2Router: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; iERC20 ( path [ 0 ] , .TypedVals ) . transferFrom ( msg . sender , uniswapV2LibraryPairFor ( path [ 0 ] , path [ 1 ] , .TypedVals ) , amounts [ 0 ] , .TypedVals ) ; fidSwap ( amounts , path , to , .TypedVals ) ; .Statements + + + + swapTokensForExactTokens + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + ListItem ( address ) + + + ListItem ( amountOut ) + ListItem ( amountInMax ) + ListItem ( path ) + ListItem ( to ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + amounts = uniswapV2LibraryGetAmountsIn ( amountOut , path , .TypedVals ) ; require ( amounts [ 0 ] <= amountInMax , "UniswapV2Router: EXCESSIVE_INPUT_AMOUNT" , .TypedVals ) ; iERC20 ( path [ 0 ] , .TypedVals ) . transferFrom ( msg . sender , uniswapV2LibraryPairFor ( path [ 0 ] , path [ 1 ] , .TypedVals ) , amounts [ 0 ] , .TypedVals ) ; fidSwap ( amounts , path , to , .TypedVals ) ; .Statements + + + + syncLocalPair + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + .List + + + .List + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; uniswapV2Pair ( localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] , .TypedVals ) . sync ( .TypedVals ) ; .Statements + + + + uniswapV2LibraryGetAmountIn + + + private + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountOut ) + ListItem ( reserveIn ) + ListItem ( reserveOut ) + + + ListItem ( uint256 ) + + + ListItem ( amountIn ) + + + false + + + require ( amountOut > 0 , "UniswapV2Library: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; require ( reserveIn > 0 && reserveOut > 0 , "UniswapV2Library: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 numerator = reserveIn * amountOut * 1000 ; uint256 denominator = ( reserveOut - amountOut ) * 997 ; amountIn = denominator != 0 ? numerator / denominator + 1 : 1 ; .Statements + + + + uniswapV2LibraryGetAmountOut + + + private + + + ListItem ( uint256 ) + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountIn ) + ListItem ( reserveIn ) + ListItem ( reserveOut ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + require ( amountIn > 0 , "UniswapV2Library: INSUFFICIENT_INPUT_AMOUNT" , .TypedVals ) ; require ( reserveIn > 0 && reserveOut > 0 , "UniswapV2Library: INSUFFICIENT_LIQUIDITY" , .TypedVals ) ; uint256 amountInWithFee = amountIn * 997 ; uint256 numerator = amountInWithFee * reserveOut ; uint256 denominator = reserveIn * 1000 + amountInWithFee ; amountOut = numerator / denominator ; .Statements + + + + uniswapV2LibraryGetAmountsIn + + + private + + + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + + + ListItem ( amountOut ) + ListItem ( path ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ amounts . length - 1 ] = amountOut ; { uint256 i = path . length - 1 ; while ( i > 0 ) { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i - 1 ] , path [ i ] , .TypedVals ) ; amounts [ i - 1 ] = uniswapV2LibraryGetAmountIn ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i -- ; .Statements } .Statements } .Statements + + + + uniswapV2LibraryGetAmountsOut + + + private + + + ListItem ( uint256 ) + ListItem ( address [ ]::TypeName ) + + + ListItem ( amountIn ) + ListItem ( path ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( amounts ) + + + false + + + require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; { uint256 i ; while ( i < path . length - 1 ) { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; amounts [ i + 1 ] = uniswapV2LibraryGetAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements + + + + uniswapV2LibraryGetReserves + + + private + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( uint256 [ ]::TypeName ) + + + ListItem ( reserves ) + + + false + + + reserves = new uint256 [ ] ( 2 , .TypedVals ) ; address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; uint112 [ ] memory pairReserves = uniswapV2Pair ( uniswapV2LibraryPairFor ( tokenA , tokenB , .TypedVals ) , .TypedVals ) . getReserves ( .TypedVals ) ; reserves [ 0 ] = tokenA == tokens [ 0 ] ? pairReserves [ 0 ] : pairReserves [ 1 ] ; reserves [ 1 ] = tokenA == tokens [ 0 ] ? pairReserves [ 1 ] : pairReserves [ 0 ] ; .Statements + + + + uniswapV2LibraryPairFor + + + private + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( address ) + + + ListItem ( pair ) + + + false + + + address [ ] memory tokens = uniswapV2LibrarySortTokens ( tokenA , tokenB , .TypedVals ) ; pair = localPairs [ tokens [ 0 ] ] [ tokens [ 1 ] ] ; .Statements + + + + uniswapV2LibrarySortTokens + + + private + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( tokenA ) + ListItem ( tokenB ) + + + ListItem ( address [ ]::TypeName ) + + + ListItem ( tokens ) + + + false + + + tokens = new address [ ] ( 2 , .TypedVals ) ; require ( tokenA != tokenB , "UniswapV2Library: IDENTICAL_ADDRESSES" , .TypedVals ) ; tokens [ 0 ] = tokenA < tokenB ? tokenA : tokenB ; tokens [ 1 ] = tokenA < tokenB ? tokenB : tokenA ; require ( tokens [ 0 ] != address ( 0 , .TypedVals ) , "UniswapV2Library: ZERO_ADDRESS" , .TypedVals ) ; .Statements + + + + ... + + + uniswapV2Swap + + + (dai |-> iERC20) + (router |-> uniswapV2Router02) + (usdc |-> iERC20) + (weth |-> iERC20) + + + .List + + + + + constructor + + + public + + + ListItem ( address ) + ListItem ( address ) + ListItem ( address ) + + + ListItem ( vidWeth ) + ListItem ( vidDai ) + ListItem ( vidUsdc ) + + + .List + + + .List + + + false + + + weth = iERC20 ( vidWeth , .TypedVals ) ; dai = iERC20 ( vidDai , .TypedVals ) ; usdc = iERC20 ( vidUsdc , .TypedVals ) ; router = new uniswapV2Router02 ( .TypedVals ) ; router . setLocalPair ( vidWeth , vidDai , .TypedVals ) ; router . setLocalPair ( vidWeth , vidUsdc , .TypedVals ) ; router . setLocalPair ( vidUsdc , vidDai , .TypedVals ) ; .Statements + + + + dai + + + public + + + .List + + + .List + + + ListItem ( iERC20 ) + + + ListItem ( noId ) + + + false + + + return dai ; .Statements + + + + router + + + public + + + .List + + + .List + + + ListItem ( uniswapV2Router02 ) + + + ListItem ( noId ) + + + false + + + return router ; .Statements + + + + swapMultiHopExactAmountIn + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountIn ) + ListItem ( amountOutMin ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + dai . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountIn , .TypedVals ) ; dai . approve ( address ( router , .TypedVals ) , amountIn , .TypedVals ) ; address [ ] memory path = new address [ ] ( 3 , .TypedVals ) ; path [ 0 ] = address ( dai , .TypedVals ) ; path [ 1 ] = address ( weth , .TypedVals ) ; path [ 2 ] = address ( usdc , .TypedVals ) ; uint256 [ ] memory amounts = router . swapExactTokensForTokens ( amountIn , amountOutMin , path , msg . sender , .TypedVals ) ; return amounts [ 2 ] ; .Statements + + + + swapMultiHopExactAmountOut + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountOutDesired ) + ListItem ( amountInMax ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + dai . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountInMax , .TypedVals ) ; dai . approve ( address ( router , .TypedVals ) , amountInMax , .TypedVals ) ; address [ ] memory path = new address [ ] ( 3 , .TypedVals ) ; path [ 0 ] = address ( dai , .TypedVals ) ; path [ 1 ] = address ( weth , .TypedVals ) ; path [ 2 ] = address ( usdc , .TypedVals ) ; uint256 [ ] memory amounts = router . swapTokensForExactTokens ( amountOutDesired , amountInMax , path , msg . sender , .TypedVals ) ; if ( amounts [ 0 ] < amountInMax ) { dai . transfer ( msg . sender , amountInMax - amounts [ 0 ] , .TypedVals ) ; .Statements } return amounts [ 2 ] ; .Statements + + + + swapSingleHopExactAmountIn + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountIn ) + ListItem ( amountOutMin ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + weth . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountIn , .TypedVals ) ; weth . approve ( address ( router , .TypedVals ) , amountIn , .TypedVals ) ; address [ ] memory path = new address [ ] ( 2 , .TypedVals ) ; path [ 0 ] = address ( weth , .TypedVals ) ; path [ 1 ] = address ( dai , .TypedVals ) ; uint256 [ ] memory amounts = router . swapExactTokensForTokens ( amountIn , amountOutMin , path , msg . sender , .TypedVals ) ; return amounts [ 1 ] ; .Statements + + + + swapSingleHopExactAmountOut + + + external + + + ListItem ( uint256 ) + ListItem ( uint256 ) + + + ListItem ( amountOutDesired ) + ListItem ( amountInMax ) + + + ListItem ( uint256 ) + + + ListItem ( amountOut ) + + + false + + + weth . transferFrom ( msg . sender , address ( this , .TypedVals ) , amountInMax , .TypedVals ) ; weth . approve ( address ( router , .TypedVals ) , amountInMax , .TypedVals ) ; address [ ] memory path = new address [ ] ( 2 , .TypedVals ) ; path [ 0 ] = address ( weth , .TypedVals ) ; path [ 1 ] = address ( dai , .TypedVals ) ; uint256 [ ] memory amounts = router . swapTokensForExactTokens ( amountOutDesired , amountInMax , path , msg . sender , .TypedVals ) ; if ( amounts [ 0 ] < amountInMax ) { weth . transfer ( msg . sender , amountInMax - amounts [ 0 ] , .TypedVals ) ; .Statements } return amounts [ 1 ] ; .Statements + + + + usdc + + + public + + + .List + + + .List + + + ListItem ( iERC20 ) + + + ListItem ( noId ) + + + false + + + return usdc ; .Statements + + + + weth + + + public + + + .List + + + .List + + + ListItem ( iERC20 ) + + + ListItem ( noId ) + + + false + + + return weth ; .Statements + + + + ... + + + uniswapV2SwapTest + + + (vidDai |-> dAIMock) + (vidUni |-> uniswapV2Swap) + (vidUsdc |-> uSDCMock) + (vidWeth |-> wETHMock) + + + .List + + + + + setUp + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + vidWeth = new wETHMock ( .TypedVals ) ; vidDai = new dAIMock ( .TypedVals ) ; vidUsdc = new uSDCMock ( .TypedVals ) ; vidUni = new uniswapV2Swap ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; .Statements + + + + testSwapMultiHopExactAmountIn + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 4 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 3 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 3 * wethAmount , .TypedVals ) ; vidUsdc . mint ( address ( this , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidUsdc . approve ( address ( vidUni , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountMin = 1 ; vidUni . swapSingleHopExactAmountIn ( wethAmount , daiAmountMin , .TypedVals ) ; uint256 daiAmountIn = 1e18 ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidUsdc . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , daiAmountIn , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; uint256 usdcAmountOutMin = 1 ; uint256 usdcAmountOut = vidUni . swapMultiHopExactAmountIn ( daiAmountIn , usdcAmountOutMin , .TypedVals ) ; assert ( usdcAmountOut >= usdcAmountOutMin , .TypedVals ) ; .Statements + + + + testSwapMultiHopExactAmountOut + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 20 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 20 * wethAmount , .TypedVals ) ; vidUsdc . mint ( address ( this , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidUsdc . approve ( address ( vidUni , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 8 * wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountOut = 2 * 1e18 ; vidUni . swapSingleHopExactAmountOut ( daiAmountOut , 4 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidUsdc . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) , 2 * daiAmountOut , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidDai , .TypedVals ) , address ( vidWeth , .TypedVals ) , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; uint256 amountOutDesired = 1e6 ; uint256 amountOut = vidUni . swapMultiHopExactAmountOut ( amountOutDesired , daiAmountOut , .TypedVals ) ; assert ( amountOut == amountOutDesired , .TypedVals ) ; .Statements + + + + testSwapSingleHopExactAmountIn + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 2 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 2 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountMin = 1 ; uint256 daiAmountOut = vidUni . swapSingleHopExactAmountIn ( wethAmount , daiAmountMin , .TypedVals ) ; assert ( daiAmountOut >= daiAmountMin , .TypedVals ) ; .Statements + + + + testSwapSingleHopExactAmountOut + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 wethAmount = 1e18 ; vidWeth . deposit { value : 10 * wethAmount , .KeyValues } ( .TypedVals ) ; vidWeth . approve ( address ( vidUni , .TypedVals ) , 6 * wethAmount , .TypedVals ) ; vidDai . mint ( address ( this , .TypedVals ) , 10 * wethAmount , .TypedVals ) ; vidDai . approve ( address ( vidUni , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidWeth . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidDai . transfer ( vidUni . router ( .TypedVals ) . getLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) , 4 * wethAmount , .TypedVals ) ; vidUni . router ( .TypedVals ) . syncLocalPair ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , .TypedVals ) ; uint256 daiAmountDesired = 1e18 ; uint256 daiAmountOut = vidUni . swapSingleHopExactAmountOut ( daiAmountDesired , 2 * wethAmount , .TypedVals ) ; assert ( daiAmountOut == daiAmountDesired , .TypedVals ) ; .Statements + + + + ... + + + wETHMock + + + (allowance |-> mapping ( address wethownr => mapping ( address wethspdr => uint256 ) )) + (balanceOf |-> mapping ( address wethact => uint256 )) + (constUINT256MAX |-> uint256) + + + ListItem ( constUINT256MAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) + + + + + allowance + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( wethownr ) + ListItem ( wethspdr ) + + + ListItem ( mapping ( address wethownr => mapping ( address wethspdr => uint256 ) ) ) + + + ListItem ( noId ) + + + false + + + return allowance [ wethownr ] [ wethspdr ] ; .Statements + + + + approve + + + external + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( spender ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + allowance [ msg . sender ] [ spender ] = value ; emit approvalEvent ( msg . sender , spender , value , .TypedVals ) ; return true ; .Statements + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( wethact ) + + + ListItem ( mapping ( address wethact => uint256 ) ) + + + ListItem ( noId ) + + + false + + + return balanceOf [ wethact ] ; .Statements + + + + decimals + + + external + + + .List + + + .List + + + ListItem ( uint8 ) + + + ListItem ( noId ) + + + false + + + return 18 ; .Statements + + + + deposit + + + external + + + .List + + + .List + + + .List + + + .List + + + true + + + balanceOf [ msg . sender ] = balanceOf [ msg . sender ] + msg . value ; emit transferEvent ( address ( 0 , .TypedVals ) , msg . sender , msg . value , .TypedVals ) ; .Statements + + + + transfer + + + external + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + if ( to != address ( 0 , .TypedVals ) && to != address ( this , .TypedVals ) ) { uint256 balance = balanceOf [ msg . sender ] ; require ( balance >= value , "WETH: transfer amount exceeds balance" , .TypedVals ) ; balanceOf [ msg . sender ] = balance - value ; balanceOf [ to ] = balanceOf [ to ] + value ; emit transferEvent ( msg . sender , to , value , .TypedVals ) ; .Statements } else { uint256 balance = balanceOf [ msg . sender ] ; require ( balance >= value , "WETH: burn amount exceeds balance" , .TypedVals ) ; balanceOf [ msg . sender ] = balance - value ; emit transferEvent ( msg . sender , address ( 0 , .TypedVals ) , value , .TypedVals ) ; ( bool success , ) = msg . sender . call { value : value , .KeyValues } ( "" , .TypedVals ) ; require ( success , "WETH: ETH transfer failed" , .TypedVals ) ; .Statements } return true ; .Statements + + + + transferFrom + + + external + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + if ( from != msg . sender ) { uint256 allowed = allowance [ from ] [ msg . sender ] ; if ( allowed != constUINT256MAX ) { require ( allowed >= value , "WETH: request exceeds allowance" , .TypedVals ) ; uint256 reduced = allowed - value ; allowance [ from ] [ msg . sender ] = reduced ; emit approvalEvent ( from , msg . sender , reduced , .TypedVals ) ; .Statements } .Statements } if ( to != address ( 0 , .TypedVals ) && to != address ( this , .TypedVals ) ) { uint256 balance = balanceOf [ from ] ; require ( balance >= value , "WETH: transfer amount exceeds balance" , .TypedVals ) ; balanceOf [ from ] = balance - value ; balanceOf [ to ] = balanceOf [ to ] + value ; emit transferEvent ( from , to , value , .TypedVals ) ; .Statements } else { uint256 balance = balanceOf [ from ] ; require ( balance >= value , "WETH: burn amount exceeds balance" , .TypedVals ) ; balanceOf [ from ] = balance - value ; emit transferEvent ( from , address ( 0 , .TypedVals ) , value , .TypedVals ) ; ( bool success , ) = msg . sender . call { value : value , .KeyValues } ( "" , .TypedVals ) ; require ( success , "WETH: ETH transfer failed" , .TypedVals ) ; .Statements } return true ; .Statements + + + + + + + approvalEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + transferEvent + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + + + + ) + [priority(40)] + +endmodule +``` From 6cedc43869f7c51f3308bb981594270c20ee9d23 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 11 Sep 2024 17:19:50 -0500 Subject: [PATCH 8/9] Made 3rd argument of krun-sol optional. --- Makefile | 4 ++-- bin/krun-sol | 17 ++++++++++++++--- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index 58f8321..873289a 100644 --- a/Makefile +++ b/Makefile @@ -75,8 +75,8 @@ test-aave: test-regression: ${REGRESSION_TESTS} -$(REGRESSION_TESTS): %.out: %.sol %.txn %.ref %.smr $(SEMANTICS_FILE_NAME)-kompiled/timestamp - ulimit -s 65536 && bin/krun-sol $*.sol $*.txn $*.smr > $*.out 2>&1 +$(REGRESSION_TESTS): %.out: %.sol %.txn %.ref $(SEMANTICS_FILE_NAME)-kompiled/timestamp + ulimit -s 65536 && bin/krun-sol $*.sol $*.txn > $*.out 2>&1 diff -U3 -w $*.ref $*.out test-examples: ${EXAMPLE_TESTS} diff --git a/bin/krun-sol b/bin/krun-sol index d8bb832..73f87e3 100755 --- a/bin/krun-sol +++ b/bin/krun-sol @@ -1,6 +1,17 @@ #!/bin/bash contract="$1" txn="$2" -isuniswap="$3" -shift; shift; shift -krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" -cISUNISWAP="$isuniswap" -pISUNISWAP="$(dirname "$0")/kparse-bool" --no-expand-macros "$@" + +if [ "$#" -lt 3 ]; then + isuniswap="" +else + isuniswap="$3" + shift +fi +shift; shift + +if [ -z "${isuniswap}" ]; then + krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" -cISUNISWAP="false" --no-expand-macros "$@" +else + krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" -cISUNISWAP="$isuniswap" -pISUNISWAP="$(dirname "$0")/kparse-bool" --no-expand-macros "$@" +fi From 41f6450e7de91c72f4b55cc735530ddd4e4df411 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 11 Sep 2024 17:23:18 -0500 Subject: [PATCH 9/9] Removed .smr files from test/regression. --- test/regression/arithmetic.smr | 1 - test/regression/arraystestcontract.smr | 1 - test/regression/block.smr | 1 - test/regression/boolean.smr | 1 - test/regression/contract.smr | 1 - test/regression/emit.smr | 1 - test/regression/eventtestcontract.smr | 1 - test/regression/for.smr | 1 - test/regression/function.smr | 1 - test/regression/if.smr | 1 - test/regression/increment.smr | 1 - test/regression/mapstestcontract.smr | 1 - test/regression/swaps.smr | 1 - 13 files changed, 13 deletions(-) delete mode 100644 test/regression/arithmetic.smr delete mode 100644 test/regression/arraystestcontract.smr delete mode 100644 test/regression/block.smr delete mode 100644 test/regression/boolean.smr delete mode 100644 test/regression/contract.smr delete mode 100644 test/regression/emit.smr delete mode 100644 test/regression/eventtestcontract.smr delete mode 100644 test/regression/for.smr delete mode 100644 test/regression/function.smr delete mode 100644 test/regression/if.smr delete mode 100644 test/regression/increment.smr delete mode 100644 test/regression/mapstestcontract.smr delete mode 100644 test/regression/swaps.smr diff --git a/test/regression/arithmetic.smr b/test/regression/arithmetic.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/arithmetic.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/arraystestcontract.smr b/test/regression/arraystestcontract.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/arraystestcontract.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/block.smr b/test/regression/block.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/block.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/boolean.smr b/test/regression/boolean.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/boolean.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/contract.smr b/test/regression/contract.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/contract.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/emit.smr b/test/regression/emit.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/emit.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/eventtestcontract.smr b/test/regression/eventtestcontract.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/eventtestcontract.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/for.smr b/test/regression/for.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/for.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/function.smr b/test/regression/function.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/function.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/if.smr b/test/regression/if.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/if.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/increment.smr b/test/regression/increment.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/increment.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/mapstestcontract.smr b/test/regression/mapstestcontract.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/mapstestcontract.smr +++ /dev/null @@ -1 +0,0 @@ -false diff --git a/test/regression/swaps.smr b/test/regression/swaps.smr deleted file mode 100644 index c508d53..0000000 --- a/test/regression/swaps.smr +++ /dev/null @@ -1 +0,0 @@ -false