From a43821ddfd2c6c7e3f2b10835737d34966a600cd Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 4 Aug 2026 15:56:52 +0000
Subject: [PATCH 01/12] [Certora] Guard liquidateAtCapRestoresHealth against
 bad-debt vacuity

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
---
 certora/specs/MaxRepaidHealthy.spec | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index 270678cc8..1626b717d 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -10,6 +10,7 @@ methods {
     function debt(bytes32 id, address user) external returns (uint128) envfree;
     function isHealthyNoBitmap(Midnight.Market, bytes32, address) external returns (bool) envfree;
     function maxRepaidFor(Midnight.Market, bytes32, uint256, address) external returns (uint256) envfree;
+    function badDebtFor(Midnight.Market, bytes32, address) external returns (uint256) envfree;
 
     // Assumption: price does not change during the rule (same value in maxRepaidFor, in liquidate and in the
     // post-state isHealthyNoBitmap). Deterministic per oracle address, as in Healthiness.spec.
@@ -130,6 +131,10 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
 
     require globalMarketCollateralLength == 2, "two-collateral market";
 
+    // No bad debt is realized, so liquidate does not reduce _position.debt before the RCF cap at
+    // Midnight.sol:699 and maxRepaidFor reproduces that cap from the same debt (Rocq assumes no bad debt).
+    require badDebtFor(globalMarket, globalId, borrower) == 0, "no bad debt realized";
+
     uint256 collatBefore = collateral(globalId, borrower, collateralIndex);
     uint256 debtBefore = debt(globalId, borrower);
 

From 9be13e872e299e68f10e2befb97acd7211e364ab Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 4 Aug 2026 16:03:29 +0000
Subject: [PATCH 02/12] [Certora] Prove liquidateAtCapRestoresHealth is
 revert-free

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
---
 certora/specs/MaxRepaidHealthy.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index 1626b717d..a20b0965a 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -150,7 +150,10 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
 
     uint256 seizedOut;
     uint256 repaidOut;
-    seizedOut, repaidOut = liquidate(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data);
+    seizedOut, repaidOut = liquidate@withrevert(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data);
+
+    // Liquidating at the RCF cap succeeds: repaidUnits == maxRepaid satisfies the RCF require (Midnight.sol:700-705).
+    assert !lastReverted;
 
     uint256 collatAfter = assert_uint256(collatBefore - seizedOut);
 

From 0255092e19287e8c0d45604eb97b631662b35609 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 4 Aug 2026 16:11:37 +0000
Subject: [PATCH 03/12] [Certora] Add liquidate's non-revert preconditions for
 revert-freedom

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
---
 certora/specs/MaxRepaidHealthy.spec | 41 ++++++++++++++++++++++++++---
 1 file changed, 37 insertions(+), 4 deletions(-)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index a20b0965a..f4e8d2aa6 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -7,10 +7,12 @@ methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
     function collateral(bytes32 id, address user, uint256) external returns (uint128) envfree;
+    function collateralBitmap(bytes32 id, address user) external returns (uint128) envfree;
     function debt(bytes32 id, address user) external returns (uint128) envfree;
     function isHealthyNoBitmap(Midnight.Market, bytes32, address) external returns (bool) envfree;
     function maxRepaidFor(Midnight.Market, bytes32, uint256, address) external returns (uint256) envfree;
     function badDebtFor(Midnight.Market, bytes32, address) external returns (uint256) envfree;
+    function liquidationLocked(bytes32, address) external returns (bool) envfree;
 
     // Assumption: price does not change during the rule (same value in maxRepaidFor, in liquidate and in the
     // post-state isHealthyNoBitmap). Deterministic per oracle address, as in Healthiness.spec.
@@ -27,7 +29,13 @@ methods {
     // maxLif is deterministic for each (lltv, liquidationCursor) pair.
     function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor);
 
-    // Unresolved callbacks and token calls use AUTO/HAVOC_ECF, which models non-reentrant callees.
+    // Token transfers move external ERC20 balances only, never the borrower's position storage, so summarizing
+    // them as non-reverting no-ops is sound for this direction. The liquidator gate and callback are ruled out by
+    // the liquidatorGate == 0 and callback == 0 preconditions, so canLiquidate / onLiquidate are never called.
+    function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET;
+    function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
+    function _.transferFrom(address from, address to, uint256 amount) external => NONDET;
+    function _.transfer(address to, uint256 amount) external => NONDET;
 }
 
 /// SUMMARY ///
@@ -148,6 +156,34 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     uint256 otherLltv = globalMarketCollateralLLTV[otherIndex];
     uint256 otherPrice = summaryPrice(globalMarket.collateralParams[otherIndex].oracle);
 
+    uint256 lltv = globalMarketCollateralLLTV[collateralIndex];
+    uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]);
+    uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle);
+
+    // Regime and guards under which liquidate at the RCF cap does not revert: the Rocq theorem's hypotheses plus
+    // liquidate's own require guards. These are preconditions of the theorem, not a weakening of the conclusion.
+    require currentContract.marketState[globalId].tickSpacing != 0, "market already created (touchMarket is a no-op)";
+    require globalMarketLiquidatorGate == 0, "no liquidator gate (Midnight.sol:635)";
+    require callback == 0, "no liquidate callback";
+    require !liquidationLocked(globalId, borrower), "borrower not liquidation-locked (Midnight.sol:660)";
+    require !isHealthyNoBitmap(globalMarket, globalId, borrower), "strictly unhealthy: debt > maxDebt (Midnight.sol:661)";
+    require lltv < WAD(), "RCF is active only for lltv < WAD (Midnight.sol:695)";
+    require lif * lltv <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD^2: RCF denominator positive (Midnight.sol:698)";
+    require price > 0, "positive liquidated-collateral price";
+    require repaidUnits < debtBefore, "maxRepaid < debt case (no debt underflow at Midnight.sol:714)";
+
+    // Both collaterals are activated, so liquidate's bitmap maxDebt loop (Midnight.sol:645) sums the same two
+    // terms as the array-based maxRepaidFor / isHealthyNoBitmap; this keeps the two-collateral scope.
+    uint128 bitmap = collateralBitmap(globalId, borrower);
+    require summaryGetBit(bitmap, 0) && summaryGetBit(bitmap, 1), "both collaterals activated";
+    require forall uint256 otherBit. otherBit != 0 && otherBit != 1 => !summaryGetBit(bitmap, otherBit), "only the two collaterals activated";
+
+    // Seized collateral (Midnight.sol:692) does not exceed the position collateral (Midnight.sol:708 subtraction).
+    require collatBefore >= ghostMulDivDown(ghostMulDivDown(repaidUnits, lif, WAD()), ORACLE_PRICE_SCALE(), price), "seized <= collateral";
+
+    // No overflow of the market's withdrawable when repaid units are credited (Midnight.sol:713).
+    require currentContract.marketState[globalId].withdrawable + repaidUnits <= max_uint128, "withdrawable credit does not overflow";
+
     uint256 seizedOut;
     uint256 repaidOut;
     seizedOut, repaidOut = liquidate@withrevert(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data);
