[Certora] Guard liquidateAtCapRestoresHealth against bad-debt vacuity - #1122
Open
claude[bot] wants to merge 21 commits into
Open
[Certora] Guard liquidateAtCapRestoresHealth against bad-debt vacuity#1122claude[bot] wants to merge 21 commits into
claude[bot] wants to merge 21 commits into
Conversation
Add `require badDebtFor(...) == 0` (and the envfree methods declaration) so the rule is non-vacuous in bad-debt states, where liquidate reduces _position.debt before the RCF cap at Midnight.sol:699 and maxRepaidFor would otherwise diverge from the on-chain cap, silently pruning the executions that reach the health assertion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
MathisGD
reviewed
Aug 4, 2026
Make the liquidate call @withrevert and assert !lastReverted, so the rule proves the liquidation at the RCF cap SUCCEEDS (not only that non-reverting runs stay healthy), per review on #1122. Keeps the badDebtFor == 0 guard. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
To prove `assert !lastReverted` at the RCF cap, restore the theorem's regime hypotheses and liquidate's own require guards that 6488be7 had dropped (relying on silent pruning): market created, no liquidator gate, no callback, borrower not liquidation-locked, strictly unhealthy, lltv < WAD with positive RCF denominator, positive price, maxRepaid < debt, both collaterals activated (bitmap maxDebt == array maxDebt, two-collateral scope kept), seized <= collateral, and no withdrawable overflow. The liquidatorGate == 0 / callback == 0 preconditions skip canLiquidate / onLiquidate entirely; token transfers are non-reverting no-ops. These are faithful preconditions, not a weakening of the conclusion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
The !lastReverted assert failed because the mulDivDown/Up summaries reverted on a nondeterministic `overflow` flag: under @withrevert the solver just sets it true on any of liquidate's mulDiv calls. No repo rule asserts !lastReverted for liquidate for this reason (Healthiness.spec only asserts lastReverted, on the locked-borrower path). Tie the summaries' revert to the real, checked overflow condition (a*b, resp. a*b+(d-1), exceeding 256 bits, or d == 0), then assume the concrete no-overflow / positive-denominator facts at liquidate's maxDebt, badDebt, seize and RCF mulDiv sites (the contract's documented LIVENESS no-overflow regime). Faithful preconditions; the conclusion is unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
The !lastReverted counterexample reverted at liquidate's entry on the compiler's non-payable callvalue check (env msg.value was unconstrained), not on any mulDiv/overflow path. Pin msg.value == 0 (Midnight is not payable), as LossFactor.spec does for its liquidate@withrevert rule. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
MathisGD
reviewed
Aug 5, 2026
Per review: maxRepaidFor now returns min(maxRepaid, debt) — a liquidator can never repay more than the outstanding debt — so the returned cap is <= debt by construction. The rule's `require repaidUnits < debtBefore` (needed only to avoid the Midnight.sol:714 debt underflow) is therefore unnecessary and removed. The clamped case repaid == debt drives newDebt to 0 (trivially healthy); the maxRepaid < debt case keeps the drop-bound proof. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
MathisGD
reviewed
Aug 5, 2026
MathisGD
reviewed
Aug 5, 2026
Per review: the rule should also hold for a single-collateral market
(the original Rocq otherCollatContribution = 0 case). Relax the
collateral-count pin to length in {1,2}; the other-collateral maxDebt
term and its no-overflow bounds are now gated on length == 2 (0 when
absent), and the bitmap pin activates exactly [0, length). Two-collateral
behaviour is unchanged.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
The forall `summaryGetBit(bitmap,bit) <=> bit < collateralLength` pin was
not instantiated by the solver at the loop's concrete bits, leaving
summaryGetBit unconstrained: it picked a garbage bitmap (0xf, countBits 6),
liquidate's loop diverged from badDebtFor, badDebt_internal > 0 and the
bad-debt block reverted (regressing the 2-collat case). Restore ground-fact
pinning (summaryGetBit(bitmap,0) [&& (,1)] + constant-bounded clear-forall),
conditionalized for collateralLength in {1,2}.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
MathisGD
reviewed
Aug 5, 2026
Per review ("split the rule in two ... it will be clearer"):
- liquidateAtCapRestoresHealth: shared setup + inline drop-bound derivation,
PLAIN liquidate call, assert isHealthyNoBitmap. Carries only the
restoration hypotheses (badDebtFor==0, strictly unhealthy, lltv<WAD +
positive denominator, price>0, the 1/2-collat bitmap pin, maxDebt
aggregation); the plain call keeps only non-reverting executions.
- liquidateAtCapDoesNotRevert (mirrors LossFactor's naming): shared setup +
the non-revert preconditions (deterministic-overflow bounds, msg.value==0,
gate/callback/lock guards, seized<=collateral, withdrawable no-overflow),
liquidate@withrevert, assert !lastReverted.
Each rule is self-contained and carries only the preconditions it needs.
maxRepaidFor clamp, badDebtFor==0, deterministic overflow model and the
1/2-collat generalization are unchanged. line-197 seized<=collateral stays
in the liveness rule pending Mathis.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
Merge the base branch, whose thumbed-up review cleanups moved comments and inlined the two single-use mulDiv axiom definitions, and keep this PR's semantics on top: - Re-add badDebtFor to MidnightWrapper: the base PR dropped it as unused there, but the liveness rule and the bad-debt guard of both rules need it. - Keep the badDebtFor == 0 guard and the maxRepaidFor debt clamp. - Keep the collateral-length axiom at <= 2, since the rules here cover both a single- and a two-collateral market. - Extend the base PR's comment cleanup (no fragile Midnight.sol:NNN references) to the rules that only exist here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
…t guard The base branch resolved its conflict with main by keeping both main's bitmap-based realizableBadDebt and its own maxRepaidFor. This branch keeps badDebtFor on top, which the two rules here need; the three helpers are distinct and each has a user. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
Fixes the Codex P1 on the L3 require. The L-requires were phrased over local uint256 mulDiv ghosts and justified by uint256-typed MulDiv.spec rules. Two of those rules (mulDivAddDownUp, mulDivAddDownDownTight) open with `require_uint256(a1 + a2)`, which prunes the case where the sum exceeds 256 bits, so L3 was not backed by any proved rule in exactly that regime: its antecedent is unbounded CVL arithmetic and holds vacuously when newCollatValue + maxSeizedValue > max_uint256. Adopt the MulDivAxioms.spec style used by Healthiness.spec on main: the shared mathint ghosts, and every L-require a ground instance of an axiom proved in MulDiv.spec. The axioms are stated over mathint, so no intermediate sum or product is assumed to fit in 256 bits, which closes the gap structurally for L1-L4 at once rather than per require. L3 becomes mathMulDivMonotoneA plus mathMulDivAddDownUp, both cast-free, so the direct bounded-increase lemma is not needed and stays deleted. No bounded-sum precondition was added and no reachable state was narrowed. Add the two mathint axioms L4 and the final bound needed, with their proofs in MulDiv.spec: mathMulDivDownUpComposition and mathMulDivCeilLeOfMulGe. Also restack on the base branch and drop the contract-line reference from maxRepaidFor's comment. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
Records the base merge properly: the previous commit carried the resolved content but lost the merge parent, which left the PR conflicting and so suppressed its checks. Also fixes a comment that justified the NONDET transfer summaries with "the liquidatorGate == 0 and callback == 0 preconditions". Only liquidateAtCapDoesNotRevert has those; liquidateAtCapRestoresHealth has neither, so the comment claimed a soundness question was settled when it was not. State what is actually true instead. Comment only: no summary and no precondition changed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B
The base branch landed the same alignment with MulDivAxioms.spec that this branch had done independently, so the overlap is resolved in favour of the base branch everywhere the two express the same thing: - MulDiv.spec and MulDivAxioms.spec: taken verbatim from the base. Both sides added mathMulDivDownUpComposition and mathMulDivCeilLeOfMulGe with identical statements, so this branch now carries no change to either file. - MaxRepaidHealthy.spec summaryMulDivDown / summaryMulDivUp: the base formulation (a * b >= 2 ^ 256) is kept over the equivalent to_mathint spelling. - MaxRepaidHealthy.spec L1-L4 and the final health bound: the base mathint formulation is kept, including its terse "axiom Ln" labels, and the intermediates stay mathint rather than require_uint256, so no intermediate is assumed to fit in 256 bits. The lltv / lif / price reads are only hoisted above the liquidate call, where this branch's regime preconditions need them. What remains specific to this branch is the bad-debt guard, the maxRepaidFor debt clamp and the badDebtFor wrapper helper that supports it, plus the liveness rule and the market-shape generalization that come with them: - require badDebtFor(...) == 0 in both rules, with badDebtFor added to the wrapper and declared envfree. - the UtilsLib.min(maxRepaid, debt) clamp at the end of maxRepaidFor. - rule liquidateAtCapDoesNotRevert, and the NONDET transfer summaries and collateralBitmap / liquidationLocked accessors it needs. - globalMarketCollateralLength <= 2 instead of == 2, so a single-collateral market is covered too, with the collateral bitmap pinned to match. - otherContrib becomes a mathint computed in the market-size branch, which also drops the require_uint256 the previous version applied to it. certoraCVLFormatter reports no diff on the three specs. 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
The merge resolution re-wrapped the "This rule checks that using `repaidUnits == maxRepaid` ..." comment onto two lines. QGarchery explicitly asked for the single-line form on the base PR, and the base branch carries it that way, so restore it verbatim rather than have this stacked PR undo the request. Comment only. certoraCVLFormatter reports no diff. 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
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>
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>
…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
…y' into claude/max-repaid-healthy-baddebt-guard
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>
#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>
MathisGD
marked this pull request as ready for review
September 1, 2026 09:30
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. |
![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: 22306e1bac
ℹ️ 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".
|
|
||
| // No bad debt is realized, so liquidate does not reduce the position debt before computing the RCF cap, and | ||
| // maxRepaidFor reproduces that cap from the same debt (Rocq assumes no bad debt). | ||
| require badDebtFor(globalMarket, globalId, borrower) == 0, "no bad debt realized"; |
There was a problem hiding this comment.
This assumption materially narrows the property, but certora/README.md:40-41 still claims that the spec covers an unhealthy borrower generally and that repaying maxRepaid restores health. The description should disclose that positions with realizable bad debt are excluded, along with the rule's other RCF and market-size restrictions, so readers do not overestimate the formal coverage.
AGENTS.md reference: AGENTS.md:L72-L75
Useful? React with 👍 / 👎.
| // The seized collateral does not exceed the position collateral, so liquidate's collateral subtraction | ||
| // does not underflow. Left as an explicit hypothesis pending review; implied by no bad debt + the | ||
| // maxRepaidFor debt clamp. | ||
| require collatBefore >= ghostMulDivDown(ghostMulDivDown(repaidUnits, lif, WAD()), ORACLE_PRICE_SCALE(), price), "seized <= collateral"; |
There was a problem hiding this comment.
In a two-collateral position, zero bad debt only says the aggregate collateral can cover the debt; it does not ensure the selected collateral can cover the seizure. For example, the borrower can have a tiny amount at collateralIndex and enough value in the other collateral to satisfy badDebtFor == 0, while the cap-derived seizure exceeds the selected amount and liquidate reverts at its collateral subtraction. This require removes exactly those counterexamples, so the new no-revert rule does not establish its stated regime; either prove the bound from stronger valid hypotheses or explicitly scope the property to sufficiently funded selected collateral.
AGENTS.md reference: AGENTS.md:L10-L11
Useful? React with 👍 / 👎.
Comment on lines
+53
to
+54
| function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; | ||
| function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; |
There was a problem hiding this comment.
When the loan or collateral token rejects a transfer—for example because the liquidator lacks balance or allowance—the real liquidate call reverts in safeTransfer or safeTransferFrom, but these non-reverting summaries prevent liquidate@withrevert from exploring that branch. This is acceptable for the restoration rule's successful-path assertion, but it makes the new universal no-revert assertion unsound unless token-transfer success is explicitly part of the rule's stated and modeled preconditions.
AGENTS.md reference: AGENTS.md:L45-L50
Useful? React with 👍 / 👎.
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
Follow-on to #1083 on the
MaxRepaidHealthyspec.liquidateAtCapRestoresHealthnow runs underbadDebtFor(...) == 0, so it no longer covers states wheremaxRepaidFordiverges from the on-chain cap.liquidateAtCapDoesNotRevert: the liquidation at that cap actually succeeds.maxRepaidForis clamped to the debt.The liveness rule still assumes
seized <= collateralrather than proving it, flagged in place.