mathSqrt summary (#51)

* mathSqrt summaries. 1. else if part. 2. If part, before while.

Rules for while are TODO.

* Added comments.

* Summarized rule for mathSqrt, while -> if.

* Summary for mathSqrt: if true -> while.

* Two additional summaries, for the end of the while loop and the function.

src/uniswap-summaries.md

@@ -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>
+       <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>
+       <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>
+       <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
@@ -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
 ```