@@ -162,10 +198,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     // seizedOut = floor(floor(repaidUnits * lif / WAD) * ORACLE_PRICE_SCALE / price), matching the ghost terms
     // below. Each require is one ground instance of a rule proved in MulDiv.spec.
 
-    uint256 lltv = globalMarketCollateralLLTV[collateralIndex];
-    uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]);
     uint256 maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD());
-    uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle);
 
     // By Midnight.sol:692, seizedOut == ghostMulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price).
     uint256 curCollatValue = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE());

From 4eefdb3af028ec559a3ea663e7e57b95ff2b229a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 4 Aug 2026 16:35:26 +0000
Subject: [PATCH 04/12] [Certora] Model mulDiv overflow deterministically for
 revert-freedom

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
---
 certora/specs/MaxRepaidHealthy.spec | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index f4e8d2aa6..b2c833769 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -61,17 +61,17 @@ definition axiomUpRoundsUp(uint256 a, uint256 b, uint256 d) returns bool = d > 0
 // Proved in mulDivCeilLeOfMulGe: a * b <= bound * d => ceil(a * b / d) <= bound.
 definition axiomCeilLeOfMulGe(uint256 a, uint256 b, uint256 d, uint256 bound) returns bool = d > 0 && a * b <= bound * d => ghostMulDivUp(a, b, d) <= bound;
 
