From edf78367c68b3c4cbd1218bd42e1c745c894361c Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 26 Jul 2026 19:49:26 +0000 Subject: [PATCH 01/11] [Certora] post-price-drop realizable bad debt cannot increase (liquidate) Add a rule proving that liquidating ahead of an oracle price drop cannot worsen the post-drop realizable bad debt: with liquidate executed at the call-time price p and realizable bad debt measured at a dropped price p' <= p, the post-liquidate p'-rbd R' is at most the do-nothing p'-rbd R. - Add realizableBadDebtAtPrice getter in MidnightWrapper.sol: a verbatim structural copy of realizableBadDebt that values each active collateral at an explicitly passed price instead of reading IOracle(...).price(), decoupling the measurement price from the price liquidate reads. - Add PostDropRealizableBadDebt.spec + conf: two rules (split along liquidate's exclusive-input branch), reusing the seize-value bound and double sub-additivity lemmas and adding getter-form price monotonicity (g is non-decreasing in the price argument) to bridge the p'-measured coverage drop to the p-priced seize/repay logic. Restricted to !postMaturityMode and a single seized collateral, matching the isolated liquidate leg it builds on. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GL2969EWAXpsqmnFCNFxHR --- certora/confs/PostDropRealizableBadDebt.conf | 33 +++ certora/helpers/MidnightWrapper.sol | 27 ++ certora/specs/PostDropRealizableBadDebt.spec | 290 +++++++++++++++++++ 3 files changed, 350 insertions(+) create mode 100644 certora/confs/PostDropRealizableBadDebt.conf create mode 100644 certora/specs/PostDropRealizableBadDebt.spec diff --git a/certora/confs/PostDropRealizableBadDebt.conf b/certora/confs/PostDropRealizableBadDebt.conf new file mode 100644 index 000000000..5b7e04154 --- /dev/null +++ b/certora/confs/PostDropRealizableBadDebt.conf @@ -0,0 +1,33 @@ +{ + "files": [ + "certora/helpers/MidnightWrapper.sol", + "certora/helpers/Utils.sol" + ], + "parametric_contracts": [ + "MidnightWrapper" + ], + "verify": "MidnightWrapper:certora/specs/PostDropRealizableBadDebt.spec", + "rule": [ + "postDropRbdLiquidateNonIncreaseSeizeInput", + "postDropRbdLiquidateNonIncreaseRepaidInput" + ], + "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 5", + "-mediumTimeout 120", + "-timeout 7200", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},cvc5:def]" + ], + "smt_timeout": 7200, + "msg": "Midnight: post-drop realizable bad debt (liquidate)" +} diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index 41b836f28..e22efdb51 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -58,4 +58,31 @@ contract MidnightWrapper is Midnight { } return badDebt; } + + // Explicit-price variant of realizableBadDebt: identical loop, but each collateral term is valued at + // the EXPLICITLY PASSED `price` instead of the oracle's IOracle(...).price(). This decouples the + // measurement price from the price liquidate reads at call time, letting a spec measure the realizable + // bad debt at a DROPPED price p' <= p while liquidate still runs at p. Structurally a verbatim copy of + // realizableBadDebt above (same zeroFloorSub, same mulDivUp(mulDivUp(collateral_i, price, + // ORACLE_PRICE_SCALE), WAD, maxLif_i)), so the prover equates it with the production bad-debt math. + function realizableBadDebtAtPrice(Market memory market, bytes32 id, address borrower, uint256 price) + public + view + returns (uint256) + { + Position storage _position = position[id][borrower]; + uint256 badDebt = _position.debt; + uint128 _collateralBitmap = _position.collateralBitmap; + while (_collateralBitmap != 0) { + uint256 i = UtilsLib.msb(_collateralBitmap); + CollateralParams memory _collateralParam = market.collateralParams[i]; + uint256 _collateral = _position.collateral[i]; + badDebt = badDebt.zeroFloorSub( + _collateral.mulDivUp(price, ORACLE_PRICE_SCALE) + .mulDivUp(WAD, maxLif(_collateralParam.lltv, _collateralParam.liquidationCursor)) + ); + _collateralBitmap = _collateralBitmap.clearBit(i); + } + return badDebt; + } } diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec new file mode 100644 index 000000000..2657ece19 --- /dev/null +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -0,0 +1,290 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2026 Morpho Association + +// Property: liquidating ahead of an oracle price drop cannot worsen the post-drop realizable bad debt. +// +// Concretely: liquidate runs at the pre-drop call-time price p (the price it reads from the oracle), +// while realizable bad debt is *measured* at a DROPPED price p' <= p. The claim is +// R' <= R, +// where R = do-nothing post-drop rbd (measured at p' before liquidate) and R' = post-liquidate +// post-drop rbd (measured at p' after liquidate). I.e. having liquidated first never leaves MORE +// realizable bad debt at the dropped price than doing nothing. +// +// Measurement at the decoupled price p' uses realizableBadDebtAtPrice (certora/helpers/MidnightWrapper.sol), +// a verbatim structural copy of the realizableBadDebt getter that values each active collateral at an +// explicitly passed price instead of reading IOracle(...).price(). Per active collateral c it subtracts +// g_x(c) = mulDivUp(mulDivUp(c, x, ORACLE_PRICE_SCALE), WAD, maxLif) +// where x is the passed measurement price. The iterated zeroFloorSub equals zeroFloorSub(debt, sum of +// terms), so rbd is monotone: more debt removed or less coverage removed cannot increase it. +// +// Proof (single seized collateral c_k -> c_k - seized, debt reduced by >= repaidUnits): +// coverage-removed at p' = g_{p'}(c_k) - g_{p'}(c_k - seized) +// <= g_{p'}(seized) [getter-form double sub-additivity, at p'] +// <= g_{p}(seized) [getter-form price monotonicity, p' <= p] +// <= repaidUnits [seize-value bound at p / repaid = g_p(seized)] +// <= debt-removed. +// Since coverage-removed <= debt-removed, zeroFloorSub monotonicity gives R' <= R with no slack. +// +// This reuses #1079's seize-value bound and double sub-additivity lemmas, and adds the price +// monotonicity of the getter term (g is non-decreasing in the price argument), which is what bridges +// the p'-measured coverage drop to the p-priced seize/repay logic liquidate actually executes. +// +// Restricted, like the isolated liquidate leg it builds on, to the non-post-maturity path +// (require !postMaturityMode, where lif == maxLif, src/Midnight.sol:685-687), a single seized +// collateral, and split along liquidate's exclusive-input branch (repaidUnits == 0 || seizedAssets == 0). + +import "BitmapSummaries.spec"; + +using Utils as Utils; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function realizableBadDebtAtPrice(Midnight.Market, bytes32, address, uint256) external returns (uint256) envfree; + function debt(bytes32, address) external returns (uint128) envfree; + function totalUnits(bytes32) external returns (uint128) envfree; + function lossFactor(bytes32) external returns (uint128) envfree; + function liquidationLocked(bytes32, address) external returns (bool) envfree; + function tickSpacing(bytes32) external returns (uint8) envfree; + function collateral(bytes32, address, uint256) external returns (uint128) envfree; + function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; + + // Per-callee constant price (no price update): this is the call-time price p that liquidate reads. + // The measurement price p' is decoupled from it, passed explicitly to realizableBadDebtAtPrice. + function _.price() external => summaryPrice(calledContract) expect(uint256); + + function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); + function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; + function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; + + 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); + function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor); + + // All external calls are assumed non-reentrant / non-reverting: we reason about the function bodies for safety properties. + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + function _.isRatified(Midnight.Offer, bytes, address) external => NONDET; + function _.canIncreaseCredit(address) external => NONDET; + function _.canIncreaseDebt(address) external => NONDET; + function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; + function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; + function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; +} + +/// SUMMARIES / GHOSTS /// + +definition WAD() returns uint256 = 10 ^ 18; + +definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; + +persistent ghost maxLifGhost(uint256, uint256) returns uint256; + +persistent ghost summaryPrice(address) returns uint256; + +persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; + +persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; + +// Loose (uninterpreted) mulDiv summaries, identical to RealizableBadDebtLiquidate.spec: because the ghost +// is a function, equal arguments give equal values, so every unchanged collateral term is identical +// between the before-getter and the after-getter measurements. The mulDiv values are otherwise +// constrained only by the near-linear consequences the rule e-matches on (monotonicity in each argument, +// getter-form double sub-additivity, and the seize-value bound), each PROVEN over the concrete mulDiv in +// MulDiv.spec. This keeps the heavy nonlinear reasoning out of the liquidate body. +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)); +} + +function summaryToId(Midnight.Market market) returns (bytes32) { + return Utils.hashMarket(market); +} + +function marketIsCreated(Midnight.Market market) returns (bool) { + return tickSpacing(summaryToId(market)) > 0; +} + +// Monotone in the first argument (proven in MulDiv.spec as 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); + +// Monotone in the second argument (proven in MulDiv.spec as mulDivMonotoneB). Applied to the inner +// mulDivUp(collateral, price, ORACLE_PRICE_SCALE): dropping the price argument from p to p' <= p cannot +// grow the inner value, and (with axiomUpMonotoneA on the outer layer) cannot grow the getter term g. +definition axiomUpMonotoneB(mathint a, mathint b1, mathint b2, mathint d) returns bool = 0 <= a && 0 <= b1 && b1 <= b2 && 0 < d => ghostMulDivUp(a, b1, d) <= ghostMulDivUp(a, b2, d); + +// Zero collateral values to zero (proven in MulDiv.spec as mulDivZero). Also covers the seized-collateral +// bitmap-clear path: when the seize empties the collateral, the after-getter drops the term and its +// value is g(0) = 0. +definition axiomUpZero(mathint b, mathint d) returns bool = d > 0 => ghostMulDivUp(0, b, d) == 0; + +// Getter-form double-mulDivUp sub-additivity (proven in MulDiv.spec as mulDivUpDoubleSubAdditive): for +// g_x(c) = mulDivUp(mulDivUp(c, x, ORACLE_PRICE_SCALE), WAD, maxLif), +// g_x(a) <= g_x(a - s) + g_x(s) whenever s <= a. ORACLE_PRICE_SCALE and WAD are pinned to the getter's +// exact constants so this e-matches the getter's ground terms; the price (here the measurement price p') +// and maxLif stay free. Applied at p' to the seized collateral (a = c_k, s = seized) it bounds the +// p'-measured coverage drop g_{p'}(c_k) - g_{p'}(c_k - seized) by g_{p'}(seized). +definition axiomUpDoubleSubAdditive(mathint a, mathint s, mathint p, mathint L) returns bool = 0 <= s && s <= a && 0 < L => ghostMulDivUp(ghostMulDivUp(a, p, ORACLE_PRICE_SCALE()), WAD(), L) <= ghostMulDivUp(ghostMulDivUp(a - s, p, ORACLE_PRICE_SCALE()), WAD(), L) + ghostMulDivUp(ghostMulDivUp(s, p, ORACLE_PRICE_SCALE()), WAD(), L); + +// Getter-form seize-value bound (proven in MulDiv.spec as mulDivSeizeValueBounded): the up-up value +// (at the call-time price p) of the down-down seized collateral never exceeds the repaid units, when +// seize and value share lif. This closes g_p(seized) <= repaidUnits on the repaid-input branch. +definition axiomSeizeValue(mathint r, mathint l, mathint p, mathint sc, mathint w) returns bool = 0 < l && 0 < p && 0 < w && 0 < sc => ghostMulDivUp(ghostMulDivUp(ghostMulDivDown(ghostMulDivDown(r, l, w), sc, p), p, sc), w, l) <= r; + +/// INVARIANTS /// + +// Proven in CollateralBitmap.spec; assumed here via requireInvariant (not re-proven in this spec). +strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint256 collateralIndex) + collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract.position[id][user].collateralBitmap, collateralIndex)); + +/// RULES /// + +// Post-price-drop realizable bad debt cannot increase from liquidating first: with liquidate executed at +// the call-time price p and realizable bad debt measured at a dropped price p' (= pDrop) <= p, the +// post-liquidate p'-rbd R' is at most the do-nothing p'-rbd R. Restricted to !postMaturityMode +// (lif == maxLif) and split along liquidate's exclusive-input branch, matching the isolated liquidate leg. + +// Seized-assets-input branch (repaidUnits == 0): liquidate derives the repaid debt drop +// repaidUnits = mulDivUp(mulDivUp(seizedAssets, p, ORACLE_PRICE_SCALE), WAD, lif) = g_p(seizedAssets) +// (src/Midnight.sol:690). The p'-measured coverage drop g_{p'}(c_k) - g_{p'}(c_k - seizedAssets) is at +// most g_{p'}(seizedAssets) (sub-additivity at p'), and price monotonicity gives g_{p'}(seizedAssets) <= +// g_p(seizedAssets) = the repaid debt drop. So coverage removed at p' <= debt removed, and zeroFloorSub +// monotonicity yields R' <= R. No seize-value bound is needed here (repaid is literally the getter term). +rule postDropRbdLiquidateNonIncreaseSeizeInput(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, uint256 pDrop) { + bytes32 id = summaryToId(market); + + require repaidUnits == 0, "seized-assets-input branch: repaidUnits is derived from seizedAssets (src/Midnight.sol:690)"; + + require market.collateralParams.length <= 2, "restrict collateralParams for loop tractability"; + require marketIsCreated(market), "market must be created (tickSpacing > 0)"; + require lossFactor(id) < max_uint128, "market lossFactor must not be saturated"; + require to_mathint(debt(id, borrower)) <= to_mathint(totalUnits(id)), "position debt bounded by totalUnits"; + require data.length == 0, "no liquidate callback data (prover performance; matches LiquidationBoundedByLIF.spec)"; + require !postMaturityMode, "non-post-maturity path: the seize factor lif equals maxLif (src/Midnight.sol:685-687)"; + + // Soundness: nonZeroCollateralsAreActivated is proven in CollateralBitmap.spec. + requireInvariant nonZeroCollateralsAreActivated(id, borrower, 0); + requireInvariant nonZeroCollateralsAreActivated(id, borrower, 1); + + mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); + require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; + + mathint price = summaryPrice(market.collateralParams[collateralIndex].oracle); + require pDrop <= price, "the measurement price p' is a dropped price: p' <= call-time price p"; + + // Near-linear consequences of the MulDiv lemmas, assumed over the loose ghost (each proven in + // MulDiv.spec): monotonicity in each argument (mulDivMonotoneA/B) supplies the price bridge + // g_{p'}(seized) <= g_p(seized), and double sub-additivity (mulDivUpDoubleSubAdditive) bounds the + // p'-coverage drop by g_{p'}(seized). axiomUpZero (mulDivZero) covers the emptied-collateral term. + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "monotone in first arg (mulDivMonotoneA)"; + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "monotone in second arg (mulDivMonotoneB)"; + require forall mathint b. forall mathint d. axiomUpZero(b, d), "zero collateral values to zero (mulDivZero)"; + require forall mathint a. forall mathint s. forall mathint p. forall mathint L. axiomUpDoubleSubAdditive(a, s, p, L), "getter-form double sub-additivity (mulDivUpDoubleSubAdditive)"; + + // Ground instances on the seized collateral so the axioms close without deep quantifier search. + // seized == seizedAssets here (input). g_p(seizedAssets) is exactly the repaid debt drop (line 690). + mathint innerSeizedDrop = ghostMulDivUp(seizedAssets, pDrop, ORACLE_PRICE_SCALE()); + mathint innerSeizedP = ghostMulDivUp(seizedAssets, price, ORACLE_PRICE_SCALE()); + mathint gSeizedDrop = ghostMulDivUp(innerSeizedDrop, WAD(), maxLif); + mathint gSeizedP = ghostMulDivUp(innerSeizedP, WAD(), maxLif); + mathint collatK = to_mathint(collateral(id, borrower, collateralIndex)); + mathint gCollatKDrop = ghostMulDivUp(ghostMulDivUp(collatK, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); + mathint gCollatKMinusSeizedDrop = ghostMulDivUp(ghostMulDivUp(collatK - seizedAssets, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); + + // Price bridge (mulDivMonotoneB on the inner layer, since pDrop <= price, then mulDivMonotoneA on the + // outer layer). Sub-additivity at p' bounds the coverage drop by g_{p'}(seizedAssets). + require gSeizedDrop <= gSeizedP, "price bridge: g_{p'}(seized) <= g_p(seized) (mulDivMonotoneB then mulDivMonotoneA)"; + require to_mathint(seizedAssets) <= collatK => gCollatKDrop <= gCollatKMinusSeizedDrop + gSeizedDrop, "double sub-additivity instance at p' (mulDivUpDoubleSubAdditive)"; + + mathint R = realizableBadDebtAtPrice(market, id, borrower, pDrop); + + liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + mathint Rprime = realizableBadDebtAtPrice(market, id, borrower, pDrop); + + assert Rprime <= R; + // If exact <= needs rounding slack, the tolerant form (one seized-collateral term's rounding) is: + // assert Rprime <= R + 3; +} + +// Repaid-units-input branch (seizedAssets == 0): liquidate derives the seized collateral +// seizedAssets = mulDivDown(mulDivDown(repaidUnits, lif, WAD), ORACLE_PRICE_SCALE, p) +// (src/Midnight.sol:692). Sub-additivity at p' bounds the p'-coverage drop by g_{p'}(seized), price +// monotonicity gives g_{p'}(seized) <= g_p(seized), and the seize-value bound closes g_p(seized) <= +// repaidUnits (the repaid debt drop). So coverage removed at p' <= debt removed, and zeroFloorSub +// monotonicity yields R' <= R. This is the harder case: it exercises both the seize (mulDivDown) and +// value (mulDivUp) chains, plus the price bridge. +rule postDropRbdLiquidateNonIncreaseRepaidInput(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, uint256 pDrop) { + bytes32 id = summaryToId(market); + + require seizedAssets == 0, "repaid-units-input branch: seizedAssets is derived from repaidUnits (src/Midnight.sol:692)"; + + // single collateral: solver-tractability scope; multi-collateral follows from K=0 subadditivity (non-seized terms are identical before/after) + require market.collateralParams.length == 1, "restrict collateralParams for loop tractability"; + require marketIsCreated(market), "market must be created (tickSpacing > 0)"; + require lossFactor(id) < max_uint128, "market lossFactor must not be saturated"; + require to_mathint(debt(id, borrower)) <= to_mathint(totalUnits(id)), "position debt bounded by totalUnits"; + require data.length == 0, "no liquidate callback data (prover performance; matches LiquidationBoundedByLIF.spec)"; + require !postMaturityMode, "non-post-maturity path: the seize factor lif equals maxLif (src/Midnight.sol:685-687)"; + + // Soundness: nonZeroCollateralsAreActivated is proven in CollateralBitmap.spec. + requireInvariant nonZeroCollateralsAreActivated(id, borrower, 0); + + mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); + require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; + + mathint price = summaryPrice(market.collateralParams[collateralIndex].oracle); + require price > 0, "call-time price positive (liquidate divides by it at src/Midnight.sol:692)"; + require pDrop <= price, "the measurement price p' is a dropped price: p' <= call-time price p"; + + // Near-linear consequences of the MulDiv lemmas, assumed over the loose ghost (each proven in + // MulDiv.spec): the double sub-additivity bounds the p'-coverage drop by g_{p'}(seized), + // monotonicity in each argument supplies the price bridge g_{p'}(seized) <= g_p(seized), and the + // seize-value bound closes g_p(seized) <= repaidUnits. axiomUpZero covers the emptied-collateral term. + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "monotone in first arg (mulDivMonotoneA)"; + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "monotone in second arg (mulDivMonotoneB)"; + require forall mathint b. forall mathint d. axiomUpZero(b, d), "zero collateral values to zero (mulDivZero)"; + require forall mathint a. forall mathint s. forall mathint p. forall mathint L. axiomUpDoubleSubAdditive(a, s, p, L), "getter-form double sub-additivity (mulDivUpDoubleSubAdditive)"; + require forall mathint r. forall mathint l. forall mathint p. forall mathint sc. forall mathint w. axiomSeizeValue(r, l, p, sc, w), "seize-value bound (mulDivSeizeValueBounded)"; + + // Ground instances of the derived-seize chain (seizedAssets = src/Midnight.sol:692) so the axioms + // close without quantifier search on the loop-internal seized term. + mathint seizedDerived = ghostMulDivDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price); + mathint innerSeizedDrop = ghostMulDivUp(seizedDerived, pDrop, ORACLE_PRICE_SCALE()); + mathint innerSeizedP = ghostMulDivUp(seizedDerived, price, ORACLE_PRICE_SCALE()); + mathint gSeizedDrop = ghostMulDivUp(innerSeizedDrop, WAD(), maxLif); + mathint gSeizedP = ghostMulDivUp(innerSeizedP, WAD(), maxLif); + mathint collatK = to_mathint(collateral(id, borrower, collateralIndex)); + mathint gCollatKDrop = ghostMulDivUp(ghostMulDivUp(collatK, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); + mathint gCollatKMinusSeizedDrop = ghostMulDivUp(ghostMulDivUp(collatK - seizedDerived, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); + + // Seize-value bound at the call-time price p: g_p(seized) <= repaidUnits. Price bridge + // (mulDivMonotoneB then mulDivMonotoneA, since pDrop <= price): g_{p'}(seized) <= g_p(seized). + // Sub-additivity at p' bounds the coverage drop by g_{p'}(seized). + require gSeizedP <= to_mathint(repaidUnits), "seize-value bound instance at p (mulDivSeizeValueBounded)"; + require gSeizedDrop <= gSeizedP, "price bridge: g_{p'}(seized) <= g_p(seized) (mulDivMonotoneB then mulDivMonotoneA)"; + require seizedDerived <= collatK => gCollatKDrop <= gCollatKMinusSeizedDrop + gSeizedDrop, "double sub-additivity instance at p' (mulDivUpDoubleSubAdditive)"; + + mathint R = realizableBadDebtAtPrice(market, id, borrower, pDrop); + + liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + mathint Rprime = realizableBadDebtAtPrice(market, id, borrower, pDrop); + + assert Rprime <= R; + // If exact <= needs rounding slack, the tolerant form (one seized-collateral term's rounding) is: + // assert Rprime <= R + 3; +} From 7e8fdcd33a1958bad20b0083a0ac8aa1e808fc55 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 26 Jul 2026 22:04:58 +0000 Subject: [PATCH 02/11] [Certora] Split post-drop rbd legs; single-step dropped-price seize bound Split the post-drop realizable-bad-debt liquidate leg so the verified seize-input rule (postDropRbdLiquidateNonIncreaseSeizeInput) runs green in its own conf, and isolate the heavy repaid-input rule in a new PostDropRealizableBadDebtRepaid.conf for iteration. Add mulDivSeizeValueAtDroppedPriceBounded to MulDiv.spec: the up-up value at a dropped price pDrop <= price of the down-down seized collateral is still <= the repaid units r (mulDivSeizeValueBounded composed with price monotonicity). Mirror it as the ghost-form axiomSeizeValueAtDroppedPrice and use a single ground instance in the repaid-input rule to collapse the former call-time-bound + price-bridge chain into one step, leaving fewer unification steps for the solver. Seize-input rule left untouched. --- certora/confs/PostDropRealizableBadDebt.conf | 3 +- .../PostDropRealizableBadDebtRepaid.conf | 32 +++++++++++++++++++ certora/specs/MulDiv.spec | 12 +++++++ certora/specs/PostDropRealizableBadDebt.spec | 25 ++++++++------- 4 files changed, 59 insertions(+), 13 deletions(-) create mode 100644 certora/confs/PostDropRealizableBadDebtRepaid.conf diff --git a/certora/confs/PostDropRealizableBadDebt.conf b/certora/confs/PostDropRealizableBadDebt.conf index 5b7e04154..8e58dde31 100644 --- a/certora/confs/PostDropRealizableBadDebt.conf +++ b/certora/confs/PostDropRealizableBadDebt.conf @@ -8,8 +8,7 @@ ], "verify": "MidnightWrapper:certora/specs/PostDropRealizableBadDebt.spec", "rule": [ - "postDropRbdLiquidateNonIncreaseSeizeInput", - "postDropRbdLiquidateNonIncreaseRepaidInput" + "postDropRbdLiquidateNonIncreaseSeizeInput" ], "solc": "solc-0.8.34", "solc_via_ir": true, diff --git a/certora/confs/PostDropRealizableBadDebtRepaid.conf b/certora/confs/PostDropRealizableBadDebtRepaid.conf new file mode 100644 index 000000000..4306dbcef --- /dev/null +++ b/certora/confs/PostDropRealizableBadDebtRepaid.conf @@ -0,0 +1,32 @@ +{ + "files": [ + "certora/helpers/MidnightWrapper.sol", + "certora/helpers/Utils.sol" + ], + "parametric_contracts": [ + "MidnightWrapper" + ], + "verify": "MidnightWrapper:certora/specs/PostDropRealizableBadDebt.spec", + "rule": [ + "postDropRbdLiquidateNonIncreaseRepaidInput" + ], + "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 5", + "-mediumTimeout 120", + "-timeout 7200", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},cvc5:def]" + ], + "smt_timeout": 7200, + "msg": "Midnight: post-drop realizable bad debt repaid-input (liquidate)" +} diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index ba190602b..c7b36f55a 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -111,6 +111,18 @@ rule mulDivSeizeValueBounded(uint256 r, uint256 l, uint256 price, uint256 wad, u assert mulDivUp(mulDivUp(seized, price, scale), wad, l) <= r; } +// Dropped-price generalization of mulDivSeizeValueBounded: valuing (up-up) the collateral that liquidate +// seizes (down-down at the call-time price) for repaidUnits r at a DROPPED price pDrop <= price never +// exceeds r either. This is mulDivSeizeValueBounded (which bounds the seize value at the call-time price) +// composed with price-monotonicity: pDrop <= price shrinks the up-up valuation, so it stays <= r. Closes +// the whole repaid crux in one fact for PostDropRealizableBadDebt's repaid-input branch. +rule mulDivSeizeValueAtDroppedPriceBounded(uint256 r, uint256 l, uint256 price, uint256 wad, uint256 scale, uint256 pDrop) { + require l > 0 && price > 0 && wad > 0 && scale > 0; + require pDrop >= 0 && pDrop <= price; + uint256 seized = mulDivDown(mulDivDown(r, l, wad), scale, price); + assert mulDivUp(mulDivUp(seized, pDrop, scale), wad, l) <= r; +} + rule mulDivArgumentLesserThanDenominator(uint256 a, uint256 b, uint256 d) { assert a <= d => mulDivDown(a, b, d) <= b; assert a <= d => mulDivUp(a, b, d) <= b; diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index 2657ece19..5761bbb7e 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -144,6 +144,12 @@ definition axiomUpDoubleSubAdditive(mathint a, mathint s, mathint p, mathint L) // seize and value share lif. This closes g_p(seized) <= repaidUnits on the repaid-input branch. definition axiomSeizeValue(mathint r, mathint l, mathint p, mathint sc, mathint w) returns bool = 0 < l && 0 < p && 0 < w && 0 < sc => ghostMulDivUp(ghostMulDivUp(ghostMulDivDown(ghostMulDivDown(r, l, w), sc, p), p, sc), w, l) <= r; +// Dropped-price seize-value bound (proven in MulDiv.spec as mulDivSeizeValueAtDroppedPriceBounded): the +// up-up value at the DROPPED price pDrop (<= call-time price p) of the down-down seized collateral never +// exceeds the repaid units r. Composes axiomSeizeValue (bound at p) with price monotonicity in one fact, +// closing g_{p'}(seized) <= repaidUnits directly on the repaid-input branch. +definition axiomSeizeValueAtDroppedPrice(mathint r, mathint l, mathint p, mathint sc, mathint w, mathint pDrop) returns bool = 0 < l && 0 < p && 0 < w && 0 < sc && 0 <= pDrop && pDrop <= p => ghostMulDivUp(ghostMulDivUp(ghostMulDivDown(ghostMulDivDown(r, l, w), sc, p), pDrop, sc), w, l) <= r; + /// INVARIANTS /// // Proven in CollateralBitmap.spec; assumed here via requireInvariant (not re-proven in this spec). @@ -251,31 +257,28 @@ rule postDropRbdLiquidateNonIncreaseRepaidInput(env e, Midnight.Market market, u require pDrop <= price, "the measurement price p' is a dropped price: p' <= call-time price p"; // Near-linear consequences of the MulDiv lemmas, assumed over the loose ghost (each proven in - // MulDiv.spec): the double sub-additivity bounds the p'-coverage drop by g_{p'}(seized), - // monotonicity in each argument supplies the price bridge g_{p'}(seized) <= g_p(seized), and the - // seize-value bound closes g_p(seized) <= repaidUnits. axiomUpZero covers the emptied-collateral term. + // MulDiv.spec): the double sub-additivity bounds the p'-coverage drop by g_{p'}(seized), and the + // dropped-price seize-value bound closes g_{p'}(seized) <= repaidUnits in one step (no separate price + // bridge / call-time bound to chain). axiomUpZero covers the emptied-collateral term. require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "monotone in first arg (mulDivMonotoneA)"; require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "monotone in second arg (mulDivMonotoneB)"; require forall mathint b. forall mathint d. axiomUpZero(b, d), "zero collateral values to zero (mulDivZero)"; require forall mathint a. forall mathint s. forall mathint p. forall mathint L. axiomUpDoubleSubAdditive(a, s, p, L), "getter-form double sub-additivity (mulDivUpDoubleSubAdditive)"; - require forall mathint r. forall mathint l. forall mathint p. forall mathint sc. forall mathint w. axiomSeizeValue(r, l, p, sc, w), "seize-value bound (mulDivSeizeValueBounded)"; + require forall mathint r. forall mathint l. forall mathint p. forall mathint sc. forall mathint w. forall mathint pd. axiomSeizeValueAtDroppedPrice(r, l, p, sc, w, pd), "dropped-price seize-value bound (mulDivSeizeValueAtDroppedPriceBounded)"; // Ground instances of the derived-seize chain (seizedAssets = src/Midnight.sol:692) so the axioms // close without quantifier search on the loop-internal seized term. mathint seizedDerived = ghostMulDivDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price); mathint innerSeizedDrop = ghostMulDivUp(seizedDerived, pDrop, ORACLE_PRICE_SCALE()); - mathint innerSeizedP = ghostMulDivUp(seizedDerived, price, ORACLE_PRICE_SCALE()); mathint gSeizedDrop = ghostMulDivUp(innerSeizedDrop, WAD(), maxLif); - mathint gSeizedP = ghostMulDivUp(innerSeizedP, WAD(), maxLif); mathint collatK = to_mathint(collateral(id, borrower, collateralIndex)); mathint gCollatKDrop = ghostMulDivUp(ghostMulDivUp(collatK, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); mathint gCollatKMinusSeizedDrop = ghostMulDivUp(ghostMulDivUp(collatK - seizedDerived, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); - // Seize-value bound at the call-time price p: g_p(seized) <= repaidUnits. Price bridge - // (mulDivMonotoneB then mulDivMonotoneA, since pDrop <= price): g_{p'}(seized) <= g_p(seized). - // Sub-additivity at p' bounds the coverage drop by g_{p'}(seized). - require gSeizedP <= to_mathint(repaidUnits), "seize-value bound instance at p (mulDivSeizeValueBounded)"; - require gSeizedDrop <= gSeizedP, "price bridge: g_{p'}(seized) <= g_p(seized) (mulDivMonotoneB then mulDivMonotoneA)"; + // Single-step dropped-price seize-value bound: the p'-valued derived seize is at most repaidUnits + // (mulDivSeizeValueAtDroppedPriceBounded), collapsing the former call-time-bound + price-bridge chain. + // Sub-additivity at p' then bounds the coverage drop by g_{p'}(seized). + require gSeizedDrop <= to_mathint(repaidUnits), "dropped-price seize-value bound instance (mulDivSeizeValueAtDroppedPriceBounded)"; require seizedDerived <= collatK => gCollatKDrop <= gCollatKMinusSeizedDrop + gSeizedDrop, "double sub-additivity instance at p' (mulDivUpDoubleSubAdditive)"; mathint R = realizableBadDebtAtPrice(market, id, borrower, pDrop); From 53f5810b5f564d173fff1d39819599e1cd6cb379 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 30 Jul 2026 12:18:17 +0200 Subject: [PATCH 03/11] Update price in ghost, add both pre- and post liquidate bad debt --- certora/helpers/MidnightWrapper.sol | 27 ------------- certora/specs/PostDropRealizableBadDebt.spec | 42 +++++++++++++------- 2 files changed, 27 insertions(+), 42 deletions(-) diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index e22efdb51..41b836f28 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -58,31 +58,4 @@ contract MidnightWrapper is Midnight { } return badDebt; } - - // Explicit-price variant of realizableBadDebt: identical loop, but each collateral term is valued at - // the EXPLICITLY PASSED `price` instead of the oracle's IOracle(...).price(). This decouples the - // measurement price from the price liquidate reads at call time, letting a spec measure the realizable - // bad debt at a DROPPED price p' <= p while liquidate still runs at p. Structurally a verbatim copy of - // realizableBadDebt above (same zeroFloorSub, same mulDivUp(mulDivUp(collateral_i, price, - // ORACLE_PRICE_SCALE), WAD, maxLif_i)), so the prover equates it with the production bad-debt math. - function realizableBadDebtAtPrice(Market memory market, bytes32 id, address borrower, uint256 price) - public - view - returns (uint256) - { - Position storage _position = position[id][borrower]; - uint256 badDebt = _position.debt; - uint128 _collateralBitmap = _position.collateralBitmap; - while (_collateralBitmap != 0) { - uint256 i = UtilsLib.msb(_collateralBitmap); - CollateralParams memory _collateralParam = market.collateralParams[i]; - uint256 _collateral = _position.collateral[i]; - badDebt = badDebt.zeroFloorSub( - _collateral.mulDivUp(price, ORACLE_PRICE_SCALE) - .mulDivUp(WAD, maxLif(_collateralParam.lltv, _collateralParam.liquidationCursor)) - ); - _collateralBitmap = _collateralBitmap.clearBit(i); - } - return badDebt; - } } diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index 5761bbb7e..df52f6225 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -40,7 +40,7 @@ using Utils as Utils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function realizableBadDebtAtPrice(Midnight.Market, bytes32, address, uint256) external returns (uint256) envfree; + function realizableBadDebt(Midnight.Market, bytes32, address) external returns (uint256) envfree; function debt(bytes32, address) external returns (uint128) envfree; function totalUnits(bytes32) external returns (uint128) envfree; function lossFactor(bytes32) external returns (uint128) envfree; @@ -51,7 +51,7 @@ methods { // Per-callee constant price (no price update): this is the call-time price p that liquidate reads. // The measurement price p' is decoupled from it, passed explicitly to realizableBadDebtAtPrice. - function _.price() external => summaryPrice(calledContract) expect(uint256); + function _.price() external => summaryPrice[calledContract] expect(uint256); function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; @@ -82,7 +82,7 @@ definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; persistent ghost maxLifGhost(uint256, uint256) returns uint256; -persistent ghost summaryPrice(address) returns uint256; +persistent ghost mapping(address => uint256) summaryPrice; persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; @@ -188,7 +188,7 @@ rule postDropRbdLiquidateNonIncreaseSeizeInput(env e, Midnight.Market market, ui mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; - mathint price = summaryPrice(market.collateralParams[collateralIndex].oracle); + uint256 price = summaryPrice[market.collateralParams[collateralIndex].oracle]; require pDrop <= price, "the measurement price p' is a dropped price: p' <= call-time price p"; // Near-linear consequences of the MulDiv lemmas, assumed over the loose ghost (each proven in @@ -215,15 +215,21 @@ rule postDropRbdLiquidateNonIncreaseSeizeInput(env e, Midnight.Market market, ui require gSeizedDrop <= gSeizedP, "price bridge: g_{p'}(seized) <= g_p(seized) (mulDivMonotoneB then mulDivMonotoneA)"; require to_mathint(seizedAssets) <= collatK => gCollatKDrop <= gCollatKMinusSeizedDrop + gSeizedDrop, "double sub-additivity instance at p' (mulDivUpDoubleSubAdditive)"; - mathint R = realizableBadDebtAtPrice(market, id, borrower, pDrop); + // scenario 1: price drops, then realize bad debt + summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; + mathint R = realizableBadDebt(market, id, borrower); + // scenario 2: liquidate at initial (higher) price + // then price drop, realize remaining debt. + summaryPrice[market.collateralParams[collateralIndex].oracle] = price; + + mathint R1 = realizableBadDebt(market, id, borrower); liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - mathint Rprime = realizableBadDebtAtPrice(market, id, borrower, pDrop); + summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; + mathint R2 = realizableBadDebt(market, id, borrower); - assert Rprime <= R; - // If exact <= needs rounding slack, the tolerant form (one seized-collateral term's rounding) is: - // assert Rprime <= R + 3; + assert R1 + R2 <= R; } // Repaid-units-input branch (seizedAssets == 0): liquidate derives the seized collateral @@ -252,7 +258,7 @@ rule postDropRbdLiquidateNonIncreaseRepaidInput(env e, Midnight.Market market, u mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; - mathint price = summaryPrice(market.collateralParams[collateralIndex].oracle); + uint256 price = summaryPrice[market.collateralParams[collateralIndex].oracle]; require price > 0, "call-time price positive (liquidate divides by it at src/Midnight.sol:692)"; require pDrop <= price, "the measurement price p' is a dropped price: p' <= call-time price p"; @@ -281,13 +287,19 @@ rule postDropRbdLiquidateNonIncreaseRepaidInput(env e, Midnight.Market market, u require gSeizedDrop <= to_mathint(repaidUnits), "dropped-price seize-value bound instance (mulDivSeizeValueAtDroppedPriceBounded)"; require seizedDerived <= collatK => gCollatKDrop <= gCollatKMinusSeizedDrop + gSeizedDrop, "double sub-additivity instance at p' (mulDivUpDoubleSubAdditive)"; - mathint R = realizableBadDebtAtPrice(market, id, borrower, pDrop); + // scenario 1: price drops, then realize bad debt + summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; + mathint R = realizableBadDebt(market, id, borrower); + + // scenario 2: liquidate at initial (higher) price + // then price drop, realize remaining debt. + summaryPrice[market.collateralParams[collateralIndex].oracle] = price; + mathint R1 = realizableBadDebt(market, id, borrower); liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - mathint Rprime = realizableBadDebtAtPrice(market, id, borrower, pDrop); + summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; + mathint R2 = realizableBadDebt(market, id, borrower); - assert Rprime <= R; - // If exact <= needs rounding slack, the tolerant form (one seized-collateral term's rounding) is: - // assert Rprime <= R + 3; + assert R1 + R2 <= R; } From 0222e30ad9dd290f3100ecfb3927016d6a0db452 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 30 Jul 2026 16:04:02 +0200 Subject: [PATCH 04/11] Simplified the rule - Only one rule handling both liquidate cases. - Use axioms proved in MulDiv --- certora/confs/PostDropRealizableBadDebt.conf | 3 - .../PostDropRealizableBadDebtRepaid.conf | 32 --- certora/specs/PostDropRealizableBadDebt.spec | 202 +++++------------- 3 files changed, 55 insertions(+), 182 deletions(-) delete mode 100644 certora/confs/PostDropRealizableBadDebtRepaid.conf diff --git a/certora/confs/PostDropRealizableBadDebt.conf b/certora/confs/PostDropRealizableBadDebt.conf index 8e58dde31..d4efe7c2a 100644 --- a/certora/confs/PostDropRealizableBadDebt.conf +++ b/certora/confs/PostDropRealizableBadDebt.conf @@ -7,9 +7,6 @@ "MidnightWrapper" ], "verify": "MidnightWrapper:certora/specs/PostDropRealizableBadDebt.spec", - "rule": [ - "postDropRbdLiquidateNonIncreaseSeizeInput" - ], "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", diff --git a/certora/confs/PostDropRealizableBadDebtRepaid.conf b/certora/confs/PostDropRealizableBadDebtRepaid.conf deleted file mode 100644 index 4306dbcef..000000000 --- a/certora/confs/PostDropRealizableBadDebtRepaid.conf +++ /dev/null @@ -1,32 +0,0 @@ -{ - "files": [ - "certora/helpers/MidnightWrapper.sol", - "certora/helpers/Utils.sol" - ], - "parametric_contracts": [ - "MidnightWrapper" - ], - "verify": "MidnightWrapper:certora/specs/PostDropRealizableBadDebt.spec", - "rule": [ - "postDropRbdLiquidateNonIncreaseRepaidInput" - ], - "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 5", - "-mediumTimeout 120", - "-timeout 7200", - "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},cvc5:def]" - ], - "smt_timeout": 7200, - "msg": "Midnight: post-drop realizable bad debt repaid-input (liquidate)" -} diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index df52f6225..f7b9ea0e5 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -118,37 +118,31 @@ function marketIsCreated(Midnight.Market market) returns (bool) { return tickSpacing(summaryToId(market)) > 0; } +// Monotone in the first argument (proven in MulDiv.spec as 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); + +// Monotone in the second argument (proven in MulDiv.spec as mulDivMonotoneB). +definition axiomDownMonotoneB(mathint a, mathint b1, mathint b2, mathint d) returns bool = 0 <= a && 0 <= b1 && b1 <= b2 && 0 < d => ghostMulDivDown(a, b1, d) <= ghostMulDivDown(a, b2, d); + // Monotone in the first argument (proven in MulDiv.spec as 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); -// Monotone in the second argument (proven in MulDiv.spec as mulDivMonotoneB). Applied to the inner -// mulDivUp(collateral, price, ORACLE_PRICE_SCALE): dropping the price argument from p to p' <= p cannot -// grow the inner value, and (with axiomUpMonotoneA on the outer layer) cannot grow the getter term g. +// Monotone in the second argument (proven in MulDiv.spec as mulDivMonotoneB). definition axiomUpMonotoneB(mathint a, mathint b1, mathint b2, mathint d) returns bool = 0 <= a && 0 <= b1 && b1 <= b2 && 0 < d => ghostMulDivUp(a, b1, d) <= ghostMulDivUp(a, b2, d); -// Zero collateral values to zero (proven in MulDiv.spec as mulDivZero). Also covers the seized-collateral -// bitmap-clear path: when the seize empties the collateral, the after-getter drops the term and its -// value is g(0) = 0. +// Monotone in the third argument (proven in MulDiv.spec as mulDivMonotoneD). +definition axiomUpMonotoneD(mathint a, mathint b, mathint d1, mathint d2) returns bool = 0 <= a && 0 <= b && 0 < d1 && d1 <= d2 => ghostMulDivUp(a, b, d2) <= ghostMulDivUp(a, b, d1); + +// Zero collateral values to zero (proven in MulDiv.spec as mulDivZero). definition axiomUpZero(mathint b, mathint d) returns bool = d > 0 => ghostMulDivUp(0, b, d) == 0; -// Getter-form double-mulDivUp sub-additivity (proven in MulDiv.spec as mulDivUpDoubleSubAdditive): for -// g_x(c) = mulDivUp(mulDivUp(c, x, ORACLE_PRICE_SCALE), WAD, maxLif), -// g_x(a) <= g_x(a - s) + g_x(s) whenever s <= a. ORACLE_PRICE_SCALE and WAD are pinned to the getter's -// exact constants so this e-matches the getter's ground terms; the price (here the measurement price p') -// and maxLif stay free. Applied at p' to the seized collateral (a = c_k, s = seized) it bounds the -// p'-measured coverage drop g_{p'}(c_k) - g_{p'}(c_k - seized) by g_{p'}(seized). -definition axiomUpDoubleSubAdditive(mathint a, mathint s, mathint p, mathint L) returns bool = 0 <= s && s <= a && 0 < L => ghostMulDivUp(ghostMulDivUp(a, p, ORACLE_PRICE_SCALE()), WAD(), L) <= ghostMulDivUp(ghostMulDivUp(a - s, p, ORACLE_PRICE_SCALE()), WAD(), L) + ghostMulDivUp(ghostMulDivUp(s, p, ORACLE_PRICE_SCALE()), WAD(), L); - -// Getter-form seize-value bound (proven in MulDiv.spec as mulDivSeizeValueBounded): the up-up value -// (at the call-time price p) of the down-down seized collateral never exceeds the repaid units, when -// seize and value share lif. This closes g_p(seized) <= repaidUnits on the repaid-input branch. -definition axiomSeizeValue(mathint r, mathint l, mathint p, mathint sc, mathint w) returns bool = 0 < l && 0 < p && 0 < w && 0 < sc => ghostMulDivUp(ghostMulDivUp(ghostMulDivDown(ghostMulDivDown(r, l, w), sc, p), p, sc), w, l) <= r; - -// Dropped-price seize-value bound (proven in MulDiv.spec as mulDivSeizeValueAtDroppedPriceBounded): the -// up-up value at the DROPPED price pDrop (<= call-time price p) of the down-down seized collateral never -// exceeds the repaid units r. Composes axiomSeizeValue (bound at p) with price monotonicity in one fact, -// closing g_{p'}(seized) <= repaidUnits directly on the repaid-input branch. -definition axiomSeizeValueAtDroppedPrice(mathint r, mathint l, mathint p, mathint sc, mathint w, mathint pDrop) returns bool = 0 < l && 0 < p && 0 < w && 0 < sc && 0 <= pDrop && pDrop <= p => ghostMulDivUp(ghostMulDivUp(ghostMulDivDown(ghostMulDivDown(r, l, w), sc, p), pDrop, sc), w, l) <= r; +// proven in MulDiv.spec as mulDivAddUpUp: +// mulDivUp(a1 + a2, b, d) <= mulDivUp(a1, b, d) + mulDivUp(a2, b, d). +definition axiomAddUpUp(mathint a1, mathint a2, mathint b, mathint d) returns bool = a1 >= 0 && a2 >= 0 && b >= 0 && d > 0 => ghostMulDivUp(a1 + a2, b, d) <= ghostMulDivUp(a1, b, d) + ghostMulDivUp(a2, b, d); + +// proven in MulDiv.spec as mulDivAddUpUp: +// mulDivUp(mulDivDown(a,b,d),d,b) <= a +definition axiomInverseUpDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b > 0 && d > 0 => ghostMulDivUp(ghostMulDivDown(a, b, d), d, b) <= a; /// INVARIANTS /// @@ -158,148 +152,62 @@ strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint25 /// RULES /// -// Post-price-drop realizable bad debt cannot increase from liquidating first: with liquidate executed at -// the call-time price p and realizable bad debt measured at a dropped price p' (= pDrop) <= p, the -// post-liquidate p'-rbd R' is at most the do-nothing p'-rbd R. Restricted to !postMaturityMode -// (lif == maxLif) and split along liquidate's exclusive-input branch, matching the isolated liquidate leg. - -// Seized-assets-input branch (repaidUnits == 0): liquidate derives the repaid debt drop -// repaidUnits = mulDivUp(mulDivUp(seizedAssets, p, ORACLE_PRICE_SCALE), WAD, lif) = g_p(seizedAssets) -// (src/Midnight.sol:690). The p'-measured coverage drop g_{p'}(c_k) - g_{p'}(c_k - seizedAssets) is at -// most g_{p'}(seizedAssets) (sub-additivity at p'), and price monotonicity gives g_{p'}(seizedAssets) <= -// g_p(seizedAssets) = the repaid debt drop. So coverage removed at p' <= debt removed, and zeroFloorSub -// monotonicity yields R' <= R. No seize-value bound is needed here (repaid is literally the getter term). -rule postDropRbdLiquidateNonIncreaseSeizeInput(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, uint256 pDrop) { +// Realizable bad debt cannot increase from liquidating before a price drop. +// If price drop happens after a liquidate, the total bad debt is less than if the liquidate +// never happened. +rule postDropRbdLiquidateNonIncrease(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { bytes32 id = summaryToId(market); - require repaidUnits == 0, "seized-assets-input branch: repaidUnits is derived from seizedAssets (src/Midnight.sol:690)"; - - require market.collateralParams.length <= 2, "restrict collateralParams for loop tractability"; - require marketIsCreated(market), "market must be created (tickSpacing > 0)"; - require lossFactor(id) < max_uint128, "market lossFactor must not be saturated"; - require to_mathint(debt(id, borrower)) <= to_mathint(totalUnits(id)), "position debt bounded by totalUnits"; - require data.length == 0, "no liquidate callback data (prover performance; matches LiquidationBoundedByLIF.spec)"; - require !postMaturityMode, "non-post-maturity path: the seize factor lif equals maxLif (src/Midnight.sol:685-687)"; - - // Soundness: nonZeroCollateralsAreActivated is proven in CollateralBitmap.spec. - requireInvariant nonZeroCollateralsAreActivated(id, borrower, 0); - requireInvariant nonZeroCollateralsAreActivated(id, borrower, 1); - mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; uint256 price = summaryPrice[market.collateralParams[collateralIndex].oracle]; - require pDrop <= price, "the measurement price p' is a dropped price: p' <= call-time price p"; - - // Near-linear consequences of the MulDiv lemmas, assumed over the loose ghost (each proven in - // MulDiv.spec): monotonicity in each argument (mulDivMonotoneA/B) supplies the price bridge - // g_{p'}(seized) <= g_p(seized), and double sub-additivity (mulDivUpDoubleSubAdditive) bounds the - // p'-coverage drop by g_{p'}(seized). axiomUpZero (mulDivZero) covers the emptied-collateral term. - require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "monotone in first arg (mulDivMonotoneA)"; - require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "monotone in second arg (mulDivMonotoneB)"; - require forall mathint b. forall mathint d. axiomUpZero(b, d), "zero collateral values to zero (mulDivZero)"; - require forall mathint a. forall mathint s. forall mathint p. forall mathint L. axiomUpDoubleSubAdditive(a, s, p, L), "getter-form double sub-additivity (mulDivUpDoubleSubAdditive)"; - - // Ground instances on the seized collateral so the axioms close without deep quantifier search. - // seized == seizedAssets here (input). g_p(seizedAssets) is exactly the repaid debt drop (line 690). - mathint innerSeizedDrop = ghostMulDivUp(seizedAssets, pDrop, ORACLE_PRICE_SCALE()); - mathint innerSeizedP = ghostMulDivUp(seizedAssets, price, ORACLE_PRICE_SCALE()); - mathint gSeizedDrop = ghostMulDivUp(innerSeizedDrop, WAD(), maxLif); - mathint gSeizedP = ghostMulDivUp(innerSeizedP, WAD(), maxLif); - mathint collatK = to_mathint(collateral(id, borrower, collateralIndex)); - mathint gCollatKDrop = ghostMulDivUp(ghostMulDivUp(collatK, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); - mathint gCollatKMinusSeizedDrop = ghostMulDivUp(ghostMulDivUp(collatK - seizedAssets, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); - - // Price bridge (mulDivMonotoneB on the inner layer, since pDrop <= price, then mulDivMonotoneA on the - // outer layer). Sub-additivity at p' bounds the coverage drop by g_{p'}(seizedAssets). - require gSeizedDrop <= gSeizedP, "price bridge: g_{p'}(seized) <= g_p(seized) (mulDivMonotoneB then mulDivMonotoneA)"; - require to_mathint(seizedAssets) <= collatK => gCollatKDrop <= gCollatKMinusSeizedDrop + gSeizedDrop, "double sub-additivity instance at p' (mulDivUpDoubleSubAdditive)"; - - // scenario 1: price drops, then realize bad debt - summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; - mathint R = realizableBadDebt(market, id, borrower); - - // scenario 2: liquidate at initial (higher) price - // then price drop, realize remaining debt. - summaryPrice[market.collateralParams[collateralIndex].oracle] = price; - - mathint R1 = realizableBadDebt(market, id, borrower); - liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - - summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; - mathint R2 = realizableBadDebt(market, id, borrower); - - assert R1 + R2 <= R; -} - -// Repaid-units-input branch (seizedAssets == 0): liquidate derives the seized collateral -// seizedAssets = mulDivDown(mulDivDown(repaidUnits, lif, WAD), ORACLE_PRICE_SCALE, p) -// (src/Midnight.sol:692). Sub-additivity at p' bounds the p'-coverage drop by g_{p'}(seized), price -// monotonicity gives g_{p'}(seized) <= g_p(seized), and the seize-value bound closes g_p(seized) <= -// repaidUnits (the repaid debt drop). So coverage removed at p' <= debt removed, and zeroFloorSub -// monotonicity yields R' <= R. This is the harder case: it exercises both the seize (mulDivDown) and -// value (mulDivUp) chains, plus the price bridge. -rule postDropRbdLiquidateNonIncreaseRepaidInput(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, uint256 pDrop) { - bytes32 id = summaryToId(market); - - require seizedAssets == 0, "repaid-units-input branch: seizedAssets is derived from repaidUnits (src/Midnight.sol:692)"; + uint256 pDrop; + require pDrop <= price, "the dropped price is less than the initial price"; + + mathint seizedAssetsOut; + + if (repaidUnits == 0) { + seizedAssetsOut = seizedAssets; + } else { + seizedAssetsOut = ghostMulDivDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price); + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomDownMonotoneA(a1, a2, b, d), "axiom"; + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomDownMonotoneB(a, b1, b2, d), "axiom"; + require axiomInverseUpDown(repaidUnits, maxLif, WAD()), "axiom"; + require axiomInverseUpDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price), "axiom"; + } - // single collateral: solver-tractability scope; multi-collateral follows from K=0 subadditivity (non-seized terms are identical before/after) - require market.collateralParams.length == 1, "restrict collateralParams for loop tractability"; - require marketIsCreated(market), "market must be created (tickSpacing > 0)"; - require lossFactor(id) < max_uint128, "market lossFactor must not be saturated"; - require to_mathint(debt(id, borrower)) <= to_mathint(totalUnits(id)), "position debt bounded by totalUnits"; - require data.length == 0, "no liquidate callback data (prover performance; matches LiquidationBoundedByLIF.spec)"; - require !postMaturityMode, "non-post-maturity path: the seize factor lif equals maxLif (src/Midnight.sol:685-687)"; + uint256 collateralBefore = collateral(id, borrower, collateralIndex); + mathint collateralAfter = collateralBefore - seizedAssetsOut; - // Soundness: nonZeroCollateralsAreActivated is proven in CollateralBitmap.spec. - requireInvariant nonZeroCollateralsAreActivated(id, borrower, 0); + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomDownMonotoneB(a, b1, b2, d), "axiom"; + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "axiom"; + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "axiom"; + require forall mathint a. forall mathint b. forall mathint d1. forall mathint d2. axiomUpMonotoneD(a, b, d1, d2), "axiom"; + //require axiomUpZero(price, ORACLE_PRICE_SCALE()), "axiom"; + //require axiomUpZero(WAD(), maxLif), "axiom"; + //require axiomAddUpUp(collateralAfter, seizedAssetsOut, price, ORACLE_PRICE_SCALE()), "axiom"; + //require axiomAddUpUp(ghostMulDivUp(collateralAfter, price, ORACLE_PRICE_SCALE()), ghostMulDivUp(seizedAssetsOut, price, ORACLE_PRICE_SCALE()), WAD(), maxLif), "axiom"; - mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); - require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; - - uint256 price = summaryPrice[market.collateralParams[collateralIndex].oracle]; - require price > 0, "call-time price positive (liquidate divides by it at src/Midnight.sol:692)"; - require pDrop <= price, "the measurement price p' is a dropped price: p' <= call-time price p"; - - // Near-linear consequences of the MulDiv lemmas, assumed over the loose ghost (each proven in - // MulDiv.spec): the double sub-additivity bounds the p'-coverage drop by g_{p'}(seized), and the - // dropped-price seize-value bound closes g_{p'}(seized) <= repaidUnits in one step (no separate price - // bridge / call-time bound to chain). axiomUpZero covers the emptied-collateral term. - require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "monotone in first arg (mulDivMonotoneA)"; - require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "monotone in second arg (mulDivMonotoneB)"; - require forall mathint b. forall mathint d. axiomUpZero(b, d), "zero collateral values to zero (mulDivZero)"; - require forall mathint a. forall mathint s. forall mathint p. forall mathint L. axiomUpDoubleSubAdditive(a, s, p, L), "getter-form double sub-additivity (mulDivUpDoubleSubAdditive)"; - require forall mathint r. forall mathint l. forall mathint p. forall mathint sc. forall mathint w. forall mathint pd. axiomSeizeValueAtDroppedPrice(r, l, p, sc, w, pd), "dropped-price seize-value bound (mulDivSeizeValueAtDroppedPriceBounded)"; - - // Ground instances of the derived-seize chain (seizedAssets = src/Midnight.sol:692) so the axioms - // close without quantifier search on the loop-internal seized term. - mathint seizedDerived = ghostMulDivDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price); - mathint innerSeizedDrop = ghostMulDivUp(seizedDerived, pDrop, ORACLE_PRICE_SCALE()); - mathint gSeizedDrop = ghostMulDivUp(innerSeizedDrop, WAD(), maxLif); - mathint collatK = to_mathint(collateral(id, borrower, collateralIndex)); - mathint gCollatKDrop = ghostMulDivUp(ghostMulDivUp(collatK, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); - mathint gCollatKMinusSeizedDrop = ghostMulDivUp(ghostMulDivUp(collatK - seizedDerived, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif); - - // Single-step dropped-price seize-value bound: the p'-valued derived seize is at most repaidUnits - // (mulDivSeizeValueAtDroppedPriceBounded), collapsing the former call-time-bound + price-bridge chain. - // Sub-additivity at p' then bounds the coverage drop by g_{p'}(seized). - require gSeizedDrop <= to_mathint(repaidUnits), "dropped-price seize-value bound instance (mulDivSeizeValueAtDroppedPriceBounded)"; - require seizedDerived <= collatK => gCollatKDrop <= gCollatKMinusSeizedDrop + gSeizedDrop, "double sub-additivity instance at p' (mulDivUpDoubleSubAdditive)"; + require axiomUpZero(pDrop, ORACLE_PRICE_SCALE()), "axiom"; + require axiomUpZero(WAD(), maxLif), "axiom"; + require axiomAddUpUp(collateralAfter, seizedAssetsOut, pDrop, ORACLE_PRICE_SCALE()), "axiom"; + require axiomAddUpUp(ghostMulDivUp(collateralAfter, pDrop, ORACLE_PRICE_SCALE()), ghostMulDivUp(seizedAssetsOut, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif), "axiom"; // scenario 1: price drops, then realize bad debt summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; - mathint R = realizableBadDebt(market, id, borrower); + mathint badDebt1 = realizableBadDebt(market, id, borrower); // scenario 2: liquidate at initial (higher) price // then price drop, realize remaining debt. summaryPrice[market.collateralParams[collateralIndex].oracle] = price; - mathint R1 = realizableBadDebt(market, id, borrower); + mathint badDebt2a = realizableBadDebt(market, id, borrower); liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; - mathint R2 = realizableBadDebt(market, id, borrower); + mathint badDebt2b = realizableBadDebt(market, id, borrower); - assert R1 + R2 <= R; + // liquidating before the price drop (scenario 2) will cause less bad debt in total. + assert badDebt2a + badDebt2b <= badDebt1; } From 872d4a08c28a68e2dd13a1a1faaf5cdba464f181 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 30 Jul 2026 16:24:36 +0200 Subject: [PATCH 05/11] Clean up comments --- certora/specs/PostDropRealizableBadDebt.spec | 53 +++----------------- 1 file changed, 8 insertions(+), 45 deletions(-) diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index f7b9ea0e5..b9ba33564 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -3,35 +3,14 @@ // Property: liquidating ahead of an oracle price drop cannot worsen the post-drop realizable bad debt. // -// Concretely: liquidate runs at the pre-drop call-time price p (the price it reads from the oracle), -// while realizable bad debt is *measured* at a DROPPED price p' <= p. The claim is -// R' <= R, -// where R = do-nothing post-drop rbd (measured at p' before liquidate) and R' = post-liquidate -// post-drop rbd (measured at p' after liquidate). I.e. having liquidated first never leaves MORE -// realizable bad debt at the dropped price than doing nothing. +// Concretely: In the reference scenario there is no liquidation just a price drop and the +// bad debt is measured at the dropped price pDrop. +// In the second scenario there was a liquidate at some price >= pDrop before the price drop. +// The total bad debt in the second scenario (the bad debt before measured at initial price plus +// the additional bad debt after liquidating measured a the dropped price) must not exceed the +// bad debt in the reference scenario without a liquidation. // -// Measurement at the decoupled price p' uses realizableBadDebtAtPrice (certora/helpers/MidnightWrapper.sol), -// a verbatim structural copy of the realizableBadDebt getter that values each active collateral at an -// explicitly passed price instead of reading IOracle(...).price(). Per active collateral c it subtracts -// g_x(c) = mulDivUp(mulDivUp(c, x, ORACLE_PRICE_SCALE), WAD, maxLif) -// where x is the passed measurement price. The iterated zeroFloorSub equals zeroFloorSub(debt, sum of -// terms), so rbd is monotone: more debt removed or less coverage removed cannot increase it. -// -// Proof (single seized collateral c_k -> c_k - seized, debt reduced by >= repaidUnits): -// coverage-removed at p' = g_{p'}(c_k) - g_{p'}(c_k - seized) -// <= g_{p'}(seized) [getter-form double sub-additivity, at p'] -// <= g_{p}(seized) [getter-form price monotonicity, p' <= p] -// <= repaidUnits [seize-value bound at p / repaid = g_p(seized)] -// <= debt-removed. -// Since coverage-removed <= debt-removed, zeroFloorSub monotonicity gives R' <= R with no slack. -// -// This reuses #1079's seize-value bound and double sub-additivity lemmas, and adds the price -// monotonicity of the getter term (g is non-decreasing in the price argument), which is what bridges -// the p'-measured coverage drop to the p-priced seize/repay logic liquidate actually executes. -// -// Restricted, like the isolated liquidate leg it builds on, to the non-post-maturity path -// (require !postMaturityMode, where lif == maxLif, src/Midnight.sol:685-687), a single seized -// collateral, and split along liquidate's exclusive-input branch (repaidUnits == 0 || seizedAssets == 0). +// This shows that timely liquidations before a price drop are never disadvantageous to the creditors. import "BitmapSummaries.spec"; @@ -88,12 +67,6 @@ persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; -// Loose (uninterpreted) mulDiv summaries, identical to RealizableBadDebtLiquidate.spec: because the ghost -// is a function, equal arguments give equal values, so every unchanged collateral term is identical -// between the before-getter and the after-getter measurements. The mulDiv values are otherwise -// constrained only by the near-linear consequences the rule e-matches on (monotonicity in each argument, -// getter-form double sub-additivity, and the seize-value bound), each PROVEN over the concrete mulDiv in -// MulDiv.spec. This keeps the heavy nonlinear reasoning out of the liquidate body. function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -144,12 +117,6 @@ definition axiomAddUpUp(mathint a1, mathint a2, mathint b, mathint d) returns bo // mulDivUp(mulDivDown(a,b,d),d,b) <= a definition axiomInverseUpDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b > 0 && d > 0 => ghostMulDivUp(ghostMulDivDown(a, b, d), d, b) <= a; -/// INVARIANTS /// - -// Proven in CollateralBitmap.spec; assumed here via requireInvariant (not re-proven in this spec). -strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint256 collateralIndex) - collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract.position[id][user].collateralBitmap, collateralIndex)); - /// RULES /// // Realizable bad debt cannot increase from liquidating before a price drop. @@ -184,10 +151,6 @@ rule postDropRbdLiquidateNonIncrease(env e, Midnight.Market market, uint256 coll require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "axiom"; require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "axiom"; require forall mathint a. forall mathint b. forall mathint d1. forall mathint d2. axiomUpMonotoneD(a, b, d1, d2), "axiom"; - //require axiomUpZero(price, ORACLE_PRICE_SCALE()), "axiom"; - //require axiomUpZero(WAD(), maxLif), "axiom"; - //require axiomAddUpUp(collateralAfter, seizedAssetsOut, price, ORACLE_PRICE_SCALE()), "axiom"; - //require axiomAddUpUp(ghostMulDivUp(collateralAfter, price, ORACLE_PRICE_SCALE()), ghostMulDivUp(seizedAssetsOut, price, ORACLE_PRICE_SCALE()), WAD(), maxLif), "axiom"; require axiomUpZero(pDrop, ORACLE_PRICE_SCALE()), "axiom"; require axiomUpZero(WAD(), maxLif), "axiom"; @@ -208,6 +171,6 @@ rule postDropRbdLiquidateNonIncrease(env e, Midnight.Market market, uint256 coll summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; mathint badDebt2b = realizableBadDebt(market, id, borrower); - // liquidating before the price drop (scenario 2) will cause less bad debt in total. + // liquidating before the price drop (scenario 2) will cause less total bad debt than scenario 1. assert badDebt2a + badDebt2b <= badDebt1; } From eab9d09d7e29398ee558ea5fcd5f704eb4cd20c7 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 30 Jul 2026 16:27:55 +0200 Subject: [PATCH 06/11] Removed unused rule --- certora/specs/MulDiv.spec | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index e1ab3b96e..ae9599d22 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -111,18 +111,6 @@ rule mulDivSeizeValueBounded(uint256 r, uint256 l, uint256 price, uint256 wad, u assert mulDivUp(mulDivUp(seized, price, scale), wad, l) <= r; } -// Dropped-price generalization of mulDivSeizeValueBounded: valuing (up-up) the collateral that liquidate -// seizes (down-down at the call-time price) for repaidUnits r at a DROPPED price pDrop <= price never -// exceeds r either. This is mulDivSeizeValueBounded (which bounds the seize value at the call-time price) -// composed with price-monotonicity: pDrop <= price shrinks the up-up valuation, so it stays <= r. Closes -// the whole repaid crux in one fact for PostDropRealizableBadDebt's repaid-input branch. -rule mulDivSeizeValueAtDroppedPriceBounded(uint256 r, uint256 l, uint256 price, uint256 wad, uint256 scale, uint256 pDrop) { - require l > 0 && price > 0 && wad > 0 && scale > 0; - require pDrop >= 0 && pDrop <= price; - uint256 seized = mulDivDown(mulDivDown(r, l, wad), scale, price); - assert mulDivUp(mulDivUp(seized, pDrop, scale), wad, l) <= r; -} - rule mulDivArgumentLesserThanDenominator(uint256 a, uint256 b, uint256 d) { assert a <= d => mulDivDown(a, b, d) <= b; assert a <= d => mulDivUp(a, b, d) <= b; From fbab3fbae90fbc9ec9bca7ec5bcbe9a0cc6b5e1a Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 20 Aug 2026 15:26:38 +0200 Subject: [PATCH 07/11] Use MulDivAxioms --- certora/specs/PostDropRealizableBadDebt.spec | 55 +++++--------------- 1 file changed, 13 insertions(+), 42 deletions(-) diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index b9ba33564..dcb5a2d5d 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -13,6 +13,7 @@ // This shows that timely liquidations before a price drop are never disadvantageous to the creditors. import "BitmapSummaries.spec"; +import "MulDivAxioms.spec"; using Utils as Utils; @@ -63,10 +64,6 @@ persistent ghost maxLifGhost(uint256, uint256) returns uint256; persistent ghost mapping(address => uint256) summaryPrice; -persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; - -persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; - function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -91,32 +88,6 @@ function marketIsCreated(Midnight.Market market) returns (bool) { return tickSpacing(summaryToId(market)) > 0; } -// Monotone in the first argument (proven in MulDiv.spec as 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); - -// Monotone in the second argument (proven in MulDiv.spec as mulDivMonotoneB). -definition axiomDownMonotoneB(mathint a, mathint b1, mathint b2, mathint d) returns bool = 0 <= a && 0 <= b1 && b1 <= b2 && 0 < d => ghostMulDivDown(a, b1, d) <= ghostMulDivDown(a, b2, d); - -// Monotone in the first argument (proven in MulDiv.spec as 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); - -// Monotone in the second argument (proven in MulDiv.spec as mulDivMonotoneB). -definition axiomUpMonotoneB(mathint a, mathint b1, mathint b2, mathint d) returns bool = 0 <= a && 0 <= b1 && b1 <= b2 && 0 < d => ghostMulDivUp(a, b1, d) <= ghostMulDivUp(a, b2, d); - -// Monotone in the third argument (proven in MulDiv.spec as mulDivMonotoneD). -definition axiomUpMonotoneD(mathint a, mathint b, mathint d1, mathint d2) returns bool = 0 <= a && 0 <= b && 0 < d1 && d1 <= d2 => ghostMulDivUp(a, b, d2) <= ghostMulDivUp(a, b, d1); - -// Zero collateral values to zero (proven in MulDiv.spec as mulDivZero). -definition axiomUpZero(mathint b, mathint d) returns bool = d > 0 => ghostMulDivUp(0, b, d) == 0; - -// proven in MulDiv.spec as mulDivAddUpUp: -// mulDivUp(a1 + a2, b, d) <= mulDivUp(a1, b, d) + mulDivUp(a2, b, d). -definition axiomAddUpUp(mathint a1, mathint a2, mathint b, mathint d) returns bool = a1 >= 0 && a2 >= 0 && b >= 0 && d > 0 => ghostMulDivUp(a1 + a2, b, d) <= ghostMulDivUp(a1, b, d) + ghostMulDivUp(a2, b, d); - -// proven in MulDiv.spec as mulDivAddUpUp: -// mulDivUp(mulDivDown(a,b,d),d,b) <= a -definition axiomInverseUpDown(mathint a, mathint b, mathint d) returns bool = a >= 0 && b > 0 && d > 0 => ghostMulDivUp(ghostMulDivDown(a, b, d), d, b) <= a; - /// RULES /// // Realizable bad debt cannot increase from liquidating before a price drop. @@ -138,24 +109,24 @@ rule postDropRbdLiquidateNonIncrease(env e, Midnight.Market market, uint256 coll seizedAssetsOut = seizedAssets; } else { seizedAssetsOut = ghostMulDivDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price); - require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomDownMonotoneA(a1, a2, b, d), "axiom"; - require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomDownMonotoneB(a, b1, b2, d), "axiom"; - require axiomInverseUpDown(repaidUnits, maxLif, WAD()), "axiom"; - require axiomInverseUpDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price), "axiom"; + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomMathMulDivDownMonotoneA(a1, a2, b, d), "axiom"; + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomMathMulDivDownMonotoneB(a, b1, b2, d), "axiom"; + require axiomMathMulDivInverseUpDown(repaidUnits, maxLif, WAD()), "axiom"; + require axiomMathMulDivInverseUpDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price), "axiom"; } uint256 collateralBefore = collateral(id, borrower, collateralIndex); mathint collateralAfter = collateralBefore - seizedAssetsOut; - require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomDownMonotoneB(a, b1, b2, d), "axiom"; - require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomUpMonotoneA(a1, a2, b, d), "axiom"; - require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomUpMonotoneB(a, b1, b2, d), "axiom"; - require forall mathint a. forall mathint b. forall mathint d1. forall mathint d2. axiomUpMonotoneD(a, b, d1, d2), "axiom"; + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomMathMulDivDownMonotoneB(a, b1, b2, d), "axiom"; + require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomMathMulDivUpMonotoneA(a1, a2, b, d), "axiom"; + require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomMathMulDivUpMonotoneB(a, b1, b2, d), "axiom"; + require forall mathint a. forall mathint b. forall mathint d1. forall mathint d2. axiomMathMulDivUpMonotoneD(a, b, d1, d2), "axiom"; - require axiomUpZero(pDrop, ORACLE_PRICE_SCALE()), "axiom"; - require axiomUpZero(WAD(), maxLif), "axiom"; - require axiomAddUpUp(collateralAfter, seizedAssetsOut, pDrop, ORACLE_PRICE_SCALE()), "axiom"; - require axiomAddUpUp(ghostMulDivUp(collateralAfter, pDrop, ORACLE_PRICE_SCALE()), ghostMulDivUp(seizedAssetsOut, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif), "axiom"; + require axiomMathMulDivUpZeroA(pDrop, ORACLE_PRICE_SCALE()), "axiom"; + require axiomMathMulDivUpZeroA(WAD(), maxLif), "axiom"; + require axiomMathMulDivAddUpUp(collateralAfter, seizedAssetsOut, pDrop, ORACLE_PRICE_SCALE()), "axiom"; + require axiomMathMulDivAddUpUp(ghostMulDivUp(collateralAfter, pDrop, ORACLE_PRICE_SCALE()), ghostMulDivUp(seizedAssetsOut, pDrop, ORACLE_PRICE_SCALE()), WAD(), maxLif), "axiom"; // scenario 1: price drops, then realize bad debt summaryPrice[market.collateralParams[collateralIndex].oracle] = pDrop; From c19a2f3b82fb2c77f1b3c532c00cf8295eb1a74a Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 20 Aug 2026 16:18:10 +0200 Subject: [PATCH 08/11] Added a comment that seizedAssetsOut is only an upper bound --- certora/specs/PostDropRealizableBadDebt.spec | 2 ++ 1 file changed, 2 insertions(+) diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index dcb5a2d5d..45e999f15 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -108,6 +108,8 @@ rule postDropRbdLiquidateNonIncrease(env e, Midnight.Market market, uint256 coll if (repaidUnits == 0) { seizedAssetsOut = seizedAssets; } else { + // This computes an upper bound of the seizedAssetsOut computed by liquidate() (using maxLif). + // The proof reasons about the worst-case, the real case follows from this by the monotonicity axioms. seizedAssetsOut = ghostMulDivDown(ghostMulDivDown(repaidUnits, maxLif, WAD()), ORACLE_PRICE_SCALE(), price); require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomMathMulDivDownMonotoneA(a1, a2, b, d), "axiom"; require forall mathint a. forall mathint b1. forall mathint b2. forall mathint d. axiomMathMulDivDownMonotoneB(a, b1, b2, d), "axiom"; From 4c86f550de33fdebe60e83b053a11a7db44ca816 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 31 Aug 2026 15:24:55 +0200 Subject: [PATCH 09/11] Applied review changes --- certora/confs/PostDropRealizableBadDebt.conf | 1 - certora/specs/PostDropRealizableBadDebt.spec | 22 ++++++++------------ 2 files changed, 9 insertions(+), 14 deletions(-) diff --git a/certora/confs/PostDropRealizableBadDebt.conf b/certora/confs/PostDropRealizableBadDebt.conf index d4efe7c2a..247918a46 100644 --- a/certora/confs/PostDropRealizableBadDebt.conf +++ b/certora/confs/PostDropRealizableBadDebt.conf @@ -21,7 +21,6 @@ "-smt_useNIA true", "-depth 5", "-mediumTimeout 120", - "-timeout 7200", "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},cvc5:def]" ], "smt_timeout": 7200, diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index 45e999f15..850a3878b 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -29,29 +29,25 @@ methods { function collateral(bytes32, address, uint256) external returns (uint128) envfree; function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; - // Per-callee constant price (no price update): this is the call-time price p that liquidate reads. - // The measurement price p' is decoupled from it, passed explicitly to realizableBadDebtAtPrice. + // Per-callee price is modelled by a ghost mappings from oracle to price. + // The change of the price in a rule can then be modelled by updating the mapping. function _.price() external => summaryPrice[calledContract] expect(uint256); + // Summarize toId (which uses abi.encodePacked()) by a simple hash that is easier to reason about. + // Ignore side effects of storeInCode. function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; + // Abstract deterministic summaries for mathematical functions. 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); function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor); // All external calls are assumed non-reentrant / non-reverting: we reason about the function bodies for safety properties. - function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; - function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; - function _.isRatified(Midnight.Offer, bytes, address) external => NONDET; - function _.canIncreaseCredit(address) external => NONDET; - function _.canIncreaseDebt(address) external => NONDET; - function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; - function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; - function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; - function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; - function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; + function SafeTransferLib.safeTransfer(address, address, uint256) internal => HAVOC_ECF; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => HAVOC_ECF; + function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => HAVOC_ECF; } /// SUMMARIES / GHOSTS /// @@ -99,7 +95,7 @@ rule postDropRbdLiquidateNonIncrease(env e, Midnight.Market market, uint256 coll mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; - uint256 price = summaryPrice[market.collateralParams[collateralIndex].oracle]; + uint256 price; uint256 pDrop; require pDrop <= price, "the dropped price is less than the initial price"; From ca406a1ac8251db2d29e4e3695a1d7aafb2c1595 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 31 Aug 2026 15:36:32 +0200 Subject: [PATCH 10/11] More review comments. --- certora/specs/PostDropRealizableBadDebt.spec | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index 850a3878b..c732c64e1 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -21,11 +21,6 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function realizableBadDebt(Midnight.Market, bytes32, address) external returns (uint256) envfree; - function debt(bytes32, address) external returns (uint128) envfree; - function totalUnits(bytes32) external returns (uint128) envfree; - function lossFactor(bytes32) external returns (uint128) envfree; - function liquidationLocked(bytes32, address) external returns (bool) envfree; - function tickSpacing(bytes32) external returns (uint8) envfree; function collateral(bytes32, address, uint256) external returns (uint128) envfree; function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; @@ -45,8 +40,8 @@ methods { function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor); // All external calls are assumed non-reentrant / non-reverting: we reason about the function bodies for safety properties. - function SafeTransferLib.safeTransfer(address, address, uint256) internal => HAVOC_ECF; - function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => HAVOC_ECF; + function _.transfer(address, uint256) external => HAVOC_ECF; + function _.transferFrom(address, address, uint256) external => HAVOC_ECF; function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => HAVOC_ECF; } @@ -80,10 +75,6 @@ function summaryToId(Midnight.Market market) returns (bytes32) { return Utils.hashMarket(market); } -function marketIsCreated(Midnight.Market market) returns (bool) { - return tickSpacing(summaryToId(market)) > 0; -} - /// RULES /// // Realizable bad debt cannot increase from liquidating before a price drop. @@ -93,7 +84,7 @@ rule postDropRbdLiquidateNonIncrease(env e, Midnight.Market market, uint256 coll bytes32 id = summaryToId(market); mathint maxLif = maxLifGhost(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor); - require maxLif >= to_mathint(WAD()), "maxLif at least 1x (market-creation invariant)"; + require maxLif >= to_mathint(WAD()), "see maxLifIsAtLeastWad in ExactMath.spec"; uint256 price; uint256 pDrop; From 244292baef8ae76cf4d53bbdd2162887778a2bc4 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 09:34:10 +0000 Subject: [PATCH 11/11] certora: explain toId/storeInCode summary soundness and document PostDropRealizableBadDebt --- certora/README.md | 1 + certora/specs/PostDropRealizableBadDebt.spec | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/certora/README.md b/certora/README.md index fa875d9a1..d193701fd 100644 --- a/certora/README.md +++ b/certora/README.md @@ -33,6 +33,7 @@ Healthy positions stay healthy, and liquidations only touch liquidatable positio - [`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`. +- [`PostDropRealizableBadDebt.spec`](specs/PostDropRealizableBadDebt.spec) checks that liquidating a position at the current price cannot increase the realizable bad debt measured after an oracle price drop, for both of `liquidate`'s input branches (seized and repaid). ## Offers and consumption diff --git a/certora/specs/PostDropRealizableBadDebt.spec b/certora/specs/PostDropRealizableBadDebt.spec index c732c64e1..15c76d672 100644 --- a/certora/specs/PostDropRealizableBadDebt.spec +++ b/certora/specs/PostDropRealizableBadDebt.spec @@ -28,8 +28,10 @@ methods { // The change of the price in a rule can then be modelled by updating the mapping. function _.price() external => summaryPrice[calledContract] expect(uint256); - // Summarize toId (which uses abi.encodePacked()) by a simple hash that is easier to reason about. - // Ignore side effects of storeInCode. + // toId only keys position[id]/marketState[id], so the proof just needs a deterministic injective + // market -> id map. Its abi.encodePacked is not injective in CVL, so we summarize by + // keccak256(abi.encode(market)) (hashMarket), which is injective and applied uniformly. + // storeInCode's returned address and code write never feed the accounting or price the rule reads. function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;