-
Notifications
You must be signed in to change notification settings - Fork 34
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #410 from morpho-org/certora/check-supply-withdraw…
…-markets [Certora] Market interactions
- Loading branch information
Showing
14 changed files
with
171 additions
and
64 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| { | ||
| "files": [ | ||
| "certora/helpers/MetaMorphoHarness.sol", | ||
| "certora/helpers/Util.sol", | ||
| ], | ||
| "solc": "solc-0.8.21", | ||
| "parametric_contracts": [ | ||
| "MetaMorphoHarness", | ||
| ], | ||
| "verify": "MetaMorphoHarness:certora/specs/MarketInteractions.spec", | ||
| "loop_iter": "2", | ||
| "optimistic_loop": true, | ||
| "prover_args": [ | ||
| "-depth 3", | ||
| "-mediumTimeout 20", | ||
| "-timeout 120", | ||
| ], | ||
| "server": "production", | ||
| "msg": "MetaMorpho Market Interactions" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,60 @@ | ||
| // SPDX-License-Identifier: GPL-2.0-or-later | ||
| import "ConsistentState.spec"; | ||
|
|
||
| methods { | ||
| function _.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summarySupply(marketParams, assets, shares, onBehalf, data) expect (uint256, uint256) ALL; | ||
| function _.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver) expect (uint256, uint256) ALL; | ||
| function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL; | ||
|
|
||
| function lastIndexWithdraw() external returns(uint256) envfree; | ||
| } | ||
|
|
||
| function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams { | ||
| MetaMorphoHarness.MarketParams marketParams; | ||
|
|
||
| // Safe require because: | ||
| // - markets in the supply/withdraw queue have positive lastUpdate (see LastUpdated.spec) | ||
| // - lastUpdate(id) > 0 => marketParams.id() == id is a verified invariant in Morpho Blue. | ||
| require Util.libId(marketParams) == id; | ||
|
|
||
| return marketParams; | ||
| } | ||
|
|
||
| function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) { | ||
| assert shares == 0; | ||
| assert assets != 0; | ||
| assert onBehalf == currentContract; | ||
| assert data.length == 0; | ||
|
|
||
| MetaMorphoHarness.Id id = Util.libId(marketParams); | ||
| // Safe require because it is a verified invariant | ||
| require hasSupplyCapIsEnabled(id); | ||
|
|
||
| // Check that all markets on which MetaMorpho supplies are enabled markets. | ||
| assert config_(id).enabled; | ||
|
|
||
| // NONDET summary, which is sound because all non view functions in Morpho Blue are abstracted away. | ||
| return (_, _); | ||
| } | ||
|
|
||
| function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) { | ||
| assert shares == 0 <=> assets != 0; | ||
| assert onBehalf == currentContract; | ||
| assert receiver == currentContract; | ||
|
|
||
| MetaMorphoHarness.Id id = Util.libId(marketParams); | ||
| uint256 index = lastIndexWithdraw(); | ||
| // Safe require because it is a verified invariant. | ||
| require isInWithdrawQueueIsEnabled(index); | ||
|
|
||
| // Check that all markets from which MetaMorpho withdraws are enabled markets. | ||
| assert config_(id).enabled; | ||
|
|
||
| // NONDET summary, which is sound because all non view functions in Morpho Blue are abstracted away. | ||
| return (_, _); | ||
| } | ||
|
|
||
| // Check assertions in the summaries. | ||
| // This requires to turn off sanity checks for this invariant that appears vacuous. | ||
| invariant checkSummaries() | ||
| true; |
Oops, something went wrong.