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

Swap summary continued #61

Merged
merged 15 commits into from
Oct 10, 2024
Merged

Swap summary continued #61

Changes from 11 commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
4e3784f
Swap summary rule: first if end -> second if condition evaluation.
mariaKt Oct 8, 2024
65cfe66
Swap summary: 2nd if condition true -> transfer call.
mariaKt Oct 8, 2024
ce2fd76
Swap summary: params and address for first balanceOf call.
mariaKt Oct 8, 2024
527216f
Swap summary: balanceOf return -> second balanceOf call
mariaKt Oct 8, 2024
043d0f6
Swap summary: 2nd balanceOf return -> 1st ternary cond eval.
mariaKt Oct 8, 2024
5e30752
Swap summaries: for ternary operations.
mariaKt Oct 8, 2024
e046c9f
Swap summaries: ternary operations, conditions evaluated to other value.
mariaKt Oct 9, 2024
92a0650
Swap summary: requirements after ternary operations
mariaKt Oct 9, 2024
cc96f91
Swap summary updated: compute args to fidUpdate in same rule for requ…
mariaKt Oct 9, 2024
c43de4d
Swap summary: fidupdate return -> end.
mariaKt Oct 9, 2024
8387d33
Added a parenthesis to make a condition clearer.
mariaKt Oct 9, 2024
f1ace85
Merge branch 'main' into swap-summary-cont
mariaKt Oct 10, 2024
9921583
Updated comment for 2nd if condition evaluation rule.
mariaKt Oct 10, 2024
866bc67
Swap summary: first if condition true -> transfer call.
mariaKt Oct 10, 2024
b6509d0
Swap summary: used single rule for the two if true branches.
mariaKt Oct 10, 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
148 changes: 148 additions & 0 deletions src/uniswap-summaries.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3155,6 +3155,154 @@ module SOLIDITY-UNISWAP-SWAP-SUMMARY
<current-function> swap </current-function>
requires Vto =/=MInt {S[token0] orDefault default(address)}:>MInt{160} andBool Vto =/=MInt {S[token1] orDefault default(address)}:>MInt{160} [priority(40)]

