diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 1421f9a..ff39468 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3148,6 +3148,17 @@ module SOLIDITY-UNISWAP-SWAP-SUMMARY swap requires Vto =/=MInt {S[token0] orDefault default(address)}:>MInt{160} andBool Vto =/=MInt {S[token1] orDefault default(address)}:>MInt{160} [priority(40)] + // First if condition evaluated to true to transfer call + rule if ( v( true, bool) ) iERC20 ( vidToken0 , .TypedVals ) . transfer ( to , amount0Out , .TypedVals ) ; => v ( Vv0 , iERC20 ) . transfer ( v ( Vto , address ) , v ( Va0 , uint256 ) , .TypedVals ) ~> freezerExpressionStatement ( ) ... + true + ... (amount0Out |-> var(Ia0, uint256)) + (to |-> var(Ito, address)) + (vidToken0 |-> var(Iv0, address)) + ... + _ [ Ia0 <- Va0 ] [ Ito <- Vto ] [ Iv0 <- Vv0 ] + uniswapV2Pair + swap [priority(40)] + // Second if condition evaluation rule if ( amount1Out > 0 ) iERC20 ( vidToken1 , .TypedVals ) . transfer ( to , amount1Out , .TypedVals ) ; Ss:Statements => if ( v( Va1 >uMInt 0p256, bool) ) iERC20 ( vidToken1 , .TypedVals ) . transfer ( to , amount1Out , .TypedVals ) ; ~> Ss ... true