[Certora] liquidate maxRepaid restores health - #1083
Merged
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
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".
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
Also added the axioms the spec needs to MulDiv and MulDivAxioms.
QGarchery
approved these changes
Aug 31, 2026
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: Jochen Hoenicke <hoenicke@gmail.com>
claude Bot
pushed a commit
that referenced
this pull request
Aug 31, 2026
Restack onto the new head of claude/certora-max-repaid-healthy (ad0e410 -> 1dbe743), which applies QGarchery's review suggestion: a descriptive comment above each axiom in the L1-L4 proof chain, with the require labels collapsed from "axiom L1".."axiom L4" to a plain "axiom". The merge is clean. Kept jhoenicke's comment block verbatim; our hoisting of the lltv / lif / price declarations to the top of liquidateAtCapRestoresHealth (needed by the no-bad-debt and RCF-active hypotheses) sits above it and does not duplicate his text. Also added the three blank lines certoraCVLFormatter requires before those new comments. ad0e410 was format-clean and 1dbe743 is not, so this applies the canonical form of jhoenicke's own text rather than diverging from it. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: af632555c1
ℹ️ 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".
claude Bot
pushed a commit
that referenced
this pull request
Aug 31, 2026
Restacks #1122 on jhoenicke's new head af63255, whose only change since 1dbe743 is the cur -> old variable rename in liquidateAtCapRestoresHealth. Conflict resolution, de-duplicating in favour of his version: - L1-L4 axiom block: his oldCollatValue / oldContrib naming, keeping the blank lines before L2, L3 and L4 that certoraCVLFormatter requires (af63255 is still not formatter-clean on its own). - maxDebtBefore: his oldContrib naming, without re-introducing the top-level otherCollatValue / otherContrib declarations - this branch already computes otherContrib once in the collateral-length-aware block, so his copies would redeclare it and reference block-scoped variables. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
jhoenicke
reviewed
Aug 31, 2026
jhoenicke
left a comment
jhoenicke
left a comment
Collaborator
There was a problem hiding this comment.
Main change requested is to require the axioms themselves instead of what follows from the axioms and the code. Especially the latter is error prone. The solver should figure out what the code does and can then use the axioms to prove the property, especially when mulDivDown is abstracted.
bhargavbh
pushed a commit
that referenced
this pull request
Aug 31, 2026
…; keep concrete instances (NIA blowup fix per #1083)
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. |
Collaborator
|
@claude fix the CI |
Restore the Rocq proof of the maxRepaidHealthy bound, deleted in b5281c1 ("clean"). Content is byte-identical to the version on main. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
Apply the `forge fmt --check` diff reported by CI (forge 1.8.1) to certora/helpers/MidnightWrapper.sol: split the chained mulDivDown call onto its own line. Apply certoraCVLFormatter to certora/specs/MaxRepaidHealthy.spec: add the blank lines it wants before the L2/L3/L4 axiom comments. Both changes are whitespace-only; every spec is now zero-diff against certoraCVLFormatter. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
MathisGD
approved these changes
Sep 1, 2026
Collaborator
|
@claude update the certora readme |
claude Bot
pushed a commit
that referenced
this pull request
Sep 1, 2026
…id-healthy-baddebt-guard Restack the bad-debt guard onto #1083's new head (ee0e9a5), which brings in Mathis's clean merge of main (db75b6e), the restored rocq/maxRepaidHealthy.v (b67df3c), and the whitespace-only formatting fix (ee0e9a5). The formatting fix and our earlier restack had added the same blank lines before the // L2: / // L3: / // L4: axiom comments in certora/specs/MaxRepaidHealthy.spec, so git took a single copy of each; there is exactly one blank line before each comment and no duplicated comment text. Their split of the chained mulDivDown call in certora/helpers/MidnightWrapper.sol is preserved. The bad-debt guard is intact: the no-bad-debt require in both liquidateAtCapRestoresHealth and liquidateAtCapDoesNotRevert, the badDebtFor declaration and wrapper implementation, and the UtilsLib.min(maxRepaid, debt) cap on maxRepaidFor. Every file in certora/specs/ is zero-diff against certoraCVLFormatter. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
Add the README entry for MaxRepaidHealthy.spec: liquidating an unhealthy position at the recovery close factor cap restores health, the restoration counterpart to Healthiness.spec's preservation property. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
claude Bot
pushed a commit
that referenced
this pull request
Sep 1, 2026
The README entry for MaxRepaidHealthy.spec described the spec as it stands on #1083. This branch relaxes the pinned market size axiom to `globalMarketCollateralLength <= 2` and adds the liveness rule `liquidateAtCapDoesNotRevert`, so the entry now records that the liquidation at the cap actually succeeds, and that the rules cover single-collateral markets too. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
MathisGD
reviewed
Sep 1, 2026
Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
MathisGD
approved these changes
Sep 1, 2026
claude Bot
pushed a commit
that referenced
this pull request
Sep 1, 2026
#1083 merged, so this branch retargets main. The README entry for MaxRepaidHealthy.spec was rewritten upstream and merged; that version stands, so the conflict is resolved to main's and our README delta is dropped. Only the spec and the wrapper remain ours. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
There was a problem hiding this comment.
💡 Codex Review
Line 41 in 2c86395
Describe repayment at the cap rather than below it
The rule sets repaidUnits to exactly maxRepaidFor(...); it does not establish that every smaller amount also restores health. Because “repaying up to it” conventionally includes any repayment below the cap—and such a repayment can leave part of the health gap—change this to “repaying it” or “repaying at the cap.”
AGENTS.md reference: AGENTS.md:L72-L76
midnight/certora/specs/MaxRepaidHealthy.spec
Line 130 in 2c86395
Remove the unsupported health-boundary claim
At the health boundary originalDebt == maxDebt, normal-mode liquidate fails its originalDebt > maxDebt check in src/Midnight.sol:659-663. Because line 149 uses a plain CVL call, that reverting execution is pruned, so the rule has no health-boundary trace and only covers strictly unhealthy positions; narrow this comment accordingly.
AGENTS.md reference: AGENTS.md:L18-L22
ℹ️ 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".
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
6 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.