Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Summarized rules for fidSwap #42

Merged
merged 5 commits into from
Sep 26, 2024
Merged

Summarized rules for fidSwap #42

Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
ebb086e
Summaries of non branching sequences for fidswap.
mariaKt Sep 24, 2024
863d8ca
Summarize additional steps: bind to declaration of i.
mariaKt Sep 24, 2024
5cfffd1
Summarize additional steps: swap result to end of loop.
mariaKt Sep 25, 2024
fc417da
Added one rewrite step in the summary for while.
mariaKt Sep 25, 2024
dc87fbc
Merge branch 'main' into fidswap-summary
mariaKt Sep 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
136 changes: 136 additions & 0 deletions src/uniswap-summaries.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2826,6 +2826,141 @@ 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

// Bind to initial block and declaration of i
rule <k> 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' ...</k>
<summarize> true </summarize>
<env> .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))
</env>
<store> S => S ListItem(STORE [ I0 ]) ListItem(STORE [ I1 ]) ListItem(V) ListItem(default(uint256)) </store>
<current-function> fidSwap </current-function> [priority(40)]

// Start of while loop to evaluated condition
rule <k> while ((i < path . length - 1) #as Cond) Body:Statement Ss:Statements => if (v(Vi <uMInt (Int2MInt(size({read(Vp, .List, Tp)}:>List))::MInt{256} -MInt Int2MInt(1)::MInt{256}), bool)) {Body while(Cond) Body} else {.Statements} ~> Ss ...</k>
<summarize> true </summarize>
<env>... (i |-> var(Ii, uint256)) (path |-> var(Ip, Tp)) ...</env>
<store> _ [ Ii <- Vi ] [ Ip <- Vp ] </store>
<current-function> fidSwap </current-function> [priority(40)]

// While loop body to SortTokens call
rule <k> ({ { 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' ...</k>
<summarize> true </summarize>
<env>
( _ (i |-> var(Ii, uint256)) (path |-> var(Ip, address [])) ) #as ENV =>
ENV (input |-> var(size(STORE), address)) (output |-> var(size(STORE) +Int 1, address))
</env>
<store>
( _ [ 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 []))
</store>
<current-function> fidSwap </current-function> [priority(40)]

// SortTokens call to evaluation of ternary operation condition, 1
// apply this instead of SortTokens summary if possible
rule <k> 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 <uMInt (Int2MInt(size({read(Vp, .List, address [])}:>List))::MInt{256} -MInt Int2MInt(2)::MInt{256}), bool) ~> freezerTernaryOperator ( uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) , vidTo ) ~> freezerVariableDeclarationStatementA ( address to ) ~> Ss ...</k>
<summarize> true </summarize>
<env>
( _ (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))
</env>
<store>
( _ [ 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 []))
</store>
<current-function> fidSwap </current-function>
requires V1 <uMInt V2 andBool V1 =/=MInt 0p160 [priority(39)]

// SortTokens call to evaluation of ternary operation condition, 2
// apply this instead of SortTokens summary if possible
rule <k> 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 <uMInt (Int2MInt(size({read(Vp, .List, address [])}:>List))::MInt{256} -MInt Int2MInt(2)::MInt{256}), bool) ~> freezerTernaryOperator ( uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) , vidTo ) ~> freezerVariableDeclarationStatementA ( address to ) ~> Ss ...</k>
<summarize> true </summarize>
<env>
( _ (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))
</env>
<store>
( _ [ 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})
</store>
<current-function> fidSwap </current-function>
requires V2 <uMInt V1 andBool V2 =/=MInt 0p160 [priority(39)]

// Ternary operator, false
rule <k> v(false, bool) ~> freezerTernaryOperator ( uniswapV2LibraryPairFor ( output , path [ i + 2 ] , .TypedVals ) , vidTo ) => v(V, T) ...</k>
<summarize> true </summarize>
<env>... vidTo |-> var(I, T) ...</env>
<store> _ [ I <- V ] </store>
<current-function> fidSwap </current-function> [priority(40)]

// Ternary operator, true
rule <k> 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 ) ...</k>
<summarize> true </summarize>
<env>... (output |-> var(Io, address)) (i |-> var(Ii, uint256)) (path |-> var(Ip, address []))...</env>
<store> _ [ Io <- Vo:MInt{160} ] [ Ii <- Vi:MInt{256} ] [ Ip <- Vp ] </store>
<current-function> fidSwap </current-function> [priority(40)]

// Assignment from ternary operator until PairFor call
rule <k> 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 ...</k>
<summarize> true </summarize>
<env>
( _ (input |-> var(Ii, address))
(output |-> var(Io, address))
(amount0Out |-> var(I0, uint256))
(amount1Out |-> var(I1, uint256)) ) #as ENV =>
ENV (to |-> var(size(STORE), address))
</env>
<store>
( _ [ Ii <- Vi:MInt{160} ] [ Io <- Vo:MInt{160} ]
[ I0 <- V0:MInt{256} ] [ I1 <- V1:MInt{256} ] ) #as STORE =>
STORE ListItem(V)
</store>
<current-function> fidSwap </current-function> [priority(40)]

// PairFor result to external call to swap
rule <k> v(V, address) ~> freezerCallArgumentListTail ( .TypedVals ) ~> freezerCallId ( uniswapV2Pair ) ~> freezerExternalCallBase ( swap , TV0 , TV1 , TV2 , .TypedVals ) => v(V, uniswapV2Pair).swap( TV0 , TV1 , TV2 , .TypedVals ) ...</k>
<summarize> true </summarize>
<current-function> fidSwap </current-function> [priority(40)]

// swap result to end of loop
rule <k> void ~> freezerExpressionStatement() ~> .Statements ~> restoreEnv(E) ~> i++ ; .Statements ~> restoreEnv(E) => .K ...</k>
<summarize> true </summarize>
<env> ( _ (i |-> var(I, uint256)) ) => E </env>
<store> ( _ [ I <- V:MInt{256} ] ) #as S => S [ I <- V +MInt Int2MInt(1)::MInt{256} ] </store>
<current-function> fidSwap </current-function> [priority(40)]

endmodule
```

```k
module SOLIDITY-UNISWAP-SUMMARIES
imports SOLIDITY-UNISWAP-INIT-SUMMARY
Expand All @@ -2834,6 +2969,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
```