Moved a general rule to semantics rather than the summaries modules. (#…

…53)
Pi-Squared-Inc · Oct 10, 2024 · 5beaa76 · 5beaa76
1 parent d145b4b
commit 5beaa76
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 15 deletions.
diff --git a/src/statement.md b/src/statement.md
@@ -82,8 +82,9 @@ module SOLIDITY-STATEMENT
        <env> E </env>
 
   syntax KItem ::= restoreEnv(Map)
+  rule <k> restoreEnv( _:Map ) ~> .Statements ~> restoreEnv( E:Map ) => restoreEnv(E) ...</k>
   rule <k> restoreEnv(E) => .K ...</k>
-       <env> _ => E </env>
+       <env> _ => E </env> [owise]
 
   // while statement
   rule while (Cond) Body => if (Cond) {Body while(Cond) Body} else {.Statements}

diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
@@ -2743,13 +2743,6 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY
        </store>
        <current-function> uniswapV2LibraryGetAmountsOut </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> uniswapV2LibraryGetAmountsOut </current-function> [priority(40)]
-
   // End of function: final environment restoration until return from getAmountsOut to caller
   rule <k> restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K </k>
        <summarize> true </summarize>
@@ -3447,13 +3440,6 @@ module SOLIDITY-MATHSQRT-SUMMARY
        </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>