From ebb086ed1f42869677661eadaf741624bed7be45 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 24 Sep 2024 11:27:55 -0500 Subject: [PATCH 1/4] Summaries of non branching sequences for fidswap. --- src/uniswap-summaries.md | 118 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 118 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index c4dd26e..71395b2 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2826,6 +2826,123 @@ module SOLIDITY-UNISWAP-FIDUPDATE-SUMMARY endmodule ``` +```k +module SOLIDITY-UNISWAP-FIDSWAP-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-EXPRESSION + imports SOLIDITY-STATEMENT + imports SOLIDITY-UNISWAP-TOKENS + + // Start of while loop to evaluated condition + rule while ((i < path . length - 1) #as Cond) Body:Statement Ss:Statements => if (v(Vi List))::MInt{256} -MInt Int2MInt(1)::MInt{256}), bool)) {Body while(Cond) Body} else {.Statements} Ss ... + true + ... (i |-> var(Ii, uint256)) (path |-> var(Ip, Tp)) ... + _ [ Ii <- Vi ] [ Ip <- Vp ] + fidSwap [priority(40)] + + // While loop body to SortTokens call + rule ({ { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2LibrarySortTokens ( input , output , .TypedVals ) ; Ss:Statements } Post:Statements } #as S) while ( E:Expression ) S Ss':Statements => uniswapV2LibrarySortTokens ( v ( read(Vp, ListItem(MInt2Unsigned(Vi)), address []) , address ) , v ( read(Vp, ListItem(MInt2Unsigned(Vi) +Int 1), address []) , address ) , .TypedVals ) ~> freezerVariableDeclarationStatementA ( address [ ] memory tokens ) ~> Ss ~> restoreEnv(ENV) ~> Post ~> restoreEnv(ENV) ~> while (E) S Ss' ... + true + + ( _ (i |-> var(Ii, uint256)) (path |-> var(Ip, address [])) ) #as ENV => + ENV (input |-> var(size(STORE), address)) (output |-> var(size(STORE) +Int 1, address)) + + + ( _ [ Ii <- Vi:MInt{256} ] [ Ip <- Vp ] ) #as STORE => + STORE ListItem(read(Vp, ListItem(MInt2Unsigned(Vi)), address [])) + ListItem(read(Vp, ListItem(MInt2Unsigned(Vi) +Int 1), address [])) + + fidSwap [priority(40)] + + // SortTokens call to evaluation of ternary operation condition, 1 + // apply this instead of SortTokens summary if possible + rule uniswapV2LibrarySortTokens ( v ( V1 , address ) , v ( V2 , address ) , .TypedVals ) ~> freezerVariableDeclarationStatementA ( address [ ] memory tokens ) ~> 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 ; Ss:Statements => v(Vi List))::MInt{256} -MInt Int2MInt(2)::MInt{256}), bool) ~> freezerTernaryOperator ( uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) , vidTo ) ~> freezerVariableDeclarationStatementA ( address to ) ~> Ss ... + true + + ( _ (i |-> var(Ii, uint256)) (amounts |-> var(Ia, uint256 [])) (path |-> var(Ip, address [])) ) #as ENV => + ENV (tokens |-> var(size(STORE) +Int 4, address [])) + (amountOut |-> var(size(STORE) +Int 5, uint256)) + (amount0Out |-> var(size(STORE) +Int 6, uint256)) + (amount1Out |-> var(size(STORE) +Int 7, uint256)) + + + ( _ [ Ii <- Vi:MInt{256} ] [ Ia <- Va ] [ Ip <- Vp ] ) #as STORE => + STORE ListItem(V1) // added by SortTokens + ListItem(V2) // added by SortTokens + ListItem(default(address[])) // added by SortTokens + ListItem(ListItem(V1) ListItem(V2)) // added by SortTokens + ListItem(ListItem(V1) ListItem(V2)) + ListItem(read(Va, ListItem(MInt2Unsigned(Vi) +Int 1), uint256 [])) + ListItem(Int2MInt(0)::MInt{256}) + ListItem(read(Va, ListItem(MInt2Unsigned(Vi) +Int 1), uint256 [])) + + fidSwap + requires V1 uniswapV2LibrarySortTokens ( v ( V1 , address ) , v ( V2 , address ) , .TypedVals ) ~> freezerVariableDeclarationStatementA ( address [ ] memory tokens ) ~> 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 ; Ss:Statements => v(Vi List))::MInt{256} -MInt Int2MInt(2)::MInt{256}), bool) ~> freezerTernaryOperator ( uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) , vidTo ) ~> freezerVariableDeclarationStatementA ( address to ) ~> Ss ... + true + + ( _ (i |-> var(Ii, uint256)) (amounts |-> var(Ia, uint256 [])) (path |-> var(Ip, address [])) ) #as ENV => + ENV (tokens |-> var(size(STORE) +Int 4, address [])) + (amountOut |-> var(size(STORE) +Int 5, uint256)) + (amount0Out |-> var(size(STORE) +Int 6, uint256)) + (amount1Out |-> var(size(STORE) +Int 7, uint256)) + + + ( _ [ Ii <- Vi:MInt{256} ] [ Ia <- Va ] [ Ip <- Vp ] ) #as STORE => + STORE ListItem(V1) // added by SortTokens + ListItem(V2) // added by SortTokens + ListItem(default(address[])) // added by SortTokens + ListItem(ListItem(V2) ListItem(V1)) // added by SortTokens + ListItem(ListItem(V2) ListItem(V1)) + ListItem(read(Va, ListItem(MInt2Unsigned(Vi) +Int 1), uint256 [])) + ListItem(read(Va, ListItem(MInt2Unsigned(Vi) +Int 1), uint256 [])) + ListItem(Int2MInt(0)::MInt{256}) + + fidSwap + requires V2 v(false, bool) ~> freezerTernaryOperator ( uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) , vidTo ) => v(V, T) ... + true + ... vidTo |-> var(I, T) ... + _ [ I <- V ] + fidSwap [priority(40)] + + // Ternary operator, true + rule v(true, bool) ~> freezerTernaryOperator ( uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) , vidTo ) => uniswapV2LibraryPairFor ( v(Vo, address), v(read(Vp, ListItem(MInt2Unsigned(Vi) +Int 2), address []), address), .TypedVals ) ... + true + ... (output |-> var(Io, address)) (i |-> var(Ii, uint256)) (path |-> var(Ip, address []))... + _ [ Io <- Vo:MInt{160} ] [ Ii <- Vi:MInt{256} ] [ Ip <- Vp ] + fidSwap [priority(40)] + + // Assignment from ternary operator until PairFor call + rule v(V, address) ~> freezerVariableDeclarationStatementA ( address to ) ~> uniswapV2Pair ( uniswapV2LibraryPairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; Ss:Statements => uniswapV2LibraryPairFor ( v ( Vi , address ) , v ( Vo , address ) , .TypedVals ) ~> freezerCallArgumentListTail ( .TypedVals ) ~> freezerCallId ( uniswapV2Pair ) ~> freezerExternalCallBase ( swap , v ( V0 , uint256 ) , v ( V1 , uint256 ) , v ( V , address ) , .TypedVals ) ~> freezerExpressionStatement ( ) ~> Ss ... + true + + ( _ (input |-> var(Ii, address)) + (output |-> var(Io, address)) + (amount0Out |-> var(I0, uint256)) + (amount1Out |-> var(I1, uint256)) ) #as ENV => + ENV (to |-> var(size(STORE), address)) + + + ( _ [ Ii <- Vi:MInt{160} ] [ Io <- Vo:MInt{160} ] + [ I0 <- V0:MInt{256} ] [ I1 <- V1:MInt{256} ] ) #as STORE => + STORE ListItem(V) + + fidSwap [priority(40)] + + // PairFor result to external call to swap + rule v(V, address) ~> freezerCallArgumentListTail ( .TypedVals ) ~> freezerCallId ( uniswapV2Pair ) ~> freezerExternalCallBase ( swap , TV0 , TV1 , TV2 , .TypedVals ) => v(V, uniswapV2Pair).swap( TV0 , TV1 , TV2 , .TypedVals ) ... + true + fidSwap [priority(40)] + +endmodule +``` + ```k module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-INIT-SUMMARY @@ -2834,6 +2951,7 @@ module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-GETAMOUNTIN-SUMMARY imports SOLIDITY-UNISWAP-PAIRFOR-SUMMARY imports SOLIDITY-UNISWAP-FIDUPDATE-SUMMARY + imports SOLIDITY-UNISWAP-FIDSWAP-SUMMARY endmodule ``` From 863d8ca7fdedd896dd345ae2247f0dc75cb9c31b Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 24 Sep 2024 18:39:13 -0500 Subject: [PATCH 2/4] Summarize additional steps: bind to declaration of i. --- src/uniswap-summaries.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 71395b2..47ec1e4 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2833,6 +2833,17 @@ module SOLIDITY-UNISWAP-FIDSWAP-SUMMARY imports SOLIDITY-STATEMENT imports SOLIDITY-UNISWAP-TOKENS + // Bind to initial block and declaration of i + rule bind(STORE, ListItem(amounts) ListItem(path) ListItem(vidTo), ListItem(uint256 [ ]:TypeName) ListItem(address [ ]:TypeName) ListItem(address), lv(I0, .List, uint256 [ ]), lv(I1, .List, address [ ]), v(V, address), .TypedVals, .List, .List) ~> {uint256 i ; Ss:Statements } Ss':Statements => Ss ~> restoreEnv((amounts |-> var(size(S), uint256 [ ])) (path |-> var(size(S) +Int 1, address [ ])) (vidTo |-> var(size(S) +Int 2, address))) ~> Ss' ... + true + .Map => .Map (amounts |-> var(size(S), uint256 [ ])) + (path |-> var(size(S) +Int 1, address [ ])) + (vidTo |-> var(size(S) +Int 2, address)) + (i |-> var(size(S) +Int 3, uint256)) + + S => S ListItem(STORE [ I0 ]) ListItem(STORE [ I1 ]) ListItem(V) ListItem(default(uint256)) + fidSwap [priority(40)] + // Start of while loop to evaluated condition rule while ((i < path . length - 1) #as Cond) Body:Statement Ss:Statements => if (v(Vi List))::MInt{256} -MInt Int2MInt(1)::MInt{256}), bool)) {Body while(Cond) Body} else {.Statements} Ss ... true From 5cfffd14089f0c7e105319cc9c9650e283018b28 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 24 Sep 2024 19:56:45 -0500 Subject: [PATCH 3/4] Summarize additional steps: swap result to end of loop. --- src/uniswap-summaries.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 47ec1e4..45b053f 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2951,6 +2951,13 @@ module SOLIDITY-UNISWAP-FIDSWAP-SUMMARY true fidSwap [priority(40)] + // swap result to end of loop + rule void ~> freezerExpressionStatement() ~> .Statements ~> restoreEnv(E) ~> i++ ; .Statements ~> restoreEnv(E) => .K ... + true + ( _ (i |-> var(I, uint256)) ) => E + ( _ [ I <- V:MInt{256} ] ) #as S => S [ I <- V +MInt Int2MInt(1)::MInt{256} ] + fidSwap [priority(40)] + endmodule ``` From fc417da003e107f74034477dd20e21740db141ac Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 24 Sep 2024 20:28:30 -0500 Subject: [PATCH 4/4] Added one rewrite step in the summary for while. --- src/uniswap-summaries.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 45b053f..18000e3 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2845,7 +2845,7 @@ module SOLIDITY-UNISWAP-FIDSWAP-SUMMARY fidSwap [priority(40)] // Start of while loop to evaluated condition - rule while ((i < path . length - 1) #as Cond) Body:Statement Ss:Statements => if (v(Vi List))::MInt{256} -MInt Int2MInt(1)::MInt{256}), bool)) {Body while(Cond) Body} else {.Statements} Ss ... + rule while ((i < path . length - 1) #as Cond) Body:Statement Ss:Statements => if (v(Vi List))::MInt{256} -MInt Int2MInt(1)::MInt{256}), bool)) {Body while(Cond) Body} else {.Statements} ~> Ss ... true ... (i |-> var(Ii, uint256)) (path |-> var(Ip, Tp)) ... _ [ Ii <- Vi ] [ Ip <- Vp ]