+// Deterministic overflow: the real mulDiv reverts iff d == 0 or the checked product overflows 256 bits. Modeling
+// that exact condition (rather than a nondeterministic overflow flag) is what makes revert-freedom provable.
 function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 {
-    bool overflow;
-    if (overflow || d == 0) {
+    if (d == 0 || to_mathint(a) * to_mathint(b) > max_uint256) {
         revert();
     }
     return ghostMulDivDown(a, b, d);
 }
 
 function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 {
-    bool overflow;
-    if (overflow || d == 0) {
+    if (d == 0 || to_mathint(a) * to_mathint(b) + (to_mathint(d) - 1) > max_uint256) {
         revert();
     }
     return ghostMulDivUp(a, b, d);
@@ -172,6 +172,21 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     require price > 0, "positive liquidated-collateral price";
     require repaidUnits < debtBefore, "maxRepaid < debt case (no debt underflow at Midnight.sol:714)";
 
+    // No-overflow regime (Midnight LIVENESS: liquidate can revert on overflow). Every checked product in
+    // liquidate's maxDebt / badDebt / seize / RCF computations stays within 256 bits, and every maxLif
+    // denominator is positive, so no summarized mulDiv takes its overflow / d == 0 revert branch.
+    uint256 maxLifOther = maxLifGhost(otherLltv, globalMarketCollateralLiquidationCursor[otherIndex]);
+    require lif > 0 && maxLifOther > 0, "positive maxLif per collateral (created-market invariant)";
+    require lif <= 2 * WAD(), "maxLif <= 2 * WAD (Midnight.sol:810)";
+    require collatBefore * price + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (index) fits 256 bits";
+    require otherCollatBefore * otherPrice + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (other) fits 256 bits";
+    require ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()) * lltv <= max_uint256, "maxDebt term (index) fits 256 bits";
+    require ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * otherLltv <= max_uint256, "maxDebt term (other) fits 256 bits";
+    require ghostMulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()) * WAD() + lif <= max_uint256, "badDebt term (index) fits 256 bits";
+    require ghostMulDivUp(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * WAD() + maxLifOther <= max_uint256, "badDebt term (other) fits 256 bits";
+    require repaidUnits * lif <= max_uint256, "maxSeizedValue product fits 256 bits";
+    require ghostMulDivDown(repaidUnits, lif, WAD()) * ORACLE_PRICE_SCALE() <= max_uint256, "seized value fits 256 bits";
+
     // Both collaterals are activated, so liquidate's bitmap maxDebt loop (Midnight.sol:645) sums the same two
     // terms as the array-based maxRepaidFor / isHealthyNoBitmap; this keeps the two-collateral scope.
     uint128 bitmap = collateralBitmap(globalId, borrower);

From cb871fbccfe0c1857e5a6fb22aa2aee1bb3c8eca Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 4 Aug 2026 16:51:45 +0000
Subject: [PATCH 05/12] [Certora] Require msg.value == 0 for liquidate
 revert-freedom

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
---
 certora/specs/MaxRepaidHealthy.spec | 1 +
 1 file changed, 1 insertion(+)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index b2c833769..4e473db38 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -162,6 +162,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
 
     // Regime and guards under which liquidate at the RCF cap does not revert: the Rocq theorem's hypotheses plus
     // liquidate's own require guards. These are preconditions of the theorem, not a weakening of the conclusion.
+    require e.msg.value == 0, "Midnight is not payable (liquidate is non-payable)";
     require currentContract.marketState[globalId].tickSpacing != 0, "market already created (touchMarket is a no-op)";
     require globalMarketLiquidatorGate == 0, "no liquidator gate (Midnight.sol:635)";
     require callback == 0, "no liquidate callback";

From ea34470469065f146b301ca51df3e690843e6ccd Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 5 Aug 2026 13:51:43 +0000
Subject: [PATCH 06/12] [Certora] Clamp maxRepaidFor to debt; drop the repaid <
 debt require
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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
---
 certora/helpers/MidnightWrapper.sol | 7 +++++--
 certora/specs/MaxRepaidHealthy.spec | 1 -
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol
index 85906a910..5863217d3 100644
--- a/certora/helpers/MidnightWrapper.sol
+++ b/certora/helpers/MidnightWrapper.sol
@@ -33,7 +33,9 @@ contract MidnightWrapper is Midnight {
 
     /* maxRepaidFor recomputes the RCF cap of Midnight.liquidate (see src/Midnight.sol:699) through a
      * bitmap-free, array-based code path. maxDebt is summed exactly as in isHealthyNoBitmap and the
-     * liquidate bad-debt loop, then the L699 mulDivUp is applied with lif = maxLif (normal mode).
+     * liquidate bad-debt loop, then the L699 mulDivUp is applied with lif = maxLif (normal mode). The result
+     * is clamped to the debt: a liquidator can never repay more than the outstanding debt, so the returned
+     * cap is always <= debt by construction (which is why the rule needs no separate repaid <= debt bound).
      * Expects the position to be unhealthy (debt > maxDebt) so that debt - maxDebt does not underflow. */
     function maxRepaidFor(Market memory market, bytes32 id, uint256 collateralIndex, address borrower)
         public
@@ -54,7 +56,8 @@ contract MidnightWrapper is Midnight {
         CollateralParams memory liquidatedParam = market.collateralParams[collateralIndex];
         uint256 lltv = liquidatedParam.lltv;
         uint256 lif = maxLif(lltv, liquidatedParam.liquidationCursor);
-        return (debt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lif * lltv);
+        uint256 maxRepaid = (debt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lif * lltv);
+        return UtilsLib.min(maxRepaid, debt);
     }
 
     /* badDebtFor recomputes the badDebt of Midnight.liquidate (see src/Midnight.sol:643-655) through a
diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index 4e473db38..98708c50f 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -171,7 +171,6 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     require lltv < WAD(), "RCF is active only for lltv < WAD (Midnight.sol:695)";
     require lif * lltv <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD^2: RCF denominator positive (Midnight.sol:698)";
     require price > 0, "positive liquidated-collateral price";
-    require repaidUnits < debtBefore, "maxRepaid < debt case (no debt underflow at Midnight.sol:714)";
 
     // No-overflow regime (Midnight LIVENESS: liquidate can revert on overflow). Every checked product in
     // liquidate's maxDebt / badDebt / seize / RCF computations stays within 256 bits, and every maxLif

From 8a863da8df0dfd57c1c48b574d0b82734a886ab1 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 5 Aug 2026 14:08:48 +0000
Subject: [PATCH 07/12] [Certora] Generalize liquidateAtCapRestoresHealth to 1
 or 2 collaterals

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
---
 certora/specs/MaxRepaidHealthy.spec | 42 ++++++++++++++++-------------
 1 file changed, 24 insertions(+), 18 deletions(-)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index 98708c50f..a295fda00 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -137,7 +137,7 @@ function summaryToId(Midnight.Market market) returns (bytes32) {
 rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrower, address receiver, address callback, bytes data) {
     Midnight.Market globalMarket = getGlobalMarket();
 
-    require globalMarketCollateralLength == 2, "two-collateral market";
+    require globalMarketCollateralLength == 1 || globalMarketCollateralLength == 2, "single- or two-collateral market";
 
     // No bad debt is realized, so liquidate does not reduce _position.debt before the RCF cap at
     // Midnight.sol:699 and maxRepaidFor reproduces that cap from the same debt (Rocq assumes no bad debt).
@@ -150,12 +150,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     // first disjunct of the RCF check at Midnight.sol:700-705, independently of the dust waiver.
     uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower);
 
-    // maxRepaidFor's non-reverting collateral lookup establishes collateralIndex < 2.
-    uint256 otherIndex = assert_uint256(1 - collateralIndex);
-    uint256 otherCollatBefore = collateral(globalId, borrower, otherIndex);
-    uint256 otherLltv = globalMarketCollateralLLTV[otherIndex];
-    uint256 otherPrice = summaryPrice(globalMarket.collateralParams[otherIndex].oracle);
-
+    // maxRepaidFor's non-reverting collateral lookup establishes collateralIndex < globalMarketCollateralLength.
     uint256 lltv = globalMarketCollateralLLTV[collateralIndex];
     uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]);
     uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle);
@@ -175,23 +170,36 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     // No-overflow regime (Midnight LIVENESS: liquidate can revert on overflow). Every checked product in
     // liquidate's maxDebt / badDebt / seize / RCF computations stays within 256 bits, and every maxLif
     // denominator is positive, so no summarized mulDiv takes its overflow / d == 0 revert branch.
-    uint256 maxLifOther = maxLifGhost(otherLltv, globalMarketCollateralLiquidationCursor[otherIndex]);
-    require lif > 0 && maxLifOther > 0, "positive maxLif per collateral (created-market invariant)";
+    require lif > 0, "positive maxLif for the liquidated collateral (created-market invariant)";
     require lif <= 2 * WAD(), "maxLif <= 2 * WAD (Midnight.sol:810)";
     require collatBefore * price + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (index) fits 256 bits";
-    require otherCollatBefore * otherPrice + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (other) fits 256 bits";
     require ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()) * lltv <= max_uint256, "maxDebt term (index) fits 256 bits";
-    require ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * otherLltv <= max_uint256, "maxDebt term (other) fits 256 bits";
     require ghostMulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()) * WAD() + lif <= max_uint256, "badDebt term (index) fits 256 bits";
-    require ghostMulDivUp(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * WAD() + maxLifOther <= max_uint256, "badDebt term (other) fits 256 bits";
     require repaidUnits * lif <= max_uint256, "maxSeizedValue product fits 256 bits";
     require ghostMulDivDown(repaidUnits, lif, WAD()) * ORACLE_PRICE_SCALE() <= max_uint256, "seized value fits 256 bits";
 
-    // Both collaterals are activated, so liquidate's bitmap maxDebt loop (Midnight.sol:645) sums the same two
-    // terms as the array-based maxRepaidFor / isHealthyNoBitmap; this keeps the two-collateral scope.
+    // The other collateral's contribution to maxDebt exists only in a two-collateral market (the Rocq
+    // otherCollatContribution); in a single-collateral market it is 0. Its no-overflow bounds are needed only
+    // when liquidate's loop actually visits that collateral.
+    uint256 otherContrib = 0;
+    if (globalMarketCollateralLength == 2) {
+        uint256 otherIndex = assert_uint256(1 - collateralIndex);
+        uint256 otherCollatBefore = collateral(globalId, borrower, otherIndex);
+        uint256 otherLltv = globalMarketCollateralLLTV[otherIndex];
+        uint256 otherPrice = summaryPrice(globalMarket.collateralParams[otherIndex].oracle);
+        uint256 maxLifOther = maxLifGhost(otherLltv, globalMarketCollateralLiquidationCursor[otherIndex]);
+        require maxLifOther > 0, "positive maxLif for the other collateral (created-market invariant)";
+        require otherCollatBefore * otherPrice + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (other) fits 256 bits";
+        require ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * otherLltv <= max_uint256, "maxDebt term (other) fits 256 bits";
+        require ghostMulDivUp(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * WAD() + maxLifOther <= max_uint256, "badDebt term (other) fits 256 bits";
+        otherContrib = ghostMulDivDown(ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()), otherLltv, WAD());
+    }
+
+    // Exactly the market's collaterals [0, globalMarketCollateralLength) are activated, so liquidate's bitmap
+    // maxDebt loop (Midnight.sol:645) ranges over the same indices as the array-based maxRepaidFor /
+    // isHealthyNoBitmap. Covers both the single- and two-collateral markets.
     uint128 bitmap = collateralBitmap(globalId, borrower);
-    require summaryGetBit(bitmap, 0) && summaryGetBit(bitmap, 1), "both collaterals activated";
-    require forall uint256 otherBit. otherBit != 0 && otherBit != 1 => !summaryGetBit(bitmap, otherBit), "only the two collaterals activated";
+    require forall uint256 bit. summaryGetBit(bitmap, bit) <=> bit < globalMarketCollateralLength, "exactly the market's collaterals are activated";
 
     // Seized collateral (Midnight.sol:692) does not exceed the position collateral (Midnight.sol:708 subtraction).
     require collatBefore >= ghostMulDivDown(ghostMulDivDown(repaidUnits, lif, WAD()), ORACLE_PRICE_SCALE(), price), "seized <= collateral";
@@ -237,8 +245,6 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     // repaidUnits is ceil(gap * WAD^2 / (WAD^2 - lif * lltv)). The two rounding facts below imply
     // maxDebtDropBound <= repaidUnits - gap. Therefore the new max debt falls by no more than the amount
     // repaid in excess of the old health gap.
-    uint256 otherCollatValue = ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE());
-    uint256 otherContrib = ghostMulDivDown(otherCollatValue, otherLltv, WAD());
     uint256 maxDebtBefore = require_uint256(curContrib + otherContrib);
 
     // Safe: maxRepaidFor's non-reverting subtraction establishes debtBefore >= maxDebtBefore.

From fbb3714107f3f5b028c32ad3bb29e964602bfefb Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 5 Aug 2026 14:22:23 +0000
Subject: [PATCH 08/12] [Certora] Fix bitmap pin for 1/2-collat generalization
 (ground facts)

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
---
 certora/specs/MaxRepaidHealthy.spec | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index a295fda00..802c79978 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -195,11 +195,18 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
         otherContrib = ghostMulDivDown(ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()), otherLltv, WAD());
     }
 
-    // Exactly the market's collaterals [0, globalMarketCollateralLength) are activated, so liquidate's bitmap
-    // maxDebt loop (Midnight.sol:645) ranges over the same indices as the array-based maxRepaidFor /
-    // isHealthyNoBitmap. Covers both the single- and two-collateral markets.
+    // The activated collaterals are exactly [0, globalMarketCollateralLength), so liquidate's bitmap maxDebt /
+    // badDebt loop (Midnight.sol:645) ranges over the same indices as the array-based maxRepaidFor /
+    // isHealthyNoBitmap. Pinned with ground facts per index (no ghost-bounded quantifier, which the solver would
+    // not instantiate at the loop's concrete bits) for each supported market size.
     uint128 bitmap = collateralBitmap(globalId, borrower);
-    require forall uint256 bit. summaryGetBit(bitmap, bit) <=> bit < globalMarketCollateralLength, "exactly the market's collaterals are activated";
+    require summaryGetBit(bitmap, 0), "collateral 0 is activated";
+    if (globalMarketCollateralLength == 2) {
+        require summaryGetBit(bitmap, 1), "collateral 1 is activated (two-collateral market)";
+        require forall uint256 otherBit. otherBit != 0 && otherBit != 1 => !summaryGetBit(bitmap, otherBit), "only the two collaterals are activated";
+    } else {
+        require forall uint256 otherBit. otherBit != 0 => !summaryGetBit(bitmap, otherBit), "single-collateral: only collateral 0 is activated";
+    }
 
     // Seized collateral (Midnight.sol:692) does not exceed the position collateral (Midnight.sol:708 subtraction).
     require collatBefore >= ghostMulDivDown(ghostMulDivDown(repaidUnits, lif, WAD()), ORACLE_PRICE_SCALE(), price), "seized <= collateral";

From 9e3e2ae3c3cd098e91eac05deec051560f1ac4e6 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 5 Aug 2026 16:15:07 +0000
Subject: [PATCH 09/12] [Certora] Split liquidateAtCap rule into health +
 liveness

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
---
 certora/specs/MaxRepaidHealthy.spec | 131 +++++++++++++++++++---------
 1 file changed, 92 insertions(+), 39 deletions(-)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index 802c79978..1486b7859 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -132,8 +132,10 @@ function summaryToId(Midnight.Market market) returns (bytes32) {
 
 /// RULE ///
 
-// In a two-collateral market, liquidating at the amount computed by maxRepaidFor leaves the position healthy.
-// The call uses normal mode and covers the strictly unhealthy and health-boundary cases.
+// RESTORATION. In a single- or two-collateral, RCF-active, no-bad-debt market, liquidating at the amount
+// computed by maxRepaidFor leaves the borrower healthy. The liquidate call is PLAIN (normal mode), so only
+// non-reverting executions are asserted healthy; the companion rule liquidateAtCapDoesNotRevert proves that the
+// liquidation actually succeeds. Covers the strictly-unhealthy case (the boundary is healthy already).
 rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrower, address receiver, address callback, bytes data) {
     Midnight.Market globalMarket = getGlobalMarket();
 
@@ -146,8 +148,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     uint256 collatBefore = collateral(globalId, borrower, collateralIndex);
     uint256 debtBefore = debt(globalId, borrower);
 
-    // 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.
+    // maxRepaidFor reproduces the RCF cap at Midnight.sol:699 (clamped to the debt).
     uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower);
 
     // maxRepaidFor's non-reverting collateral lookup establishes collateralIndex < globalMarketCollateralLength.
@@ -155,43 +156,22 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]);
     uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle);
 
-    // Regime and guards under which liquidate at the RCF cap does not revert: the Rocq theorem's hypotheses plus
-    // liquidate's own require guards. These are preconditions of the theorem, not a weakening of the conclusion.
-    require e.msg.value == 0, "Midnight is not payable (liquidate is non-payable)";
-    require currentContract.marketState[globalId].tickSpacing != 0, "market already created (touchMarket is a no-op)";
-    require globalMarketLiquidatorGate == 0, "no liquidator gate (Midnight.sol:635)";
-    require callback == 0, "no liquidate callback";
-    require !liquidationLocked(globalId, borrower), "borrower not liquidation-locked (Midnight.sol:660)";
+    // Restoration hypotheses (Rocq): strictly unhealthy, RCF active (lltv < WAD) with a positive L699
+    // denominator, and a positive price. No revert-clearing guards are needed here: the plain call keeps only
+    // the non-reverting executions.
     require !isHealthyNoBitmap(globalMarket, globalId, borrower), "strictly unhealthy: debt > maxDebt (Midnight.sol:661)";
     require lltv < WAD(), "RCF is active only for lltv < WAD (Midnight.sol:695)";
     require lif * lltv <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD^2: RCF denominator positive (Midnight.sol:698)";
     require price > 0, "positive liquidated-collateral price";
 
-    // No-overflow regime (Midnight LIVENESS: liquidate can revert on overflow). Every checked product in
-    // liquidate's maxDebt / badDebt / seize / RCF computations stays within 256 bits, and every maxLif
-    // denominator is positive, so no summarized mulDiv takes its overflow / d == 0 revert branch.
-    require lif > 0, "positive maxLif for the liquidated collateral (created-market invariant)";
-    require lif <= 2 * WAD(), "maxLif <= 2 * WAD (Midnight.sol:810)";
-    require collatBefore * price + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (index) fits 256 bits";
-    require ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()) * lltv <= max_uint256, "maxDebt term (index) fits 256 bits";
-    require ghostMulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()) * WAD() + lif <= max_uint256, "badDebt term (index) fits 256 bits";
-    require repaidUnits * lif <= max_uint256, "maxSeizedValue product fits 256 bits";
-    require ghostMulDivDown(repaidUnits, lif, WAD()) * ORACLE_PRICE_SCALE() <= max_uint256, "seized value fits 256 bits";
-
     // The other collateral's contribution to maxDebt exists only in a two-collateral market (the Rocq
-    // otherCollatContribution); in a single-collateral market it is 0. Its no-overflow bounds are needed only
-    // when liquidate's loop actually visits that collateral.
+    // otherCollatContribution); in a single-collateral market it is 0.
     uint256 otherContrib = 0;
     if (globalMarketCollateralLength == 2) {
         uint256 otherIndex = assert_uint256(1 - collateralIndex);
         uint256 otherCollatBefore = collateral(globalId, borrower, otherIndex);
         uint256 otherLltv = globalMarketCollateralLLTV[otherIndex];
         uint256 otherPrice = summaryPrice(globalMarket.collateralParams[otherIndex].oracle);
-        uint256 maxLifOther = maxLifGhost(otherLltv, globalMarketCollateralLiquidationCursor[otherIndex]);
-        require maxLifOther > 0, "positive maxLif for the other collateral (created-market invariant)";
-        require otherCollatBefore * otherPrice + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (other) fits 256 bits";
-        require ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * otherLltv <= max_uint256, "maxDebt term (other) fits 256 bits";
-        require ghostMulDivUp(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * WAD() + maxLifOther <= max_uint256, "badDebt term (other) fits 256 bits";
         otherContrib = ghostMulDivDown(ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()), otherLltv, WAD());
     }
 
@@ -208,18 +188,9 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
         require forall uint256 otherBit. otherBit != 0 => !summaryGetBit(bitmap, otherBit), "single-collateral: only collateral 0 is activated";
     }
 
-    // Seized collateral (Midnight.sol:692) does not exceed the position collateral (Midnight.sol:708 subtraction).
-    require collatBefore >= ghostMulDivDown(ghostMulDivDown(repaidUnits, lif, WAD()), ORACLE_PRICE_SCALE(), price), "seized <= collateral";
-
-    // No overflow of the market's withdrawable when repaid units are credited (Midnight.sol:713).
-    require currentContract.marketState[globalId].withdrawable + repaidUnits <= max_uint128, "withdrawable credit does not overflow";
-
     uint256 seizedOut;
     uint256 repaidOut;
-    seizedOut, repaidOut = liquidate@withrevert(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data);
-
-    // Liquidating at the RCF cap succeeds: repaidUnits == maxRepaid satisfies the RCF require (Midnight.sol:700-705).
-    assert !lastReverted;
+    seizedOut, repaidOut = liquidate(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data);
 
     uint256 collatAfter = assert_uint256(collatBefore - seizedOut);
 
@@ -263,3 +234,85 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
 
     assert isHealthyNoBitmap(globalMarket, globalId, borrower);
 }
+
+// LIVENESS. In the same single- or two-collateral, RCF-active, no-bad-debt regime, liquidating at maxRepaidFor
+// does not revert. Mirrors LossFactor.spec's liquidateLossFactorDoesNotRevert. This rule proves only no-revert;
+// the restoration of health is proved by liquidateAtCapRestoresHealth.
+rule liquidateAtCapDoesNotRevert(env e, uint256 collateralIndex, address borrower, address receiver, address callback, bytes data) {
+    Midnight.Market globalMarket = getGlobalMarket();
+
+    require globalMarketCollateralLength == 1 || globalMarketCollateralLength == 2, "single- or two-collateral market";
+
+    // No bad debt is realized, so the socialization block (Midnight.sol:665-680) is skipped.
+    require badDebtFor(globalMarket, globalId, borrower) == 0, "no bad debt realized";
+
+    uint256 collatBefore = collateral(globalId, borrower, collateralIndex);
+    uint256 debtBefore = debt(globalId, borrower);
+    uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower);
+
+    uint256 lltv = globalMarketCollateralLLTV[collateralIndex];
+    uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]);
+    uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle);
+
+    // liquidate's own require guards + RCF-active regime.
+    require e.msg.value == 0, "Midnight is not payable (liquidate is non-payable)";
+    require currentContract.marketState[globalId].tickSpacing != 0, "market already created (touchMarket is a no-op)";
+    require globalMarketLiquidatorGate == 0, "no liquidator gate (Midnight.sol:635)";
+    require callback == 0, "no liquidate callback";
+    require !liquidationLocked(globalId, borrower), "borrower not liquidation-locked (Midnight.sol:660)";
+    require !isHealthyNoBitmap(globalMarket, globalId, borrower), "strictly unhealthy: debt > maxDebt (Midnight.sol:661)";
+    require lltv < WAD(), "RCF is active only for lltv < WAD (Midnight.sol:695)";
+    require lif * lltv <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD^2: RCF denominator positive (Midnight.sol:698)";
+    require price > 0, "positive liquidated-collateral price";
+
+    // No-overflow regime (Midnight LIVENESS: the checked mulDiv reverts on 256-bit overflow). Every checked
+    // product in liquidate's maxDebt / badDebt / seize / RCF computations stays within 256 bits, and every
+    // maxLif denominator is positive, so no summarized mulDiv takes its overflow / d == 0 revert branch.
+    require lif > 0, "positive maxLif for the liquidated collateral (created-market invariant)";
+    require lif <= 2 * WAD(), "maxLif <= 2 * WAD (Midnight.sol:810)";
+    require collatBefore * price + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (index) fits 256 bits";
+    require ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()) * lltv <= max_uint256, "maxDebt term (index) fits 256 bits";
+    require ghostMulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()) * WAD() + lif <= max_uint256, "badDebt term (index) fits 256 bits";
+    require repaidUnits * lif <= max_uint256, "maxSeizedValue product fits 256 bits";
+    require ghostMulDivDown(repaidUnits, lif, WAD()) * ORACLE_PRICE_SCALE() <= max_uint256, "seized value fits 256 bits";
+
+    // The other collateral's no-overflow bounds are needed only when liquidate's loop visits that collateral.
+    if (globalMarketCollateralLength == 2) {
+        uint256 otherIndex = assert_uint256(1 - collateralIndex);
+        uint256 otherCollatBefore = collateral(globalId, borrower, otherIndex);
+        uint256 otherLltv = globalMarketCollateralLLTV[otherIndex];
+        uint256 otherPrice = summaryPrice(globalMarket.collateralParams[otherIndex].oracle);
+        uint256 maxLifOther = maxLifGhost(otherLltv, globalMarketCollateralLiquidationCursor[otherIndex]);
+        require maxLifOther > 0, "positive maxLif for the other collateral (created-market invariant)";
+        require otherCollatBefore * otherPrice + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (other) fits 256 bits";
+        require ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * otherLltv <= max_uint256, "maxDebt term (other) fits 256 bits";
+        require ghostMulDivUp(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * WAD() + maxLifOther <= max_uint256, "badDebt term (other) fits 256 bits";
+    }
+
+    // The activated collaterals are exactly [0, globalMarketCollateralLength): liquidate's bitmap loop
+    // (Midnight.sol:645) ranges over the same indices as maxRepaidFor / badDebtFor, and the L661 liquidatable
+    // check reads the same maxDebt. Ground-fact pin per supported market size.
+    uint128 bitmap = collateralBitmap(globalId, borrower);
+    require summaryGetBit(bitmap, 0), "collateral 0 is activated";
+    if (globalMarketCollateralLength == 2) {
+        require summaryGetBit(bitmap, 1), "collateral 1 is activated (two-collateral market)";
+        require forall uint256 otherBit. otherBit != 0 && otherBit != 1 => !summaryGetBit(bitmap, otherBit), "only the two collaterals are activated";
+    } else {
+        require forall uint256 otherBit. otherBit != 0 => !summaryGetBit(bitmap, otherBit), "single-collateral: only collateral 0 is activated";
+    }
+
+    // Seized collateral (Midnight.sol:692) does not exceed the position collateral (Midnight.sol:708
+    // subtraction). 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";
+
+    // No overflow of the market's withdrawable when repaid units are credited (Midnight.sol:713).
+    require currentContract.marketState[globalId].withdrawable + repaidUnits <= max_uint128, "withdrawable credit does not overflow";
+
+    uint256 seizedOut;
+    uint256 repaidOut;
+    seizedOut, repaidOut = liquidate@withrevert(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data);
+
+    // Liquidating at the RCF cap succeeds: repaidUnits <= maxRepaid satisfies the RCF require (Midnight.sol:700-705).
+    assert !lastReverted, "liquidating at the RCF cap does not revert";
+}

From 2433e5681ddc96e30a1d804196021b35a97f163f Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Thu, 27 Aug 2026 10:28:38 +0000
Subject: [PATCH 10/12] [Certora] Align MaxRepaidHealthy with the shared mulDiv
 axioms

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
---
 certora/helpers/MidnightWrapper.sol | 10 ++--
 certora/specs/MaxRepaidHealthy.spec | 72 ++++++++++++++++-------------
 certora/specs/MulDiv.spec           | 10 ++++
 certora/specs/MulDivAxioms.spec     |  6 +++
 4 files changed, 60 insertions(+), 38 deletions(-)

diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol
index ecc41bb74..d989ff8ce 100644
--- a/certora/helpers/MidnightWrapper.sol
+++ b/certora/helpers/MidnightWrapper.sol
@@ -31,11 +31,11 @@ contract MidnightWrapper is Midnight {
         return maxDebt >= debt;
     }
 
-    /* maxRepaidFor recomputes the RCF cap of Midnight.liquidate (see src/Midnight.sol:699) through a
-     * bitmap-free, array-based code path. maxDebt is summed exactly as in isHealthyNoBitmap and the
-     * liquidate bad-debt loop, then the L699 mulDivUp is applied with lif = maxLif (normal mode). The result
-     * is clamped to the debt: a liquidator can never repay more than the outstanding debt, so the returned
-     * cap is always <= debt by construction (which is why the rule needs no separate repaid <= debt bound).
+    /* maxRepaidFor recomputes the repay-cap-factor cap of Midnight.liquidate through a bitmap-free,
+     * array-based code path. maxDebt is summed exactly as in isHealthyNoBitmap and the liquidate bad-debt
+     * loop, then the cap's mulDivUp is applied with lif = maxLif (normal mode). The result is clamped to the
+     * debt: a liquidator can never repay more than the outstanding debt, so the returned cap is always
+     * <= debt by construction (which is why the rule needs no separate repaid <= debt bound).
      * Expects the position to be unhealthy (debt > maxDebt) so that debt - maxDebt does not underflow. */
     function maxRepaidFor(Market memory market, bytes32 id, uint256 collateralIndex, address borrower)
         public
diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index b1dcdc886..095c18073 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -2,6 +2,7 @@
 // Copyright (c) 2026 Morpho Association
 
 import "BitmapSummaries.spec";
+import "MulDivAxioms.spec";
 
 methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
@@ -32,10 +33,12 @@ methods {
     function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
     function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET;
 
-    // Summarizing mulDivDown and mulDivUp by unconstrained deterministic ghosts adds no assumption about
-    // mulDiv: the ghosts are arbitrary, and the summaries reproduce exactly the revert condition of the real
-    // mulDiv, so every real mulDiv behaviour is still allowed. All the arithmetic the rule actually needs is
-    // required explicitly below, one ground instance per rule proved over the concrete mulDiv in MulDiv.spec.
+    // Summarizing mulDivDown and mulDivUp by the shared ghosts of MulDivAxioms.spec adds no assumption
+    // about mulDiv: the ghosts are arbitrary, and the summaries reproduce exactly the revert condition of the
+    // real mulDiv, so every real mulDiv behaviour is still allowed. All the arithmetic the rules need is
+    // required explicitly below as ground instances of the axioms of MulDivAxioms.spec, each proved over the
+    // real math functions in MulDiv.spec. Those axioms are stated over mathint, so requiring them never
+    // prunes a case where an intermediate sum or product exceeds 256 bits.
     function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d);
     function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d);
 
@@ -61,24 +64,20 @@ definition WAD_SQUARED() returns uint256 = 10 ^ 36;
 
 persistent ghost summaryPrice(address) returns uint256;
 
-persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256;
-
-persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256;
-
 // Deterministic overflow: the real mulDiv reverts iff d == 0 or the checked product overflows 256 bits. Modeling
 // that exact condition (rather than a nondeterministic overflow flag) is what makes revert-freedom provable.
 function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 {
     if (d == 0 || to_mathint(a) * to_mathint(b) > max_uint256) {
         revert();
     }
-    return ghostMulDivDown(a, b, d);
+    return require_uint256(ghostMulDivDown(a, b, d));
 }
 
 function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 {
     if (d == 0 || to_mathint(a) * to_mathint(b) + (to_mathint(d) - 1) > max_uint256) {
         revert();
     }
-    return ghostMulDivUp(a, b, d);
+    return require_uint256(ghostMulDivUp(a, b, d));
 }
 
 // Pin every field that contributes to the market id, making the toId summary deterministic and injective.
@@ -182,7 +181,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
         uint256 otherCollatBefore = collateral(globalId, borrower, otherIndex);
         uint256 otherLltv = globalMarketCollateralLLTV[otherIndex];
         uint256 otherPrice = summaryPrice(globalMarket.collateralParams[otherIndex].oracle);
-        otherContrib = ghostMulDivDown(ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()), otherLltv, WAD());
+        otherContrib = require_uint256(mathMulDivDown(mathMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()), otherLltv, WAD()));
     }
 
     // The activated collaterals are exactly [0, globalMarketCollateralLength), so liquidate's bitmap maxDebt /
