From eb2acdc40fe8a11efd5e714ed58924f519b8da67 Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Tue, 8 Oct 2024 14:38:27 -0300
Subject: [PATCH] Introducing `approve` summary from `bind` to `return` on
 `dAIMock` (#56)

* Introducing `approve` summary from `bind` to `return` on `dAIMock`

* Deleting temporary symbol

* Fixing approve rule

* Matching contract-state
---
 src/uniswap-summaries.md | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
index bd737c8..619d975 100644
--- a/src/uniswap-summaries.md
+++ b/src/uniswap-summaries.md
@@ -3493,7 +3493,7 @@ module SOLIDITY-UNISWAP-MINT-SUMMARY
                       ListItem(V2) // wad
         </store> 
         <env>
-          ENV => ENV [ usr <- var(size(S)      , address) ]
+          ENV => ENV [ usr <- var(size(S)       , address) ]
                      [ wad <- var(size(S) +Int 1, uint256) ]
         </env>
         <contract-storage> Storage => Storage [ totalSupply <- {Storage[totalSupply] orDefault 0p256}:>MInt{256} +MInt V2:MInt{256} ]
@@ -3502,6 +3502,39 @@ module SOLIDITY-UNISWAP-MINT-SUMMARY
 endmodule
 ```
 
+```k
+module SOLIDITY-UNISWAP-APPROVE-SUMMARY
+  imports SOLIDITY-CONFIGURATION
+  imports SOLIDITY-EXPRESSION
+  imports SOLIDITY-UNISWAP-TOKENS
+
+  rule <k> bind ( _STORE,
+                  ListItem ( usr ) ListItem ( wad ),
+                  ListItem ( address ) ListItem ( uint256 ) ,
+                  v ( V1:MInt{160} , address ),
+                  v ( V2:MInt{256} , uint256 ),
+                  .TypedVals , ListItem ( bool ) , ListItem ( noId ) ) ~> allowance [ msg . sender ] [ usr ] = wad ;  emit approvalEvent ( msg . sender , usr , wad , .TypedVals ) ;  return true ;  .Statements ~> return void ; ~> .K => return v ( true , bool ) ;  ~> .Statements ~> return void ; ... </k>
+       <summarize> true </summarize>
+        <this> THIS </this>
+        <contract-address> THIS </contract-address>
+        <this-type> TYPE </this-type>
+        <contract-id> TYPE </contract-id>
+        <current-function> approve </current-function>
+        <contract-state>  (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) </contract-state>
+        <store> S => S ListItem(V1) // usr
+                       ListItem(V2) // wad
+        </store>
+        <env>
+          ENV => ENV [ usr <- var(size(S)       , address) ]
+                     [ wad <- var(size(S) +Int 1, uint256) ]
+        </env>
+        <msg-sender> SENDER </msg-sender>
+        <contract-storage>
+          Storage => Storage [ allowance <- write( { Storage [ allowance ] orDefault .Map}:>Value, ListItem(SENDER), write(read({Storage [ allowance ] orDefault .Map}:>Value, ListItem(SENDER), (mapping ( address daiownr => mapping ( address daispdr => uint256)))), ListItem(V1), V2:MInt{256}, (mapping ( address spender => uint256 ))),(mapping ( address daiownr => mapping ( address daispdr => uint256))))]
+        </contract-storage> [priority(40)]
+endmodule
+```
+
 ```k
 module SOLIDITY-UNISWAP-SUMMARIES
   imports SOLIDITY-UNISWAP-INIT-SUMMARY
@@ -3519,6 +3552,7 @@ module SOLIDITY-UNISWAP-SUMMARIES
   imports SOLIDITY-UNISWAP-SETUP-SUMMARY
   imports SOLIDITY-MATHSQRT-SUMMARY
   imports SOLIDITY-UNISWAP-MINT-SUMMARY
+  imports SOLIDITY-UNISWAP-APPROVE-SUMMARY
 
 endmodule
 ```