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
- ENV => ENV [ usr <- var(size(S) , address) ]
+ ENV => ENV [ usr <- var(size(S) , address) ]
[ wad <- var(size(S) +Int 1, uint256) ]
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 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 ; ...
+ true
+ THIS
+ THIS
+ TYPE
+ TYPE
+ approve
+ (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) ))
+ S => S ListItem(V1) // usr
+ ListItem(V2) // wad
+
+
+ ENV => ENV [ usr <- var(size(S) , address) ]
+ [ wad <- var(size(S) +Int 1, uint256) ]
+
+ SENDER
+
+ 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))))]
+ [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
```