@@ -207,27 +206,34 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     /// MAX-DEBT DROP BOUND ///
     // Establish curContrib - newContrib <= maxDebtDropBound. When it seizes, liquidate computes
     // seizedOut = floor(floor(repaidUnits * lif / WAD) * ORACLE_PRICE_SCALE / price), matching the ghost terms
-    // below. Each require is one ground instance of a rule proved in MulDiv.spec.
+    // below. Each require is one ground instance of an axiom of MulDivAxioms.spec, proved in MulDiv.spec.
 
-    uint256 maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD());
+    uint256 maxSeizedValue = require_uint256(mathMulDivDown(repaidUnits, lif, WAD()));
 
-    // By that same computation, seizedOut == ghostMulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price).
-    uint256 curCollatValue = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE());
-    uint256 newCollatValue = ghostMulDivDown(collatAfter, price, ORACLE_PRICE_SCALE());
+    // By that same computation, seizedOut == mathMulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price).
+    uint256 curCollatValue = require_uint256(mathMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()));
+    uint256 newCollatValue = require_uint256(mathMulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()));
 
-    uint256 curContrib = ghostMulDivDown(curCollatValue, lltv, WAD());
-    uint256 newContrib = ghostMulDivDown(newCollatValue, lltv, WAD());
+    uint256 curContrib = require_uint256(mathMulDivDown(curCollatValue, lltv, WAD()));
+    uint256 newContrib = require_uint256(mathMulDivDown(newCollatValue, lltv, WAD()));
 
     uint256 lifTimesLltv = assert_uint256(lif * lltv);
