[Certora] liquidate maxRepaid restores health - #1083
Open
claude[bot] wants to merge 15 commits into
Open
Conversation
Add MaxRepaidHealthy.spec proving the on-contract version of the Rocq theorem max_repaid_liquidation_leaves_healthy: in the RCF-active regime (!postMaturityMode && lltv < WAD), liquidating an unhealthy single-collateral position at the RCF cap repaid = maxRepaid (src/Midnight.sol:699) restores health. This is the restoration direction, complementing the preservation direction in Healthiness.spec. - MidnightWrapper.sol: add bitmap-free views maxRepaidFor (recomputes the L699 cap) and badDebtFor (recomputes the L643-655 badDebt). - MulDiv.spec: add mulDivCeilLeOfMulGe lemma (Rocq ceil_div_le_of_mul_ge). - MaxRepaidHealthy.spec/.conf: new rule + Healthiness-style mulDiv/price/ toId/global-market machinery and nonlinear NIA conf. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
The initial rule timed out (~2h) because it asked the SMT to rediscover a multi-step nonlinear chain under two unbounded `forall mathint` quantifiers. Delegate the single hard nonlinear step to axiomMaxDebtDrop (the Rocq lemma max_debt_contribution_drop_bound, machine-checked over the integers), drop the `forall` quantifiers, and leave only linear glue plus two cheap axioms proven in MulDiv.spec (mulDivUpRoundsUp, mulDivCeilLeOfMulGe). The on-contract goal is now essentially linear, so the prover no longer has to search the chain. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
Add standalone MaxDebtDropBound.spec proving the Rocq lemma max_debt_contribution_drop_bound (maxDebt drop <= ceil(maxRepaid*lif*lltv/WAD^2)) over concrete mulDivDown/mulDivUp (not summarized). If this leg verifies, the axiomMaxDebtDrop assumed in MaxRepaidHealthy.spec is fully Certora-discharged. Isolated in its own spec + hard-NIA conf so a possible ~2h timeout on this hardest Rocq lemma cannot gate the fast MulDiv leg. MaxRepaidHealthy.spec is unchanged and stays green either way. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
The lemma spec failed remotely ("Could not find job results", 3 min, no
artifacts) because `WAD() * WAD()` was passed as the uint256 denominator of
mulDivUp; a product of two uint256 is a mathint in CVL and must be cast. CI
skips the local CVL check, so it only surfaced on the remote run.
Hoist `lif * lltv` and `WAD * WAD` into require_uint256 locals. The lemma
statement is unchanged (no math weakening); this only makes it compile so it
can get a real green/timeout verdict.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
claude Bot
pushed a commit
that referenced
this pull request
Jul 27, 2026
…; keep concrete instances (NIA blowup fix per #1083)
… composition The monolithic single-assert version (5 nested divisions in one NIA query) timed out at 2h. Mirror the Rocq proof max_debt_contribution_drop_bound (rocq/maxRepaidHealthy.v:162) decomposition: prove each nested-mulDiv fact as its own small concrete rule (<=2 nested divisions), then assemble them in a composition rule over uninterpreted (ghost) mulDiv with only linear/NIA glue, using the assume-ghost / prove-concrete split from PR #1079. The final bound is unchanged: drop <= ceil(maxRepaid*lif*lltv/WAD^2). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
Move the two nonlinear steps of the ghost composition (multiply a hypothesis by lltv; cancel the WAD factor) into pure-arithmetic helper lemmas (lemmaMulMono, lemmaCancelPos, no mulDiv), so the composition rule's SMT goal is purely linear + modus ponens over uninterpreted mulDiv. The final bound is unchanged: drop <= ceil(maxRepaid*lif*lltv/WAD^2). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
…d rule Fold the LLTV-weighted maxDebt-drop bound derivation directly into liquidateAtCapRestoresHealth, so a single rule proves health-restoration end-to-end. The bare axiomMaxDebtDrop assumption is gone: the drop bound (Rocq max_debt_contribution_drop_bound) is now derived inline from primitive mulDiv rounding facts (each proven over concrete mulDiv in MulDiv.spec, applied at the specific ground instances) plus two isolated pure-arithmetic moves and linear glue -- no nested-division goal, no forall in the rule body, no hypothesis-times-variable or variable cancellation inside a nonlinear goal. Remove the now-redundant MaxDebtDropBound.spec / .conf (its composition is inlined; its sub-lemmas already live in MulDiv.spec). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
MathisGD
changed the title
MathisGD
marked this pull request as ready for review
August 4, 2026 12:22
![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: 6488be74bb
ℹ️ 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".
bhargavbh
reviewed
Aug 10, 2026
bhargavbh
left a comment
bhargavbh
left a comment
Contributor
There was a problem hiding this comment.
Finally! this rule was evasive for a long time.
QGarchery
reviewed
Aug 27, 2026
Comment on lines
+136
to
+137
| // maxRepaidFor reproduces the RCF cap at Midnight.sol:699. Passing that value to liquidate satisfies the | ||
| // first disjunct of the RCF check at Midnight.sol:700-705, independently of the dust waiver. |
Collaborator
There was a problem hiding this comment.
We usually don't reference contract lines, this is too fragile as it can change if comments are added/removed. There 2 more occurrences below
Collaborator
There was a problem hiding this comment.
Suggested change
| // maxRepaidFor reproduces the RCF cap at Midnight.sol:699. Passing that value to liquidate satisfies the | |
| // first disjunct of the RCF check at Midnight.sol:700-705, independently of the dust waiver. | |
| // This rule checks that using `repaidUnits == maxRepaid` is enough to put the account healthy. This means that the RCF doesn't prevent to put the position back to health. |
| uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower); | ||
|
|
||
| // maxRepaidFor's non-reverting collateral lookup establishes collateralIndex < 2. | ||
| uint256 otherIndex = assert_uint256(1 - collateralIndex); |
Collaborator
There was a problem hiding this comment.
(optional) hardcode collateralIndex at 0 and otherIndex at 1 since the order shouldn't matter
Comment on lines
+172
to
+175
| require price > 0 => ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()) <= maxSeizedValue, "L1: mulDivInverseUpDown with a=maxSeizedValue, b=ORACLE_PRICE_SCALE, d=price (MulDiv.spec)"; | ||
| require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()), "L2: mulDivAddDownUp with a1=collatAfter, a2=seizedOut, b=price, d=ORACLE_PRICE_SCALE (MulDiv.spec)"; | ||
| require curCollatValue <= newCollatValue + maxSeizedValue => curContrib <= newContrib + ghostMulDivUp(maxSeizedValue, lltv, WAD()), "L3: mulDivDownBoundedIncrease with a1=curCollatValue, a2=newCollatValue, delta=maxSeizedValue, b=lltv, d=WAD (MulDiv.spec)"; | ||
| require ghostMulDivUp(maxSeizedValue, lltv, WAD()) <= maxDebtDropBound, "L4: mulDivDownUpComposition with a=repaidUnits, b=lif, c=lltv, d=WAD (MulDiv.spec)"; |
Collaborator
There was a problem hiding this comment.
We should align with the new way use mulDiv axioms (see Healthiness.spec on main for example). This would make it much easier to see that we are not introducing bad assumptions
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
Review cleanups from @QGarchery's review that @MathisGD approved: - Remove the unused badDebtFor helper from MidnightWrapper (it is only needed by the liveness rule of the stacked PR, which re-adds it there). - Document why the tickToPrice / toId / storeInCode summaries are sound, and why the mulDiv ghost summaries add no assumption. - Document why exactly two collaterals is general: liquidating touches a single collateral, so the second one realizes the arbitrary otherCollatContribution of the Rocq proof. Moved the market size from a require in the rule into the ghost axiom. - Inline the two single-use axiomUpRoundsUp / axiomCeilLeOfMulGe definitions. - Drop mulDivDownBoundedIncrease from MulDiv.spec: it follows from mulDivMonotoneA and mulDivAddDownUp, which the L3 justification now cites directly. - Drop the MaxRepaidHealthy back-reference comment on mulDivCeilLeOfMulGe and the remaining fragile Midnight.sol:NNN line references. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 616c217dc9
ℹ️ 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".
|
|
||
| require price > 0 => ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()) <= maxSeizedValue, "L1: mulDivInverseUpDown with a=maxSeizedValue, b=ORACLE_PRICE_SCALE, d=price (MulDiv.spec)"; | ||
| require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()), "L2: mulDivAddDownUp with a1=collatAfter, a2=seizedOut, b=price, d=ORACLE_PRICE_SCALE (MulDiv.spec)"; | ||
| require curCollatValue <= newCollatValue + maxSeizedValue => curContrib <= newContrib + ghostMulDivUp(maxSeizedValue, lltv, WAD()), "L3: mulDivMonotoneA then mulDivAddDownUp with a1=newCollatValue, a2=maxSeizedValue, b=lltv, d=WAD (MulDiv.spec)"; |
There was a problem hiding this comment.
When newCollatValue + maxSeizedValue > type(uint256).max, this L3 assumption is not established by the cited rules: mulDivAddDownUp first applies require_uint256(a1 + a2), so that case is pruned, while the addition in this implication is unbounded CVL arithmetic. Requiring L3 directly can therefore exclude arbitrary ghost valuations and let the health assertion pass without a corresponding MulDiv.spec proof; restore a direct bounded-increase rule without the cast, or prove the sum fits here.
AGENTS.md reference: AGENTS.md:L53-L56
Useful? React with 👍 / 👎.
Resolve certora/helpers/MidnightWrapper.sol by keeping both helpers: main's bitmap-based realizableBadDebt (used by RealizableBadDebt.spec and RealizableBadDebtLiquidate.spec) and this branch's array-based maxRepaidFor (used by MaxRepaidHealthy.spec). badDebtFor stays removed, as requested in review; the stacked PR that needs it defines it there. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3c7d2b5dbc
ℹ️ 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".
Same thumbed-up review point as the spec cleanup: contract line numbers are fragile, so name the mechanism instead. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Requested by Mathis GD · Slack thread
Proves in Certora, directly on
liquidate, that a liquidator repaying the RCF cap restores an unhealthy position to health — so the maxRepaid/RCF cap can't lock a position out of recovery. Removes the RocqmaxRepaidHealthy.v, now subsumed by the on-contract rule.