[Certora] post-price-drop realizable bad debt cannot increase (liquidate) - #1084
Conversation
…ate) Add a rule proving that liquidating ahead of an oracle price drop cannot worsen the post-drop realizable bad debt: with liquidate executed at the call-time price p and realizable bad debt measured at a dropped price p' <= p, the post-liquidate p'-rbd R' is at most the do-nothing p'-rbd R. - Add realizableBadDebtAtPrice getter in MidnightWrapper.sol: a verbatim structural copy of realizableBadDebt that values each active collateral at an explicitly passed price instead of reading IOracle(...).price(), decoupling the measurement price from the price liquidate reads. - Add PostDropRealizableBadDebt.spec + conf: two rules (split along liquidate's exclusive-input branch), reusing the seize-value bound and double sub-additivity lemmas and adding getter-form price monotonicity (g is non-decreasing in the price argument) to bridge the p'-measured coverage drop to the p-priced seize/repay logic. Restricted to !postMaturityMode and a single seized collateral, matching the isolated liquidate leg it builds on. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GL2969EWAXpsqmnFCNFxHR
…ound Split the post-drop realizable-bad-debt liquidate leg so the verified seize-input rule (postDropRbdLiquidateNonIncreaseSeizeInput) runs green in its own conf, and isolate the heavy repaid-input rule in a new PostDropRealizableBadDebtRepaid.conf for iteration. Add mulDivSeizeValueAtDroppedPriceBounded to MulDiv.spec: the up-up value at a dropped price pDrop <= price of the down-down seized collateral is still <= the repaid units r (mulDivSeizeValueBounded composed with price monotonicity). Mirror it as the ghost-form axiomSeizeValueAtDroppedPrice and use a single ground instance in the repaid-input rule to collapse the former call-time-bound + price-bridge chain into one step, leaving fewer unification steps for the solver. Seize-input rule left untouched.
- Only one rule handling both liquidate cases. - Use axioms proved in MulDiv
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Claude Code Review
This repository is configured for manual code reviews. Comment @claude review for a one-time review, or @claude review always to subscribe this PR to a review on every future push.
Tip: disable this comment in your organization's Code Review settings.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: eab9d09d7e
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
…DropRealizableBadDebt
Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e37b053f8c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| function _.transfer(address, uint256) external => HAVOC_ECF; | ||
| function _.transferFrom(address, address, uint256) external => HAVOC_ECF; | ||
| function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => HAVOC_ECF; |
There was a problem hiding this comment.
When callback is nonzero and authorized to act for the borrower, Midnight.liquidate invokes it after changing the position (src/Midnight.sol:737-754), so it can reenter and alter collateral or debt before this rule measures badDebt2b; these HAVOC_ECF summaries model only a non-reentrant callee footprint and therefore omit such legal executions while the README states the property without that qualification. Either scope and document the rule with callback == 0 or use a summary that accounts for reentrant Midnight state changes.
AGENTS.md reference: AGENTS.md:L45-L50
Useful? React with 👍 / 👎.
5 participants
Requested by Mathis GD · Slack thread
Before / After
Before: there is no Certora statement that liquidating a position ahead of an oracle price drop cannot make the post-drop bad debt worse. The existing liquidate leg only reasons at a single, static price.
After: a rule proving
R' <= Rforliquidate, where the realizable bad debt is measured at a dropped measurement pricep' <= pwhileliquidateitself executes at the pre-drop call-time pricep.Ris the do-nothing post-drop rbd (measured before liquidating) andR'is the post-liquidate post-drop rbd. In words: having liquidated first never leaves more realizable bad debt at the dropped price than doing nothing.How
realizableBadDebtAtPriceincertora/helpers/MidnightWrapper.sol): a verbatim structural copy of therealizableBadDebtgetter that values each active collateral at an explicitly passedpriceinstead of readingIOracle(...).price(). This decouples the measurement pricep'from the priceliquidatereads._.price()pinned top: the per-callee constant price summary is the call-time pricepliquidate reads; the measurement pricep'is a separate rule variable, constrainedp' <= pon the liquidated collateral's oracle.!postMaturityMode(solif == maxLif), and a split along liquidate's exclusive-input branch (repaidUnits == 0 || seizedAssets == 0), one CI leg rule per branch.p'-measured coverage drop is bounded byg_{p'}(seized)(reuses [Certora] realizable bad debt cannot increase without price update #1079's getter-form double sub-additivity), then price-monotonicity of the getter term givesg_{p'}(seized) <= g_p(seized), and [Certora] realizable bad debt cannot increase without price update #1079's seize-value bound closesg_p(seized) <= repaidUnits. So coverage removed atp'is at most the debt removed, andzeroFloorSubmonotonicity yieldsR' <= R. The one new ingredient over [Certora] realizable bad debt cannot increase without price update #1079 is getter-form price-monotonicity (composed from the already-provenmulDivMonotoneA/mulDivMonotoneBinMulDiv.spec).Builds on #1079 (base branch
claude/certora-realizable-bad-debt), inheriting its rbd getter and MulDiv lemmas.corresponding thread