From b0fe354e46c66f82dcfb86d3e3cae804cd6f2658 Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Mon, 23 Sep 2024 12:33:40 -0300
Subject: [PATCH] Summary for `uniswapV2LibraryGetAmountOut` and
 `uniswapV2LibraryGetAmountIn` (#35)

* Summary for `uniswapV2LibraryGetAmountOut`

* Summary for `uniswapV2LibraryGetAmountIn`
---
 src/uniswap-summaries.md | 50 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
index d066d1f..83c4651 100644
--- a/src/uniswap-summaries.md
+++ b/src/uniswap-summaries.md
@@ -2679,6 +2679,53 @@ endmodule
 ```
 
 ```k
+module SOLIDITY-UNISWAP-GETAMOUNTOUT-SUMMARY
+  imports SOLIDITY-CONFIGURATION
+  imports SOLIDITY-UNISWAP-TOKENS
+  
+  rule <k> uniswapV2LibraryGetAmountOut:Id ( v(V1:MInt{256}, uint256 #as T), v(V2:MInt{256}, T), v(V3:MInt{256}, T), .TypedVals ) => v((V1 *MInt 997p256  *MInt V3) /uMInt (V2 *MInt 1000p256 +MInt V1 *MInt 997p256), T) ...</k>
+       <summarize> true </summarize>
+       <store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
+                      ListItem((V1 *MInt 997p256  *MInt V3) /uMInt (V2 *MInt 1000p256 +MInt V1 *MInt 997p256) ) // amountOut
+                      ListItem( V1 *MInt 997p256)                                                               // amountInWithFee
+                      ListItem( V1 *MInt 997p256  *MInt V3)                                                     // numerator
+                      ListItem( V2 *MInt 1000p256 +MInt V1  *MInt 997p256)                                      // denominator
+       </store>
+    requires V1 >uMInt 0p256 andBool V2 >uMInt 0p256 andBool V3 >uMInt 0p256 [priority(40)]
+
+endmodule
+```
+
+```k
+module SOLIDITY-UNISWAP-GETAMOUNTIN-SUMMARY
+  imports SOLIDITY-CONFIGURATION
+  imports SOLIDITY-UNISWAP-TOKENS
+
+  rule <k> uniswapV2LibraryGetAmountIn:Id ( v(V1:MInt{256}, uint256 #as T), v(V2:MInt{256}, T), v(V3:MInt{256}, T), .TypedVals ) => v(((V2 *MInt V1 *MInt 1000p256) /uMInt ((V3 -MInt V1) *MInt 997p256)) +MInt 1p256, T) ...</k>
+       <summarize> true </summarize>
+       <store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
+                      ListItem(((V2 *MInt V1 *MInt 1000p256) /uMInt ((V3 -MInt V1) *MInt 997p256)) +MInt 1p256) // amountIn
+                      ListItem(V2 *MInt V1 *MInt 1000p256)                                                      // numerator
+                      ListItem((V3 -MInt V1) *MInt 997p256)                                                     // denominator
+       </store>
+    requires V1 >uMInt 0p256 andBool V2 >uMInt 0p256 andBool V3 >uMInt 0p256
+     andBool ((V3 -MInt V1) *MInt 997p256) =/=MInt 0p256 [priority(40)]
+
+
+    rule <k> uniswapV2LibraryGetAmountIn:Id ( v(V1:MInt{256}, uint256 #as T), v(V2:MInt{256}, T), v(V3:MInt{256}, T), .TypedVals ) => v(1p256, T) ...</k>
+       <summarize> true </summarize>
+       <store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
+                      ListItem(1p256)                        // amountIn
+                      ListItem(V2 *MInt V1 *MInt 1000p256)   // numerator
+                      ListItem((V3 -MInt V1) *MInt 997p256)  // denominator
+       </store>
+    requires V1 >uMInt 0p256 andBool V2 >uMInt 0p256 andBool V3 >uMInt 0p256
+     andBool ((V3 -MInt V1) *MInt 997p256) ==MInt 0p256 [priority(40)]
+
+endmodule
+```
+
+```k  
 module SOLIDITY-UNISWAP-PAIRFOR-SUMMARY
   imports SOLIDITY-CONFIGURATION
   imports SOLIDITY-EXPRESSION
@@ -2731,6 +2778,9 @@ endmodule
 module SOLIDITY-UNISWAP-SUMMARIES
   imports SOLIDITY-UNISWAP-INIT-SUMMARY
   imports SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY
+  imports SOLIDITY-UNISWAP-GETAMOUNTOUT-SUMMARY
+  imports SOLIDITY-UNISWAP-GETAMOUNTIN-SUMMARY
   imports SOLIDITY-UNISWAP-PAIRFOR-SUMMARY
+
 endmodule
 ```