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

[Certora] Accrue interest interactions #59

Merged
merged 6 commits into from
Dec 17, 2024
Merged

[Certora] Accrue interest interactions #59

Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9f976d5
feat: prove that there are no unauthorized accrue interest interactio…
QGarchery Dec 17, 2024
aac7689
refactor: simplify munging
QGarchery Dec 17, 2024
e5d9741
fix: couple of changed paths
QGarchery Dec 17, 2024
3a4f42c
fix: erc20 helper target munged
QGarchery Dec 17, 2024
0482572
fix: increase Range timeout
QGarchery Dec 17, 2024
a35a993
Merge pull request #60 from morpho-org/certora/simplify-munging
QGarchery Dec 17, 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
13 changes: 13 additions & 0 deletions certora/specs/MarketInteractions.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ 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 _.accrueInterest(MetaMorphoHarness.MarketParams marketParams) external => summaryAccrueInterest(marketParams) expect void ALL;
function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;

function lastIndexWithdraw() external returns(uint256) envfree;
Expand Down Expand Up @@ -52,6 +53,18 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
return (_, _);
}

function summaryAccrueInterest(MetaMorphoHarness.MarketParams marketParams) {
MetaMorphoHarness.Id id = Util.libId(marketParams);
uint256 index = lastIndexWithdraw();
requireInvariant inWithdrawQueueIsEnabled(index);
requireInvariant supplyCapIsEnabled(id);

// Check that all markets from which MetaMorpho accrues interest are enabled markets.
assert config_(id).enabled;

// View summary, which is sound because all non view functions in Morpho Blue are abstracted away.
}

// Check assertions in the summaries.
rule checkSummary(method f, env e, calldataarg args) {
f(e, args);
Expand Down
Loading