From f6278d30c7c9ab8357bb94b528a174ca216cf2d2 Mon Sep 17 00:00:00 2001
From: Maria Kotsifakou <kotsifakou.maria@gmail.com>
Date: Mon, 16 Sep 2024 16:43:28 -0500
Subject: [PATCH 1/2] Summaries for SortTokens function (for non reverting
 cases).

---
 src/solidity.md          |  2 +-
 src/uniswap-summaries.md | 34 ++++++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/src/solidity.md b/src/solidity.md
index 3b55f6b..82ad844 100644
--- a/src/solidity.md
+++ b/src/solidity.md
@@ -181,7 +181,7 @@ module SOLIDITY
   imports SOLIDITY-TRANSACTION
   imports SOLIDITY-EXPRESSION
   imports SOLIDITY-STATEMENT
-  imports SOLIDITY-UNISWAP-INIT-SUMMARY
+  imports SOLIDITY-UNISWAP-SUMMARIES
 
   rule <k> _:PragmaDefinition Ss:SourceUnits => Ss ...</k>
        <summarize> false </summarize>
diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
index e6e11eb..26e1122 100644
--- a/src/uniswap-summaries.md
+++ b/src/uniswap-summaries.md
@@ -2397,3 +2397,37 @@ module SOLIDITY-UNISWAP-INIT-SUMMARY
 
 endmodule
 ```
+
+```k
+module SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY
+  imports SOLIDITY-CONFIGURATION
+  imports SOLIDITY-EXPRESSION
+  imports SOLIDITY-UNISWAP-TOKENS
+
+  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)))
+                     )
+       </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)))
+                     )
+       </store>
+    requires V2 <uMInt V1 andBool V2 =/=MInt 0p160 [priority(40)]
+
+endmodule
+```
+
+```k
+module SOLIDITY-UNISWAP-SUMMARIES
+  imports SOLIDITY-UNISWAP-INIT-SUMMARY
+  imports SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY
+endmodule
+```

From e3295cb646814ab7373587a6207a63a4be920180 Mon Sep 17 00:00:00 2001
From: Maria Kotsifakou <kotsifakou.maria@gmail.com>
Date: Wed, 18 Sep 2024 17:16:53 -0500
Subject: [PATCH 2/2] Updated summary with store cell being a list

---
 src/uniswap-summaries.md | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
index 26e1122..5c3854c 100644
--- 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)]