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

mathSqrt summary #51

Merged
merged 6 commits into from
Oct 3, 2024
Merged

mathSqrt summary #51

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
a3cdcbd
mathSqrt summaries. 1. else if part. 2. If part, before while.
mariaKt Oct 2, 2024
69574dd
Added comments.
mariaKt Oct 2, 2024
c50019f
Summarized rule for mathSqrt, while -> if.
mariaKt Oct 2, 2024
00ba216
Summary for mathSqrt: if true -> while.
mariaKt Oct 2, 2024
a6f66df
Two additional summaries, for the end of the while loop and the funct…
mariaKt Oct 3, 2024
d43fa62
Merge branch 'main' into mathsqrt-summary
mariaKt Oct 3, 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
73 changes: 73 additions & 0 deletions src/uniswap-summaries.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3336,6 +3336,78 @@ module SOLIDITY-UNISWAP-GETRESERVES-SUMMARY
endmodule
```

```k
module SOLIDITY-MATHSQRT-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-UNISWAP-TOKENS
imports SOLIDITY-EXPRESSION
imports SOLIDITY-STATEMENT

// y > 3. Start to while loop
rule <k> mathSqrt:Id ( v(V:MInt{256}, uint256), .TypedVals ) ~> K => Ss ~> restoreEnv( (y |-> var(size(STORE), uint256)) (z |-> var(size(STORE) +Int 1, uint256)) ) ~> .Statements ~> return z ; ~> .K </k>
<summarize> true </summarize>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-fn-id> mathSqrt </contract-fn-id>
<contract-fn-body> if ( y > 3 ) { z = y ; uint256 x = y / 2 + 1 ; Ss:Statements } else if ( y != 0 ) { _:Statements } .Statements </contract-fn-body>
<env> E => (y |-> var(size(STORE), uint256))
(z |-> var(size(STORE) +Int 1, uint256))
(x |-> var(size(STORE) +Int 2, uint256))
</env>
<store> STORE =>
STORE ListItem(V) // y
ListItem(V) // z
ListItem((V /uMInt 2p256) +MInt 1p256) // x
</store>
<current-function> FUNC => mathSqrt </current-function>
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
<call-stack>... .List => ListItem(frame(K, E, FUNC)) </call-stack>
requires V >uMInt 3p256 [priority(40)]

// While loop rewrite and condition evaluation
rule <k> while (( x < z ) #as Cond) Body:Statement Ss:Statements => if (v(Vx <uMInt Vz, bool)) {Body while(Cond) Body} else {.Statements} ~> Ss ...</k>
<summarize> true </summarize>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same question from the case y <= 3 && y != 0 about the cell variables

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here, we are already within the body of the function mathSqrt, i.e. to get to this rule the one doing the matching and changes to the configuration related to the call itself has already matched and done its rewriting. So, we don't need to match any of those cells.

<env>... (x |-> var(Ix, uint256)) (z |-> var(Iz, uint256)) ...</env>
<store> _ [ Ix <- Vx:MInt{256} ] [ Iz <- Vz:MInt{256} ] </store>
<current-function> mathSqrt </current-function> [priority(40)]

// While condition evaluated to true until next while statement
rule <k> if ( v ( true , bool ) ) { { z = x ; x = ( y / x + x ) / 2 ; .Statements } Ss:Statements } else { .Statements } => Ss ~> restoreEnv(E) ...</k>
<summarize> true </summarize>
<env>
( _ (x |-> var(Ix, uint256))
(y |-> var(Iy, uint256))
(z |-> var(Iz, uint256)) ) #as E
</env>
<store>
( _ [ Ix <- Vx:MInt{256} ] [ Iy <- Vy:MInt{256} ] ) #as STORE =>
STORE [ Iz <- Vx ] [ Ix <- ((Vy /uMInt Vx) +MInt Vx) /uMInt 2p256 ]
</store>
<current-function> mathSqrt </current-function> [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 <k> restoreEnv( _:Map ) ~> .Statements ~> restoreEnv( E:Map ) => restoreEnv(E) ...</k>
<summarize> true </summarize>
<current-function> mathSqrt </current-function> [priority(40)]

// End of function: final environment restoration to return to caller
rule <k> restoreEnv ( _:Map (z |-> var(Iz, uint256)) ) ~> .Statements ~> return z ; ~> .K => v (Vz, uint256) ~> K </k>
<summarize> true </summarize>
<env> _ => E </env>
<store> _ [ Iz <- Vz ] </store>
<current-function> mathSqrt => FUNC </current-function>
<call-stack>... ListItem(frame(K, E, FUNC)) => .List </call-stack> [priority(40)]

// y <= 3 && y != 0
rule <k> mathSqrt:Id ( v(V:MInt{256}, uint256), .TypedVals ) => v (1p256, uint256) ...</k>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a reason why the cells: <this-type>, <contract-id>, <contract-fn-id>, etc. wouldn't be necessary here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. This rule replaces the entire call. So, we do not need to try and find the code of the function, we simply return a TypedVal. We know that a <contract-fn> with <contract-fn-id> mathSqrt </contract-fn-id> exists, but we do not need to find any information from the cells in that <contract-fn>.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can think of it just like any other summary of en entire call (which it is with these conditions), e.g.

solidity-demo-semantics/src/uniswap-summaries.md

Line 2658 in c94634e

rule <k> uniswapV2LibrarySortTokens:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), .TypedVals ) => v(ListItem(V1) ListItem(V2), T[]) ...</k>

<summarize> true </summarize>
<store> STORE => STORE ListItem(V) ListItem(1p256) </store>
requires V <=uMInt 3p256 andBool V =/=MInt 0p256 [priority(40)]

endmodule
```

```k
module SOLIDITY-UNISWAP-SUMMARIES
imports SOLIDITY-UNISWAP-INIT-SUMMARY
Expand All @@ -3350,6 +3422,7 @@ module SOLIDITY-UNISWAP-SUMMARIES
imports SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY
imports SOLIDITY-UNISWAP-GETRESERVES-SUMMARY
imports SOLIDITY-UNISWAP-SETUP-SUMMARY
imports SOLIDITY-MATHSQRT-SUMMARY

endmodule
```