// End of first if statement to second if condition evaluation
rule <k> 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 ...</k>
<summarize> true </summarize>
<env>... amount1Out |-> var(Ia1, uint256) ...</env>
<store> _ [ Ia1 <- Va1 ] </store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// Second if condition evaluated to true to transfer call
rule <k> if ( v( true, bool) ) iERC20 ( vidToken1 , .TypedVals ) . transfer ( to , amount1Out , .TypedVals ) ; => v ( Vv1 , iERC20 ) . transfer ( v ( Vto , address ) , v ( Va1 , uint256 ) , .TypedVals ) ~> freezerExpressionStatement ( ) ...</k>
<summarize> true </summarize>
<env>... (amount1Out |-> var(Ia1, uint256))
(to |-> var(Ito, address))
(vidToken1 |-> var(Iv1, address))
...</env>
<store> _ [ Ia1 <- Va1 ] [ Ito <- Vto ] [ Iv1 <- Vv1 ] </store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// After if conditions: compute params and address for first balanceOf call
rule <k> balance0 = iERC20 ( vidToken0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; Ss:Statements => v ( Vv0 , iERC20 ) . balanceOf ( v ( THIS , address ) , .TypedVals ) ~> freezerAssignment ( balance0 ) ~> freezerExpressionStatement ( ) ~> Ss...</k>
<summarize> true </summarize>
<env>... (vidToken0 |-> var(Iv0, address)) ...</env>
<store> _ [ Iv0 <- Vv0 ] </store>
<this> THIS:MInt{160} </this>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// First balanceOf return to compute params and address for second balanceOf call
rule <k> v ( V:MInt{256} , uint256 ) ~> freezerAssignment ( balance0 ) ~> freezerExpressionStatement ( ) ~> balance1 = iERC20 ( vidToken1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ; Ss:Statements => v ( Vv1 , iERC20 ) . balanceOf ( v ( THIS , address ) , .TypedVals ) ~> freezerAssignment ( balance1 ) ~> freezerExpressionStatement ( ) ~> Ss ...</k>
<summarize> true </summarize>
<env>... (balance0 |-> var(Ib0, uint256)) (vidToken1 |-> var(Iv1, address)) ...</env>
<store> ( _ [ Iv1 <- Vv1 ] [ Ib0 <- _ ] ) #as STORE => STORE [ Ib0 <- V ] </store>
<this> THIS:MInt{160} </this>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// Second balanceOf return to condition of first ternary operator evaluation
rule <k> v ( V:MInt{256} , uint256 ) ~> freezerAssignment ( balance1 ) ~> freezerExpressionStatement ( ) ~> .Statements ~> restoreEnv ( ( _:Map (amount0Out |-> var ( Ia0 , uint256 )) (balance0 |-> var ( Ib0 , uint256 )) (reserves |-> var ( Ir , uint112 [ ] )) ) #as ENV ) ~> uint256 amount0In = balance0 > reserves [ 0 ] - amount0Out ? balance0 - ( reserves [ 0 ] - amount0Out ) : 0 ; Ss:Statements => v ( Vb0 >uMInt (roundMInt(Vr0)::MInt{256} -MInt Va0), bool ) ? balance0 - ( reserves [ 0 ] - amount0Out ) : 0 ~> freezerVariableDeclarationStatementA ( uint256 amount0In ) ~> Ss ...</k>
<summarize> true </summarize>
<env> ( _ (balance1 |-> var(Ib1, uint256)) ) => ENV </env>
<store> ( _ [ Ia0 <- Va0:MInt{256} ]
[ Ib0 <- Vb0:MInt{256} ]
[ Ib1 <- _ ]
[ Ir <- ListItem(Vr0:MInt{112}) ListItem(_) ListItem(_) ]
) #as STORE => STORE [ Ib1 <- V ]
</store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// First ternary operator evaluated to true -> assignment to amount0In
rule <k> v ( true , bool ) ? balance0 - ( reserves [ 0 ] - amount0Out ) : 0 ~> freezerVariableDeclarationStatementA ( uint256 amount0In ) => .K ...</k>
<summarize> true </summarize>
<env> ( _ (amount0Out |-> var ( Ia0 , uint256 ))
(balance0 |-> var ( Ib0 , uint256 ))
(reserves |-> var ( Ir , uint112 [ ] )) ) #as ENV =>
ENV [ amount0In <- var(size(STORE), uint256)]
</env>
<store> ( _ [ Ia0 <- Va0:MInt{256} ]
[ Ib0 <- Vb0:MInt{256} ]
[ Ir <- ListItem(Vr0:MInt{112}) ListItem(_) ListItem(_) ]
) #as STORE => STORE ListItem(Vb0 -MInt (roundMInt(Vr0)::MInt{256} -MInt Va0))
</store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// First ternary operator evaluated to false -> assignment to amount0In
rule <k> v ( false , bool ) ? balance0 - ( reserves [ 0 ] - amount0Out ) : 0 ~> freezerVariableDeclarationStatementA ( uint256 amount0In ) => .K ...</k>
<summarize> true </summarize>
<env> ENV => ENV [ amount0In <- var(size(STORE), uint256)] </env>
<store> STORE => STORE ListItem(0p256) </store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// Second ternary operator, to its condition evaluation
rule <k> uint256 amount1In = balance1 > reserves [ 1 ] - amount1Out ? balance1 - ( reserves [ 1 ] - amount1Out ) : 0 ; Ss:Statements => v ( Vb1 >uMInt (roundMInt(Vr1)::MInt{256} -MInt Va1), bool ) ? balance1 - ( reserves [ 1 ] - amount1Out ) : 0 ~> freezerVariableDeclarationStatementA ( uint256 amount1In ) ~> Ss ...</k>
<summarize> true </summarize>
<env>... (amount1Out |-> var ( Ia1 , uint256 ))
(balance1 |-> var ( Ib1 , uint256 ))
(reserves |-> var ( Ir , uint112 [ ] ))
...</env>
<store> _ [ Ia1 <- Va1:MInt{256} ]
[ Ib1 <- Vb1:MInt{256} ]
[ Ir <- ListItem(_) ListItem(Vr1:MInt{112}) ListItem(_) ]
</store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// Second ternary operator evaluated to false -> assignment to amount1In
rule <k> v ( false , bool ) ? balance1 - ( reserves [ 1 ] - amount1Out ) : 0 ~> freezerVariableDeclarationStatementA ( uint256 amount1In ) => .K ...</k>
<summarize> true </summarize>
<env> ENV => ENV [ amount1In <- var(size(STORE), uint256)] </env>
<store> STORE => STORE ListItem(0p256) </store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// Second ternary operator evaluated to true -> assignment to amount1In
rule <k> v ( true , bool ) ? balance1 - ( reserves [ 1 ] - amount1Out ) : 0 ~> freezerVariableDeclarationStatementA ( uint256 amount1In ) => .K ...</k>
<summarize> true </summarize>
<env> ( _ (amount1Out |-> var ( Ia1 , uint256 ))
(balance1 |-> var ( Ib1 , uint256 ))
(reserves |-> var ( Ir , uint112 [ ] )) ) #as ENV =>
ENV [ amount1In <- var(size(STORE), uint256)]
</env>
<store> ( _ [ Ia1 <- Va1:MInt{256} ]
[ Ib1 <- Vb1:MInt{256} ]
[ Ir <- ListItem(_) ListItem(Vr1:MInt{112}) ListItem(_) ]
) #as STORE => STORE ListItem(Vb1 -MInt (roundMInt(Vr1)::MInt{256} -MInt Va1))
</store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

// Requirements after ternary operators and args to fidUpdate
rule <k> require ( amount0In > 0 || amount1In > 0 , "UniswapV2: INSUFFICIENT_INPUT_AMOUNT" , .TypedVals ) ; { uint256 balance0Adjusted = balance0 * 1000 - amount0In * 3 ; uint256 balance1Adjusted = balance1 * 1000 - amount1In * 3 ; require ( balance0Adjusted * balance1Adjusted >= uint256 ( reserves [ 0 ] , .TypedVals ) * reserves [ 1 ] * 1000 ** 2 , "UniswapV2: K" , .TypedVals ) ; .Statements } fidUpdate ( balance0 , balance1 , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; Ss:Statements => fidUpdate ( v ( Vb0 , uint256 ) , v ( Vb1 , uint256 ) , v ( Vr0 , uint112 ) , v ( Vr1 , uint112 ) , .TypedVals ) ~> freezerExpressionStatement ( ) ~> Ss ...</k>
<summarize> true </summarize>
<env>... (amount0In |-> var ( Ia0 , uint256 ))
(amount1In |-> var ( Ia1 , uint256 ))
(balance0 |-> var ( Ib0 , uint256 ))
(balance1 |-> var ( Ib1 , uint256 ))
(reserves |-> var ( Ir , uint112 [ ] ))
...</env>
<store> ( _ [ Ia0 <- Va0:MInt{256} ]
[ Ia1 <- Va1:MInt{256} ]
[ Ib0 <- Vb0:MInt{256} ]
[ Ib1 <- Vb1:MInt{256} ]
[ Ir <- ListItem(Vr0:MInt{112}) ListItem(Vr1:MInt{112}) ListItem(_) ]
) #as STORE =>
STORE ListItem(Vb0 *MInt 1000p256 -MInt Va0 *MInt 3p256)
ListItem(Vb1 *MInt 1000p256 -MInt Va1 *MInt 3p256)
</store>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function>
requires (Va0 >uMInt 0p256 orBool Va1 >uMInt 0p256)
andBool (((Vb0 *MInt 1000p256 -MInt Va0 *MInt 3p256) *MInt (Vb1 *MInt 1000p256 -MInt Va1 *MInt 3p256)) >=uMInt (roundMInt(Vr0)::MInt{256} *MInt roundMInt(Vr1)::MInt{256} *MInt 1000000p256)) [priority(40)]

// fidUpdate return to end of swap
rule <k> void ~> freezerExpressionStatement ( ) ~> emit swapEvent ( msg . sender , amount0In , amount1In , amount0Out , amount1Out , to , .TypedVals ) ; .Statements => .K ...</k>
<summarize> true </summarize>
<msg-sender> _ </msg-sender>
<env>... (amount0In |-> var ( _ , uint256 ))
(amount1In |-> var ( _ , uint256 ))
(amount0Out |-> var ( _ , uint256 ))
(amount1Out |-> var ( _ , uint256 ))
(to |-> var ( _ , address ))
...</env>
<this-type> uniswapV2Pair </this-type>
<current-function> swap </current-function> [priority(40)]

endmodule
```

Expand Down