diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index bd6e40b..350e009 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -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 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 + true + THIS + THIS + TYPE + TYPE + mint + S => S ListItem(V1) // usr + ListItem(V2) // wad + + + 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} ] + [ 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))) ] + [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 ```