mathSqrt summary

[mariaKt]

This PR introduces summarized rules for the mathSqrt function.

These rules are saving 818 steps.

I would like your opinion specifically on this rule here:

  // 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)]

Due to the while statement rewriting to an if statement, as the function is executed, there are a lot of block statements that eventually lead to a sequence of

restoreEnv(E) ~> .Statements ~> restoreEnv(E) ~> .Statements ~> ...

I added this rule to skip the unneeded updates. Due to the number of while loop body executions being input dependent, I cannot specify the exact number that this is repeated, so this is a step per loop iteration.

My question is: is this rule OK to include in a summary, or is it considered a general semantic rule?

[Robertorosmaninho]

I have just a few clarification questions before approving it:

[Robertorosmaninho]

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

[mariaKt]

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>.

[mariaKt]

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>

[Robertorosmaninho]

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

[mariaKt]

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.

[Robertorosmaninho]

LGTM