Introducing mint summary from bind on dAIMock

Pi-Squared-Inc · Oct 4, 2024 · 5f2ba62 · 5f2ba62
1 parent b5d68d8
commit 5f2ba62
Showing 1 changed file with 34 additions and 2 deletions.
diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
@@ -3312,12 +3312,12 @@ endmodule
 ```
 
 ```k
-module SOLIDITY-UNISWAP-GETRESERVES-SUMMARY 
+module SOLIDITY-UNISWAP-GETRESERVES-SUMMARY
   imports SOLIDITY-CONFIGURATION
   imports SOLIDITY-EXPRESSION
   imports SOLIDITY-UNISWAP-TOKENS
 
-  rule <k> bind ( _STORE , .List , .List , .TypedVals , ListItem ( uint112 []:TypeName ) , ListItem ( reserves ) ) ~> reserves = new uint112 [ ] ( 3 , .TypedVals ) ;  reserves [ 0 ] = reserve0 ;  reserves [ 1 ] = reserve1 ;  reserves [ 2 ] = blockTimestampLast ;  .Statements ~> return reserves ; ~> .K => return v ( ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) ListItem({Storage[reserve1] orDefault 0p112}:>MInt{112}) ListItem(roundMInt({Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}):MInt{112}) , uint112 [ ] ) ; ~> .K</k> 
+  rule <k> bind ( _STORE , .List , .List , .TypedVals , ListItem ( uint112 []:TypeName ) , ListItem ( reserves ) ) ~> reserves = new uint112 [ ] ( 3 , .TypedVals ) ;  reserves [ 0 ] = reserve0 ;  reserves [ 1 ] = reserve1 ;  reserves [ 2 ] = blockTimestampLast ;  .Statements ~> return reserves ; ~> .K => return v ( ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) ListItem({Storage[reserve1] orDefault 0p112}:>MInt{112}) ListItem(roundMInt({Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}):MInt{112}) , uint112 [ ] ) ; ~> .K</k>
         <summarize> true </summarize>
         <this> THIS </this>
         <contract-address> THIS </contract-address>
@@ -3408,6 +3408,37 @@ module SOLIDITY-MATHSQRT-SUMMARY
 endmodule
 ```
 
+```k
+module SOLIDITY-UNISWAP-MINT-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 , .List , .List ) ~> balanceOf [ usr ] = balanceOf [ usr ] + wad ;  totalSupply = totalSupply + wad ;  emit transferEvent ( address ( 0 , .TypedVals ) , usr , wad , .TypedVals ) ;  .Statements ~> return void ; ~> .K => return void ; ~> .K </k>
+        <summarize> true </summarize>
+        <this> THIS </this>
+        <contract-address> THIS </contract-address>
+        <this-type> TYPE </this-type>
+        <contract-id> TYPE </contract-id>
+        <current-function> mint </current-function>
+        <store> S => S ListItem(V1) // usr
+                      ListItem(V2) // wad
+        </store> 
+        <env>
+          ENV => ENV [ usr <- var(size(S) +Int 0, address) ]
+                    [ wad <- var(size(S) +Int 1, uint256) ]
+        </env>
+        <contract-storage> Storage => Storage [ totalSupply <- {Storage[totalSupply] orDefault 0p256}:>MInt{256} +MInt V2:MInt{256} ]
+                                              [ balanceOf   <- write({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), ({read({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} +MInt V2:MInt{256}), (mapping ( address account => uint256))) ]
+        </contract-storage> [priority(40)]
+endmodule
+```
+
 ```k
 module SOLIDITY-UNISWAP-SUMMARIES
   imports SOLIDITY-UNISWAP-INIT-SUMMARY
@@ -3423,6 +3454,7 @@ module SOLIDITY-UNISWAP-SUMMARIES
   imports SOLIDITY-UNISWAP-GETRESERVES-SUMMARY
   imports SOLIDITY-UNISWAP-SETUP-SUMMARY
   imports SOLIDITY-MATHSQRT-SUMMARY
+  imports SOLIDITY-UNISWAP-MINT-SUMMARY
 
 endmodule
 ```