From ce710372de68f70bd2ec0e434a011e0d5abe5b64 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 25 Sep 2024 01:02:59 -0500 Subject: [PATCH] Summary for the body of setUp. --- src/uniswap-summaries.md | 103 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 102 insertions(+), 1 deletion(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 8bf8e8f..7aacd27 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2886,6 +2886,106 @@ module SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY Storage => Storage [ vidBalances <- write({write({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} -MInt V3:MInt{256}), (mapping ( address account => uint256)))}:>Value, ListItem(V2), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V2), (mapping ( address account => uint256 )))}:>MInt{256} +MInt V3:MInt{256}), (mapping ( address account => uint256))) ] requires V1 =/=MInt 0p160 andBool V2 =/=MInt 0p160 andBool {read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} >=uMInt V3:MInt{256} [priority(40)] +endmodule +``` + +```k +module SOLIDITY-UNISWAP-SETUP-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-UNISWAP-TOKENS + imports SOLIDITY-EXPRESSION + imports SOLIDITY-STATEMENT + + rule bind ( .List , .List , .List , .TypedVals , .List , .List ) ~> vidWeth = new wETHMock ( .TypedVals ) ; vidDai = new dAIMock ( .TypedVals ) ; vidUsdc = new uSDCMock ( .TypedVals ) ; vidUni = new uniswapV2Swap ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; .Statements => .K ... + true + THIS + TYPE + TYPE + + ... + + THIS + TYPE + + S => S [ vidWeth <- ADDR ] [ vidDai <- ADDR +MInt 1p160 ] [ vidUsdc <- ADDR +MInt 2p160 ] [ vidUni <- ADDR +MInt 3p160 ] + + ... + + (.Bag => + ADDR + wETHMock + + constUINT256MAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256 + + ... + + + ADDR +MInt 1p160 + dAIMock + + constUINTMAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256 + + + + ADDR +MInt 2p160 + uSDCMock + + constUINT256MAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256 + + + + ADDR +MInt 3p160 + uniswapV2Swap + + dai |-> ADDR +MInt 1p160 + router |-> ADDR +MInt 4p160 + usdc |-> ADDR +MInt 2p160 + weth |-> ADDR + + + + ADDR +MInt 4p160 + uniswapV2Router02 + + localPairs |-> ( ADDR |-> ( (ADDR +MInt 1p160 |-> ADDR +MInt 5p160) + (ADDR +MInt 2p160 |-> ADDR +MInt 6p160) ) + (ADDR +MInt 1p160 |-> ( ADDR +MInt 2p160 |-> ADDR +MInt 7p160 )) ) + + + + ADDR +MInt 5p160 + uniswapV2Pair + + constMINIMUMLIQUIDITY |-> 1000p256 + constUINT112MAX |-> 5192296858534827628530496329220095p256 + token0 |-> ADDR + token1 |-> ADDR +MInt 1p160 + + + + ADDR +MInt 6p160 + uniswapV2Pair + + constMINIMUMLIQUIDITY |-> 1000p256 + constUINT112MAX |-> 5192296858534827628530496329220095p256 + token0 |-> ADDR + token1 |-> ADDR +MInt 2p160 + + + + ADDR +MInt 7p160 + uniswapV2Pair + + constMINIMUMLIQUIDITY |-> 1000p256 + constUINT112MAX |-> 5192296858534827628530496329220095p256 + token0 |-> ADDR +MInt 1p160 + token1 |-> ADDR +MInt 2p160 + + ) + ... + + ADDR => ADDR +MInt 8p160 + setUp [priority(40)] endmodule ``` @@ -2899,6 +2999,7 @@ module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-PAIRFOR-SUMMARY imports SOLIDITY-UNISWAP-FIDUPDATE-4-SUMMARY imports SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY + imports SOLIDITY-UNISWAP-SETUP-SUMMARY endmodule -``` \ No newline at end of file +```