diff --git a/certora/README.md b/certora/README.md index 5680c7947..3763ff3b6 100644 --- a/certora/README.md +++ b/certora/README.md @@ -37,6 +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 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`. 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 2b7d54c02..0c9dfda48 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -32,6 +32,33 @@ contract MidnightWrapper is Midnight { return maxDebt >= debt; } + /* 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 + 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); + } + // This realizableBadDebt function recomputes, verbatim, the badDebt local that // liquidate() computes at src/Midnight.sol:643-657, so that the prover can equate this // getter's result with liquidate's inlined bad-debt computation. diff --git a/certora/specs/MaxRepaidHealthy.spec b/certora/specs/MaxRepaidHealthy.spec new file mode 100644 index 000000000..cc1d0985f --- /dev/null +++ b/certora/specs/MaxRepaidHealthy.spec @@ -0,0 +1,205 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2026 Morpho Association + +import "BitmapSummaries.spec"; +import "MulDivAxioms.spec"; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function collateral(bytes32 id, address user, uint256) 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; + + // 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; + + // 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); + + // maxLif is deterministic for each (lltv, liquidationCursor) pair. + function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor); + + // Unresolved callbacks and token calls use AUTO/HAVOC_ECF, which models non-reentrant callees. +} + +/// SUMMARY /// + +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; + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + if (d == 0 || a * b >= 2 ^ 256) { + revert(); + } + return require_uint256(ghostMulDivDown(a, b, d)); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + if (d == 0 || a * b + d - 1 >= 2 ^ 256) { + revert(); + } + return require_uint256(ghostMulDivUp(a, b, d)); +} + +// Pin every field that contributes to the market id, making the toId summary deterministic and injective. + +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; +} + +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; + +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; +} + +/// 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. 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(); + + uint256 collatBefore = collateral(globalId, borrower, collateralIndex); + uint256 debtBefore = debt(globalId, borrower); + + // This rule checks that using `repaidUnits == maxRepaid` is enough to put the account healthy. This means that the RCF doesn't prevent to put the position back to health. + uint256 repaidUnits = maxRepaidFor(globalMarket, globalId, collateralIndex, borrower); + + // maxRepaidFor's non-reverting collateral lookup establishes collateralIndex < 2. + uint256 otherIndex = assert_uint256(1 - collateralIndex); + uint256 otherCollatBefore = collateral(globalId, borrower, otherIndex); + uint256 otherLltv = globalMarketCollateralLLTV[otherIndex]; + uint256 otherPrice = summaryPrice(globalMarket.collateralParams[otherIndex].oracle); + + uint256 seizedOut; + uint256 repaidOut; + 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 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. + + uint256 lltv = globalMarketCollateralLLTV[collateralIndex]; + uint256 lif = maxLifGhost(lltv, globalMarketCollateralLiquidationCursor[collateralIndex]); + mathint maxSeizedValue = ghostMulDivDown(repaidUnits, lif, WAD()); + uint256 price = summaryPrice(globalMarket.collateralParams[collateralIndex].oracle); + + // By that same computation, seizedOut == ghostMulDivDown(maxSeizedValue, ORACLE_PRICE_SCALE(), price). + mathint oldCollatValue = ghostMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + mathint newCollatValue = ghostMulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); + + mathint oldContrib = ghostMulDivDown(oldCollatValue, lltv, WAD()); + mathint newContrib = ghostMulDivDown(newCollatValue, lltv, WAD()); + + mathint lifTimesLltv = lif * lltv; + mathint maxDebtDropBound = ghostMulDivUp(repaidUnits, lifTimesLltv, WAD_SQUARED()); + + // 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"; + + // 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. + mathint otherCollatValue = ghostMulDivDown(otherCollatBefore, otherPrice, ORACLE_PRICE_SCALE()); + mathint otherContrib = ghostMulDivDown(otherCollatValue, otherLltv, WAD()); + mathint maxDebtBefore = oldContrib + 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 946a794b1..d00508070 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -88,6 +88,13 @@ rule mulDivAddDownUp(uint256 a1, uint256 a2, uint256 b, uint256 d) { assert mulDivDown(a1, b, d) + mulDivUp(a2, b, d) >= mulDivDown(a1plusa2, 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); } @@ -133,6 +140,11 @@ 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. +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; @@ -200,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); } @@ -245,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;