-    uint256 maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED());
+    uint256 maxDebtDropBound = require_uint256(mathMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()));
+
+    // L1: what liquidate seized is worth at most maxSeizedValue.
+    require axiomMathMulDivInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "proved in mathMulDivInverseUpDown";
+
+    // L2: the collateral value falls by at most the value of the seized collateral.
+    require axiomMathMulDivAddDownUp(collatAfter, seizedOut, price, ORACLE_PRICE_SCALE()), "proved in mathMulDivAddDownUp";
 
-    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)";
-    require ghostMulDivUp(maxSeizedValue, lltv, WAD()) <= maxDebtDropBound, "L4: mulDivDownUpComposition with a=repaidUnits, b=lif, c=lltv, d=WAD (MulDiv.spec)";
+    // L3: transport that bound through the LLTV contribution. Monotonicity in the first argument plus
+    // sub-additivity give curContrib <= newContrib + ceil(maxSeizedValue * lltv / WAD). Both axioms are over
+    // mathint, so newCollatValue + maxSeizedValue is never assumed to fit in 256 bits.
+    require axiomMathMulDivDownMonotoneA(curCollatValue, newCollatValue + maxSeizedValue, lltv, WAD()), "proved in mathMulDivMonotoneA";
+    require axiomMathMulDivAddDownUp(newCollatValue, maxSeizedValue, lltv, WAD()), "proved in mathMulDivAddDownUp";
 
