Summarize additional steps: swap result to end of loop.

Pi-Squared-Inc · Sep 25, 2024 · 5cfffd1 · 5cfffd1
1 parent 863d8ca
commit 5cfffd1
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
@@ -2951,6 +2951,13 @@ module SOLIDITY-UNISWAP-FIDSWAP-SUMMARY
        <summarize> true </summarize>
        <current-function> fidSwap </current-function> [priority(40)]
 
+  // swap result to end of loop
+  rule <k> void ~> freezerExpressionStatement() ~> .Statements ~> restoreEnv(E) ~> i++ ; .Statements ~> restoreEnv(E) => .K ...</k>
+       <summarize> true </summarize>
+       <env> ( _ (i |-> var(I, uint256)) ) => E </env>
+       <store> ( _ [ I <- V:MInt{256} ] ) #as S => S [ I <- V +MInt Int2MInt(1)::MInt{256} ] </store>
+       <current-function> fidSwap </current-function> [priority(40)]
+
 endmodule
 ```