From 768cd6d7bf2e41d6636e61562fb02345634302cd Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 26 Jul 2026 19:29:01 +0000 Subject: [PATCH 01/19] [Certora] Prove liquidate at RCF cap restores health (single-collateral) 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) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/confs/MaxRepaidHealthy.conf | 29 +++ certora/helpers/MidnightWrapper.sol | 47 ++++- certora/specs/MaxRepaidHealthy.spec | 267 ++++++++++++++++++++++++++++ certora/specs/MulDiv.spec | 6 + 4 files changed, 348 insertions(+), 1 deletion(-) create mode 100644 certora/confs/MaxRepaidHealthy.conf create mode 100644 certora/specs/MaxRepaidHealthy.spec diff --git a/certora/confs/MaxRepaidHealthy.conf b/certora/confs/MaxRepaidHealthy.conf new file mode 100644 index 000000000..fa7dd33a3 --- /dev/null +++ b/certora/confs/MaxRepaidHealthy.conf @@ -0,0 +1,29 @@ +{ + "files": [ + "certora/helpers/MidnightWrapper.sol", + "certora/helpers/Havoc.sol" + ], + "parametric_contracts": [ + "MidnightWrapper" + ], + "verify": "MidnightWrapper:certora/specs/MaxRepaidHealthy.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 2048, + "prover_args": [ + "-destructiveOptimizations twostage", + "-backendStrategy singleRace", + "-smt_useLIA false", + "-smt_useNIA true", + "-depth 0", + "-mediumTimeout 60", + "-timeout 7200", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "smt_timeout": 7200, + "msg": "Midnight MaxRepaidHealthy" +} diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index 2cb6432d3..85906a910 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -6,7 +6,7 @@ import {Midnight} from "../../src/Midnight.sol"; import {Position, CollateralParams, Market} from "../../src/interfaces/IMidnight.sol"; import {IOracle} from "../../src/interfaces/IOracle.sol"; import {UtilsLib} from "../../src/libraries/UtilsLib.sol"; -import {ORACLE_PRICE_SCALE, WAD} from "../../src/libraries/ConstantsLib.sol"; +import {ORACLE_PRICE_SCALE, WAD, maxLif} from "../../src/libraries/ConstantsLib.sol"; contract MidnightWrapper is Midnight { using UtilsLib for uint256; @@ -30,4 +30,49 @@ 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). + * 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 + view + returns (uint256) + { + Position storage _position = position[id][borrower]; + uint256 debt = _position.debt; + uint256 maxDebt; + uint256 len = market.collateralParams.length; + for (uint256 i = len; i > 0;) { + i--; + CollateralParams memory collateralParam = market.collateralParams[i]; + uint256 price = IOracle(collateralParam.oracle).price(); + maxDebt += _position.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE) + .mulDivDown(collateralParam.lltv, WAD); + } + 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); + } + + /* badDebtFor recomputes the badDebt of Midnight.liquidate (see src/Midnight.sol:643-655) through a + * bitmap-free, array-based code path. Used to pin the no-bad-debt case (badDebtFor == 0), under which + * liquidate does not reduce _position.debt before the L699 cap computation. */ + function badDebtFor(Market memory market, bytes32 id, address borrower) public view returns (uint256) { + Position storage _position = position[id][borrower]; + uint256 badDebt = _position.debt; + uint256 len = market.collateralParams.length; + for (uint256 i = len; i > 0;) { + i--; + CollateralParams memory collateralParam = market.collateralParams[i]; + uint256 price = IOracle(collateralParam.oracle).price(); + badDebt = badDebt.zeroFloorSub( + _position.collateral[i].mulDivUp(price, ORACLE_PRICE_SCALE) + .mulDivUp(WAD, maxLif(collateralParam.lltv, collateralParam.liquidationCursor)) + ); + } + return badDebt; + } } diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec new file mode 100644 index 000000000..86ca68f73 --- /dev/null +++ b/certora/specs/MaxRepaidHealthy.spec @@ -0,0 +1,267 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2026 Morpho Association + +import "BitmapSummaries.spec"; + +// On-contract version of the Rocq theorem max_repaid_liquidation_leaves_healthy (rocq/maxRepaidHealthy.v): +// in the RCF-active regime (!postMaturityMode && lltv < WAD), liquidating an unhealthy position at the RCF +// cap repaid = maxRepaid (see src/Midnight.sol:699) restores health (newDebt <= newMaxDebt, newDebt >= 0). +// This is the RESTORATION direction; Healthiness.spec proves the PRESERVATION direction. +// Single-collateral first: the Rocq otherCollatContribution is 0 here (the market has one collateral). + +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. + function _.price() external => summaryPrice(calledContract) expect(uint256); + function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; + function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); + function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; + + // Summarize mulDivDown and mulDivUp deterministically; the axioms about them are proved in MulDiv.spec. + 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); + + // maxLif is recomputed on the fly from (lltv, liquidationCursor); its lltv * maxLif <= WAD * WAD bound is + // assumed below (see lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec). + function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor); + + // No reentrancy is modeled for this direction: transfers move external ERC20 balances only, never the + // borrower's position storage, so summarizing them as no-ops is sound. The callback is disabled below. + 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; + function _.canLiquidate(address) external => NONDET; + function _.onLiquidate(address liquidator, bytes32 id, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, bytes data, uint256 badDebt) external => NONDET; +} + +/// SUMMARY /// + +definition WAD() returns uint256 = 10 ^ 18; + +definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; + +persistent ghost summaryPrice(address) returns uint256; + +persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; + +persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; + +/* Axioms proved by MulDiv.spec, used to reconstruct the Rocq integer-division argument. */ + +/* proved in mulDivMonotoneA */ +definition axiomDownMonotoneA(mathint a1, mathint a2, mathint b, mathint d) returns bool = 0 <= a1 && a1 <= a2 && 0 <= b && 0 < d => ghostMulDivDown(a1, b, d) <= ghostMulDivDown(a2, b, d); + +/* proved in mulDivMonotoneA */ +definition axiomUpMonotoneA(mathint a1, mathint a2, mathint b, mathint d) returns bool = 0 <= a1 && a1 <= a2 && 0 <= b && 0 < d => ghostMulDivUp(a1, b, d) <= ghostMulDivUp(a2, b, d); + +/* proved in mulDivAddDownUp: floor(a1*b/d) + ceil(a2*b/d) >= floor((a1+a2)*b/d), i.e. the drop bound + floor((a1+a2)*b/d) - floor(a1*b/d) <= ceil(a2*b/d) (Rocq floor_drop_div_le_ceil). */ +definition axiomAddDownUp(mathint a1, mathint a2, mathint b, mathint d) returns bool = a1 >= 0 && a2 >= 0 && b >= 0 && d > 0 => ghostMulDivDown(a1, b, d) + ghostMulDivUp(a2, b, d) >= ghostMulDivDown(a1 + a2, b, d); + +/* proved in mulDivInverseUpDown: ceil(floor(a*b/d)*d/b) <= a (Rocq seized_value_drop_le_maxSeizedValue). */ +definition axiomInverseUpDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b > 0 && d > 0 => ghostMulDivUp(ghostMulDivDown(a, b, d), d, b) <= a; + +/* proved in mulDivDownRoundsDown: floor(a*b/d)*d <= a*b (Rocq floor_mul_le). */ +definition axiomDownRoundsDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => ghostMulDivDown(a, b, d) * d <= a * b; + +/* proved in mulDivUpRoundsUp: a*b <= ceil(a*b/d)*d (Rocq ceil_div_mul_ge). */ +definition axiomUpRoundsUp(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => a * b <= ghostMulDivUp(a, b, d) * d; + +/* proved in mulDivCeilLeOfMulGe: a*b <= bound*d => ceil(a*b/d) <= bound (Rocq ceil_div_le_of_mul_ge). */ +definition axiomCeilLeOfMulGe(mathint a, mathint b, mathint d, mathint bound) returns bool = a >= 0 && b >= 0 && d > 0 && a * b <= bound * d => ghostMulDivUp(a, b, d) <= bound; + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(ghostMulDivDown(a, b, d)); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(ghostMulDivUp(a, b, d)); +} + +// Global market machinery (mirrors Healthiness.spec): pins the market so that IdLib.toId is deterministic and +// the collateral params are known. globalMarketCollateralLength is fixed to 1 in the rule (single collateral). + +persistent ghost address globalMarketLoanToken; + +persistent ghost uint256 globalMarketChainId; + +persistent ghost uint256 globalMarketCollateralLength { + axiom globalMarketCollateralLength <= 2; +} + +persistent ghost mapping(uint256 => address) globalMarketCollateralOracle; + +persistent ghost mapping(uint256 => address) globalMarketCollateralToken; + +persistent ghost mapping(uint256 => uint256) globalMarketCollateralLLTV; + +persistent ghost mapping(uint256 => uint256) globalMarketCollateralLiquidationCursor; + +persistent ghost maxLifGhost(uint256, uint256) returns uint256; + +persistent ghost uint256 globalMarketMaturity; + +persistent ghost uint256 globalMarketRcfThreshold; + +persistent ghost address globalMarketEnterGate; + +persistent ghost address globalMarketLiquidatorGate; + +persistent ghost bytes32 globalId; + +persistent ghost address globalBorrower; + +definition collateralMatches(Midnight.Market market, uint256 index) returns bool = (index < globalMarketCollateralLength => market.collateralParams[index].oracle == globalMarketCollateralOracle[index] && market.collateralParams[index].token == globalMarketCollateralToken[index] && market.collateralParams[index].lltv == globalMarketCollateralLLTV[index] && market.collateralParams[index].liquidationCursor == globalMarketCollateralLiquidationCursor[index]); + +function equalsGlobalMarket(Midnight.Market market) returns (bool) { + return market.chainId == globalMarketChainId && market.midnight == currentContract && market.loanToken == globalMarketLoanToken && market.collateralParams.length == globalMarketCollateralLength && collateralMatches(market, 0) && collateralMatches(market, 1) && market.maturity == globalMarketMaturity && market.rcfThreshold == globalMarketRcfThreshold && market.enterGate == globalMarketEnterGate && market.liquidatorGate == globalMarketLiquidatorGate; +} + +function getGlobalMarket() returns (Midnight.Market) { + Midnight.Market market; + require equalsGlobalMarket(market), "get global market"; + return market; +} + +function summaryToId(Midnight.Market market) returns (bytes32) { + bytes32 id; + if (equalsGlobalMarket(market)) { + require id == globalId, "toId() is deterministic"; + } else { + require id != globalId, "toId() is injective"; + } + return id; +} + +// Single-collateral maxDebt contribution: floor(floor(collat * price / OPS) * lltv / WAD). +function maxDebtContribution(uint256 collat, mathint price, uint256 lltv) returns mathint { + return ghostMulDivDown(ghostMulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()); +} + +//// RULE ////// + +// Liquidating an unhealthy position at the RCF cap restores its health, in the single-collateral, +// RCF-active (!postMaturityMode && lltv < WAD), no-bad-debt regime. This is the on-contract analog of the +// Rocq theorem max_repaid_liquidation_leaves_healthy, maxRepaid < debt case (newDebt = debt - maxRepaid > 0). +rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address receiver, address callback, bytes data) { + // Post-state health is read bitmap-free; combined with single-collateral this avoids bitmap iteration. + Midnight.Market globalMarket = getGlobalMarket(); + + // Single collateral: the Rocq otherCollatContribution is 0. + require globalMarketCollateralLength == 1, "single-collateral market"; + require collateralIndex == 0, "the only collateral index"; + + uint256 lltv = globalMarketCollateralLLTV[collateralIndex]; + uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]); + + // RCF-active regime. + require lltv < WAD(), "RCF is active only for lltv < WAD"; + + // maxLif * lltv <= 0.999 * WAD * WAD is enforced at market creation for lltv < WAD (see Midnight.sol:698, + // createdMarketsRespectMaxLifBound in CreatedMarkets.spec); it makes the L699 denominator strictly positive. + require lltv * lif <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD * WAD"; + + // lltv * maxLif <= WAD * WAD (see lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec). + require lltv * lif <= WAD() * WAD(), "lltv * maxLif <= WAD * WAD"; + + address oracle = globalMarket.collateralParams[collateralIndex].oracle; + mathint price = summaryPrice(oracle); + + // 0 < price (Rocq hypothesis); otherwise the mulDiv by price reverts and the case is vacuous. + require price > 0, "positive price"; + + // Single-collateral bitmap: only collateralIndex is activated, so the liquidate maxDebt loop and the + // array-based maxRepaidFor / isHealthyNoBitmap all range over exactly {collateralIndex}. + uint128 bitmap = collateralBitmap(globalId, globalBorrower); + require summaryGetBit(bitmap, collateralIndex), "collateral is activated (see nonZeroCollateralsAreActivated)"; + require forall uint256 otherBit. otherBit != collateralIndex => !summaryGetBit(bitmap, otherBit), "single-collateral: only collateralIndex activated"; + + // Borrower must not be liquidation-locked (see Midnight.sol:660). + require !liquidationLocked(globalId, globalBorrower), "borrower not locked"; + + // No callback, so onLiquidate is skipped and no reentrancy occurs. + require callback == 0, "no liquidate callback"; + + // No liquidator gate, so canLiquidate is skipped (see Midnight.sol:635-638). + require globalMarketLiquidatorGate == 0, "no liquidator gate"; + + // Market is already created, so touchMarket is a no-op that returns globalId. + require currentContract.marketState[globalId].tickSpacing != 0, "market already created"; + + // No bad debt is realized: liquidate does not reduce _position.debt before the L699 cap computation, so the + // debt used at L699 equals the pre-liquidation debt read by maxRepaidFor (Rocq assumes no bad-debt path). + require badDebtFor(globalMarket, globalId, globalBorrower) == 0, "no bad debt realized"; + + // Unhealthy pre-state: maxDebt < debt (Rocq maxDebt <= debt with the strict RCF trigger of Midnight.sol:661). + require !isHealthyNoBitmap(globalMarket, globalId, globalBorrower), "unhealthy before liquidation"; + + uint256 collatBefore = collateral(globalId, globalBorrower, collateralIndex); + uint256 debtBefore = debt(globalId, globalBorrower); + + // Pin repaid to the RCF cap. maxRepaidFor reproduces Midnight.sol:699 exactly, so repaidUnits equals the + // maxRepaid recomputed inside liquidate and the RCF require (Midnight.sol:700-705) passes on its first + // disjunct (repaidUnits <= maxRepaid), independently of the dust waiver. + uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, globalBorrower); + + // Interesting case: maxRepaid < debt (repaid = maxRepaid, newDebt = debt - maxRepaid > 0). The maxRepaid >= debt + // case gives repaid = debt, newDebt = 0, which is trivially healthy. + require repaidUnits < debtBefore, "maxRepaid < debt case"; + + uint256 seizedOut; + uint256 repaidOut; + seizedOut, repaidOut = liquidate(e, globalMarket, collateralIndex, 0, repaidUnits, globalBorrower, false, receiver, callback, data); + + // The seized collateral must not exceed the current collateral (Rocq seizedAssets <= collat); otherwise + // liquidate reverts independently of the RCF mechanism, so this does not narrow the generality. + require collatBefore >= seizedOut, "seized <= collateral"; + + // The current and post-liquidation LLTV-weighted collateral values (single collateral). + mathint gap = debtBefore - maxDebtContribution(collatBefore, price, lltv); + mathint maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD()); + mathint cv = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + mathint ncv = ghostMulDivDown(collatBefore - seizedOut, price, ORACLE_PRICE_SCALE()); + + // Axioms needed to reconstruct the Rocq argument (see rocq/maxRepaidHealthy.v, maxRepaid < debt case). + // Universal monotonicity backups. + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "axiom"; + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomDownMonotoneA(a1, a2, b, d), "axiom"; + + // Fact I: the RCF cap over-repays the gap: gap * WAD^2 <= maxRepaid * (WAD^2 - lif*lltv) (ceil_div_mul_ge). + require axiomUpRoundsUp(gap, WAD() * WAD(), WAD() * WAD() - lif * lltv), "axiom"; + + // Step (a): the collateral-value drop is at most the seized value in loan units. + require axiomAddDownUp(collatBefore - seizedOut, seizedOut, price, ORACLE_PRICE_SCALE()), "axiom"; + require axiomInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "axiom"; + + // Step (b): the LLTV-weighted maxDebt drop is at most ceil(valueDrop * lltv / WAD). + require axiomAddDownUp(ncv, cv - ncv, lltv, WAD()), "axiom"; + + // Step (c): ceil is monotone, and valueDrop <= maxSeizedValue (from step (a)). + require axiomUpMonotoneA(cv - ncv, maxSeizedValue, lltv, WAD()), "axiom"; + + // Step (d): ceil(maxSeizedValue * lltv / WAD) <= maxRepaid - gap, closing the bound. + require axiomDownRoundsDown(repaidUnits, lif, WAD()), "axiom"; + require axiomCeilLeOfMulGe(maxSeizedValue, lltv, WAD(), repaidUnits - gap), "axiom"; + + // newDebt >= 0 and newDebt <= newMaxDebt, i.e. the position is healthy after liquidation. + assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower), "position is healthy after liquidation at the RCF cap"; +} diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index 7eecf9733..57af3b090 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -113,6 +113,12 @@ rule mulDivUpUpperBound(uint256 a, uint256 b, uint256 d) { assert mulDivUp(a, b, d) * d <= a * b + d - 1; } +// If the exact product is at most bound * d, then the ceiling is at most bound. +// Used by MaxRepaidHealthy.spec (axiomCeilLeOfMulGe) to bound the collateral-value drop. +rule mulDivCeilLeOfMulGe(uint256 a, uint256 b, uint256 d, uint256 bound) { + assert d != 0 && a * b <= bound * d => mulDivUp(a, b, d) <= bound; +} + rule mulDivResidualBound(uint256 a, uint256 b, uint256 d) { assert a <= d && b <= d => a - mulDivDown(a, b, d) <= d - b; assert a <= d && b <= d => a - mulDivUp(a, b, d) <= d - b; From b6ea78be428e1a521dce2d72d806ef24040aa976 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 26 Jul 2026 21:42:13 +0000 Subject: [PATCH 02/19] [Certora] Make liquidateAtCapRestoresHealth tractable (fix SMT timeout) 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) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/specs/MaxRepaidHealthy.spec | 61 +++++++++-------------------- 1 file changed, 19 insertions(+), 42 deletions(-) diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index 86ca68f73..b4f9cb7b6 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -57,23 +57,10 @@ persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; -/* Axioms proved by MulDiv.spec, used to reconstruct the Rocq integer-division argument. */ - -/* proved in mulDivMonotoneA */ -definition axiomDownMonotoneA(mathint a1, mathint a2, mathint b, mathint d) returns bool = 0 <= a1 && a1 <= a2 && 0 <= b && 0 < d => ghostMulDivDown(a1, b, d) <= ghostMulDivDown(a2, b, d); - -/* proved in mulDivMonotoneA */ -definition axiomUpMonotoneA(mathint a1, mathint a2, mathint b, mathint d) returns bool = 0 <= a1 && a1 <= a2 && 0 <= b && 0 < d => ghostMulDivUp(a1, b, d) <= ghostMulDivUp(a2, b, d); - -/* proved in mulDivAddDownUp: floor(a1*b/d) + ceil(a2*b/d) >= floor((a1+a2)*b/d), i.e. the drop bound - floor((a1+a2)*b/d) - floor(a1*b/d) <= ceil(a2*b/d) (Rocq floor_drop_div_le_ceil). */ -definition axiomAddDownUp(mathint a1, mathint a2, mathint b, mathint d) returns bool = a1 >= 0 && a2 >= 0 && b >= 0 && d > 0 => ghostMulDivDown(a1, b, d) + ghostMulDivUp(a2, b, d) >= ghostMulDivDown(a1 + a2, b, d); - -/* proved in mulDivInverseUpDown: ceil(floor(a*b/d)*d/b) <= a (Rocq seized_value_drop_le_maxSeizedValue). */ -definition axiomInverseUpDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b > 0 && d > 0 => ghostMulDivUp(ghostMulDivDown(a, b, d), d, b) <= a; - -/* proved in mulDivDownRoundsDown: floor(a*b/d)*d <= a*b (Rocq floor_mul_le). */ -definition axiomDownRoundsDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => ghostMulDivDown(a, b, d) * d <= a * b; +/* Axioms used to reconstruct the Rocq integer-division argument. + The two cheap rounding facts are proved over concrete mulDiv in MulDiv.spec. The single hard nonlinear step + (the LLTV-weighted maxDebt drop bound) is delegated to axiomMaxDebtDrop, machine-checked over the integers in + Rocq; assuming it here keeps the on-contract goal linear, so the prover does not have to rediscover the chain. */ /* proved in mulDivUpRoundsUp: a*b <= ceil(a*b/d)*d (Rocq ceil_div_mul_ge). */ definition axiomUpRoundsUp(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => a * b <= ghostMulDivUp(a, b, d) * d; @@ -81,6 +68,12 @@ definition axiomUpRoundsUp(mathint a, mathint b, mathint d) returns bool = a >= /* proved in mulDivCeilLeOfMulGe: a*b <= bound*d => ceil(a*b/d) <= bound (Rocq ceil_div_le_of_mul_ge). */ definition axiomCeilLeOfMulGe(mathint a, mathint b, mathint d, mathint bound) returns bool = a >= 0 && b >= 0 && d > 0 && a * b <= bound * d => ghostMulDivUp(a, b, d) <= bound; +/* Rocq max_debt_contribution_drop_bound (rocq/maxRepaidHealthy.v:162), the one hard nonlinear step: when + seized is the L692 seizedAssets = floor(floor(maxRepaid*lif/WAD)*OPS/price), the LLTV-weighted maxDebt + contribution drops by at most ceil(maxRepaid*lif*lltv/WAD^2). Proved over the integers in Rocq; the Solidity + quantities are shown equal to its variables in the rule below, and the CVL bounds wire it to on-chain health. */ +definition axiomMaxDebtDrop(mathint collat, mathint seized, mathint price, mathint lltv, mathint maxRepaid, mathint lif) returns bool = price > 0 && collat >= 0 && 0 <= seized && seized <= collat && lltv >= 0 && maxRepaid >= 0 && lif >= 0 && seized == ghostMulDivDown(ghostMulDivDown(maxRepaid, lif, WAD()), ORACLE_PRICE_SCALE(), price) => ghostMulDivDown(ghostMulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()) - ghostMulDivDown(ghostMulDivDown(collat - seized, price, ORACLE_PRICE_SCALE()), lltv, WAD()) <= ghostMulDivUp(maxRepaid, lif * lltv, WAD() * WAD()); + function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -234,33 +227,17 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address receiv // liquidate reverts independently of the RCF mechanism, so this does not narrow the generality. require collatBefore >= seizedOut, "seized <= collateral"; - // The current and post-liquidation LLTV-weighted collateral values (single collateral). + // gap = debt - maxDebt > 0 (the position is unhealthy). Both are the single-collateral quantities that + // liquidate uses internally: maxDebt at L699 and debt (unchanged, since no bad debt) equal these. mathint gap = debtBefore - maxDebtContribution(collatBefore, price, lltv); - mathint maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD()); - mathint cv = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); - mathint ncv = ghostMulDivDown(collatBefore - seizedOut, price, ORACLE_PRICE_SCALE()); - - // Axioms needed to reconstruct the Rocq argument (see rocq/maxRepaidHealthy.v, maxRepaid < debt case). - // Universal monotonicity backups. - require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "axiom"; - require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomDownMonotoneA(a1, a2, b, d), "axiom"; - - // Fact I: the RCF cap over-repays the gap: gap * WAD^2 <= maxRepaid * (WAD^2 - lif*lltv) (ceil_div_mul_ge). - require axiomUpRoundsUp(gap, WAD() * WAD(), WAD() * WAD() - lif * lltv), "axiom"; - - // Step (a): the collateral-value drop is at most the seized value in loan units. - require axiomAddDownUp(collatBefore - seizedOut, seizedOut, price, ORACLE_PRICE_SCALE()), "axiom"; - require axiomInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "axiom"; - - // Step (b): the LLTV-weighted maxDebt drop is at most ceil(valueDrop * lltv / WAD). - require axiomAddDownUp(ncv, cv - ncv, lltv, WAD()), "axiom"; - - // Step (c): ceil is monotone, and valueDrop <= maxSeizedValue (from step (a)). - require axiomUpMonotoneA(cv - ncv, maxSeizedValue, lltv, WAD()), "axiom"; - // Step (d): ceil(maxSeizedValue * lltv / WAD) <= maxRepaid - gap, closing the bound. - require axiomDownRoundsDown(repaidUnits, lif, WAD()), "axiom"; - require axiomCeilLeOfMulGe(maxSeizedValue, lltv, WAD(), repaidUnits - gap), "axiom"; + // Three axioms close the goal with only linear glue (see rocq/maxRepaidHealthy.v, maxRepaid < debt case): + // the maxDebt drop is bounded by ceil(maxRepaid*lif*lltv/WAD^2) (axiomMaxDebtDrop), the RCF cap over-repays + // the gap so maxRepaid*lif*lltv <= (maxRepaid - gap)*WAD^2 (axiomUpRoundsUp), hence that ceil is at most + // maxRepaid - gap (axiomCeilLeOfMulGe); so newMaxDebt = maxDebt - drop >= debt - maxRepaid = newDebt. + require axiomMaxDebtDrop(collatBefore, seizedOut, price, lltv, repaidUnits, lif), "Rocq max_debt_contribution_drop_bound"; + require axiomUpRoundsUp(gap, WAD() * WAD(), WAD() * WAD() - lif * lltv), "proved in mulDivUpRoundsUp (Rocq ceil_div_mul_ge)"; + require axiomCeilLeOfMulGe(repaidUnits, lif * lltv, WAD() * WAD(), repaidUnits - gap), "proved in mulDivCeilLeOfMulGe (Rocq ceil_div_le_of_mul_ge)"; // newDebt >= 0 and newDebt <= newMaxDebt, i.e. the position is healthy after liquidation. assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower), "position is healthy after liquidation at the RCF cap"; From 8f6913064e73a19511637717bd7ba5d4393dabed Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 27 Jul 2026 09:59:57 +0000 Subject: [PATCH 03/19] [Certora] Attempt concrete discharge of the maxDebt-drop bound 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) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/confs/MaxDebtDropBound.conf | 25 ++++++++++++++++++++++ certora/specs/MaxDebtDropBound.spec | 32 +++++++++++++++++++++++++++++ 2 files changed, 57 insertions(+) create mode 100644 certora/confs/MaxDebtDropBound.conf create mode 100644 certora/specs/MaxDebtDropBound.spec diff --git a/certora/confs/MaxDebtDropBound.conf b/certora/confs/MaxDebtDropBound.conf new file mode 100644 index 000000000..23b57c861 --- /dev/null +++ b/certora/confs/MaxDebtDropBound.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/helpers/MulDiv.sol" + ], + "verify": "MulDiv:certora/specs/MaxDebtDropBound.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 2048, + "prover_args": [ + "-destructiveOptimizations twostage", + "-backendStrategy singleRace", + "-smt_useLIA false", + "-smt_useNIA true", + "-depth 0", + "-mediumTimeout 60", + "-timeout 7200", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "smt_timeout": 7200, + "msg": "Midnight MaxDebtDropBound" +} diff --git a/certora/specs/MaxDebtDropBound.spec b/certora/specs/MaxDebtDropBound.spec new file mode 100644 index 000000000..47cdfc12c --- /dev/null +++ b/certora/specs/MaxDebtDropBound.spec @@ -0,0 +1,32 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2026 Morpho Association + +// Standalone discharge of axiomMaxDebtDrop assumed in MaxRepaidHealthy.spec: the Rocq lemma +// max_debt_contribution_drop_bound (rocq/maxRepaidHealthy.v:162), proven over concrete mulDivDown/mulDivUp +// (NOT summarized). Isolated in its own spec/conf so a hard-nonlinear timeout cannot gate the fast MulDiv leg. + +methods { + function mulDivDown(uint256 a, uint256 b, uint256 d) external returns (uint256) envfree; + function mulDivUp(uint256 a, uint256 b, uint256 d) external returns (uint256) envfree; +} + +definition WAD() returns uint256 = 10 ^ 18; + +definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; + +// The LLTV-weighted maxDebt contribution drops by at most ceil(maxRepaid * lif * lltv / WAD^2) when seized is +// the L692 seizedAssets = floor(floor(maxRepaid * lif / WAD) * OPS / price). See rocq/maxRepaidHealthy.v:162. +rule maxDebtContributionDropBound(uint256 collat, uint256 price, uint256 lltv, uint256 maxRepaid, uint256 lif) { + require price > 0, "0 < price"; + require lltv <= WAD(), "enabled lltv <= WAD"; + require lif <= 2 * WAD(), "maxLif <= 2 * WAD (see Midnight.sol:810)"; + + uint256 maxSeizedValue = mulDivDown(maxRepaid, lif, WAD()); + uint256 seized = mulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price); + require seized <= collat, "seized <= collateral (else liquidate reverts)"; + + uint256 curContrib = mulDivDown(mulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + uint256 newContrib = mulDivDown(mulDivDown(assert_uint256(collat - seized), price, ORACLE_PRICE_SCALE()), lltv, WAD()); + + assert curContrib - newContrib <= mulDivUp(maxRepaid, require_uint256(lif * lltv), WAD() * WAD()); +} From b8ade92a05c903a45ea407b43215f79c8c40d42a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 27 Jul 2026 10:08:17 +0000 Subject: [PATCH 04/19] [Certora] Fix type error in MaxDebtDropBound lemma 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) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/specs/MaxDebtDropBound.spec | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/certora/specs/MaxDebtDropBound.spec b/certora/specs/MaxDebtDropBound.spec index 47cdfc12c..fcafb473f 100644 --- a/certora/specs/MaxDebtDropBound.spec +++ b/certora/specs/MaxDebtDropBound.spec @@ -28,5 +28,10 @@ rule maxDebtContributionDropBound(uint256 collat, uint256 price, uint256 lltv, u uint256 curContrib = mulDivDown(mulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()); uint256 newContrib = mulDivDown(mulDivDown(assert_uint256(collat - seized), price, ORACLE_PRICE_SCALE()), lltv, WAD()); - assert curContrib - newContrib <= mulDivUp(maxRepaid, require_uint256(lif * lltv), WAD() * WAD()); + // lif * lltv and WAD * WAD are mathint products; cast them to pass as uint256 mulDivUp arguments. Both fit: + // lif <= 2 * WAD and lltv <= WAD, and WAD * WAD == 10^36. + uint256 lifTimesLltv = require_uint256(lif * lltv); + uint256 wadSquared = require_uint256(WAD() * WAD()); + + assert curContrib - newContrib <= mulDivUp(maxRepaid, lifTimesLltv, wadSquared); } From 728d7c593071710c9914c328e076dd4c6e962640 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 30 Jul 2026 14:03:15 +0000 Subject: [PATCH 05/19] [Certora] Decompose MaxDebtDropBound into concrete sub-lemmas + ghost 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) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/specs/MaxDebtDropBound.spec | 140 +++++++++++++++++++++++++--- 1 file changed, 127 insertions(+), 13 deletions(-) diff --git a/certora/specs/MaxDebtDropBound.spec b/certora/specs/MaxDebtDropBound.spec index fcafb473f..8dbbfcee3 100644 --- a/certora/specs/MaxDebtDropBound.spec +++ b/certora/specs/MaxDebtDropBound.spec @@ -2,8 +2,15 @@ // Copyright (c) 2026 Morpho Association // Standalone discharge of axiomMaxDebtDrop assumed in MaxRepaidHealthy.spec: the Rocq lemma -// max_debt_contribution_drop_bound (rocq/maxRepaidHealthy.v:162), proven over concrete mulDivDown/mulDivUp -// (NOT summarized). Isolated in its own spec/conf so a hard-nonlinear timeout cannot gate the fast MulDiv leg. +// max_debt_contribution_drop_bound (rocq/maxRepaidHealthy.v:162), proven over concrete mulDivDown/mulDivUp. +// +// A single monolithic assert of the full bound (5-nested divisions in one NIA query) times out at 2h. Instead we +// mirror the Rocq proof's decomposition (rocq/maxRepaidHealthy.v:75-247): each nested-mulDiv fact is proven as its +// own SMALL concrete rule (<= 2 nested divisions, so the solver closes it fast), and a final composition rule +// (maxDebtContributionDropBound) assembles them over UNINTERPRETED (ghost) mulDiv with only linear/NIA glue -- so +// the SMT never faces the nested-division goal in one query. This is the assume-ghost / prove-concrete split used +// by RealizableBadDebtLiquidate.spec + MulDiv.spec in PR #1079. Isolated in its own spec/conf so a hard-nonlinear +// timeout cannot gate the fast MulDiv leg. methods { function mulDivDown(uint256 a, uint256 b, uint256 d) external returns (uint256) envfree; @@ -14,24 +21,131 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; -// The LLTV-weighted maxDebt contribution drops by at most ceil(maxRepaid * lif * lltv / WAD^2) when seized is -// the L692 seizedAssets = floor(floor(maxRepaid * lif / WAD) * OPS / price). See rocq/maxRepaidHealthy.v:162. +// Uninterpreted mulDiv, used ONLY by the composition rule so its goal stays linear (no nested division). Each +// assumed instance below is discharged by one of the concrete sub-lemma rules further down, over the real +// mulDivDown/mulDivUp of MulDiv.sol. +persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; + +persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; + +/// CONCRETE SUB-LEMMAS (each is a small standalone sub-goal over the real mulDiv) /// + +// L1 == Rocq seized_value_drop_le_maxSeizedValue (:141) / MulDiv.spec mulDivInverseUpDown. +// Valuing (ceil) the assets that a floor-seize took never exceeds what was seized in value: up(down(a,b,d),d,b) <= a. +rule lemmaInverseUpDown(uint256 a, uint256 b, uint256 d) { + assert mulDivUp(mulDivDown(a, b, d), d, b) <= a; +} + +// L2 & L3 == Rocq floor_drop_div_le_ceil (:122) / MulDiv.spec mulDivAddDownUp. +// A floor drop over an added chunk is bounded by the ceil of that chunk: down(a1+a2,b,d) <= down(a1,b,d)+up(a2,b,d). +rule lemmaDropLeCeil(uint256 a1, uint256 a2, uint256 b, uint256 d) { + uint256 a1plusa2 = require_uint256(a1 + a2); + assert mulDivDown(a1plusa2, b, d) <= mulDivDown(a1, b, d) + mulDivUp(a2, b, d); +} + +// L4 == Rocq ceil_div_mono (:112) / MulDiv.spec mulDivMonotoneA (up leg): ceil is monotone in its numerator. +rule lemmaMonotoneUpNum(uint256 a1, uint256 a2, uint256 b, uint256 d) { + assert a1 <= a2 => mulDivUp(a1, b, d) <= mulDivUp(a2, b, d); +} + +// Monotonicity of floor in its numerator (used to know newCollatValue <= curCollatValue, i.e. the drop is >= 0). +rule lemmaMonotoneDownNum(uint256 a1, uint256 a2, uint256 b, uint256 d) { + assert a1 <= a2 => mulDivDown(a1, b, d) <= mulDivDown(a2, b, d); +} + +// L5.a == Rocq floor_mul_le (:75) / MulDiv.spec mulDivDownRoundsDown: down(a,b,d)*d <= a*b. +rule lemmaDownRoundsDown(uint256 a, uint256 b, uint256 d) { + assert mulDivDown(a, b, d) * d <= a * b; +} + +// L5.b == Rocq ceil_div_mul_ge (:87) / MulDiv.spec mulDivUpRoundsUp: up(a,b,d)*d >= a*b. +rule lemmaUpRoundsUp(uint256 a, uint256 b, uint256 d) { + assert mulDivUp(a, b, d) * d >= a * b; +} + +// L5.c == Rocq ceil_div_le_of_mul_ge (:100) / MulDiv.spec mulDivCeilLeOfMulGe: +// if the exact product is at most bound*d then the ceiling is at most bound. +rule lemmaCeilLeOfMulGe(uint256 a, uint256 b, uint256 d, uint256 bound) { + assert d != 0 && a * b <= bound * d => mulDivUp(a, b, d) <= bound; +} + +// mulDiv of non-negatives is non-negative (uint256 result). Needed to pin the sign of the ghost values below. +rule lemmaNonneg(uint256 a, uint256 b, uint256 d) { + assert mulDivDown(a, b, d) >= 0; + assert mulDivUp(a, b, d) >= 0; +} + +/// COMPOSITION (the discharge of axiomMaxDebtDrop) /// + +// The LLTV-weighted maxDebt contribution drops by at most ceil(maxRepaid * lif * lltv / WAD^2) when seized is the +// L692 seizedAssets = floor(floor(maxRepaid * lif / WAD) * OPS / price). See rocq/maxRepaidHealthy.v:162. Proven over +// UNINTERPRETED mulDiv (ghost*), assuming each nested fact in the exact instance the concrete sub-lemmas above prove, +// then closing with linear/NIA glue -- exactly the composition structure of the Rocq proof body (:180-246). rule maxDebtContributionDropBound(uint256 collat, uint256 price, uint256 lltv, uint256 maxRepaid, uint256 lif) { require price > 0, "0 < price"; require lltv <= WAD(), "enabled lltv <= WAD"; require lif <= 2 * WAD(), "maxLif <= 2 * WAD (see Midnight.sol:810)"; - uint256 maxSeizedValue = mulDivDown(maxRepaid, lif, WAD()); - uint256 seized = mulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price); + mathint W = WAD(); + mathint S = ORACLE_PRICE_SCALE(); + + // Ghost-form quantities, mirroring the concrete definitions of the original monolithic rule. + mathint maxSeizedValue = ghostMulDivDown(maxRepaid, lif, W); + mathint seized = ghostMulDivDown(maxSeizedValue, S, price); require seized <= collat, "seized <= collateral (else liquidate reverts)"; + mathint collatMinusSeized = collat - seized; + + mathint curCollatValue = ghostMulDivDown(collat, price, S); + mathint newCollatValue = ghostMulDivDown(collatMinusSeized, price, S); + mathint collatValueDrop = curCollatValue - newCollatValue; + + mathint curContrib = ghostMulDivDown(curCollatValue, lltv, W); + mathint newContrib = ghostMulDivDown(newCollatValue, lltv, W); + + mathint lifTimesLltv = lif * lltv; + mathint wadSquared = W * W; + mathint maxDebtDropBound = ghostMulDivUp(maxRepaid, lifTimesLltv, wadSquared); + + // Non-negativity of the ghost values (lemmaNonneg). + require maxSeizedValue >= 0 && seized >= 0; + require curCollatValue >= 0 && newCollatValue >= 0; + require curContrib >= 0 && newContrib >= 0; + require maxDebtDropBound >= 0; + + // L1 (lemmaInverseUpDown), instance a=maxSeizedValue, b=S, d=price: + // up(down(maxSeizedValue,S,price),price,S) == up(seized,price,S) <= maxSeizedValue. + require ghostMulDivUp(seized, price, S) <= maxSeizedValue; + + // L2 (lemmaDropLeCeil), instance a1=collatMinusSeized, a2=seized, b=price, d=S (a1+a2 == collat): + // curCollatValue <= newCollatValue + up(seized,price,S). + require curCollatValue <= newCollatValue + ghostMulDivUp(seized, price, S); + + // newCollatValue <= curCollatValue (lemmaMonotoneDownNum, collatMinusSeized <= collat): the drop is >= 0. + require newCollatValue <= curCollatValue; + + // L3 (lemmaDropLeCeil), instance a1=newCollatValue, a2=collatValueDrop, b=lltv, d=W (a1+a2 == curCollatValue): + // curContrib <= newContrib + up(collatValueDrop,lltv,W). + require curContrib <= newContrib + ghostMulDivUp(collatValueDrop, lltv, W); + + // L4 (lemmaMonotoneUpNum), instance a1=collatValueDrop, a2=maxSeizedValue, b=lltv, d=W. + require collatValueDrop <= maxSeizedValue => ghostMulDivUp(collatValueDrop, lltv, W) <= ghostMulDivUp(maxSeizedValue, lltv, W); + + // L5.a (lemmaDownRoundsDown), instance a=maxRepaid, b=lif, d=W: maxSeizedValue*W <= maxRepaid*lif. + require maxSeizedValue * W <= maxRepaid * lif; + + // L5.b (lemmaUpRoundsUp), instance a=maxRepaid, b=lifTimesLltv, d=wadSquared: + // maxDebtDropBound*wadSquared >= maxRepaid*lifTimesLltv. + require maxDebtDropBound * wadSquared >= maxRepaid * lifTimesLltv; - uint256 curContrib = mulDivDown(mulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()); - uint256 newContrib = mulDivDown(mulDivDown(assert_uint256(collat - seized), price, ORACLE_PRICE_SCALE()), lltv, WAD()); + // L5.c (lemmaCeilLeOfMulGe), instance a=maxSeizedValue, b=lltv, d=W, bound=maxDebtDropBound: + // maxSeizedValue*lltv <= maxDebtDropBound*W => up(maxSeizedValue,lltv,W) <= maxDebtDropBound. + require maxSeizedValue * lltv <= maxDebtDropBound * W => ghostMulDivUp(maxSeizedValue, lltv, W) <= maxDebtDropBound; - // lif * lltv and WAD * WAD are mathint products; cast them to pass as uint256 mulDivUp arguments. Both fit: - // lif <= 2 * WAD and lltv <= WAD, and WAD * WAD == 10^36. - uint256 lifTimesLltv = require_uint256(lif * lltv); - uint256 wadSquared = require_uint256(WAD() * WAD()); + // --- linear / NIA glue (mirrors rocq/maxRepaidHealthy.v:185-246), no nested division here --- + // (a) collatValueDrop <= maxSeizedValue: from L2 (drop <= up(seized,price,S)) and L1 (up(seized,..) <= maxSeizedValue). + // (b) up(collatValueDrop,lltv,W) <= up(maxSeizedValue,lltv,W): L4 with (a). + // (c) up(maxSeizedValue,lltv,W) <= maxDebtDropBound: from L5.a * lltv, L5.b, cancel W>0, then L5.c. + // (d) curContrib - newContrib <= up(collatValueDrop,lltv,W) (L3), chained through (b),(c). - assert curContrib - newContrib <= mulDivUp(maxRepaid, lifTimesLltv, wadSquared); + assert curContrib - newContrib <= maxDebtDropBound; } From afd9682c3a5f81bee28cda31f6975bcf7dc299ce Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 30 Jul 2026 14:07:25 +0000 Subject: [PATCH 06/19] [Certora] Harden MaxDebtDropBound composition: isolate nonlinear steps 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) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/specs/MaxDebtDropBound.spec | 36 +++++++++++++++++++++++------ 1 file changed, 29 insertions(+), 7 deletions(-) diff --git a/certora/specs/MaxDebtDropBound.spec b/certora/specs/MaxDebtDropBound.spec index 8dbbfcee3..629f25095 100644 --- a/certora/specs/MaxDebtDropBound.spec +++ b/certora/specs/MaxDebtDropBound.spec @@ -7,9 +7,11 @@ // A single monolithic assert of the full bound (5-nested divisions in one NIA query) times out at 2h. Instead we // mirror the Rocq proof's decomposition (rocq/maxRepaidHealthy.v:75-247): each nested-mulDiv fact is proven as its // own SMALL concrete rule (<= 2 nested divisions, so the solver closes it fast), and a final composition rule -// (maxDebtContributionDropBound) assembles them over UNINTERPRETED (ghost) mulDiv with only linear/NIA glue -- so -// the SMT never faces the nested-division goal in one query. This is the assume-ghost / prove-concrete split used -// by RealizableBadDebtLiquidate.spec + MulDiv.spec in PR #1079. Isolated in its own spec/conf so a hard-nonlinear +// (maxDebtContributionDropBound) assembles them over UNINTERPRETED (ghost) mulDiv with only linear glue + modus +// ponens -- so the SMT never faces the nested-division goal in one query, and never has to multiply a hypothesis +// by a variable or cancel a factor (those two nonlinear steps are isolated in the pure-arithmetic helpers +// lemmaMulMono / lemmaCancelPos). This is the assume-ghost / prove-concrete split used by +// RealizableBadDebtLiquidate.spec + MulDiv.spec in PR #1079. Isolated in its own spec/conf so a hard-nonlinear // timeout cannot gate the fast MulDiv leg. methods { @@ -75,12 +77,23 @@ rule lemmaNonneg(uint256 a, uint256 b, uint256 d) { assert mulDivUp(a, b, d) >= 0; } +// Pure-arithmetic helper (no mulDiv): multiplying both sides of an inequality by a non-negative uint256 preserves it. +// Isolates the "multiply a hypothesis by lltv" step out of the composition so its SMT goal stays linear. +rule lemmaMulMono(uint256 x, uint256 y, uint256 c) { + assert x <= y => x * c <= y * c; +} + +// Pure-arithmetic helper (no mulDiv): a positive common factor can be cancelled. Isolates the "cancel W" step. +rule lemmaCancelPos(uint256 x, uint256 y, uint256 d) { + assert d != 0 && x * d <= y * d => x <= y; +} + /// COMPOSITION (the discharge of axiomMaxDebtDrop) /// // The LLTV-weighted maxDebt contribution drops by at most ceil(maxRepaid * lif * lltv / WAD^2) when seized is the // L692 seizedAssets = floor(floor(maxRepaid * lif / WAD) * OPS / price). See rocq/maxRepaidHealthy.v:162. Proven over // UNINTERPRETED mulDiv (ghost*), assuming each nested fact in the exact instance the concrete sub-lemmas above prove, -// then closing with linear/NIA glue -- exactly the composition structure of the Rocq proof body (:180-246). +// then closing with linear glue + modus ponens -- exactly the composition structure of the Rocq proof body (:180-246). rule maxDebtContributionDropBound(uint256 collat, uint256 price, uint256 lltv, uint256 maxRepaid, uint256 lif) { require price > 0, "0 < price"; require lltv <= WAD(), "enabled lltv <= WAD"; @@ -133,18 +146,27 @@ rule maxDebtContributionDropBound(uint256 collat, uint256 price, uint256 lltv, u // L5.a (lemmaDownRoundsDown), instance a=maxRepaid, b=lif, d=W: maxSeizedValue*W <= maxRepaid*lif. require maxSeizedValue * W <= maxRepaid * lif; + // lemmaMulMono, instance x=maxSeizedValue*W, y=maxRepaid*lif, c=lltv: scale L5.a by lltv >= 0. + require maxSeizedValue * W <= maxRepaid * lif => maxSeizedValue * W * lltv <= maxRepaid * lif * lltv; + // L5.b (lemmaUpRoundsUp), instance a=maxRepaid, b=lifTimesLltv, d=wadSquared: - // maxDebtDropBound*wadSquared >= maxRepaid*lifTimesLltv. + // maxDebtDropBound*wadSquared >= maxRepaid*lifTimesLltv (== maxRepaid*lif*lltv, == maxDebtDropBound*W*W). require maxDebtDropBound * wadSquared >= maxRepaid * lifTimesLltv; + // lemmaCancelPos, instance x=maxSeizedValue*lltv, y=maxDebtDropBound*W, d=W: cancel W>0 from the chained bound + // (maxSeizedValue*lltv)*W <= (maxDebtDropBound*W)*W ==> maxSeizedValue*lltv <= maxDebtDropBound*W. + require maxSeizedValue * lltv * W <= maxDebtDropBound * W * W => maxSeizedValue * lltv <= maxDebtDropBound * W; + // L5.c (lemmaCeilLeOfMulGe), instance a=maxSeizedValue, b=lltv, d=W, bound=maxDebtDropBound: // maxSeizedValue*lltv <= maxDebtDropBound*W => up(maxSeizedValue,lltv,W) <= maxDebtDropBound. require maxSeizedValue * lltv <= maxDebtDropBound * W => ghostMulDivUp(maxSeizedValue, lltv, W) <= maxDebtDropBound; - // --- linear / NIA glue (mirrors rocq/maxRepaidHealthy.v:185-246), no nested division here --- + // --- linear glue + modus ponens (mirrors rocq/maxRepaidHealthy.v:185-246); no nested division, no + // hypothesis-times-variable, no cancellation done by the SMT here (both isolated in the helpers above): // (a) collatValueDrop <= maxSeizedValue: from L2 (drop <= up(seized,price,S)) and L1 (up(seized,..) <= maxSeizedValue). // (b) up(collatValueDrop,lltv,W) <= up(maxSeizedValue,lltv,W): L4 with (a). - // (c) up(maxSeizedValue,lltv,W) <= maxDebtDropBound: from L5.a * lltv, L5.b, cancel W>0, then L5.c. + // (c) maxSeizedValue*lltv*W <= maxDebtDropBound*W*W: from (L5.a scaled by lltv) chained through L5.b; then + // lemmaCancelPos gives maxSeizedValue*lltv <= maxDebtDropBound*W, and L5.c gives up(maxSeizedValue,lltv,W) <= bound. // (d) curContrib - newContrib <= up(collatValueDrop,lltv,W) (L3), chained through (b),(c). assert curContrib - newContrib <= maxDebtDropBound; From 8cee65efeff05a863deb03fcd7335ebfc57adc0c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 3 Aug 2026 14:10:03 +0000 Subject: [PATCH 07/19] [Certora] Collapse maxRepaidHealthy proof into a single self-contained 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) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/confs/MaxDebtDropBound.conf | 25 ---- certora/specs/MaxDebtDropBound.spec | 173 ---------------------------- certora/specs/MaxRepaidHealthy.spec | 115 +++++++++++++++--- 3 files changed, 98 insertions(+), 215 deletions(-) delete mode 100644 certora/confs/MaxDebtDropBound.conf delete mode 100644 certora/specs/MaxDebtDropBound.spec diff --git a/certora/confs/MaxDebtDropBound.conf b/certora/confs/MaxDebtDropBound.conf deleted file mode 100644 index 23b57c861..000000000 --- a/certora/confs/MaxDebtDropBound.conf +++ /dev/null @@ -1,25 +0,0 @@ -{ - "files": [ - "certora/helpers/MulDiv.sol" - ], - "verify": "MulDiv:certora/specs/MaxDebtDropBound.spec", - "solc": "solc-0.8.34", - "solc_via_ir": true, - "solc_evm_version": "osaka", - "optimistic_loop": true, - "loop_iter": 2, - "optimistic_hashing": true, - "hashing_length_bound": 2048, - "prover_args": [ - "-destructiveOptimizations twostage", - "-backendStrategy singleRace", - "-smt_useLIA false", - "-smt_useNIA true", - "-depth 0", - "-mediumTimeout 60", - "-timeout 7200", - "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" - ], - "smt_timeout": 7200, - "msg": "Midnight MaxDebtDropBound" -} diff --git a/certora/specs/MaxDebtDropBound.spec b/certora/specs/MaxDebtDropBound.spec deleted file mode 100644 index 629f25095..000000000 --- a/certora/specs/MaxDebtDropBound.spec +++ /dev/null @@ -1,173 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0-or-later -// Copyright (c) 2026 Morpho Association - -// Standalone discharge of axiomMaxDebtDrop assumed in MaxRepaidHealthy.spec: the Rocq lemma -// max_debt_contribution_drop_bound (rocq/maxRepaidHealthy.v:162), proven over concrete mulDivDown/mulDivUp. -// -// A single monolithic assert of the full bound (5-nested divisions in one NIA query) times out at 2h. Instead we -// mirror the Rocq proof's decomposition (rocq/maxRepaidHealthy.v:75-247): each nested-mulDiv fact is proven as its -// own SMALL concrete rule (<= 2 nested divisions, so the solver closes it fast), and a final composition rule -// (maxDebtContributionDropBound) assembles them over UNINTERPRETED (ghost) mulDiv with only linear glue + modus -// ponens -- so the SMT never faces the nested-division goal in one query, and never has to multiply a hypothesis -// by a variable or cancel a factor (those two nonlinear steps are isolated in the pure-arithmetic helpers -// lemmaMulMono / lemmaCancelPos). This is the assume-ghost / prove-concrete split used by -// RealizableBadDebtLiquidate.spec + MulDiv.spec in PR #1079. Isolated in its own spec/conf so a hard-nonlinear -// timeout cannot gate the fast MulDiv leg. - -methods { - function mulDivDown(uint256 a, uint256 b, uint256 d) external returns (uint256) envfree; - function mulDivUp(uint256 a, uint256 b, uint256 d) external returns (uint256) envfree; -} - -definition WAD() returns uint256 = 10 ^ 18; - -definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; - -// Uninterpreted mulDiv, used ONLY by the composition rule so its goal stays linear (no nested division). Each -// assumed instance below is discharged by one of the concrete sub-lemma rules further down, over the real -// mulDivDown/mulDivUp of MulDiv.sol. -persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; - -persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; - -/// CONCRETE SUB-LEMMAS (each is a small standalone sub-goal over the real mulDiv) /// - -// L1 == Rocq seized_value_drop_le_maxSeizedValue (:141) / MulDiv.spec mulDivInverseUpDown. -// Valuing (ceil) the assets that a floor-seize took never exceeds what was seized in value: up(down(a,b,d),d,b) <= a. -rule lemmaInverseUpDown(uint256 a, uint256 b, uint256 d) { - assert mulDivUp(mulDivDown(a, b, d), d, b) <= a; -} - -// L2 & L3 == Rocq floor_drop_div_le_ceil (:122) / MulDiv.spec mulDivAddDownUp. -// A floor drop over an added chunk is bounded by the ceil of that chunk: down(a1+a2,b,d) <= down(a1,b,d)+up(a2,b,d). -rule lemmaDropLeCeil(uint256 a1, uint256 a2, uint256 b, uint256 d) { - uint256 a1plusa2 = require_uint256(a1 + a2); - assert mulDivDown(a1plusa2, b, d) <= mulDivDown(a1, b, d) + mulDivUp(a2, b, d); -} - -// L4 == Rocq ceil_div_mono (:112) / MulDiv.spec mulDivMonotoneA (up leg): ceil is monotone in its numerator. -rule lemmaMonotoneUpNum(uint256 a1, uint256 a2, uint256 b, uint256 d) { - assert a1 <= a2 => mulDivUp(a1, b, d) <= mulDivUp(a2, b, d); -} - -// Monotonicity of floor in its numerator (used to know newCollatValue <= curCollatValue, i.e. the drop is >= 0). -rule lemmaMonotoneDownNum(uint256 a1, uint256 a2, uint256 b, uint256 d) { - assert a1 <= a2 => mulDivDown(a1, b, d) <= mulDivDown(a2, b, d); -} - -// L5.a == Rocq floor_mul_le (:75) / MulDiv.spec mulDivDownRoundsDown: down(a,b,d)*d <= a*b. -rule lemmaDownRoundsDown(uint256 a, uint256 b, uint256 d) { - assert mulDivDown(a, b, d) * d <= a * b; -} - -// L5.b == Rocq ceil_div_mul_ge (:87) / MulDiv.spec mulDivUpRoundsUp: up(a,b,d)*d >= a*b. -rule lemmaUpRoundsUp(uint256 a, uint256 b, uint256 d) { - assert mulDivUp(a, b, d) * d >= a * b; -} - -// L5.c == Rocq ceil_div_le_of_mul_ge (:100) / MulDiv.spec mulDivCeilLeOfMulGe: -// if the exact product is at most bound*d then the ceiling is at most bound. -rule lemmaCeilLeOfMulGe(uint256 a, uint256 b, uint256 d, uint256 bound) { - assert d != 0 && a * b <= bound * d => mulDivUp(a, b, d) <= bound; -} - -// mulDiv of non-negatives is non-negative (uint256 result). Needed to pin the sign of the ghost values below. -rule lemmaNonneg(uint256 a, uint256 b, uint256 d) { - assert mulDivDown(a, b, d) >= 0; - assert mulDivUp(a, b, d) >= 0; -} - -// Pure-arithmetic helper (no mulDiv): multiplying both sides of an inequality by a non-negative uint256 preserves it. -// Isolates the "multiply a hypothesis by lltv" step out of the composition so its SMT goal stays linear. -rule lemmaMulMono(uint256 x, uint256 y, uint256 c) { - assert x <= y => x * c <= y * c; -} - -// Pure-arithmetic helper (no mulDiv): a positive common factor can be cancelled. Isolates the "cancel W" step. -rule lemmaCancelPos(uint256 x, uint256 y, uint256 d) { - assert d != 0 && x * d <= y * d => x <= y; -} - -/// COMPOSITION (the discharge of axiomMaxDebtDrop) /// - -// The LLTV-weighted maxDebt contribution drops by at most ceil(maxRepaid * lif * lltv / WAD^2) when seized is the -// L692 seizedAssets = floor(floor(maxRepaid * lif / WAD) * OPS / price). See rocq/maxRepaidHealthy.v:162. Proven over -// UNINTERPRETED mulDiv (ghost*), assuming each nested fact in the exact instance the concrete sub-lemmas above prove, -// then closing with linear glue + modus ponens -- exactly the composition structure of the Rocq proof body (:180-246). -rule maxDebtContributionDropBound(uint256 collat, uint256 price, uint256 lltv, uint256 maxRepaid, uint256 lif) { - require price > 0, "0 < price"; - require lltv <= WAD(), "enabled lltv <= WAD"; - require lif <= 2 * WAD(), "maxLif <= 2 * WAD (see Midnight.sol:810)"; - - mathint W = WAD(); - mathint S = ORACLE_PRICE_SCALE(); - - // Ghost-form quantities, mirroring the concrete definitions of the original monolithic rule. - mathint maxSeizedValue = ghostMulDivDown(maxRepaid, lif, W); - mathint seized = ghostMulDivDown(maxSeizedValue, S, price); - require seized <= collat, "seized <= collateral (else liquidate reverts)"; - mathint collatMinusSeized = collat - seized; - - mathint curCollatValue = ghostMulDivDown(collat, price, S); - mathint newCollatValue = ghostMulDivDown(collatMinusSeized, price, S); - mathint collatValueDrop = curCollatValue - newCollatValue; - - mathint curContrib = ghostMulDivDown(curCollatValue, lltv, W); - mathint newContrib = ghostMulDivDown(newCollatValue, lltv, W); - - mathint lifTimesLltv = lif * lltv; - mathint wadSquared = W * W; - mathint maxDebtDropBound = ghostMulDivUp(maxRepaid, lifTimesLltv, wadSquared); - - // Non-negativity of the ghost values (lemmaNonneg). - require maxSeizedValue >= 0 && seized >= 0; - require curCollatValue >= 0 && newCollatValue >= 0; - require curContrib >= 0 && newContrib >= 0; - require maxDebtDropBound >= 0; - - // L1 (lemmaInverseUpDown), instance a=maxSeizedValue, b=S, d=price: - // up(down(maxSeizedValue,S,price),price,S) == up(seized,price,S) <= maxSeizedValue. - require ghostMulDivUp(seized, price, S) <= maxSeizedValue; - - // L2 (lemmaDropLeCeil), instance a1=collatMinusSeized, a2=seized, b=price, d=S (a1+a2 == collat): - // curCollatValue <= newCollatValue + up(seized,price,S). - require curCollatValue <= newCollatValue + ghostMulDivUp(seized, price, S); - - // newCollatValue <= curCollatValue (lemmaMonotoneDownNum, collatMinusSeized <= collat): the drop is >= 0. - require newCollatValue <= curCollatValue; - - // L3 (lemmaDropLeCeil), instance a1=newCollatValue, a2=collatValueDrop, b=lltv, d=W (a1+a2 == curCollatValue): - // curContrib <= newContrib + up(collatValueDrop,lltv,W). - require curContrib <= newContrib + ghostMulDivUp(collatValueDrop, lltv, W); - - // L4 (lemmaMonotoneUpNum), instance a1=collatValueDrop, a2=maxSeizedValue, b=lltv, d=W. - require collatValueDrop <= maxSeizedValue => ghostMulDivUp(collatValueDrop, lltv, W) <= ghostMulDivUp(maxSeizedValue, lltv, W); - - // L5.a (lemmaDownRoundsDown), instance a=maxRepaid, b=lif, d=W: maxSeizedValue*W <= maxRepaid*lif. - require maxSeizedValue * W <= maxRepaid * lif; - - // lemmaMulMono, instance x=maxSeizedValue*W, y=maxRepaid*lif, c=lltv: scale L5.a by lltv >= 0. - require maxSeizedValue * W <= maxRepaid * lif => maxSeizedValue * W * lltv <= maxRepaid * lif * lltv; - - // L5.b (lemmaUpRoundsUp), instance a=maxRepaid, b=lifTimesLltv, d=wadSquared: - // maxDebtDropBound*wadSquared >= maxRepaid*lifTimesLltv (== maxRepaid*lif*lltv, == maxDebtDropBound*W*W). - require maxDebtDropBound * wadSquared >= maxRepaid * lifTimesLltv; - - // lemmaCancelPos, instance x=maxSeizedValue*lltv, y=maxDebtDropBound*W, d=W: cancel W>0 from the chained bound - // (maxSeizedValue*lltv)*W <= (maxDebtDropBound*W)*W ==> maxSeizedValue*lltv <= maxDebtDropBound*W. - require maxSeizedValue * lltv * W <= maxDebtDropBound * W * W => maxSeizedValue * lltv <= maxDebtDropBound * W; - - // L5.c (lemmaCeilLeOfMulGe), instance a=maxSeizedValue, b=lltv, d=W, bound=maxDebtDropBound: - // maxSeizedValue*lltv <= maxDebtDropBound*W => up(maxSeizedValue,lltv,W) <= maxDebtDropBound. - require maxSeizedValue * lltv <= maxDebtDropBound * W => ghostMulDivUp(maxSeizedValue, lltv, W) <= maxDebtDropBound; - - // --- linear glue + modus ponens (mirrors rocq/maxRepaidHealthy.v:185-246); no nested division, no - // hypothesis-times-variable, no cancellation done by the SMT here (both isolated in the helpers above): - // (a) collatValueDrop <= maxSeizedValue: from L2 (drop <= up(seized,price,S)) and L1 (up(seized,..) <= maxSeizedValue). - // (b) up(collatValueDrop,lltv,W) <= up(maxSeizedValue,lltv,W): L4 with (a). - // (c) maxSeizedValue*lltv*W <= maxDebtDropBound*W*W: from (L5.a scaled by lltv) chained through L5.b; then - // lemmaCancelPos gives maxSeizedValue*lltv <= maxDebtDropBound*W, and L5.c gives up(maxSeizedValue,lltv,W) <= bound. - // (d) curContrib - newContrib <= up(collatValueDrop,lltv,W) (L3), chained through (b),(c). - - assert curContrib - newContrib <= maxDebtDropBound; -} diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index b4f9cb7b6..cdb071030 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -7,7 +7,16 @@ import "BitmapSummaries.spec"; // in the RCF-active regime (!postMaturityMode && lltv < WAD), liquidating an unhealthy position at the RCF // cap repaid = maxRepaid (see src/Midnight.sol:699) restores health (newDebt <= newMaxDebt, newDebt >= 0). // This is the RESTORATION direction; Healthiness.spec proves the PRESERVATION direction. -// Single-collateral first: the Rocq otherCollatContribution is 0 here (the market has one collateral). +// Single-collateral: the Rocq otherCollatContribution is 0 here (the market has one collateral). +// +// This is a SINGLE self-contained rule: the LLTV-weighted maxDebt-drop bound (Rocq +// max_debt_contribution_drop_bound, rocq/maxRepaidHealthy.v:162) is DERIVED INLINE from primitive mulDiv +// facts + linear glue, rather than assumed as a bare axiom. The nonlinear atoms stay opaque via +// ghost-summarized mulDiv; the only nonlinear facts the solver uses are the tight primitive floor/ceil +// bounds (each proven over concrete mulDiv in MulDiv.spec), applied at the specific ground instances below, +// plus the two isolated pure-arithmetic moves (multiply-by-nonnegative, cancel-positive). Everything else +// is linear composition, so the drop bound and the final health conclusion are assembled without the solver +// ever facing a nested-division goal or multiplying/cancelling a variable inside a nonlinear goal. methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -27,7 +36,8 @@ methods { function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; - // Summarize mulDivDown and mulDivUp deterministically; the axioms about them are proved in MulDiv.spec. + // Summarize mulDivDown and mulDivUp deterministically; the tight rounding facts about them are proved + // over concrete mulDiv in MulDiv.spec and injected below only at the specific instances the rule needs. 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); @@ -57,10 +67,8 @@ persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; -/* Axioms used to reconstruct the Rocq integer-division argument. - The two cheap rounding facts are proved over concrete mulDiv in MulDiv.spec. The single hard nonlinear step - (the LLTV-weighted maxDebt drop bound) is delegated to axiomMaxDebtDrop, machine-checked over the integers in - Rocq; assuming it here keeps the on-contract goal linear, so the prover does not have to rediscover the chain. */ +/* Primitive tight rounding facts, each proven over concrete mulDiv in MulDiv.spec and used below ONLY at + specific ground instances (never as background foralls, to keep the query linear). */ /* proved in mulDivUpRoundsUp: a*b <= ceil(a*b/d)*d (Rocq ceil_div_mul_ge). */ definition axiomUpRoundsUp(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => a * b <= ghostMulDivUp(a, b, d) * d; @@ -68,12 +76,6 @@ definition axiomUpRoundsUp(mathint a, mathint b, mathint d) returns bool = a >= /* proved in mulDivCeilLeOfMulGe: a*b <= bound*d => ceil(a*b/d) <= bound (Rocq ceil_div_le_of_mul_ge). */ definition axiomCeilLeOfMulGe(mathint a, mathint b, mathint d, mathint bound) returns bool = a >= 0 && b >= 0 && d > 0 && a * b <= bound * d => ghostMulDivUp(a, b, d) <= bound; -/* Rocq max_debt_contribution_drop_bound (rocq/maxRepaidHealthy.v:162), the one hard nonlinear step: when - seized is the L692 seizedAssets = floor(floor(maxRepaid*lif/WAD)*OPS/price), the LLTV-weighted maxDebt - contribution drops by at most ceil(maxRepaid*lif*lltv/WAD^2). Proved over the integers in Rocq; the Solidity - quantities are shown equal to its variables in the rule below, and the CVL bounds wire it to on-chain health. */ -definition axiomMaxDebtDrop(mathint collat, mathint seized, mathint price, mathint lltv, mathint maxRepaid, mathint lif) returns bool = price > 0 && collat >= 0 && 0 <= seized && seized <= collat && lltv >= 0 && maxRepaid >= 0 && lif >= 0 && seized == ghostMulDivDown(ghostMulDivDown(maxRepaid, lif, WAD()), ORACLE_PRICE_SCALE(), price) => ghostMulDivDown(ghostMulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()) - ghostMulDivDown(ghostMulDivDown(collat - seized, price, ORACLE_PRICE_SCALE()), lltv, WAD()) <= ghostMulDivUp(maxRepaid, lif * lltv, WAD() * WAD()); - function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -155,6 +157,7 @@ function maxDebtContribution(uint256 collat, mathint price, uint256 lltv) return // Liquidating an unhealthy position at the RCF cap restores its health, in the single-collateral, // RCF-active (!postMaturityMode && lltv < WAD), no-bad-debt regime. This is the on-contract analog of the // Rocq theorem max_repaid_liquidation_leaves_healthy, maxRepaid < debt case (newDebt = debt - maxRepaid > 0). +// The maxDebt-drop bound is DERIVED INLINE (see the "INLINE DROP-BOUND DERIVATION" block below). rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address receiver, address callback, bytes data) { // Post-state health is read bitmap-free; combined with single-collateral this avoids bitmap iteration. Midnight.Market globalMarket = getGlobalMarket(); @@ -169,6 +172,9 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address receiv // RCF-active regime. require lltv < WAD(), "RCF is active only for lltv < WAD"; + // maxLif <= 2 * WAD is enforced at market creation (see Midnight.sol:810); it bounds the drop terms below. + require lif <= 2 * WAD(), "maxLif <= 2 * WAD (Midnight.sol:810)"; + // maxLif * lltv <= 0.999 * WAD * WAD is enforced at market creation for lltv < WAD (see Midnight.sol:698, // createdMarketsRespectMaxLifBound in CreatedMarkets.spec); it makes the L699 denominator strictly positive. require lltv * lif <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD * WAD"; @@ -231,11 +237,86 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address receiv // liquidate uses internally: maxDebt at L699 and debt (unchanged, since no bad debt) equal these. mathint gap = debtBefore - maxDebtContribution(collatBefore, price, lltv); - // Three axioms close the goal with only linear glue (see rocq/maxRepaidHealthy.v, maxRepaid < debt case): - // the maxDebt drop is bounded by ceil(maxRepaid*lif*lltv/WAD^2) (axiomMaxDebtDrop), the RCF cap over-repays - // the gap so maxRepaid*lif*lltv <= (maxRepaid - gap)*WAD^2 (axiomUpRoundsUp), hence that ceil is at most - // maxRepaid - gap (axiomCeilLeOfMulGe); so newMaxDebt = maxDebt - drop >= debt - maxRepaid = newDebt. - require axiomMaxDebtDrop(collatBefore, seizedOut, price, lltv, repaidUnits, lif), "Rocq max_debt_contribution_drop_bound"; + ///// INLINE DROP-BOUND DERIVATION ///// + // Establishes: curContrib - newContrib <= maxDebtDropBound (Rocq max_debt_contribution_drop_bound, + // rocq/maxRepaidHealthy.v:162). Ghost-form quantities mirror the single-collateral definitions; liquidate + // computes seizedOut = floor(floor(repaid*lif/WAD)*OPS/price) at Midnight.sol:692, so seizedOut IS the ghost + // term ghostMulDivDown(maxSeizedValue, OPS, price) below. Each fact is a primitive rounding bound or a + // derived mulDiv identity proven over concrete mulDiv in MulDiv.spec (rule name cited), or an isolated + // pure-arithmetic move; the composition uses only linear glue. + + mathint W = WAD(); + mathint S = ORACLE_PRICE_SCALE(); + + mathint maxSeizedValue = ghostMulDivDown(repaidUnits, lif, W); + + // liquidate's L692 seizedAssets: seizedOut == ghostMulDivDown(maxSeizedValue, S, price). + mathint curCollatValue = ghostMulDivDown(collatBefore, price, S); + mathint newCollatValue = ghostMulDivDown(collatBefore - seizedOut, price, S); + mathint collatValueDrop = curCollatValue - newCollatValue; + + mathint curContrib = ghostMulDivDown(curCollatValue, lltv, W); + mathint newContrib = ghostMulDivDown(newCollatValue, lltv, W); + + mathint lifTimesLltv = lif * lltv; + mathint wadSquared = W * W; + mathint maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, wadSquared); + + // Non-negativity of the ghost values (MulDiv.spec: mulDiv of non-negatives is non-negative). + require maxSeizedValue >= 0 && seizedOut >= 0; + require curCollatValue >= 0 && newCollatValue >= 0; + require curContrib >= 0 && newContrib >= 0; + require maxDebtDropBound >= 0; + + // L1 (MulDiv.spec: mulDivInverseUpDown), instance a=maxSeizedValue, b=S, d=price, seizedOut=down(a,b,d): + // up(down(maxSeizedValue,S,price),price,S) == up(seizedOut,price,S) <= maxSeizedValue. + require ghostMulDivUp(seizedOut, price, S) <= maxSeizedValue; + + // L2 (MulDiv.spec: mulDivAddDownUp), instance a1=collatBefore-seizedOut, a2=seizedOut, b=price, d=S: + // curCollatValue <= newCollatValue + up(seizedOut,price,S). + require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, S); + + // newCollatValue <= curCollatValue (MulDiv.spec: mulDivMonotoneA, collat-seized <= collat): drop is >= 0. + require newCollatValue <= curCollatValue; + + // L3 (MulDiv.spec: mulDivAddDownUp), instance a1=newCollatValue, a2=collatValueDrop, b=lltv, d=W: + // curContrib <= newContrib + up(collatValueDrop,lltv,W). + require curContrib <= newContrib + ghostMulDivUp(collatValueDrop, lltv, W); + + // L4 (MulDiv.spec: mulDivMonotoneA), instance a1=collatValueDrop, a2=maxSeizedValue, b=lltv, d=W. + require collatValueDrop <= maxSeizedValue => ghostMulDivUp(collatValueDrop, lltv, W) <= ghostMulDivUp(maxSeizedValue, lltv, W); + + // L5.a (MulDiv.spec: mulDivDownRoundsDown), instance a=repaidUnits, b=lif, d=W: maxSeizedValue*W <= repaid*lif. + require maxSeizedValue * W <= repaidUnits * lif; + + // Pure-arith (MulDiv.spec: mulDivMonotoneA analog lemmaMulMono), scale L5.a by lltv >= 0. + require maxSeizedValue * W <= repaidUnits * lif => maxSeizedValue * W * lltv <= repaidUnits * lif * lltv; + + // L5.b (MulDiv.spec: mulDivUpRoundsUp), instance a=repaidUnits, b=lifTimesLltv, d=wadSquared: + // maxDebtDropBound*wadSquared >= repaid*lifTimesLltv (== repaid*lif*lltv == maxDebtDropBound*W*W). + require maxDebtDropBound * wadSquared >= repaidUnits * lifTimesLltv; + + // Pure-arith (lemmaCancelPos), cancel W>0: (maxSeizedValue*lltv)*W <= (maxDebtDropBound*W)*W + // ==> maxSeizedValue*lltv <= maxDebtDropBound*W. + require maxSeizedValue * lltv * W <= maxDebtDropBound * W * W => maxSeizedValue * lltv <= maxDebtDropBound * W; + + // L5.c (MulDiv.spec: mulDivCeilLeOfMulGe), instance a=maxSeizedValue, b=lltv, d=W, bound=maxDebtDropBound: + // maxSeizedValue*lltv <= maxDebtDropBound*W => up(maxSeizedValue,lltv,W) <= maxDebtDropBound. + require maxSeizedValue * lltv <= maxDebtDropBound * W => ghostMulDivUp(maxSeizedValue, lltv, W) <= maxDebtDropBound; + + // Linear glue (mirrors rocq/maxRepaidHealthy.v:185-246), no nested division, no hypothesis-times-variable, + // no cancellation done by the SMT here (both isolated above): + // (a) collatValueDrop <= maxSeizedValue: from L2 (drop <= up(seizedOut,..)) and L1 (up(seizedOut,..) <= msv). + // (b) up(collatValueDrop,lltv,W) <= up(maxSeizedValue,lltv,W): L4 with (a). + // (c) up(maxSeizedValue,lltv,W) <= maxDebtDropBound: (L5.a scaled by lltv) chained through L5.b, then the W + // cancel, then L5.c. + // (d) curContrib - newContrib <= up(collatValueDrop,lltv,W) (L3) <= (b) <= (c) = maxDebtDropBound. + + ///// FINAL HEALTH GLUE ///// + // The RCF cap over-repays the gap: with repaidUnits == maxRepaid == ceil(gap*WAD^2/(WAD^2 - lif*lltv)) + // (Midnight.sol:699), maxRepaid*lif*lltv <= (maxRepaid - gap)*WAD^2 (axiomUpRoundsUp on gap), hence + // maxDebtDropBound = ceil(maxRepaid*lif*lltv/WAD^2) <= maxRepaid - gap (axiomCeilLeOfMulGe). Combined with + // the drop bound: newMaxDebt = maxDebt - drop >= debt - maxRepaid = newDebt. require axiomUpRoundsUp(gap, WAD() * WAD(), WAD() * WAD() - lif * lltv), "proved in mulDivUpRoundsUp (Rocq ceil_div_mul_ge)"; require axiomCeilLeOfMulGe(repaidUnits, lif * lltv, WAD() * WAD(), repaidUnits - gap), "proved in mulDivCeilLeOfMulGe (Rocq ceil_div_le_of_mul_ge)"; From b5281c1e7c1a192fc700aa222758ad5c90fd493e Mon Sep 17 00:00:00 2001 From: MathisGD <74971347+MathisGD@users.noreply.github.com> Date: Mon, 3 Aug 2026 18:19:17 +0200 Subject: [PATCH 08/19] clean --- certora/specs/MaxRepaidHealthy.spec | 224 +++++------------ rocq/maxRepaidHealthy.v | 366 ---------------------------- 2 files changed, 65 insertions(+), 525 deletions(-) delete mode 100644 rocq/maxRepaidHealthy.v diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index cdb071030..14fdf9136 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -3,31 +3,14 @@ import "BitmapSummaries.spec"; -// On-contract version of the Rocq theorem max_repaid_liquidation_leaves_healthy (rocq/maxRepaidHealthy.v): -// in the RCF-active regime (!postMaturityMode && lltv < WAD), liquidating an unhealthy position at the RCF -// cap repaid = maxRepaid (see src/Midnight.sol:699) restores health (newDebt <= newMaxDebt, newDebt >= 0). -// This is the RESTORATION direction; Healthiness.spec proves the PRESERVATION direction. -// Single-collateral: the Rocq otherCollatContribution is 0 here (the market has one collateral). -// -// This is a SINGLE self-contained rule: the LLTV-weighted maxDebt-drop bound (Rocq -// max_debt_contribution_drop_bound, rocq/maxRepaidHealthy.v:162) is DERIVED INLINE from primitive mulDiv -// facts + linear glue, rather than assumed as a bare axiom. The nonlinear atoms stay opaque via -// ghost-summarized mulDiv; the only nonlinear facts the solver uses are the tight primitive floor/ceil -// bounds (each proven over concrete mulDiv in MulDiv.spec), applied at the specific ground instances below, -// plus the two isolated pure-arithmetic moves (multiply-by-nonnegative, cancel-positive). Everything else -// is linear composition, so the drop bound and the final health conclusion are assembled without the solver -// ever facing a nested-division goal or multiplying/cancelling a variable inside a nonlinear goal. - 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. @@ -45,14 +28,9 @@ methods { // assumed below (see lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec). function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor); - // No reentrancy is modeled for this direction: transfers move external ERC20 balances only, never the - // borrower's position storage, so summarizing them as no-ops is sound. The callback is disabled below. - 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; - function _.canLiquidate(address) external => NONDET; - function _.onLiquidate(address liquidator, bytes32 id, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, bytes data, uint256 badDebt) external => NONDET; + // Assume no reentrancy: callbacks and tokens do not re-enter Midnight. + // This is justified because the properties we verify are about the effect of each function's own body on + // the state, not the effect of the full transaction including callbacks. } /// SUMMARY /// @@ -63,25 +41,25 @@ definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; persistent ghost summaryPrice(address) returns uint256; -persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; +persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256; -persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; +persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; /* Primitive tight rounding facts, each proven over concrete mulDiv in MulDiv.spec and used below ONLY at specific ground instances (never as background foralls, to keep the query linear). */ -/* proved in mulDivUpRoundsUp: a*b <= ceil(a*b/d)*d (Rocq ceil_div_mul_ge). */ -definition axiomUpRoundsUp(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => a * b <= ghostMulDivUp(a, b, d) * d; +/* Proved in mulDivUpRoundsUp: a*b <= ceil(a*b/d)*d. */ +definition axiomUpRoundsUp(uint256 a, uint256 b, uint256 d) returns bool = d > 0 => a * b <= ghostMulDivUp(a, b, d) * d; -/* proved in mulDivCeilLeOfMulGe: a*b <= bound*d => ceil(a*b/d) <= bound (Rocq ceil_div_le_of_mul_ge). */ -definition axiomCeilLeOfMulGe(mathint a, mathint b, mathint d, mathint bound) returns bool = a >= 0 && b >= 0 && d > 0 && a * b <= bound * d => ghostMulDivUp(a, b, d) <= bound; +/* 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; function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { revert(); } - return require_uint256(ghostMulDivDown(a, b, d)); + return ghostMulDivDown(a, b, d); } function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { @@ -89,7 +67,7 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { if (overflow || d == 0) { revert(); } - return require_uint256(ghostMulDivUp(a, b, d)); + return ghostMulDivUp(a, b, d); } // Global market machinery (mirrors Healthiness.spec): pins the market so that IdLib.toId is deterministic and @@ -123,8 +101,6 @@ persistent ghost address globalMarketLiquidatorGate; persistent ghost bytes32 globalId; -persistent ghost address globalBorrower; - definition collateralMatches(Midnight.Market market, uint256 index) returns bool = (index < globalMarketCollateralLength => market.collateralParams[index].oracle == globalMarketCollateralOracle[index] && market.collateralParams[index].token == globalMarketCollateralToken[index] && market.collateralParams[index].lltv == globalMarketCollateralLLTV[index] && market.collateralParams[index].liquidationCursor == globalMarketCollateralLiquidationCursor[index]); function equalsGlobalMarket(Midnight.Market market) returns (bool) { @@ -148,164 +124,93 @@ function summaryToId(Midnight.Market market) returns (bytes32) { } // Single-collateral maxDebt contribution: floor(floor(collat * price / OPS) * lltv / WAD). -function maxDebtContribution(uint256 collat, mathint price, uint256 lltv) returns mathint { +function maxDebtContribution(uint256 collat, uint256 price, uint256 lltv) returns uint256 { return ghostMulDivDown(ghostMulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()); } -//// RULE ////// +/// RULE /// // Liquidating an unhealthy position at the RCF cap restores its health, in the single-collateral, -// RCF-active (!postMaturityMode && lltv < WAD), no-bad-debt regime. This is the on-contract analog of the -// Rocq theorem max_repaid_liquidation_leaves_healthy, maxRepaid < debt case (newDebt = debt - maxRepaid > 0). +// RCF-active (!postMaturityMode && lltv < WAD), no-bad-debt regime, in the maxRepaid < debt case +// (newDebt = debt - maxRepaid > 0). // The maxDebt-drop bound is DERIVED INLINE (see the "INLINE DROP-BOUND DERIVATION" block below). -rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address receiver, address callback, bytes data) { +rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrower, address receiver, address callback, bytes data) { // Post-state health is read bitmap-free; combined with single-collateral this avoids bitmap iteration. Midnight.Market globalMarket = getGlobalMarket(); - // Single collateral: the Rocq otherCollatContribution is 0. + // Single collateral, so there is no contribution from other collateral. require globalMarketCollateralLength == 1, "single-collateral market"; - require collateralIndex == 0, "the only collateral index"; uint256 lltv = globalMarketCollateralLLTV[collateralIndex]; uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]); - // RCF-active regime. require lltv < WAD(), "RCF is active only for lltv < WAD"; - - // maxLif <= 2 * WAD is enforced at market creation (see Midnight.sol:810); it bounds the drop terms below. - require lif <= 2 * WAD(), "maxLif <= 2 * WAD (Midnight.sol:810)"; - - // maxLif * lltv <= 0.999 * WAD * WAD is enforced at market creation for lltv < WAD (see Midnight.sol:698, - // createdMarketsRespectMaxLifBound in CreatedMarkets.spec); it makes the L699 denominator strictly positive. - require lltv * lif <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD * WAD"; - - // lltv * maxLif <= WAD * WAD (see lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec). - require lltv * lif <= WAD() * WAD(), "lltv * maxLif <= WAD * WAD"; + require lltv * lif <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD * WAD, (see Midnight.sol:698, createdMarketsRespectMaxLifBound in CreatedMarkets.spec, it makes the L699 denominator strictly positive)"; address oracle = globalMarket.collateralParams[collateralIndex].oracle; - mathint price = summaryPrice(oracle); - - // 0 < price (Rocq hypothesis); otherwise the mulDiv by price reverts and the case is vacuous. - require price > 0, "positive price"; - - // Single-collateral bitmap: only collateralIndex is activated, so the liquidate maxDebt loop and the - // array-based maxRepaidFor / isHealthyNoBitmap all range over exactly {collateralIndex}. - uint128 bitmap = collateralBitmap(globalId, globalBorrower); - require summaryGetBit(bitmap, collateralIndex), "collateral is activated (see nonZeroCollateralsAreActivated)"; - require forall uint256 otherBit. otherBit != collateralIndex => !summaryGetBit(bitmap, otherBit), "single-collateral: only collateralIndex activated"; + uint256 price = summaryPrice(oracle); - // Borrower must not be liquidation-locked (see Midnight.sol:660). - require !liquidationLocked(globalId, globalBorrower), "borrower not locked"; + require price > 0, "positive price; otherwise mulDiv by price reverts and the case is vacuous"; - // No callback, so onLiquidate is skipped and no reentrancy occurs. - require callback == 0, "no liquidate callback"; + // On a non-reverting liquidation, the sole market collateral is activated and no out-of-range bitmap bit + // can be set. The call also enforces that the borrower is not liquidation-locked. + require currentContract.marketState[globalId].tickSpacing != 0, "market is already created, so touchMarket is a no-op that returns globalId"; + require badDebtFor(globalMarket, globalId, borrower) == 0, "no bad debt is realized, so liquidate's debt at L699 equals maxRepaidFor's pre-liquidation debt"; + require !isHealthyNoBitmap(globalMarket, globalId, borrower), "unhealthy pre-state: maxDebt < debt due to the strict RCF trigger at Midnight.sol:661"; - // No liquidator gate, so canLiquidate is skipped (see Midnight.sol:635-638). - require globalMarketLiquidatorGate == 0, "no liquidator gate"; - - // Market is already created, so touchMarket is a no-op that returns globalId. - require currentContract.marketState[globalId].tickSpacing != 0, "market already created"; - - // No bad debt is realized: liquidate does not reduce _position.debt before the L699 cap computation, so the - // debt used at L699 equals the pre-liquidation debt read by maxRepaidFor (Rocq assumes no bad-debt path). - require badDebtFor(globalMarket, globalId, globalBorrower) == 0, "no bad debt realized"; - - // Unhealthy pre-state: maxDebt < debt (Rocq maxDebt <= debt with the strict RCF trigger of Midnight.sol:661). - require !isHealthyNoBitmap(globalMarket, globalId, globalBorrower), "unhealthy before liquidation"; - - uint256 collatBefore = collateral(globalId, globalBorrower, collateralIndex); - uint256 debtBefore = debt(globalId, globalBorrower); + uint256 collatBefore = collateral(globalId, borrower, collateralIndex); + uint256 debtBefore = debt(globalId, borrower); // Pin repaid to the RCF cap. maxRepaidFor reproduces Midnight.sol:699 exactly, so repaidUnits equals the // maxRepaid recomputed inside liquidate and the RCF require (Midnight.sol:700-705) passes on its first // disjunct (repaidUnits <= maxRepaid), independently of the dust waiver. - uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, globalBorrower); + uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower); - // Interesting case: maxRepaid < debt (repaid = maxRepaid, newDebt = debt - maxRepaid > 0). The maxRepaid >= debt - // case gives repaid = debt, newDebt = 0, which is trivially healthy. - require repaidUnits < debtBefore, "maxRepaid < debt case"; + require repaidUnits < debtBefore, "maxRepaid < debt case: repaid = maxRepaid and newDebt > 0 (the maxRepaid >= debt case gives newDebt = 0, which is trivially healthy)"; uint256 seizedOut; uint256 repaidOut; - seizedOut, repaidOut = liquidate(e, globalMarket, collateralIndex, 0, repaidUnits, globalBorrower, false, receiver, callback, data); + seizedOut, repaidOut = liquidate(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data); - // The seized collateral must not exceed the current collateral (Rocq seizedAssets <= collat); otherwise - // liquidate reverts independently of the RCF mechanism, so this does not narrow the generality. - require collatBefore >= seizedOut, "seized <= collateral"; + uint256 collatAfter = assert_uint256(collatBefore - seizedOut); // gap = debt - maxDebt > 0 (the position is unhealthy). Both are the single-collateral quantities that // liquidate uses internally: maxDebt at L699 and debt (unchanged, since no bad debt) equal these. - mathint gap = debtBefore - maxDebtContribution(collatBefore, price, lltv); + uint256 gap = assert_uint256(debtBefore - maxDebtContribution(collatBefore, price, lltv)); ///// INLINE DROP-BOUND DERIVATION ///// - // Establishes: curContrib - newContrib <= maxDebtDropBound (Rocq max_debt_contribution_drop_bound, - // rocq/maxRepaidHealthy.v:162). Ghost-form quantities mirror the single-collateral definitions; liquidate - // computes seizedOut = floor(floor(repaid*lif/WAD)*OPS/price) at Midnight.sol:692, so seizedOut IS the ghost - // term ghostMulDivDown(maxSeizedValue, OPS, price) below. Each fact is a primitive rounding bound or a - // derived mulDiv identity proven over concrete mulDiv in MulDiv.spec (rule name cited), or an isolated - // pure-arithmetic move; the composition uses only linear glue. + // Establishes: curContrib - newContrib <= maxDebtDropBound. Ghost-form quantities mirror the + // single-collateral definitions; liquidate computes seizedOut = floor(floor(repaid*lif/WAD)*OPS/price) at + // Midnight.sol:692, so seizedOut IS the ghost term ghostMulDivDown(maxSeizedValue, OPS, price) below. Each + // fact is a primitive rounding bound or a derived mulDiv identity proven over concrete mulDiv in + // MulDiv.spec (rule name cited); the composition uses arithmetic glue. - mathint W = WAD(); - mathint S = ORACLE_PRICE_SCALE(); + uint256 W = WAD(); + uint256 S = ORACLE_PRICE_SCALE(); - mathint maxSeizedValue = ghostMulDivDown(repaidUnits, lif, W); + uint256 maxSeizedValue = ghostMulDivDown(repaidUnits, lif, W); // liquidate's L692 seizedAssets: seizedOut == ghostMulDivDown(maxSeizedValue, S, price). - mathint curCollatValue = ghostMulDivDown(collatBefore, price, S); - mathint newCollatValue = ghostMulDivDown(collatBefore - seizedOut, price, S); - mathint collatValueDrop = curCollatValue - newCollatValue; - - mathint curContrib = ghostMulDivDown(curCollatValue, lltv, W); - mathint newContrib = ghostMulDivDown(newCollatValue, lltv, W); - - mathint lifTimesLltv = lif * lltv; - mathint wadSquared = W * W; - mathint maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, wadSquared); - - // Non-negativity of the ghost values (MulDiv.spec: mulDiv of non-negatives is non-negative). - require maxSeizedValue >= 0 && seizedOut >= 0; - require curCollatValue >= 0 && newCollatValue >= 0; - require curContrib >= 0 && newContrib >= 0; - require maxDebtDropBound >= 0; - - // L1 (MulDiv.spec: mulDivInverseUpDown), instance a=maxSeizedValue, b=S, d=price, seizedOut=down(a,b,d): - // up(down(maxSeizedValue,S,price),price,S) == up(seizedOut,price,S) <= maxSeizedValue. - require ghostMulDivUp(seizedOut, price, S) <= maxSeizedValue; - - // L2 (MulDiv.spec: mulDivAddDownUp), instance a1=collatBefore-seizedOut, a2=seizedOut, b=price, d=S: - // curCollatValue <= newCollatValue + up(seizedOut,price,S). - require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, S); - - // newCollatValue <= curCollatValue (MulDiv.spec: mulDivMonotoneA, collat-seized <= collat): drop is >= 0. - require newCollatValue <= curCollatValue; - - // L3 (MulDiv.spec: mulDivAddDownUp), instance a1=newCollatValue, a2=collatValueDrop, b=lltv, d=W: - // curContrib <= newContrib + up(collatValueDrop,lltv,W). - require curContrib <= newContrib + ghostMulDivUp(collatValueDrop, lltv, W); - - // L4 (MulDiv.spec: mulDivMonotoneA), instance a1=collatValueDrop, a2=maxSeizedValue, b=lltv, d=W. - require collatValueDrop <= maxSeizedValue => ghostMulDivUp(collatValueDrop, lltv, W) <= ghostMulDivUp(maxSeizedValue, lltv, W); - - // L5.a (MulDiv.spec: mulDivDownRoundsDown), instance a=repaidUnits, b=lif, d=W: maxSeizedValue*W <= repaid*lif. - require maxSeizedValue * W <= repaidUnits * lif; - - // Pure-arith (MulDiv.spec: mulDivMonotoneA analog lemmaMulMono), scale L5.a by lltv >= 0. - require maxSeizedValue * W <= repaidUnits * lif => maxSeizedValue * W * lltv <= repaidUnits * lif * lltv; - - // L5.b (MulDiv.spec: mulDivUpRoundsUp), instance a=repaidUnits, b=lifTimesLltv, d=wadSquared: - // maxDebtDropBound*wadSquared >= repaid*lifTimesLltv (== repaid*lif*lltv == maxDebtDropBound*W*W). - require maxDebtDropBound * wadSquared >= repaidUnits * lifTimesLltv; - - // Pure-arith (lemmaCancelPos), cancel W>0: (maxSeizedValue*lltv)*W <= (maxDebtDropBound*W)*W - // ==> maxSeizedValue*lltv <= maxDebtDropBound*W. - require maxSeizedValue * lltv * W <= maxDebtDropBound * W * W => maxSeizedValue * lltv <= maxDebtDropBound * W; - - // L5.c (MulDiv.spec: mulDivCeilLeOfMulGe), instance a=maxSeizedValue, b=lltv, d=W, bound=maxDebtDropBound: - // maxSeizedValue*lltv <= maxDebtDropBound*W => up(maxSeizedValue,lltv,W) <= maxDebtDropBound. - require maxSeizedValue * lltv <= maxDebtDropBound * W => ghostMulDivUp(maxSeizedValue, lltv, W) <= maxDebtDropBound; - - // Linear glue (mirrors rocq/maxRepaidHealthy.v:185-246), no nested division, no hypothesis-times-variable, - // no cancellation done by the SMT here (both isolated above): + uint256 curCollatValue = ghostMulDivDown(collatBefore, price, S); + uint256 newCollatValue = ghostMulDivDown(collatAfter, price, S); + require newCollatValue <= curCollatValue, "mulDivMonotoneA with collatAfter <= collatBefore, so the collateral-value drop is non-negative (MulDiv.spec)"; + uint256 collatValueDrop = assert_uint256(curCollatValue - newCollatValue); + + uint256 curContrib = ghostMulDivDown(curCollatValue, lltv, W); + uint256 newContrib = ghostMulDivDown(newCollatValue, lltv, W); + + uint256 lifTimesLltv = assert_uint256(lif * lltv); + uint256 maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, S); + + require ghostMulDivUp(seizedOut, price, S) <= maxSeizedValue, "L1: mulDivInverseUpDown with a=maxSeizedValue, b=S, d=price (MulDiv.spec)"; + require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, S), "L2: mulDivAddDownUp with a1=collatAfter, a2=seizedOut, b=price, d=S (MulDiv.spec)"; + require curContrib <= newContrib + ghostMulDivUp(collatValueDrop, lltv, W), "L3: mulDivAddDownUp with a1=newCollatValue, a2=collatValueDrop, b=lltv, d=W (MulDiv.spec)"; + require collatValueDrop <= maxSeizedValue => ghostMulDivUp(collatValueDrop, lltv, W) <= ghostMulDivUp(maxSeizedValue, lltv, W), "L4: mulDivMonotoneA with a1=collatValueDrop, a2=maxSeizedValue, b=lltv, d=W (MulDiv.spec)"; + require maxSeizedValue * W <= repaidUnits * lif, "L5.a: mulDivDownRoundsDown with a=repaidUnits, b=lif, d=W (MulDiv.spec)"; + require maxDebtDropBound * S >= repaidUnits * lifTimesLltv, "L5.b: mulDivUpRoundsUp with a=repaidUnits, b=lifTimesLltv, d=WAD^2 (MulDiv.spec)"; + require maxSeizedValue * lltv <= maxDebtDropBound * W => ghostMulDivUp(maxSeizedValue, lltv, W) <= maxDebtDropBound, "L5.c: mulDivCeilLeOfMulGe with a=maxSeizedValue, b=lltv, d=W, bound=maxDebtDropBound (MulDiv.spec)"; + + // Linear glue, with no nested division: // (a) collatValueDrop <= maxSeizedValue: from L2 (drop <= up(seizedOut,..)) and L1 (up(seizedOut,..) <= msv). // (b) up(collatValueDrop,lltv,W) <= up(maxSeizedValue,lltv,W): L4 with (a). // (c) up(maxSeizedValue,lltv,W) <= maxDebtDropBound: (L5.a scaled by lltv) chained through L5.b, then the W @@ -317,9 +222,10 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address receiv // (Midnight.sol:699), maxRepaid*lif*lltv <= (maxRepaid - gap)*WAD^2 (axiomUpRoundsUp on gap), hence // maxDebtDropBound = ceil(maxRepaid*lif*lltv/WAD^2) <= maxRepaid - gap (axiomCeilLeOfMulGe). Combined with // the drop bound: newMaxDebt = maxDebt - drop >= debt - maxRepaid = newDebt. - require axiomUpRoundsUp(gap, WAD() * WAD(), WAD() * WAD() - lif * lltv), "proved in mulDivUpRoundsUp (Rocq ceil_div_mul_ge)"; - require axiomCeilLeOfMulGe(repaidUnits, lif * lltv, WAD() * WAD(), repaidUnits - gap), "proved in mulDivCeilLeOfMulGe (Rocq ceil_div_le_of_mul_ge)"; + uint256 rcfDenominator = assert_uint256(S - lifTimesLltv); + require axiomUpRoundsUp(gap, S, rcfDenominator), "proved in mulDivUpRoundsUp"; + uint256 repaidExcess = assert_uint256(repaidUnits - gap); + require axiomCeilLeOfMulGe(repaidUnits, lifTimesLltv, S, repaidExcess), "proved in mulDivCeilLeOfMulGe"; - // newDebt >= 0 and newDebt <= newMaxDebt, i.e. the position is healthy after liquidation. - assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower), "position is healthy after liquidation at the RCF cap"; + assert isHealthyNoBitmap(globalMarket, globalId, borrower); } diff --git a/rocq/maxRepaidHealthy.v b/rocq/maxRepaidHealthy.v deleted file mode 100644 index 273b6a77c..000000000 --- a/rocq/maxRepaidHealthy.v +++ /dev/null @@ -1,366 +0,0 @@ -From Stdlib Require Import ZArith Lia Psatz. - -Open Scope Z_scope. - -Definition WAD : Z := 1000000000000000000. -Definition ORACLE_PRICE_SCALE : Z := 1000000000000000000000000000000000000. - -Definition ceil_div (numerator denominator : Z) : Z := - (numerator + denominator - 1) / denominator. - -(** -If: -- maxRepaid is computed as: - ceil((debt - maxDebt) * WAD^2 / (WAD^2 - lif * lltv)) -- repaid is the amount actually repaid: min(maxRepaid, debt) -- seizedAssets is computed as: - floor(floor(repaid * lif / WAD) * ORACLE_PRICE_SCALE / price) -- maxDebt is computed from the current collateral as: - otherCollatContribution + floor(floor(collat * price / ORACLE_PRICE_SCALE) * lltv / WAD) - -then after liquidating repaid, the borrower is healthy: - newDebt <= newMaxDebt - -This proof is entirely over integer arithmetic. -It does not use real-number approximations. -The assumptions that the collateral seized does not exceed the current collateral does not narrow the generality of the proof: in that case the transaction would revert independently of the RCF mechanism, so that mechanism does not restrict the possibility to go back to health. -*) - -Definition max_repaid_liquidation_leaves_healthy_statement : Prop := - forall debt otherCollatContribution collat price lltv lif, - let maxDebt := - otherCollatContribution - + (collat * price / ORACLE_PRICE_SCALE) * lltv / WAD in - let maxRepaid := - ceil_div ((debt - maxDebt) * (WAD * WAD)) - (WAD * WAD - lif * lltv) in - let repaid := Z.min maxRepaid debt in - let seizedAssets := - (repaid * lif / WAD * ORACLE_PRICE_SCALE) / price in - let newDebt := debt - repaid in - let newMaxDebt := - otherCollatContribution - + ((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv / WAD in - 0 < price -> - 0 <= debt -> 0 <= otherCollatContribution -> - 0 <= collat -> - 0 <= lltv -> 0 <= lif -> - lif * lltv < WAD * WAD -> - maxDebt <= debt -> - seizedAssets <= collat -> - 0 <= newDebt /\ newDebt <= newMaxDebt. - -(* -------------------------------------------------------------------------- *) -(* Generic integer-division lemmas *) -(* -------------------------------------------------------------------------- *) - -Lemma WAD_pos : 0 < WAD. -Proof. unfold WAD; lia. Qed. - -Lemma ORACLE_PRICE_SCALE_pos : 0 < ORACLE_PRICE_SCALE. -Proof. unfold ORACLE_PRICE_SCALE; lia. Qed. - -Lemma div_upper_strict : - forall numerator denominator, - 0 < denominator -> 0 <= numerator -> - numerator < denominator * (numerator / denominator + 1). -Proof. - intros numerator denominator Hden Hnum. - pose proof (Z.div_mod numerator denominator) as Hdivmod. - specialize (Hdivmod ltac:(lia)). - pose proof (Z.mod_pos_bound numerator denominator Hden) as Hmod. - nia. -Qed. - -Lemma floor_mul_le : - forall numerator denominator, - 0 < denominator -> 0 <= numerator -> - (numerator / denominator) * denominator <= numerator. -Proof. - intros numerator denominator Hden Hnum. - pose proof (Z.div_mod numerator denominator) as Hdivmod. - specialize (Hdivmod ltac:(lia)). - pose proof (Z.mod_pos_bound numerator denominator Hden) as Hmod. - nia. -Qed. - -Lemma ceil_div_mul_ge : - forall numerator denominator, - 0 < denominator -> 0 <= numerator -> - numerator <= ceil_div numerator denominator * denominator. -Proof. - intros numerator denominator Hden Hnum. - unfold ceil_div. - pose proof (Z.div_mod (numerator + denominator - 1) denominator) as Hdivmod. - specialize (Hdivmod ltac:(lia)). - pose proof (Z.mod_pos_bound (numerator + denominator - 1) denominator Hden) as Hmod. - nia. -Qed. - -Lemma ceil_div_le_of_mul_ge : - forall numerator denominator bound, - 0 < denominator -> 0 <= numerator -> numerator <= bound * denominator -> - ceil_div numerator denominator <= bound. -Proof. - intros numerator denominator bound Hden Hnum Hbound. - unfold ceil_div. - assert ((numerator + denominator - 1) / denominator < bound + 1) as Hlt. - { apply Z.div_lt_upper_bound; nia. } - lia. -Qed. - -Lemma ceil_div_mono : - forall left right denominator, - 0 < denominator -> left <= right -> - ceil_div left denominator <= ceil_div right denominator. -Proof. - intros left right denominator Hden Hle. - unfold ceil_div. - apply Z.div_le_mono; lia. -Qed. - -Lemma floor_drop_div_le_ceil : - forall base drop denominator, - 0 < denominator -> 0 <= base -> 0 <= drop -> - (base + drop) / denominator - base / denominator <= ceil_div drop denominator. -Proof. - intros base drop denominator Hden Hbase Hdrop. - assert (Hbase_lt : base < denominator * (base / denominator + 1)). - { apply div_upper_strict; lia. } - assert (Hdrop_le : drop <= ceil_div drop denominator * denominator). - { apply ceil_div_mul_ge; lia. } - assert ((base + drop) / denominator < base / denominator + ceil_div drop denominator + 1) as Hlt. - { apply Z.div_lt_upper_bound; nia. } - lia. -Qed. - -(* -------------------------------------------------------------------------- *) -(* Midnight-specific rounding lemmas *) -(* -------------------------------------------------------------------------- *) - -Lemma seized_value_drop_le_maxSeizedValue : - forall maxRepaid lif price seizedAssets, - 0 < price -> - 0 <= maxRepaid -> 0 <= lif -> - seizedAssets = (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> - ceil_div (seizedAssets * price) ORACLE_PRICE_SCALE <= maxRepaid * lif / WAD. -Proof. - intros maxRepaid lif price seizedAssets Hprice HmaxRepaid Hlif Hseized. - subst seizedAssets. - assert (HWAD : 0 < WAD) by apply WAD_pos. - assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. - assert (HmaxSeizedValue_nonneg : 0 <= maxRepaid * lif / WAD). - { apply Z.div_pos; nia. } - apply ceil_div_le_of_mul_ge. - - exact Hscale. - - apply Z.mul_nonneg_nonneg; [apply Z.div_pos |]; nia. - - pose proof (floor_mul_le (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) price Hprice) as Hfloor. - specialize (Hfloor ltac:(nia)). - nia. -Qed. - -Lemma max_debt_contribution_drop_bound : - forall collat seizedAssets price lltv maxRepaid lif, - 0 < price -> - 0 <= collat -> 0 <= seizedAssets -> seizedAssets <= collat -> - 0 <= lltv -> 0 <= maxRepaid -> 0 <= lif -> - seizedAssets = (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> - let currentCollatValue := collat * price / ORACLE_PRICE_SCALE in - let newCollatValue := (collat - seizedAssets) * price / ORACLE_PRICE_SCALE in - currentCollatValue * lltv / WAD - newCollatValue * lltv / WAD - <= ceil_div (maxRepaid * lif * lltv) (WAD * WAD). -Proof. - intros collat seizedAssets price lltv maxRepaid lif - Hprice Hcollat HseizedNonneg HseizedLe Hlltv HmaxRepaid Hlif HseizedEq - currentCollatValue newCollatValue. - subst currentCollatValue newCollatValue. - assert (HWAD : 0 < WAD) by apply WAD_pos. - assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. - - set (collatValueDrop := - collat * price / ORACLE_PRICE_SCALE - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE). - set (maxSeizedValue := maxRepaid * lif / WAD). - set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). - - assert (HcollatValueDrop_le : collatValueDrop <= maxSeizedValue). - { - unfold collatValueDrop, maxSeizedValue. - replace (collat * price) - with ((collat - seizedAssets) * price + seizedAssets * price) by nia. - eapply Z.le_trans. - - apply floor_drop_div_le_ceil; nia. - - eapply seized_value_drop_le_maxSeizedValue; eauto; nia. - } - - assert (Hold_ge_new_value : - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE <= collat * price / ORACLE_PRICE_SCALE). - { - apply Z.div_le_mono; nia. - } - - assert (HmaxDebtDrop_by_valueDrop : - collat * price / ORACLE_PRICE_SCALE * lltv / WAD - - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD - <= ceil_div (collatValueDrop * lltv) WAD). - { - unfold collatValueDrop. - replace (collat * price / ORACLE_PRICE_SCALE * lltv) - with (((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv - + (collat * price / ORACLE_PRICE_SCALE - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv) by nia. - eapply floor_drop_div_le_ceil. - - exact HWAD. - - apply Z.mul_nonneg_nonneg; try nia. - apply Z.div_pos; nia. - - apply Z.mul_nonneg_nonneg; nia. - } - - assert (Hceil_valueDrop_le_maxSeizedValue : - ceil_div (collatValueDrop * lltv) WAD <= ceil_div (maxSeizedValue * lltv) WAD). - { - apply ceil_div_mono; nia. - } - - assert (HmaxSeizedValue_floor : maxSeizedValue * WAD <= maxRepaid * lif). - { - unfold maxSeizedValue. - apply floor_mul_le; nia. - } - - assert (HmaxDebtDropBound_mul : maxRepaid * lif * lltv <= maxDebtDropBound * (WAD * WAD)). - { - unfold maxDebtDropBound. - apply ceil_div_mul_ge; nia. - } - - assert (HmaxSeizedValue_to_maxDebtDropBound : maxSeizedValue * lltv <= maxDebtDropBound * WAD). - { - nia. - } - - assert (Hceil_maxSeizedValue_le_maxDebtDropBound : - ceil_div (maxSeizedValue * lltv) WAD <= maxDebtDropBound). - { - apply ceil_div_le_of_mul_ge; nia. - } - - lia. -Qed. - -(* -------------------------------------------------------------------------- *) -(* Final theorem *) -(* -------------------------------------------------------------------------- *) - -Theorem max_repaid_liquidation_leaves_healthy : - max_repaid_liquidation_leaves_healthy_statement. -Proof. - unfold max_repaid_liquidation_leaves_healthy_statement. - intros debt otherCollatContribution collat price lltv lif. - set (maxDebt := otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD). - set (maxRepaid := ceil_div ((debt - maxDebt) * (WAD * WAD)) (WAD * WAD - lif * lltv)). - set (repaid := Z.min maxRepaid debt). - set (seizedAssets := repaid * lif / WAD * ORACLE_PRICE_SCALE / price). - set (newDebt := debt - repaid). - set (newMaxDebt := otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD). - intros Hprice Hdebt Hother Hcollat Hlltv Hlif Hden HmaxDebtLeDebt HseizedLeCollat. - assert (HWAD : 0 < WAD) by apply WAD_pos. - assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. - assert (Hden_pos : 0 < WAD * WAD - lif * lltv) by nia. - assert (HmaxDebt_nonneg : 0 <= maxDebt). - { - subst maxDebt. - assert (HcollatValue_nonneg : 0 <= collat * price / ORACLE_PRICE_SCALE). - { apply Z.div_pos; nia. } - assert (HcollatContribution_nonneg : 0 <= collat * price / ORACLE_PRICE_SCALE * lltv / WAD). - { apply Z.div_pos; nia. } - nia. - } - assert (HmaxRepaid_nonneg : 0 <= maxRepaid). - { - subst maxRepaid. - unfold ceil_div. - apply Z.div_pos; nia. - } - assert (Hrepaid_nonneg : 0 <= repaid). - { - subst repaid. - apply Z.min_glb; assumption. - } - assert (Hrepaid_le_debt : repaid <= debt). - { - subst repaid. - apply Z.le_min_r. - } - split. - - subst newDebt; lia. - - destruct (Z.leb_spec0 debt maxRepaid) as [Hdebt_le_maxRepaid | HmaxRepaid_lt_debt]. - + assert (Hrepaid_eq : repaid = debt). - { subst repaid. apply Z.min_r. lia. } - subst newDebt newMaxDebt. - rewrite Hrepaid_eq. - assert (Hseized_nonneg : 0 <= seizedAssets). - { - subst seizedAssets. - rewrite Hrepaid_eq. - apply Z.div_pos. - - apply Z.mul_nonneg_nonneg. - + apply Z.div_pos; nia. - + lia. - - lia. - } - assert (HnewCollatValue_nonneg : 0 <= (collat - seizedAssets) * price / ORACLE_PRICE_SCALE). - { apply Z.div_pos; nia. } - assert (HnewContribution_nonneg : - 0 <= (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD). - { apply Z.div_pos; nia. } - nia. - + assert (Hrepaid_eq : repaid = maxRepaid). - { subst repaid. apply Z.min_l. lia. } - set (gap := debt - maxDebt). - set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). - assert (Hgap_nonneg : 0 <= gap) by (unfold gap; lia). - assert (HmaxRepaid_def_le : - gap * (WAD * WAD) <= maxRepaid * (WAD * WAD - lif * lltv)). - { - subst maxRepaid. - unfold gap. - apply ceil_div_mul_ge; nia. - } - assert (Hextra_mul : - (maxRepaid - gap) * (WAD * WAD) >= maxRepaid * lif * lltv). - { nia. } - assert (HmaxDebtDropBound_le_extra : maxDebtDropBound <= maxRepaid - gap). - { - unfold maxDebtDropBound. - apply ceil_div_le_of_mul_ge; nia. - } - assert (Hseized_nonneg : 0 <= seizedAssets). - { - subst seizedAssets. - rewrite Hrepaid_eq. - apply Z.div_pos. - - apply Z.mul_nonneg_nonneg. - + apply Z.div_pos; nia. - + lia. - - lia. - } - assert (HseizedEq : seizedAssets = maxRepaid * lif / WAD * ORACLE_PRICE_SCALE / price). - { - subst seizedAssets. - rewrite Hrepaid_eq. - reflexivity. - } - assert (HmaxDebtDrop_le_bound : maxDebt - newMaxDebt <= maxDebtDropBound). - { - subst maxDebt newMaxDebt. - replace (otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD - - (otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD)) - with (collat * price / ORACLE_PRICE_SCALE * lltv / WAD - - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD) by lia. - unfold maxDebtDropBound. - eapply max_debt_contribution_drop_bound; eauto; nia. - } - subst newDebt. - rewrite Hrepaid_eq. - unfold gap in *. - lia. -Qed. From bdf6467aa0fccff0f173309a7d3a0df083c9cced Mon Sep 17 00:00:00 2001 From: MathisGD <74971347+MathisGD@users.noreply.github.com> Date: Tue, 4 Aug 2026 11:46:41 +0200 Subject: [PATCH 09/19] iterate --- certora/specs/MaxRepaidHealthy.spec | 147 +++++++++++----------------- certora/specs/MulDiv.spec | 14 ++- 2 files changed, 69 insertions(+), 92 deletions(-) diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index 14fdf9136..270678cc8 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -10,7 +10,6 @@ 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. @@ -24,13 +23,10 @@ methods { 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); - // maxLif is recomputed on the fly from (lltv, liquidationCursor); its lltv * maxLif <= WAD * WAD bound is - // assumed below (see lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec). + // maxLif is deterministic for each (lltv, liquidationCursor) pair. function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor); - // Assume no reentrancy: callbacks and tokens do not re-enter Midnight. - // This is justified because the properties we verify are about the effect of each function's own body on - // the state, not the effect of the full transaction including callbacks. + // Unresolved callbacks and token calls use AUTO/HAVOC_ECF, which models non-reentrant callees. } /// SUMMARY /// @@ -39,19 +35,21 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; +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; -/* Primitive tight rounding facts, each proven over concrete mulDiv in MulDiv.spec and used below ONLY at - specific ground instances (never as background foralls, to keep the query linear). */ +// Tight rounding facts proved over concrete mulDiv in MulDiv.spec. The rule assumes only the ground instances +// it uses, avoiding quantified background axioms. -/* Proved in mulDivUpRoundsUp: a*b <= ceil(a*b/d)*d. */ +// Proved in mulDivUpRoundsUp: a * b <= ceil(a * b / d) * d. definition axiomUpRoundsUp(uint256 a, uint256 b, uint256 d) returns bool = d > 0 => a * b <= ghostMulDivUp(a, b, d) * d; -/* Proved in mulDivCeilLeOfMulGe: a*b <= bound*d => ceil(a*b/d) <= bound. */ +// 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; function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { @@ -70,8 +68,8 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { return ghostMulDivUp(a, b, d); } -// Global market machinery (mirrors Healthiness.spec): pins the market so that IdLib.toId is deterministic and -// the collateral params are known. globalMarketCollateralLength is fixed to 1 in the rule (single collateral). +// Pin every field that contributes to the market id, making the toId summary deterministic and injective. +// The rule specializes this market to two collaterals. persistent ghost address globalMarketLoanToken; @@ -123,50 +121,27 @@ function summaryToId(Midnight.Market market) returns (bytes32) { return id; } -// Single-collateral maxDebt contribution: floor(floor(collat * price / OPS) * lltv / WAD). -function maxDebtContribution(uint256 collat, uint256 price, uint256 lltv) returns uint256 { - return ghostMulDivDown(ghostMulDivDown(collat, price, ORACLE_PRICE_SCALE()), lltv, WAD()); -} - /// RULE /// -// Liquidating an unhealthy position at the RCF cap restores its health, in the single-collateral, -// RCF-active (!postMaturityMode && lltv < WAD), no-bad-debt regime, in the maxRepaid < debt case -// (newDebt = debt - maxRepaid > 0). -// The maxDebt-drop bound is DERIVED INLINE (see the "INLINE DROP-BOUND DERIVATION" block below). +// 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. rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrower, address receiver, address callback, bytes data) { - // Post-state health is read bitmap-free; combined with single-collateral this avoids bitmap iteration. Midnight.Market globalMarket = getGlobalMarket(); - // Single collateral, so there is no contribution from other collateral. - require globalMarketCollateralLength == 1, "single-collateral market"; - - uint256 lltv = globalMarketCollateralLLTV[collateralIndex]; - uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]); - - require lltv < WAD(), "RCF is active only for lltv < WAD"; - require lltv * lif <= 999 * 10 ^ 15 * WAD(), "maxLif * lltv <= 0.999 * WAD * WAD, (see Midnight.sol:698, createdMarketsRespectMaxLifBound in CreatedMarkets.spec, it makes the L699 denominator strictly positive)"; - - address oracle = globalMarket.collateralParams[collateralIndex].oracle; - uint256 price = summaryPrice(oracle); - - require price > 0, "positive price; otherwise mulDiv by price reverts and the case is vacuous"; - - // On a non-reverting liquidation, the sole market collateral is activated and no out-of-range bitmap bit - // can be set. The call also enforces that the borrower is not liquidation-locked. - require currentContract.marketState[globalId].tickSpacing != 0, "market is already created, so touchMarket is a no-op that returns globalId"; - require badDebtFor(globalMarket, globalId, borrower) == 0, "no bad debt is realized, so liquidate's debt at L699 equals maxRepaidFor's pre-liquidation debt"; - require !isHealthyNoBitmap(globalMarket, globalId, borrower), "unhealthy pre-state: maxDebt < debt due to the strict RCF trigger at Midnight.sol:661"; + require globalMarketCollateralLength == 2, "two-collateral market"; uint256 collatBefore = collateral(globalId, borrower, collateralIndex); uint256 debtBefore = debt(globalId, borrower); - // Pin repaid to the RCF cap. maxRepaidFor reproduces Midnight.sol:699 exactly, so repaidUnits equals the - // maxRepaid recomputed inside liquidate and the RCF require (Midnight.sol:700-705) passes on its first - // disjunct (repaidUnits <= maxRepaid), independently of the dust waiver. + // 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. uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower); - require repaidUnits < debtBefore, "maxRepaid < debt case: repaid = maxRepaid and newDebt > 0 (the maxRepaid >= debt case gives newDebt = 0, which is trivially healthy)"; + // 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); uint256 seizedOut; uint256 repaidOut; @@ -174,58 +149,48 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow uint256 collatAfter = assert_uint256(collatBefore - seizedOut); - // gap = debt - maxDebt > 0 (the position is unhealthy). Both are the single-collateral quantities that - // liquidate uses internally: maxDebt at L699 and debt (unchanged, since no bad debt) equal these. - uint256 gap = assert_uint256(debtBefore - maxDebtContribution(collatBefore, price, lltv)); - - ///// INLINE DROP-BOUND DERIVATION ///// - // Establishes: curContrib - newContrib <= maxDebtDropBound. Ghost-form quantities mirror the - // single-collateral definitions; liquidate computes seizedOut = floor(floor(repaid*lif/WAD)*OPS/price) at - // Midnight.sol:692, so seizedOut IS the ghost term ghostMulDivDown(maxSeizedValue, OPS, price) below. Each - // fact is a primitive rounding bound or a derived mulDiv identity proven over concrete mulDiv in - // MulDiv.spec (rule name cited); the composition uses arithmetic glue. + /// MAX-DEBT DROP BOUND /// + // Establish curContrib - newContrib <= maxDebtDropBound. At Midnight.sol:692, 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. - uint256 W = WAD(); - uint256 S = ORACLE_PRICE_SCALE(); - - uint256 maxSeizedValue = ghostMulDivDown(repaidUnits, lif, W); + uint256 lltv = globalMarketCollateralLLTV[collateralIndex]; + uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]); + uint256 maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD()); + uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle); - // liquidate's L692 seizedAssets: seizedOut == ghostMulDivDown(maxSeizedValue, S, price). - uint256 curCollatValue = ghostMulDivDown(collatBefore, price, S); - uint256 newCollatValue = ghostMulDivDown(collatAfter, price, S); - require newCollatValue <= curCollatValue, "mulDivMonotoneA with collatAfter <= collatBefore, so the collateral-value drop is non-negative (MulDiv.spec)"; - uint256 collatValueDrop = assert_uint256(curCollatValue - newCollatValue); + // By Midnight.sol:692, seizedOut == ghostMulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price). + uint256 curCollatValue = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 newCollatValue = ghostMulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); - uint256 curContrib = ghostMulDivDown(curCollatValue, lltv, W); - uint256 newContrib = ghostMulDivDown(newCollatValue, lltv, W); + uint256 curContrib = ghostMulDivDown(curCollatValue, lltv, WAD()); + uint256 newContrib = ghostMulDivDown(newCollatValue, lltv, WAD()); uint256 lifTimesLltv = assert_uint256(lif * lltv); - uint256 maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, S); - - require ghostMulDivUp(seizedOut, price, S) <= maxSeizedValue, "L1: mulDivInverseUpDown with a=maxSeizedValue, b=S, d=price (MulDiv.spec)"; - require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, S), "L2: mulDivAddDownUp with a1=collatAfter, a2=seizedOut, b=price, d=S (MulDiv.spec)"; - require curContrib <= newContrib + ghostMulDivUp(collatValueDrop, lltv, W), "L3: mulDivAddDownUp with a1=newCollatValue, a2=collatValueDrop, b=lltv, d=W (MulDiv.spec)"; - require collatValueDrop <= maxSeizedValue => ghostMulDivUp(collatValueDrop, lltv, W) <= ghostMulDivUp(maxSeizedValue, lltv, W), "L4: mulDivMonotoneA with a1=collatValueDrop, a2=maxSeizedValue, b=lltv, d=W (MulDiv.spec)"; - require maxSeizedValue * W <= repaidUnits * lif, "L5.a: mulDivDownRoundsDown with a=repaidUnits, b=lif, d=W (MulDiv.spec)"; - require maxDebtDropBound * S >= repaidUnits * lifTimesLltv, "L5.b: mulDivUpRoundsUp with a=repaidUnits, b=lifTimesLltv, d=WAD^2 (MulDiv.spec)"; - require maxSeizedValue * lltv <= maxDebtDropBound * W => ghostMulDivUp(maxSeizedValue, lltv, W) <= maxDebtDropBound, "L5.c: mulDivCeilLeOfMulGe with a=maxSeizedValue, b=lltv, d=W, bound=maxDebtDropBound (MulDiv.spec)"; - - // Linear glue, with no nested division: - // (a) collatValueDrop <= maxSeizedValue: from L2 (drop <= up(seizedOut,..)) and L1 (up(seizedOut,..) <= msv). - // (b) up(collatValueDrop,lltv,W) <= up(maxSeizedValue,lltv,W): L4 with (a). - // (c) up(maxSeizedValue,lltv,W) <= maxDebtDropBound: (L5.a scaled by lltv) chained through L5.b, then the W - // cancel, then L5.c. - // (d) curContrib - newContrib <= up(collatValueDrop,lltv,W) (L3) <= (b) <= (c) = maxDebtDropBound. - - ///// FINAL HEALTH GLUE ///// - // The RCF cap over-repays the gap: with repaidUnits == maxRepaid == ceil(gap*WAD^2/(WAD^2 - lif*lltv)) - // (Midnight.sol:699), maxRepaid*lif*lltv <= (maxRepaid - gap)*WAD^2 (axiomUpRoundsUp on gap), hence - // maxDebtDropBound = ceil(maxRepaid*lif*lltv/WAD^2) <= maxRepaid - gap (axiomCeilLeOfMulGe). Combined with - // the drop bound: newMaxDebt = maxDebt - drop >= debt - maxRepaid = newDebt. - uint256 rcfDenominator = assert_uint256(S - lifTimesLltv); - require axiomUpRoundsUp(gap, S, rcfDenominator), "proved in mulDivUpRoundsUp"; + uint256 maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()); + + require price > 0 => ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()) <= maxSeizedValue, "L1: mulDivInverseUpDown with a=maxSeizedValue, b=ORACLE_PRICE_SCALE, d=price (MulDiv.spec)"; + require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()), "L2: mulDivAddDownUp with a1=collatAfter, a2=seizedOut, b=price, d=ORACLE_PRICE_SCALE (MulDiv.spec)"; + require curCollatValue <= newCollatValue + maxSeizedValue => curContrib <= newContrib + ghostMulDivUp(maxSeizedValue, lltv, WAD()), "L3: mulDivDownBoundedIncrease with a1=curCollatValue, a2=newCollatValue, delta=maxSeizedValue, b=lltv, d=WAD (MulDiv.spec)"; + require ghostMulDivUp(maxSeizedValue, lltv, WAD()) <= maxDebtDropBound, "L4: mulDivDownUpComposition with a=repaidUnits, b=lif, c=lltv, d=WAD (MulDiv.spec)"; + + // 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. + + /// FINAL HEALTH BOUND /// + // 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. + uint256 gap = require_uint256(debtBefore - maxDebtBefore); + uint256 rcfDenominator = assert_uint256(WAD_SQUARED() - lifTimesLltv); + require axiomUpRoundsUp(gap, WAD_SQUARED(), rcfDenominator), "proved in mulDivUpRoundsUp"; uint256 repaidExcess = assert_uint256(repaidUnits - gap); - require axiomCeilLeOfMulGe(repaidUnits, lifTimesLltv, S, repaidExcess), "proved in mulDivCeilLeOfMulGe"; + require axiomCeilLeOfMulGe(repaidUnits, lifTimesLltv, WAD_SQUARED(), repaidExcess), "proved in mulDivCeilLeOfMulGe"; assert isHealthyNoBitmap(globalMarket, globalId, borrower); } diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index 57af3b090..27ba3924b 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -72,6 +72,18 @@ rule mulDivAddDownUp(uint256 a1, uint256 a2, uint256 b, uint256 d) { assert mulDivDown(a1, b, d) + mulDivUp(a2, b, d) >= mulDivDown(a1plusa2, b, d); } +// Increasing the first argument by at most delta increases mulDivDown by at most mulDivUp(delta, b, d). +rule mulDivDownBoundedIncrease(uint256 a1, uint256 a2, uint256 delta, uint256 b, uint256 d) { + assert a1 <= a2 + delta => mulDivDown(a1, b, d) <= mulDivDown(a2, b, d) + mulDivUp(delta, b, d); +} + +// Rounding down the first scaling step cannot increase the result of a second scaling rounded up. +rule mulDivDownUpComposition(uint256 a, uint256 b, uint256 c, uint256 d) { + uint256 bc = require_uint256(b * c); + uint256 dSquared = require_uint256(d * d); + assert mulDivUp(mulDivDown(a, b, d), c, d) <= mulDivUp(a, bc, dSquared); +} + rule mulDivInverseDownUp(uint256 a, uint256 b, uint256 d) { assert a <= mulDivDown(mulDivUp(a, b, d), d, b); } @@ -114,7 +126,7 @@ rule mulDivUpUpperBound(uint256 a, uint256 b, uint256 d) { } // If the exact product is at most bound * d, then the ceiling is at most bound. -// Used by MaxRepaidHealthy.spec (axiomCeilLeOfMulGe) to bound the collateral-value drop. +// Used by MaxRepaidHealthy.spec (axiomCeilLeOfMulGe) for its final max-debt-drop bound. rule mulDivCeilLeOfMulGe(uint256 a, uint256 b, uint256 d, uint256 bound) { assert d != 0 && a * b <= bound * d => mulDivUp(a, b, d) <= bound; } From 9a6bb8a808481ded1427d07d9d5dd131eee2cf47 Mon Sep 17 00:00:00 2001 From: MathisGD <74971347+MathisGD@users.noreply.github.com> Date: Thu, 27 Aug 2026 11:56:41 +0200 Subject: [PATCH 10/19] Update certora/specs/MaxRepaidHealthy.spec Co-authored-by: Quentin Garchery Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com> --- 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 270678cc8..5a707adc9 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -133,8 +133,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. + // This rule checks that using `repaidUnits == maxRepaid` is enough to put the account healthy. This means that the RCF doesn't prevent to put the position back to health. uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower); // maxRepaidFor's non-reverting collateral lookup establishes collateralIndex < 2. From 616c217dc9c9080da12ce5c41de0e52f79f383c0 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 27 Aug 2026 10:06:30 +0000 Subject: [PATCH 11/19] [Certora] Apply thumbed-up review comments on MaxRepaidHealthy Review cleanups from @QGarchery's review that @MathisGD approved: - Remove the unused badDebtFor helper from MidnightWrapper (it is only needed by the liveness rule of the stacked PR, which re-adds it there). - Document why the tickToPrice / toId / storeInCode summaries are sound, and why the mulDiv ghost summaries add no assumption. - Document why exactly two collaterals is general: liquidating touches a single collateral, so the second one realizes the arbitrary otherCollatContribution of the Rocq proof. Moved the market size from a require in the rule into the ghost axiom. - Inline the two single-use axiomUpRoundsUp / axiomCeilLeOfMulGe definitions. - Drop mulDivDownBoundedIncrease from MulDiv.spec: it follows from mulDivMonotoneA and mulDivAddDownUp, which the L3 justification now cites directly. - Drop the MaxRepaidHealthy back-reference comment on mulDivCeilLeOfMulGe and the remaining fragile Midnight.sol:NNN line references. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/helpers/MidnightWrapper.sol | 19 ----------- certora/specs/MaxRepaidHealthy.spec | 49 ++++++++++++++++------------- certora/specs/MulDiv.spec | 6 ---- 3 files changed, 28 insertions(+), 46 deletions(-) diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index 85906a910..4b254dc9d 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -56,23 +56,4 @@ contract MidnightWrapper is Midnight { uint256 lif = maxLif(lltv, liquidatedParam.liquidationCursor); return (debt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lif * lltv); } - - /* badDebtFor recomputes the badDebt of Midnight.liquidate (see src/Midnight.sol:643-655) through a - * bitmap-free, array-based code path. Used to pin the no-bad-debt case (badDebtFor == 0), under which - * liquidate does not reduce _position.debt before the L699 cap computation. */ - function badDebtFor(Market memory market, bytes32 id, address borrower) public view returns (uint256) { - Position storage _position = position[id][borrower]; - uint256 badDebt = _position.debt; - uint256 len = market.collateralParams.length; - for (uint256 i = len; i > 0;) { - i--; - CollateralParams memory collateralParam = market.collateralParams[i]; - uint256 price = IOracle(collateralParam.oracle).price(); - badDebt = badDebt.zeroFloorSub( - _position.collateral[i].mulDivUp(price, ORACLE_PRICE_SCALE) - .mulDivUp(WAD, maxLif(collateralParam.lltv, collateralParam.liquidationCursor)) - ); - } - return badDebt; - } } diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index 5a707adc9..33f57a8a4 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -14,12 +14,25 @@ methods { // 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. function _.price() external => summaryPrice(calledContract) expect(uint256); + + // The three summaries below do not restrict the verified behaviours: + // - tickToPrice: NONDET havocs the return value, which is an over-approximation (it allows every tick + // price, including the real one). Tick prices only feed the order-book accounting, never the health + // computation this rule reasons about, so losing that information costs nothing. + // - toId: replaces the keccak derivation by a ghost that is only required to be deterministic and + // injective on the pinned market. Both hold for the real derivation up to hash collisions, which is + // the standing assumption everywhere ids are summarized (see Healthiness.spec). + // - storeInCode: NONDET havocs the returned address. The function only mirrors the market into code for + // cheap retrieval; the position and market storage the rule reads is untouched, so over-approximating + // the address it returns cannot hide a counterexample. function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; - // Summarize mulDivDown and mulDivUp deterministically; the tight rounding facts about them are proved - // over concrete mulDiv in MulDiv.spec and injected below only at the specific instances the rule needs. + // Summarizing mulDivDown and mulDivUp by unconstrained deterministic ghosts adds no assumption about + // mulDiv: the ghosts are arbitrary, and the summaries revert on a nondeterministic overflow flag, 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. 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); @@ -43,15 +56,6 @@ persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256; persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; -// Tight rounding facts proved over concrete mulDiv in MulDiv.spec. The rule assumes only the ground instances -// it uses, avoiding quantified background axioms. - -// Proved in mulDivUpRoundsUp: a * b <= ceil(a * b / d) * d. -definition axiomUpRoundsUp(uint256 a, uint256 b, uint256 d) returns bool = d > 0 => a * b <= ghostMulDivUp(a, b, d) * d; - -// 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; - function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -69,14 +73,18 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { } // Pin every field that contributes to the market id, making the toId summary deterministic and injective. -// The rule specializes this market to two collaterals. persistent ghost address globalMarketLoanToken; persistent ghost uint256 globalMarketChainId; +// Exactly two collaterals is not a restriction on the result. Liquidating touches a single collateral, so the +// whole contribution of every other collateral to maxDebt enters the reasoning as one arbitrary non-negative +// value, and one extra collateral with an arbitrary amount, price and LLTV already realizes every such value. +// The second collateral therefore plays the role of the arbitrary otherCollatContribution of the Rocq proof, +// and a market with more collaterals is covered by the same argument. persistent ghost uint256 globalMarketCollateralLength { - axiom globalMarketCollateralLength <= 2; + axiom globalMarketCollateralLength == 2; } persistent ghost mapping(uint256 => address) globalMarketCollateralOracle; @@ -124,12 +132,11 @@ 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. +// The call uses normal mode and covers the strictly unhealthy and health-boundary cases. See the +// globalMarketCollateralLength axiom for why two collaterals is general enough. rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrower, address receiver, address callback, bytes data) { Midnight.Market globalMarket = getGlobalMarket(); - require globalMarketCollateralLength == 2, "two-collateral market"; - uint256 collatBefore = collateral(globalId, borrower, collateralIndex); uint256 debtBefore = debt(globalId, borrower); @@ -149,7 +156,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow uint256 collatAfter = assert_uint256(collatBefore - seizedOut); /// MAX-DEBT DROP BOUND /// - // Establish curContrib - newContrib <= maxDebtDropBound. At Midnight.sol:692, liquidate computes + // 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. @@ -158,7 +165,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow uint256 maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD()); uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle); - // By Midnight.sol:692, seizedOut == ghostMulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price). + // 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()); @@ -170,7 +177,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow require price > 0 => ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()) <= maxSeizedValue, "L1: mulDivInverseUpDown with a=maxSeizedValue, b=ORACLE_PRICE_SCALE, d=price (MulDiv.spec)"; require curCollatValue <= newCollatValue + ghostMulDivUp(seizedOut, price, ORACLE_PRICE_SCALE()), "L2: mulDivAddDownUp with a1=collatAfter, a2=seizedOut, b=price, d=ORACLE_PRICE_SCALE (MulDiv.spec)"; - require curCollatValue <= newCollatValue + maxSeizedValue => curContrib <= newContrib + ghostMulDivUp(maxSeizedValue, lltv, WAD()), "L3: mulDivDownBoundedIncrease with a1=curCollatValue, a2=newCollatValue, delta=maxSeizedValue, b=lltv, d=WAD (MulDiv.spec)"; + require 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)"; // L1-L2 bound the collateral-value decrease by maxSeizedValue. L3 transports that bound through the LLTV @@ -187,9 +194,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 axiomUpRoundsUp(gap, WAD_SQUARED(), rcfDenominator), "proved in mulDivUpRoundsUp"; + require rcfDenominator > 0 => gap * WAD_SQUARED() <= ghostMulDivUp(gap, WAD_SQUARED(), rcfDenominator) * rcfDenominator, "proved in mulDivUpRoundsUp"; uint256 repaidExcess = assert_uint256(repaidUnits - gap); - require axiomCeilLeOfMulGe(repaidUnits, lifTimesLltv, WAD_SQUARED(), repaidExcess), "proved in mulDivCeilLeOfMulGe"; + require repaidUnits * lifTimesLltv <= repaidExcess * WAD_SQUARED() => ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()) <= repaidExcess, "proved in mulDivCeilLeOfMulGe"; assert isHealthyNoBitmap(globalMarket, globalId, borrower); } diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index 27ba3924b..be925411b 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -72,11 +72,6 @@ rule mulDivAddDownUp(uint256 a1, uint256 a2, uint256 b, uint256 d) { assert mulDivDown(a1, b, d) + mulDivUp(a2, b, d) >= mulDivDown(a1plusa2, b, d); } -// Increasing the first argument by at most delta increases mulDivDown by at most mulDivUp(delta, b, d). -rule mulDivDownBoundedIncrease(uint256 a1, uint256 a2, uint256 delta, uint256 b, uint256 d) { - assert a1 <= a2 + delta => mulDivDown(a1, b, d) <= mulDivDown(a2, b, d) + mulDivUp(delta, b, d); -} - // Rounding down the first scaling step cannot increase the result of a second scaling rounded up. rule mulDivDownUpComposition(uint256 a, uint256 b, uint256 c, uint256 d) { uint256 bc = require_uint256(b * c); @@ -126,7 +121,6 @@ rule mulDivUpUpperBound(uint256 a, uint256 b, uint256 d) { } // If the exact product is at most bound * d, then the ceiling is at most bound. -// Used by MaxRepaidHealthy.spec (axiomCeilLeOfMulGe) for its final max-debt-drop bound. rule mulDivCeilLeOfMulGe(uint256 a, uint256 b, uint256 d, uint256 bound) { assert d != 0 && a * b <= bound * d => mulDivUp(a, b, d) <= bound; } From 231137375d3a8dba8bb1461e573efb6b340ca1c2 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 27 Aug 2026 10:24:39 +0000 Subject: [PATCH 12/19] [Certora] Drop contract-line references from maxRepaidFor's comment Same thumbed-up review point as the spec cleanup: contract line numbers are fragile, so name the mechanism instead. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01LCJKePb6Hd7MnhvwJsFT1B --- certora/helpers/MidnightWrapper.sol | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index 66f20dca0..945438092 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -31,9 +31,9 @@ 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). + /* 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). * 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 From ad0e410b1a1a614404186673c5aec4d3836d0efa Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 31 Aug 2026 17:42:30 +0200 Subject: [PATCH 13/19] Use MulDivAxioms. Also added the axioms the spec needs to MulDiv and MulDivAxioms. --- certora/specs/MaxRepaidHealthy.spec | 62 ++++++++++++++--------------- certora/specs/MulDiv.spec | 8 ++++ certora/specs/MulDivAxioms.spec | 4 ++ 3 files changed, 41 insertions(+), 33 deletions(-) diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index 33f57a8a4..5e78be0e0 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; @@ -52,24 +53,18 @@ 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; - function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { - bool overflow; - if (overflow || d == 0) { + if (d == 0 || a * b >= 2 ^ 256) { revert(); } - return ghostMulDivDown(a, b, d); + return require_uint256(ghostMulDivDown(a, b, d)); } function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { - bool overflow; - if (overflow || d == 0) { + if (d == 0 || a * b + d - 1 >= 2 ^ 256) { 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. @@ -154,6 +149,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow seizedOut, repaidOut = liquidate(e, globalMarket, collateralIndex, 0, repaidUnits, borrower, false, receiver, callback, data); uint256 collatAfter = assert_uint256(collatBefore - seizedOut); + bool isHealthyAfter = isHealthyNoBitmap(globalMarket, globalId, borrower); /// MAX-DEBT DROP BOUND /// // Establish curContrib - newContrib <= maxDebtDropBound. When it seizes, liquidate computes @@ -162,23 +158,24 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow uint256 lltv = globalMarketCollateralLLTV[collateralIndex]; uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]); - uint256 maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD()); + mathint maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD()); uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle); // 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()); + mathint curCollatValue = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + mathint newCollatValue = ghostMulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); - uint256 curContrib = ghostMulDivDown(curCollatValue, lltv, WAD()); - uint256 newContrib = ghostMulDivDown(newCollatValue, lltv, WAD()); + mathint curContrib = ghostMulDivDown(curCollatValue, lltv, WAD()); + mathint newContrib = ghostMulDivDown(newCollatValue, lltv, WAD()); - uint256 lifTimesLltv = assert_uint256(lif * lltv); - uint256 maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()); + mathint lifTimesLltv = lif * lltv; + mathint maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()); - 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)"; + require axiomMathMulDivInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "axiom L1"; + require axiomMathMulDivAddDownUp(collatAfter, seizedOut, price, ORACLE_PRICE_SCALE()), "axiom L2"; + require axiomMathMulDivDownMonotoneA(curCollatValue, newCollatValue + maxSeizedValue, lltv, WAD()), "axiom L3"; + require axiomMathMulDivAddDownUp(newCollatValue, maxSeizedValue, lltv, WAD()), "axiom L3"; + require axiomMathMulDivDownUpComposition(repaidUnits, lif, lltv, WAD()), "axiom L4"; // 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. @@ -187,16 +184,15 @@ 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. - 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"; - uint256 repaidExcess = assert_uint256(repaidUnits - gap); - require repaidUnits * lifTimesLltv <= repaidExcess * WAD_SQUARED() => ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()) <= repaidExcess, "proved in mulDivCeilLeOfMulGe"; - - assert isHealthyNoBitmap(globalMarket, globalId, borrower); + mathint otherCollatValue = ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()); + mathint otherContrib = ghostMulDivDown(otherCollatValue, otherLltv, WAD()); + mathint maxDebtBefore = curContrib + otherContrib; + + mathint gap = debtBefore - maxDebtBefore; + mathint rcfDenominator = WAD_SQUARED() - lifTimesLltv; + require axiomMathMulDivUpRoundsUp(gap, WAD_SQUARED(), rcfDenominator), "axiom"; + mathint repaidExcess = repaidUnits - gap; + require axiomMathMulDivCeilLeOfMulGe(repaidUnits, lifTimesLltv, WAD_SQUARED(), repaidExcess), "axiom"; + + assert isHealthyAfter; } diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index f2e1073eb..d00508070 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -212,6 +212,10 @@ 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); } +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); +} + rule mathMulDivInverseDownUp(mathint a, mathint b, mathint d) { assert b > 0 && d > 0 => a <= mathMulDivDown(mathMulDivUp(a, b, d), d, b); } @@ -257,6 +261,10 @@ rule mathMulDivUpUpperBound(mathint a, mathint b, mathint d) { assert a >= 0 && b >= 0 && d > 0 => mathMulDivUp(a, b, d) * d <= a * b + d - 1; } +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 mathMulDivResidualBound(mathint a, mathint b, mathint d) { assert a >= 0 && b >= 0 && a <= d && b <= d => a - mathMulDivDown(a, b, d) <= d - b; assert a >= 0 && b >= 0 && a <= d && b <= d => a - mathMulDivUp(a, b, d) <= d - b; diff --git a/certora/specs/MulDivAxioms.spec b/certora/specs/MulDivAxioms.spec index 659a29e1a..5c10cbd4a 100644 --- a/certora/specs/MulDivAxioms.spec +++ b/certora/specs/MulDivAxioms.spec @@ -58,6 +58,8 @@ 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); +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); + 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; @@ -87,6 +89,8 @@ definition axiomMathMulDivUpTightBound(mathint a, mathint b, mathint d) returns definition axiomMathMulDivUpUpperBound(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && d > 0 => mathMulDivUp(a, b, d) * d <= a * b + d - 1; +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 axiomMathMulDivDownResidualBound(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && a <= d && b <= d => a - mathMulDivDown(a, b, d) <= d - b; definition axiomMathMulDivUpResidualBound(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 && a <= d && b <= d => a - mathMulDivUp(a, b, d) <= d - b; From 1dbe74379c24c81c8d0170962f5460b2ed7e04d6 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 31 Aug 2026 19:47:28 +0200 Subject: [PATCH 14/19] Update certora/specs/MaxRepaidHealthy.spec Co-authored-by: Quentin Garchery Signed-off-by: Jochen Hoenicke --- certora/specs/MaxRepaidHealthy.spec | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index 5e78be0e0..f7511e4bc 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -171,11 +171,15 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow mathint lifTimesLltv = lif * lltv; mathint maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()); - require axiomMathMulDivInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "axiom L1"; - require axiomMathMulDivAddDownUp(collatAfter, seizedOut, price, ORACLE_PRICE_SCALE()), "axiom L2"; - require axiomMathMulDivDownMonotoneA(curCollatValue, newCollatValue + maxSeizedValue, lltv, WAD()), "axiom L3"; - require axiomMathMulDivAddDownUp(newCollatValue, maxSeizedValue, lltv, WAD()), "axiom L3"; - require axiomMathMulDivDownUpComposition(repaidUnits, lif, lltv, WAD()), "axiom L4"; + // L1: seizedOut * price <= maxSeizedValue + require axiomMathMulDivInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "axiom"; + // L2: curCollatValue <= newCollatValue + seizedOut * price + require axiomMathMulDivAddDownUp(collatAfter, seizedOut, price, ORACLE_PRICE_SCALE()), "axiom"; + // L3: curCollatValue <= newCollatValue + maxSeizedValue => curContrib <= newContrib + maxSeizedValue * lltv + require axiomMathMulDivDownMonotoneA(curCollatValue, newCollatValue + maxSeizedValue, lltv, WAD()), "axiom"; + require axiomMathMulDivAddDownUp(newCollatValue, maxSeizedValue, lltv, WAD()), "axiom"; + // L4: maxSeizedValue * lltv <= maxDebtDropBound + require axiomMathMulDivDownUpComposition(repaidUnits, lif, lltv, WAD()), "axiom"; // 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. From af632555c17ca5db5621af0bace0da3f09a6dca5 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 31 Aug 2026 19:52:12 +0200 Subject: [PATCH 15/19] Rename cur -> old --- certora/specs/MaxRepaidHealthy.spec | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index f7511e4bc..e912965e0 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -152,7 +152,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow bool isHealthyAfter = isHealthyNoBitmap(globalMarket, globalId, borrower); /// MAX-DEBT DROP BOUND /// - // Establish curContrib - newContrib <= maxDebtDropBound. When it seizes, liquidate computes + // Establish oldContrib - 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. @@ -162,10 +162,10 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle); // By that same computation, seizedOut == ghostMulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price). - mathint curCollatValue = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + mathint oldCollatValue = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); mathint newCollatValue = ghostMulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); - mathint curContrib = ghostMulDivDown(curCollatValue, lltv, WAD()); + mathint oldContrib = ghostMulDivDown(oldCollatValue, lltv, WAD()); mathint newContrib = ghostMulDivDown(newCollatValue, lltv, WAD()); mathint lifTimesLltv = lif * lltv; @@ -173,10 +173,10 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow // L1: seizedOut * price <= maxSeizedValue require axiomMathMulDivInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "axiom"; - // L2: curCollatValue <= newCollatValue + seizedOut * price + // L2: oldCollatValue <= newCollatValue + seizedOut * price require axiomMathMulDivAddDownUp(collatAfter, seizedOut, price, ORACLE_PRICE_SCALE()), "axiom"; - // L3: curCollatValue <= newCollatValue + maxSeizedValue => curContrib <= newContrib + maxSeizedValue * lltv - require axiomMathMulDivDownMonotoneA(curCollatValue, newCollatValue + maxSeizedValue, lltv, WAD()), "axiom"; + // L3: oldCollatValue <= newCollatValue + maxSeizedValue => oldContrib <= newContrib + maxSeizedValue * lltv + require axiomMathMulDivDownMonotoneA(oldCollatValue, newCollatValue + maxSeizedValue, lltv, WAD()), "axiom"; require axiomMathMulDivAddDownUp(newCollatValue, maxSeizedValue, lltv, WAD()), "axiom"; // L4: maxSeizedValue * lltv <= maxDebtDropBound require axiomMathMulDivDownUpComposition(repaidUnits, lif, lltv, WAD()), "axiom"; @@ -190,7 +190,7 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow // repaid in excess of the old health gap. mathint otherCollatValue = ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()); mathint otherContrib = ghostMulDivDown(otherCollatValue, otherLltv, WAD()); - mathint maxDebtBefore = curContrib + otherContrib; + mathint maxDebtBefore = oldContrib + otherContrib; mathint gap = debtBefore - maxDebtBefore; mathint rcfDenominator = WAD_SQUARED() - lifTimesLltv; From b67df3c235e6a21f228d90f20f37c0007afc594e Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 08:44:03 +0000 Subject: [PATCH 16/19] [Certora] Re-add rocq/maxRepaidHealthy.v Restore the Rocq proof of the maxRepaidHealthy bound, deleted in b5281c1e ("clean"). Content is byte-identical to the version on main. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> --- rocq/maxRepaidHealthy.v | 366 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 366 insertions(+) create mode 100644 rocq/maxRepaidHealthy.v diff --git a/rocq/maxRepaidHealthy.v b/rocq/maxRepaidHealthy.v new file mode 100644 index 000000000..273b6a77c --- /dev/null +++ b/rocq/maxRepaidHealthy.v @@ -0,0 +1,366 @@ +From Stdlib Require Import ZArith Lia Psatz. + +Open Scope Z_scope. + +Definition WAD : Z := 1000000000000000000. +Definition ORACLE_PRICE_SCALE : Z := 1000000000000000000000000000000000000. + +Definition ceil_div (numerator denominator : Z) : Z := + (numerator + denominator - 1) / denominator. + +(** +If: +- maxRepaid is computed as: + ceil((debt - maxDebt) * WAD^2 / (WAD^2 - lif * lltv)) +- repaid is the amount actually repaid: min(maxRepaid, debt) +- seizedAssets is computed as: + floor(floor(repaid * lif / WAD) * ORACLE_PRICE_SCALE / price) +- maxDebt is computed from the current collateral as: + otherCollatContribution + floor(floor(collat * price / ORACLE_PRICE_SCALE) * lltv / WAD) + +then after liquidating repaid, the borrower is healthy: + newDebt <= newMaxDebt + +This proof is entirely over integer arithmetic. +It does not use real-number approximations. +The assumptions that the collateral seized does not exceed the current collateral does not narrow the generality of the proof: in that case the transaction would revert independently of the RCF mechanism, so that mechanism does not restrict the possibility to go back to health. +*) + +Definition max_repaid_liquidation_leaves_healthy_statement : Prop := + forall debt otherCollatContribution collat price lltv lif, + let maxDebt := + otherCollatContribution + + (collat * price / ORACLE_PRICE_SCALE) * lltv / WAD in + let maxRepaid := + ceil_div ((debt - maxDebt) * (WAD * WAD)) + (WAD * WAD - lif * lltv) in + let repaid := Z.min maxRepaid debt in + let seizedAssets := + (repaid * lif / WAD * ORACLE_PRICE_SCALE) / price in + let newDebt := debt - repaid in + let newMaxDebt := + otherCollatContribution + + ((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv / WAD in + 0 < price -> + 0 <= debt -> 0 <= otherCollatContribution -> + 0 <= collat -> + 0 <= lltv -> 0 <= lif -> + lif * lltv < WAD * WAD -> + maxDebt <= debt -> + seizedAssets <= collat -> + 0 <= newDebt /\ newDebt <= newMaxDebt. + +(* -------------------------------------------------------------------------- *) +(* Generic integer-division lemmas *) +(* -------------------------------------------------------------------------- *) + +Lemma WAD_pos : 0 < WAD. +Proof. unfold WAD; lia. Qed. + +Lemma ORACLE_PRICE_SCALE_pos : 0 < ORACLE_PRICE_SCALE. +Proof. unfold ORACLE_PRICE_SCALE; lia. Qed. + +Lemma div_upper_strict : + forall numerator denominator, + 0 < denominator -> 0 <= numerator -> + numerator < denominator * (numerator / denominator + 1). +Proof. + intros numerator denominator Hden Hnum. + pose proof (Z.div_mod numerator denominator) as Hdivmod. + specialize (Hdivmod ltac:(lia)). + pose proof (Z.mod_pos_bound numerator denominator Hden) as Hmod. + nia. +Qed. + +Lemma floor_mul_le : + forall numerator denominator, + 0 < denominator -> 0 <= numerator -> + (numerator / denominator) * denominator <= numerator. +Proof. + intros numerator denominator Hden Hnum. + pose proof (Z.div_mod numerator denominator) as Hdivmod. + specialize (Hdivmod ltac:(lia)). + pose proof (Z.mod_pos_bound numerator denominator Hden) as Hmod. + nia. +Qed. + +Lemma ceil_div_mul_ge : + forall numerator denominator, + 0 < denominator -> 0 <= numerator -> + numerator <= ceil_div numerator denominator * denominator. +Proof. + intros numerator denominator Hden Hnum. + unfold ceil_div. + pose proof (Z.div_mod (numerator + denominator - 1) denominator) as Hdivmod. + specialize (Hdivmod ltac:(lia)). + pose proof (Z.mod_pos_bound (numerator + denominator - 1) denominator Hden) as Hmod. + nia. +Qed. + +Lemma ceil_div_le_of_mul_ge : + forall numerator denominator bound, + 0 < denominator -> 0 <= numerator -> numerator <= bound * denominator -> + ceil_div numerator denominator <= bound. +Proof. + intros numerator denominator bound Hden Hnum Hbound. + unfold ceil_div. + assert ((numerator + denominator - 1) / denominator < bound + 1) as Hlt. + { apply Z.div_lt_upper_bound; nia. } + lia. +Qed. + +Lemma ceil_div_mono : + forall left right denominator, + 0 < denominator -> left <= right -> + ceil_div left denominator <= ceil_div right denominator. +Proof. + intros left right denominator Hden Hle. + unfold ceil_div. + apply Z.div_le_mono; lia. +Qed. + +Lemma floor_drop_div_le_ceil : + forall base drop denominator, + 0 < denominator -> 0 <= base -> 0 <= drop -> + (base + drop) / denominator - base / denominator <= ceil_div drop denominator. +Proof. + intros base drop denominator Hden Hbase Hdrop. + assert (Hbase_lt : base < denominator * (base / denominator + 1)). + { apply div_upper_strict; lia. } + assert (Hdrop_le : drop <= ceil_div drop denominator * denominator). + { apply ceil_div_mul_ge; lia. } + assert ((base + drop) / denominator < base / denominator + ceil_div drop denominator + 1) as Hlt. + { apply Z.div_lt_upper_bound; nia. } + lia. +Qed. + +(* -------------------------------------------------------------------------- *) +(* Midnight-specific rounding lemmas *) +(* -------------------------------------------------------------------------- *) + +Lemma seized_value_drop_le_maxSeizedValue : + forall maxRepaid lif price seizedAssets, + 0 < price -> + 0 <= maxRepaid -> 0 <= lif -> + seizedAssets = (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> + ceil_div (seizedAssets * price) ORACLE_PRICE_SCALE <= maxRepaid * lif / WAD. +Proof. + intros maxRepaid lif price seizedAssets Hprice HmaxRepaid Hlif Hseized. + subst seizedAssets. + assert (HWAD : 0 < WAD) by apply WAD_pos. + assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. + assert (HmaxSeizedValue_nonneg : 0 <= maxRepaid * lif / WAD). + { apply Z.div_pos; nia. } + apply ceil_div_le_of_mul_ge. + - exact Hscale. + - apply Z.mul_nonneg_nonneg; [apply Z.div_pos |]; nia. + - pose proof (floor_mul_le (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) price Hprice) as Hfloor. + specialize (Hfloor ltac:(nia)). + nia. +Qed. + +Lemma max_debt_contribution_drop_bound : + forall collat seizedAssets price lltv maxRepaid lif, + 0 < price -> + 0 <= collat -> 0 <= seizedAssets -> seizedAssets <= collat -> + 0 <= lltv -> 0 <= maxRepaid -> 0 <= lif -> + seizedAssets = (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> + let currentCollatValue := collat * price / ORACLE_PRICE_SCALE in + let newCollatValue := (collat - seizedAssets) * price / ORACLE_PRICE_SCALE in + currentCollatValue * lltv / WAD - newCollatValue * lltv / WAD + <= ceil_div (maxRepaid * lif * lltv) (WAD * WAD). +Proof. + intros collat seizedAssets price lltv maxRepaid lif + Hprice Hcollat HseizedNonneg HseizedLe Hlltv HmaxRepaid Hlif HseizedEq + currentCollatValue newCollatValue. + subst currentCollatValue newCollatValue. + assert (HWAD : 0 < WAD) by apply WAD_pos. + assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. + + set (collatValueDrop := + collat * price / ORACLE_PRICE_SCALE - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE). + set (maxSeizedValue := maxRepaid * lif / WAD). + set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). + + assert (HcollatValueDrop_le : collatValueDrop <= maxSeizedValue). + { + unfold collatValueDrop, maxSeizedValue. + replace (collat * price) + with ((collat - seizedAssets) * price + seizedAssets * price) by nia. + eapply Z.le_trans. + - apply floor_drop_div_le_ceil; nia. + - eapply seized_value_drop_le_maxSeizedValue; eauto; nia. + } + + assert (Hold_ge_new_value : + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE <= collat * price / ORACLE_PRICE_SCALE). + { + apply Z.div_le_mono; nia. + } + + assert (HmaxDebtDrop_by_valueDrop : + collat * price / ORACLE_PRICE_SCALE * lltv / WAD + - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD + <= ceil_div (collatValueDrop * lltv) WAD). + { + unfold collatValueDrop. + replace (collat * price / ORACLE_PRICE_SCALE * lltv) + with (((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv + + (collat * price / ORACLE_PRICE_SCALE - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv) by nia. + eapply floor_drop_div_le_ceil. + - exact HWAD. + - apply Z.mul_nonneg_nonneg; try nia. + apply Z.div_pos; nia. + - apply Z.mul_nonneg_nonneg; nia. + } + + assert (Hceil_valueDrop_le_maxSeizedValue : + ceil_div (collatValueDrop * lltv) WAD <= ceil_div (maxSeizedValue * lltv) WAD). + { + apply ceil_div_mono; nia. + } + + assert (HmaxSeizedValue_floor : maxSeizedValue * WAD <= maxRepaid * lif). + { + unfold maxSeizedValue. + apply floor_mul_le; nia. + } + + assert (HmaxDebtDropBound_mul : maxRepaid * lif * lltv <= maxDebtDropBound * (WAD * WAD)). + { + unfold maxDebtDropBound. + apply ceil_div_mul_ge; nia. + } + + assert (HmaxSeizedValue_to_maxDebtDropBound : maxSeizedValue * lltv <= maxDebtDropBound * WAD). + { + nia. + } + + assert (Hceil_maxSeizedValue_le_maxDebtDropBound : + ceil_div (maxSeizedValue * lltv) WAD <= maxDebtDropBound). + { + apply ceil_div_le_of_mul_ge; nia. + } + + lia. +Qed. + +(* -------------------------------------------------------------------------- *) +(* Final theorem *) +(* -------------------------------------------------------------------------- *) + +Theorem max_repaid_liquidation_leaves_healthy : + max_repaid_liquidation_leaves_healthy_statement. +Proof. + unfold max_repaid_liquidation_leaves_healthy_statement. + intros debt otherCollatContribution collat price lltv lif. + set (maxDebt := otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD). + set (maxRepaid := ceil_div ((debt - maxDebt) * (WAD * WAD)) (WAD * WAD - lif * lltv)). + set (repaid := Z.min maxRepaid debt). + set (seizedAssets := repaid * lif / WAD * ORACLE_PRICE_SCALE / price). + set (newDebt := debt - repaid). + set (newMaxDebt := otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD). + intros Hprice Hdebt Hother Hcollat Hlltv Hlif Hden HmaxDebtLeDebt HseizedLeCollat. + assert (HWAD : 0 < WAD) by apply WAD_pos. + assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. + assert (Hden_pos : 0 < WAD * WAD - lif * lltv) by nia. + assert (HmaxDebt_nonneg : 0 <= maxDebt). + { + subst maxDebt. + assert (HcollatValue_nonneg : 0 <= collat * price / ORACLE_PRICE_SCALE). + { apply Z.div_pos; nia. } + assert (HcollatContribution_nonneg : 0 <= collat * price / ORACLE_PRICE_SCALE * lltv / WAD). + { apply Z.div_pos; nia. } + nia. + } + assert (HmaxRepaid_nonneg : 0 <= maxRepaid). + { + subst maxRepaid. + unfold ceil_div. + apply Z.div_pos; nia. + } + assert (Hrepaid_nonneg : 0 <= repaid). + { + subst repaid. + apply Z.min_glb; assumption. + } + assert (Hrepaid_le_debt : repaid <= debt). + { + subst repaid. + apply Z.le_min_r. + } + split. + - subst newDebt; lia. + - destruct (Z.leb_spec0 debt maxRepaid) as [Hdebt_le_maxRepaid | HmaxRepaid_lt_debt]. + + assert (Hrepaid_eq : repaid = debt). + { subst repaid. apply Z.min_r. lia. } + subst newDebt newMaxDebt. + rewrite Hrepaid_eq. + assert (Hseized_nonneg : 0 <= seizedAssets). + { + subst seizedAssets. + rewrite Hrepaid_eq. + apply Z.div_pos. + - apply Z.mul_nonneg_nonneg. + + apply Z.div_pos; nia. + + lia. + - lia. + } + assert (HnewCollatValue_nonneg : 0 <= (collat - seizedAssets) * price / ORACLE_PRICE_SCALE). + { apply Z.div_pos; nia. } + assert (HnewContribution_nonneg : + 0 <= (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD). + { apply Z.div_pos; nia. } + nia. + + assert (Hrepaid_eq : repaid = maxRepaid). + { subst repaid. apply Z.min_l. lia. } + set (gap := debt - maxDebt). + set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). + assert (Hgap_nonneg : 0 <= gap) by (unfold gap; lia). + assert (HmaxRepaid_def_le : + gap * (WAD * WAD) <= maxRepaid * (WAD * WAD - lif * lltv)). + { + subst maxRepaid. + unfold gap. + apply ceil_div_mul_ge; nia. + } + assert (Hextra_mul : + (maxRepaid - gap) * (WAD * WAD) >= maxRepaid * lif * lltv). + { nia. } + assert (HmaxDebtDropBound_le_extra : maxDebtDropBound <= maxRepaid - gap). + { + unfold maxDebtDropBound. + apply ceil_div_le_of_mul_ge; nia. + } + assert (Hseized_nonneg : 0 <= seizedAssets). + { + subst seizedAssets. + rewrite Hrepaid_eq. + apply Z.div_pos. + - apply Z.mul_nonneg_nonneg. + + apply Z.div_pos; nia. + + lia. + - lia. + } + assert (HseizedEq : seizedAssets = maxRepaid * lif / WAD * ORACLE_PRICE_SCALE / price). + { + subst seizedAssets. + rewrite Hrepaid_eq. + reflexivity. + } + assert (HmaxDebtDrop_le_bound : maxDebt - newMaxDebt <= maxDebtDropBound). + { + subst maxDebt newMaxDebt. + replace (otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD - + (otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD)) + with (collat * price / ORACLE_PRICE_SCALE * lltv / WAD - + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD) by lia. + unfold maxDebtDropBound. + eapply max_debt_contribution_drop_bound; eauto; nia. + } + subst newDebt. + rewrite Hrepaid_eq. + unfold gap in *. + lia. +Qed. From ee0e9a52708e1026d49fc18f1db14f900b537370 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 08:54:12 +0000 Subject: [PATCH 17/19] Fix formatting for forge fmt and CVL linter Apply the `forge fmt --check` diff reported by CI (forge 1.8.1) to certora/helpers/MidnightWrapper.sol: split the chained mulDivDown call onto its own line. Apply certoraCVLFormatter to certora/specs/MaxRepaidHealthy.spec: add the blank lines it wants before the L2/L3/L4 axiom comments. Both changes are whitespace-only; every spec is now zero-diff against certoraCVLFormatter. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> --- certora/helpers/MidnightWrapper.sol | 3 ++- certora/specs/MaxRepaidHealthy.spec | 3 +++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index e856f1346..0c9dfda48 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -49,7 +49,8 @@ contract MidnightWrapper is Midnight { i--; CollateralParams memory collateralParam = market.collateralParams[i]; uint256 price = IOracle(collateralParam.oracle).price(); - maxDebt += _position.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE) + maxDebt += _position.collateral[i] + .mulDivDown(price, ORACLE_PRICE_SCALE) .mulDivDown(collateralParam.lltv, WAD); } CollateralParams memory liquidatedParam = market.collateralParams[collateralIndex]; diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec index e912965e0..cc1d0985f 100644 --- a/certora/specs/MaxRepaidHealthy.spec +++ b/certora/specs/MaxRepaidHealthy.spec @@ -173,11 +173,14 @@ rule liquidateAtCapRestoresHealth(env e, uint256 collateralIndex, address borrow // L1: seizedOut * price <= maxSeizedValue require axiomMathMulDivInverseUpDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price), "axiom"; + // L2: oldCollatValue <= newCollatValue + seizedOut * price require axiomMathMulDivAddDownUp(collatAfter, seizedOut, price, ORACLE_PRICE_SCALE()), "axiom"; + // L3: oldCollatValue <= newCollatValue + maxSeizedValue => oldContrib <= newContrib + maxSeizedValue * lltv require axiomMathMulDivDownMonotoneA(oldCollatValue, newCollatValue + maxSeizedValue, lltv, WAD()), "axiom"; require axiomMathMulDivAddDownUp(newCollatValue, maxSeizedValue, lltv, WAD()), "axiom"; + // L4: maxSeizedValue * lltv <= maxDebtDropBound require axiomMathMulDivDownUpComposition(repaidUnits, lif, lltv, WAD()), "axiom"; From f037e30abdf9530474cab2ab15d8029eb28321e9 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 09:01:17 +0000 Subject: [PATCH 18/19] docs(certora): document MaxRepaidHealthy.spec Add the README entry for MaxRepaidHealthy.spec: liquidating an unhealthy position at the recovery close factor cap restores health, the restoration counterpart to Healthiness.spec's preservation property. Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> --- certora/README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/certora/README.md b/certora/README.md index 5680c7947..af9c8b97f 100644 --- a/certora/README.md +++ b/certora/README.md @@ -37,6 +37,9 @@ Global invariants on positions, markets and accounting. Healthy positions stay healthy, and liquidations only touch liquidatable positions within the incentive bound. - [`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. - [`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`. From 2c86395f2120ca8e22e0ec8a9a39a1d9fe73fbf2 Mon Sep 17 00:00:00 2001 From: MathisGD <74971347+MathisGD@users.noreply.github.com> Date: Tue, 1 Sep 2026 11:06:16 +0200 Subject: [PATCH 19/19] Apply batched suggestions from code review Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com> --- certora/README.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/certora/README.md b/certora/README.md index af9c8b97f..3763ff3b6 100644 --- a/certora/README.md +++ b/certora/README.md @@ -37,9 +37,8 @@ Global invariants on positions, markets and accounting. Healthy positions stay healthy, and liquidations only touch liquidatable positions within the incentive bound. - [`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. +- [`MaxRepaidHealthy.spec`](specs/MaxRepaidHealthy.spec) checks that an unhealthy borrower liquidated in normal mode is healthy again once the liquidator has repaid `maxRepaid`, the recovery close factor cap. + `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. - [`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`.