-    // L1-L2 bound the collateral-value decrease by maxSeizedValue. L3 transports that bound through the LLTV
-    // contribution, and L4 bounds the composed rounding by maxDebtDropBound.
+    // L4: bound the two-step rounding by the single-step maxDebtDropBound.
+    require axiomMathMulDivDownUpComposition(repaidUnits, lif, lltv, WAD()), "proved in mathMulDivDownUpComposition";
 
     /// FINAL HEALTH BOUND ///
     // repaidUnits is ceil(gap * WAD^2 / (WAD^2 - lif * lltv)). The two rounding facts below imply
@@ -238,9 +244,9 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     // Safe: maxRepaidFor's non-reverting subtraction establishes debtBefore >= maxDebtBefore.
     uint256 gap = require_uint256(debtBefore - maxDebtBefore);
     uint256 rcfDenominator = assert_uint256(WAD_SQUARED() - lifTimesLltv);
-    require rcfDenominator > 0 => gap * WAD_SQUARED() <= ghostMulDivUp(gap, WAD_SQUARED(), rcfDenominator) * rcfDenominator, "proved in mulDivUpRoundsUp";
+    require axiomMathMulDivUpRoundsUp(gap, WAD_SQUARED(), rcfDenominator), "proved in mathMulDivUpRoundsUp";
     uint256 repaidExcess = assert_uint256(repaidUnits - gap);
