[Certora] liquidate maxRepaid restores health - #1083
Open
claude[bot] wants to merge 11 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".
|
|
||
| uint256 seizedOut; | ||
| uint256 repaidOut; | ||
| seizedOut, repaidOut = liquidate(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data); |
There was a problem hiding this comment.
When badDebt > 0, liquidate first reduces _position.debt at lines 665–680, so maxRepaidFor—which uses the original debt—does not reproduce the cap calculated at line 699 and may exceed the remaining debt. The plain liquidate call then silently prunes branches that revert from the RCF check or debt underflow, so the rule does not show that repaying the claimed cap is possible in these states. The added badDebtFor helper is never declared or used; require it to be zero before computing the cap, or use @withrevert and assert the relevant call succeeds.
AGENTS.md reference: AGENTS.md:L20-L22
Useful? React with 👍 / 👎.
Collaborator
There was a problem hiding this comment.
@claude open a PR on top to fix that. it might be hard.
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
2 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.