From a7ef0a10fba66ebfc93e6ccaa692728b52850ffd Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Mon, 30 Sep 2024 18:44:50 -0500 Subject: [PATCH 1/4] getAmountsOut summary. --- src/uniswap-summaries.md | 71 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 510f304..50b3b25 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2678,6 +2678,76 @@ module SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY endmodule ``` +```k +module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-UNISWAP-TOKENS + imports SOLIDITY-EXPRESSION + imports SOLIDITY-STATEMENT + + rule uniswapV2LibraryGetAmountsOut:Id ( v ( V1:MInt{256} , uint256 ) , lv ( I2 , .List , address [ ]:TypeName ) , .TypedVals:CallArgumentList ) ~> K => SsFor ~> restoreEnv((amountIn |-> var(size(STORE), uint256)) (path |-> var(size(STORE) +Int 1, address [ ])) (amounts |-> var(size(STORE) +Int 3, uint256 [ ]))) ~> Ss ~> return amounts ; ~> .K + true + TYPE + TYPE + uniswapV2LibraryGetAmountsOut + require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; { uint256 i ; SsFor:Statements } Ss:Statements + E => (amountIn |-> var(size(STORE), uint256)) + (path |-> var(size(STORE) +Int 1, address [ ])) + (amounts |-> var(size(STORE) +Int 3, uint256 [ ])) + (i |-> var(size(STORE) +Int 4, uint256)) + + ( _ [ I2 <- V2 ] ) #as STORE => + STORE ListItem(V1) ListItem(V2) ListItem(default(uint256 [ ])) + ListItem((makeList(size({read(V2, .List, address [ ])}:>List), default(uint256))) [ 0 <- V1 ] ) + ListItem(default(uint256)) + + FUNC => uniswapV2LibraryGetAmountsOut + ... .List => ListItem(frame(K, E, FUNC)) + requires Int2MInt(size({read(V2, .List, address [ ])}:>List))::MInt{256} >=uMInt 2p256 [priority(40)] + + rule while (( i < path . length - 1 ) #as Cond) Body:Statement Ss:Statements => if (v(Vi List))::MInt{256} -MInt 1p256), bool)) {Body while(Cond) Body} else {.Statements} ~> Ss ... + true + ... (i |-> var(Ii, uint256)) (path |-> var(Ip, address [ ])) ... + _ [ Ii <- Vi ] [ Ip <- Vp ] + uniswapV2LibraryGetAmountsOut [priority(40)] + + rule if ( v ( true , bool ) ) { { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; Ss'':Statements } Ss':Statements } Ss:Statements } else { .Statements } => uniswapV2LibraryGetReserves ( v ( read(Vp, ListItem(MInt2Unsigned(Vi)), address []) , address ) , v ( read(Vp, ListItem(MInt2Unsigned(Vi) +Int 1), address []) , address ) , .TypedVals ) ~> freezerVariableDeclarationStatementA ( uint256 [ ] memory reserves ) ~> Ss'' ~> restoreEnv(E) ~> Ss' ~> restoreEnv(E) ~> Ss ~> restoreEnv(E) ... + true + ( _ (i |-> var(Ii, uint256)) (path |-> var(Ip, address [])) ) #as E + _ [ Ii <- Vi:MInt{256} ] [ Ip <- Vp ] + uniswapV2LibraryGetAmountsOut [priority(40)] + + rule v ( ListItem ( V1:MInt{256} ) ListItem ( V2:MInt{256} ) , uint256 [ ] ) ~> freezerVariableDeclarationStatementA ( uint256 [ ] memory reserves ) ~> amounts [ i + 1 ] = uniswapV2LibraryGetAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; Ss:Statements => uniswapV2LibraryGetAmountOut ( v ( read(Va, ListItem(MInt2Unsigned(Vi)), uint256 []) , uint256 ) , v ( V1 , uint256 ) , v ( V2 , uint256 ) , .TypedVals ) ~> freezerAssignment ( amounts [ i + 1 ] ) ~> freezerExpressionStatement ( ) ~> Ss ... + true + + ( _ (i |-> var(Ii, uint256)) (amounts |-> var(Ia, uint256 [])) ) #as E => + E (reserves |-> var(size(STORE), uint256 [ ])) + + ( _ [ Ii <- Vi:MInt{256} ] [ Ia <- Va ]) #as STORE => + STORE ListItem(ListItem(V1) ListItem(V2)) + + uniswapV2LibraryGetAmountsOut [priority(40)] + + rule v ( V , uint256 ) ~> freezerAssignment ( amounts [ i + 1 ] ) ~> freezerExpressionStatement ( ) ~> .Statements ~> restoreEnv ( ( _ (i |-> var ( Ii , uint256 )) ) #as ENV ) ~> i ++ ; .Statements ~> restoreEnv ( ENV ) => .K ... + true + + ( _ (i |-> var(Ii, uint256)) (amounts |-> var(Ia, uint256 [])) ) => ENV + + ( _ [ Ii <- Vi:MInt{256} ] ) #as STORE => + STORE [Ia <- write({STORE [ Ia ]}:>Value, ListItem(MInt2Unsigned(Vi) +Int 1), V, uint256[])] [ Ii <- Vi +MInt 1p256 ] + + uniswapV2LibraryGetAmountsOut [priority(40)] + + rule if ( v ( false , bool ) ) { _:Statements } else { .Statements } ~> .Statements ~> restoreEnv ( _:Map ) ~> .Statements ~> restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K + true + _ => E + _ [ Ia <- Va ] + uniswapV2LibraryGetAmountsOut => FUNC + ... ListItem(frame(K, E, FUNC)) => .List [priority(40)] + +endmodule +``` + ```k module SOLIDITY-UNISWAP-GETAMOUNTOUT-SUMMARY imports SOLIDITY-CONFIGURATION @@ -3257,6 +3327,7 @@ endmodule module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-INIT-SUMMARY imports SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY + imports SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY imports SOLIDITY-UNISWAP-GETAMOUNTOUT-SUMMARY imports SOLIDITY-UNISWAP-UNISWAPV2LIBRARYGETRESERVES-SUMMARY imports SOLIDITY-UNISWAP-GETAMOUNTIN-SUMMARY From 4dac6d7350d4d1f47377dcb61add1d3f6f3bb9d4 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 1 Oct 2024 19:13:44 -0500 Subject: [PATCH 2/4] Added comments. --- src/uniswap-summaries.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 50b3b25..d81ae13 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2685,6 +2685,7 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY imports SOLIDITY-EXPRESSION imports SOLIDITY-STATEMENT + // Call to GetAmountsOut to beginning of while loop rule uniswapV2LibraryGetAmountsOut:Id ( v ( V1:MInt{256} , uint256 ) , lv ( I2 , .List , address [ ]:TypeName ) , .TypedVals:CallArgumentList ) ~> K => SsFor ~> restoreEnv((amountIn |-> var(size(STORE), uint256)) (path |-> var(size(STORE) +Int 1, address [ ])) (amounts |-> var(size(STORE) +Int 3, uint256 [ ]))) ~> Ss ~> return amounts ; ~> .K true TYPE @@ -2705,18 +2706,21 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY ... .List => ListItem(frame(K, E, FUNC)) requires Int2MInt(size({read(V2, .List, address [ ])}:>List))::MInt{256} >=uMInt 2p256 [priority(40)] + // While loop rewrite and condition evaluation rule while (( i < path . length - 1 ) #as Cond) Body:Statement Ss:Statements => if (v(Vi List))::MInt{256} -MInt 1p256), bool)) {Body while(Cond) Body} else {.Statements} ~> Ss ... true ... (i |-> var(Ii, uint256)) (path |-> var(Ip, address [ ])) ... _ [ Ii <- Vi ] [ Ip <- Vp ] uniswapV2LibraryGetAmountsOut [priority(40)] + // While condition evaluated to true until call to uniswapV2LibraryGetReserves rule if ( v ( true , bool ) ) { { { uint256 [ ] memory reserves = uniswapV2LibraryGetReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; Ss'':Statements } Ss':Statements } Ss:Statements } else { .Statements } => uniswapV2LibraryGetReserves ( v ( read(Vp, ListItem(MInt2Unsigned(Vi)), address []) , address ) , v ( read(Vp, ListItem(MInt2Unsigned(Vi) +Int 1), address []) , address ) , .TypedVals ) ~> freezerVariableDeclarationStatementA ( uint256 [ ] memory reserves ) ~> Ss'' ~> restoreEnv(E) ~> Ss' ~> restoreEnv(E) ~> Ss ~> restoreEnv(E) ... true ( _ (i |-> var(Ii, uint256)) (path |-> var(Ip, address [])) ) #as E _ [ Ii <- Vi:MInt{256} ] [ Ip <- Vp ] uniswapV2LibraryGetAmountsOut [priority(40)] + // uniswapV2LibraryGetReserves return until call to uniswapV2LibraryGetAmountOut rule v ( ListItem ( V1:MInt{256} ) ListItem ( V2:MInt{256} ) , uint256 [ ] ) ~> freezerVariableDeclarationStatementA ( uint256 [ ] memory reserves ) ~> amounts [ i + 1 ] = uniswapV2LibraryGetAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; Ss:Statements => uniswapV2LibraryGetAmountOut ( v ( read(Va, ListItem(MInt2Unsigned(Vi)), uint256 []) , uint256 ) , v ( V1 , uint256 ) , v ( V2 , uint256 ) , .TypedVals ) ~> freezerAssignment ( amounts [ i + 1 ] ) ~> freezerExpressionStatement ( ) ~> Ss ... true @@ -2728,6 +2732,7 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY uniswapV2LibraryGetAmountsOut [priority(40)] + // uniswapV2LibraryGetAmountOut to end of while body rule v ( V , uint256 ) ~> freezerAssignment ( amounts [ i + 1 ] ) ~> freezerExpressionStatement ( ) ~> .Statements ~> restoreEnv ( ( _ (i |-> var ( Ii , uint256 )) ) #as ENV ) ~> i ++ ; .Statements ~> restoreEnv ( ENV ) => .K ... true @@ -2738,6 +2743,7 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY uniswapV2LibraryGetAmountsOut [priority(40)] + // While condition evaluated to false until return from getAmountsOut to caller rule if ( v ( false , bool ) ) { _:Statements } else { .Statements } ~> .Statements ~> restoreEnv ( _:Map ) ~> .Statements ~> restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K true _ => E From df1585d8938bca8760b4649dcd58bc890462bfc3 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 2 Oct 2024 19:50:22 -0500 Subject: [PATCH 3/4] Edited end of function summary. Number of expected restoreEnv (closing scopes) is input dependent). --- src/uniswap-summaries.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index d81ae13..326b677 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2743,8 +2743,8 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY uniswapV2LibraryGetAmountsOut [priority(40)] - // While condition evaluated to false until return from getAmountsOut to caller - rule if ( v ( false , bool ) ) { _:Statements } else { .Statements } ~> .Statements ~> restoreEnv ( _:Map ) ~> .Statements ~> restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K + // End of function: final environment restoration until return from getAmountsOut to caller + rule restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K true _ => E _ [ Ia <- Va ] From ebd68ff563e380385381eb340a9090f28f70fc4d Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 2 Oct 2024 19:58:22 -0500 Subject: [PATCH 4/4] Added rule to skip unneeded enrironment updates. --- src/uniswap-summaries.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 326b677..63fe6bb 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2743,6 +2743,13 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY uniswapV2LibraryGetAmountsOut [priority(40)] + // Skip environment updates when not needed. + // These occur due to the multiple block statements, introduced by the if + // statement that the while rewrites to. + rule restoreEnv( _:Map ) ~> .Statements ~> restoreEnv( E:Map ) => restoreEnv(E) ... + true + uniswapV2LibraryGetAmountsOut [priority(40)] + // End of function: final environment restoration until return from getAmountsOut to caller rule restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K true