-    require repaidUnits * lifTimesLltv <= repaidExcess * WAD_SQUARED() => ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()) <= repaidExcess, "proved in mulDivCeilLeOfMulGe";
+    require axiomMathMulDivCeilLeOfMulGe(repaidUnits, lifTimesLltv, WAD_SQUARED(), repaidExcess), "proved in mathMulDivCeilLeOfMulGe";
 
     assert isHealthyNoBitmap(globalMarket, globalId, borrower);
 }
@@ -281,10 +287,10 @@ rule liquidateAtCapDoesNotRevert(env e, uint256 collateralIndex, address borrowe
     require lif > 0, "positive maxLif for the liquidated collateral (created-market invariant)";
     require lif <= 2 * WAD(), "maxLif <= 2 * WAD";
     require collatBefore * price + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (index) fits 256 bits";
-    require ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()) * lltv <= max_uint256, "maxDebt term (index) fits 256 bits";
-    require ghostMulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()) * WAD() + lif <= max_uint256, "badDebt term (index) fits 256 bits";
+    require mathMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()) * lltv <= max_uint256, "maxDebt term (index) fits 256 bits";
+    require mathMulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()) * WAD() + lif <= max_uint256, "badDebt term (index) fits 256 bits";
     require repaidUnits * lif <= max_uint256, "maxSeizedValue product fits 256 bits";
