From 0d5b0287d22845012f417c0638df8cd5e5a1865e Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Thu, 26 Sep 2024 13:56:27 -0500 Subject: [PATCH] Summary for the body of setUp. (#44) --- src/uniswap-summaries.md | 101 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 101 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 25bad17..5dc5e5c 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3020,6 +3020,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 ``` @@ -3034,6 +3134,7 @@ module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-FIDSWAP-SUMMARY imports SOLIDITY-UNISWAP-FIDUPDATE-4-SUMMARY imports SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY + imports SOLIDITY-UNISWAP-SETUP-SUMMARY endmodule ```