Updated summary with store cell being a list

Pi-Squared-Inc · Sep 18, 2024 · e3295cb · e3295cb
1 parent f6278d3
commit e3295cb
Showing 1 changed file with 8 additions and 6 deletions.
diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
@@ -2407,18 +2407,20 @@ module SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY
   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>
-         ... .Map => ((!_:Int |-> V1) (!_:Int |-> V2) (!_:Int |-> default(T[]))
-                      (!_:Int |-> (ListItem(V1) ListItem(V2)))
-                     )
+         S => S ListItem(V1)
+                ListItem(V2)
+                ListItem(default(T[]))
+                ListItem(ListItem(V1) ListItem(V2))
        </store>
     requires V1 <uMInt V2 andBool V1 =/=MInt 0p160 [priority(40)]
 
   rule <k> uniswapV2LibrarySortTokens:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), .TypedVals ) => v(ListItem(V2) ListItem(V1), T[]) ...</k>
        <summarize> true </summarize>
        <store>
-         ... .Map => ((!_:Int |-> V1) (!_:Int |-> V2) (!_:Int |-> default(T[]))
-                      (!_:Int |-> (ListItem(V2) ListItem(V1)))
-                     )
+         S => S ListItem(V1)
+                ListItem(V2)
+                ListItem(default(T[]))
+                ListItem(ListItem(V2) ListItem(V1))
        </store>
     requires V2 <uMInt V1 andBool V2 =/=MInt 0p160 [priority(40)]