diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index ff39468..8febe0e 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3148,17 +3148,6 @@ 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 @@ -3167,14 +3156,15 @@ module SOLIDITY-UNISWAP-SWAP-SUMMARY uniswapV2Pair swap [priority(40)] + // First if condition evaluated to true to transfer call // Second if condition evaluated to true to transfer call - rule if ( v( true, bool) ) iERC20 ( vidToken1 , .TypedVals ) . transfer ( to , amount1Out , .TypedVals ) ; => v ( Vv1 , iERC20 ) . transfer ( v ( Vto , address ) , v ( Va1 , uint256 ) , .TypedVals ) ~> freezerExpressionStatement ( ) ... + rule if ( v( true, bool) ) iERC20 ( Token:Id , .TypedVals ) . transfer ( to , AmountOut:Id , .TypedVals ) ; => v ( Vtoken , iERC20 ) . transfer ( v ( Vto , address ) , v ( Vamount , uint256 ) , .TypedVals ) ~> freezerExpressionStatement ( ) ... true - ... (amount1Out |-> var(Ia1, uint256)) + ... (AmountOut |-> var(Iamount, uint256)) (to |-> var(Ito, address)) - (vidToken1 |-> var(Iv1, address)) + (Token |-> var(Itoken, address)) ... - _ [ Ia1 <- Va1 ] [ Ito <- Vto ] [ Iv1 <- Vv1 ] + _ [ Iamount <- Vamount ] [ Ito <- Vto ] [ Itoken <- Vtoken ] uniswapV2Pair swap [priority(40)]