Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Summary for the body of setUp #44

Merged
merged 2 commits into from
Sep 26, 2024
Merged

Summary for the body of setUp #44

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ce71037
Summary for the body of setUp.
mariaKt Sep 25, 2024
10886ad
Merge branch 'main' into setUp-summary
mariaKt Sep 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
101 changes: 101 additions & 0 deletions src/uniswap-summaries.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3020,6 +3020,106 @@ module SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY
<contract-storage> 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))) ] </contract-storage>
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 <k> 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 ...</k>
<summarize> true </summarize>
<this> THIS </this>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<live-contracts>
...
<live-contract>
<contract-address> THIS </contract-address>
<contract-type> TYPE </contract-type>
<contract-storage>
S => S [ vidWeth <- ADDR ] [ vidDai <- ADDR +MInt 1p160 ] [ vidUsdc <- ADDR +MInt 2p160 ] [ vidUni <- ADDR +MInt 3p160 ]
</contract-storage>
...
</live-contract>
(.Bag => <live-contract>
<contract-address> ADDR </contract-address>
<contract-type> wETHMock </contract-type>
<contract-storage>
constUINT256MAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256
</contract-storage>
...
</live-contract>
<live-contract>
<contract-address> ADDR +MInt 1p160 </contract-address>
<contract-type> dAIMock </contract-type>
<contract-storage>
constUINTMAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256
</contract-storage>
</live-contract>
<live-contract>
<contract-address> ADDR +MInt 2p160 </contract-address>
<contract-type> uSDCMock </contract-type>
<contract-storage>
constUINT256MAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256
</contract-storage>
</live-contract>
<live-contract>
<contract-address> ADDR +MInt 3p160 </contract-address>
<contract-type> uniswapV2Swap </contract-type>
<contract-storage>
dai |-> ADDR +MInt 1p160
router |-> ADDR +MInt 4p160
usdc |-> ADDR +MInt 2p160
weth |-> ADDR
</contract-storage>
</live-contract>
<live-contract>
<contract-address> ADDR +MInt 4p160 </contract-address>
<contract-type> uniswapV2Router02 </contract-type>
<contract-storage>
localPairs |-> ( ADDR |-> ( (ADDR +MInt 1p160 |-> ADDR +MInt 5p160)
(ADDR +MInt 2p160 |-> ADDR +MInt 6p160) )
(ADDR +MInt 1p160 |-> ( ADDR +MInt 2p160 |-> ADDR +MInt 7p160 )) )
</contract-storage>
</live-contract>
<live-contract>
<contract-address> ADDR +MInt 5p160 </contract-address>
<contract-type> uniswapV2Pair </contract-type>
<contract-storage>
constMINIMUMLIQUIDITY |-> 1000p256
constUINT112MAX |-> 5192296858534827628530496329220095p256
token0 |-> ADDR
token1 |-> ADDR +MInt 1p160
</contract-storage>
</live-contract>
<live-contract>
<contract-address> ADDR +MInt 6p160 </contract-address>
<contract-type> uniswapV2Pair </contract-type>
<contract-storage>
constMINIMUMLIQUIDITY |-> 1000p256
constUINT112MAX |-> 5192296858534827628530496329220095p256
token0 |-> ADDR
token1 |-> ADDR +MInt 2p160
</contract-storage>
</live-contract>
<live-contract>
<contract-address> ADDR +MInt 7p160 </contract-address>
<contract-type> uniswapV2Pair </contract-type>
<contract-storage>
constMINIMUMLIQUIDITY |-> 1000p256
constUINT112MAX |-> 5192296858534827628530496329220095p256
token0 |-> ADDR +MInt 1p160
token1 |-> ADDR +MInt 2p160
</contract-storage>
</live-contract>)
...
</live-contracts>
<next-address> ADDR => ADDR +MInt 8p160 </next-address>
<current-function> setUp </current-function> [priority(40)]

endmodule
```
Expand All @@ -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
```