Summaries for SortTokens function (for non reverting cases).

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>

src/uniswap-summaries.md

@@ -2648,3 +2648,39 @@ 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>
+         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>
+         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)]
+
+endmodule
+```
+
+```k
+module SOLIDITY-UNISWAP-SUMMARIES
+  imports SOLIDITY-UNISWAP-INIT-SUMMARY
+  imports SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY
+endmodule
+```