-    require ghostMulDivDown(repaidUnits, lif, WAD()) * ORACLE_PRICE_SCALE() <= max_uint256, "seized value fits 256 bits";
+    require mathMulDivDown(repaidUnits, lif, WAD()) * ORACLE_PRICE_SCALE() <= max_uint256, "seized value fits 256 bits";
 
     // The other collateral's no-overflow bounds are needed only when liquidate's loop visits that collateral.
     if (globalMarketCollateralLength == 2) {
@@ -295,8 +301,8 @@ rule liquidateAtCapDoesNotRevert(env e, uint256 collateralIndex, address borrowe
         uint256 maxLifOther = maxLifGhost(otherLltv, globalMarketCollateralLiquidationCursor[otherIndex]);
         require maxLifOther > 0, "positive maxLif for the other collateral (created-market invariant)";
         require otherCollatBefore * otherPrice + ORACLE_PRICE_SCALE() <= max_uint256, "collateral value (other) fits 256 bits";
-        require ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * otherLltv <= max_uint256, "maxDebt term (other) fits 256 bits";
-        require ghostMulDivUp(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * WAD() + maxLifOther <= max_uint256, "badDebt term (other) fits 256 bits";
+        require mathMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * otherLltv <= max_uint256, "maxDebt term (other) fits 256 bits";
+        require mathMulDivUp(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()) * WAD() + maxLifOther <= max_uint256, "badDebt term (other) fits 256 bits";
     }
 
     // The activated collaterals are exactly [0, globalMarketCollateralLength): liquidate's bitmap loop ranges
@@ -314,7 +320,7 @@ rule liquidateAtCapDoesNotRevert(env e, uint256 collateralIndex, address borrowe
     // 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";
+    require collatBefore >= mathMulDivDown(mathMulDivDown(repaidUnits, lif, WAD()), ORACLE_PRICE_SCALE(), price), "seized <= collateral";
 
     // No overflow of the market's withdrawable when the repaid units are credited.
     require currentContract.marketState[globalId].withdrawable + repaidUnits <= max_uint128, "withdrawable credit does not overflow";
diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec
index f2e1073eb..f884564f7 100644
--- a/certora/specs/MulDiv.spec
+++ b/certora/specs/MulDiv.spec
@@ -212,6 +212,16 @@ rule mathMulDivAddDownUp(mathint a1, mathint a2, mathint b, mathint d) {
     assert a1 >= 0 && a2 >= 0 => mathMulDivDown(a1, b, d) + mathMulDivUp(a2, b, d) >= mathMulDivDown(a1 + a2, b, d);
 }
 
+// Rounding down the first scaling step cannot increase the result of a second scaling rounded up.
+rule mathMulDivDownUpComposition(mathint a, mathint b, mathint c, mathint d) {
+    assert a >= 0 && b >= 0 && c >= 0 && d > 0 => mathMulDivUp(mathMulDivDown(a, b, d), c, d) <= mathMulDivUp(a, b * c, d * d);
+}
+
+// If the exact product is at most bound * d, then the ceiling is at most bound.
+rule mathMulDivCeilLeOfMulGe(mathint a, mathint b, mathint d, mathint bound) {
+    assert a >= 0 && b >= 0 && d > 0 && a * b <= bound * d => mathMulDivUp(a, b, d) <= bound;
+}
+
 rule mathMulDivInverseDownUp(mathint a, mathint b, mathint d) {
     assert b > 0 && d > 0 => a <= mathMulDivDown(mathMulDivUp(a, b, d), d, b);
 }
diff --git a/certora/specs/MulDivAxioms.spec b/certora/specs/MulDivAxioms.spec
index 659a29e1a..6b35d23ab 100644
--- a/certora/specs/MulDivAxioms.spec
+++ b/certora/specs/MulDivAxioms.spec
@@ -58,6 +58,12 @@ definition axiomMathMulDivAddUpUpTight(mathint a1, mathint a2, mathint b, mathin
 
 definition axiomMathMulDivAddDownUp(mathint a1, mathint a2, mathint b, mathint d) returns bool = a1 >= 0 && a2 >= 0 => mathMulDivDown(a1, b, d) + mathMulDivUp(a2, b, d) >= mathMulDivDown(a1 + a2, b, d);
 
+// Rounding down the first scaling step cannot increase the result of a second scaling rounded up.
+definition axiomMathMulDivDownUpComposition(mathint a, mathint b, mathint c, mathint d) returns bool = a >= 0 && b >= 0 && c >= 0 && d > 0 => mathMulDivUp(mathMulDivDown(a, b, d), c, d) <= mathMulDivUp(a, b * c, d * d);
+
+// If the exact product is at most bound * d, then the ceiling is at most bound.
+definition axiomMathMulDivCeilLeOfMulGe(mathint a, mathint b, mathint d, mathint bound) returns bool = a >= 0 && b >= 0 && d > 0 && a * b <= bound * d => mathMulDivUp(a, b, d) <= bound;
+
 definition axiomMathMulDivInverseDownUp(mathint a, mathint b, mathint d) returns bool = b > 0 && d > 0 => a <= mathMulDivDown(mathMulDivUp(a, b, d), d, b);
 
 definition axiomMathMulDivInverseUpDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => mathMulDivUp(mathMulDivDown(a, b, d), d, b) <= a;

From 962c2166f1e978df847a0b03ffd80d59e517cfdd Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 31 Aug 2026 16:06:26 +0000
Subject: [PATCH 11/12] [Certora] Keep the base branch's one-line rule comment

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
---
 certora/specs/MaxRepaidHealthy.spec | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec
index 438a14f40..5422c4903 100644
--- a/certora/specs/MaxRepaidHealthy.spec
+++ b/certora/specs/MaxRepaidHealthy.spec
@@ -156,8 +156,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow
     uint256 collatBefore = collateral(globalId, borrower, collateralIndex);
     uint256 debtBefore = debt(globalId, borrower);
 
-    // 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.
+    // 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 < globalMarketCollateralLength.

From ead78c44c3d2dd2614b95bc4d79f851571a6a995 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 1 Sep 2026 09:04:58 +0000
Subject: [PATCH 12/12] docs(certora): cover liveness rule and
 single-collateral scope

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>
---
 certora/README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/certora/README.md b/certora/README.md
index af9c8b97f..8d2c7ebb7 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -39,7 +39,8 @@ Healthy positions stay healthy, and liquidations only touch liquidatable positio
 - [`Healthiness.spec`](specs/Healthiness.spec) checks that after any action (except oracle update) a healthy borrower is still healthy, or is liquidation-locked: a transient state that cannot be liquidated and that is always cleared by the end of the transaction.
 - [`MaxRepaidHealthy.spec`](specs/MaxRepaidHealthy.spec) checks the restoration counterpart of that preservation property: an unhealthy borrower liquidated in normal mode is healthy again once the liquidator has repaid `maxRepaid`, the recovery close factor cap.
   `liquidate` runs no health check after the fact, so this rests on the cap formula alone: `maxRepaid` is rounded up so that repaying up to it always suffices, the roundings of the seized collateral and of the resulting max debt included.
-  The rule covers markets with two collaterals, and the case where the recovery close factor is active.
+  A second rule checks the matching liveness property: liquidating at that cap does not revert, so the restoration is not vacuous.
+  The rules cover markets with one or two collaterals, and the case where the recovery close factor is active.
 - [`Liquidate.spec`](specs/Liquidate.spec) checks that `liquidate` can only act on a liquidatable position, leaves credit unchanged, and can only decrease the borrower's debt and the seized collateral.
 - [`LiquidationProfitability.spec`](specs/LiquidationProfitability.spec) shows that the liquidation is profitable.
 - [`LiquidationBoundedByLIF.spec`](specs/LiquidationBoundedByLIF.spec) checks the upper side: liquidation profit is bounded by `maxLif`.