From e719780416efb29c737ef2383bdf9db9b8ccd2f7 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 23 Jun 2026 13:59:40 +0200 Subject: [PATCH 1/5] Replace require->assert for recovery >= maxDebtContrib Make the price/lif/lltv accessors a definition --- certora/specs/LiquidateLiveness.spec | 59 +++++++++++++++++----------- 1 file changed, 35 insertions(+), 24 deletions(-) diff --git a/certora/specs/LiquidateLiveness.spec b/certora/specs/LiquidateLiveness.spec index 5dc88baf..7268ad37 100644 --- a/certora/specs/LiquidateLiveness.spec +++ b/certora/specs/LiquidateLiveness.spec @@ -54,6 +54,17 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; + +definition getPrice(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = + collateralIndex == 0 ? ghostPrice(params[0].oracle) : collateralIndex == 1 ? ghostPrice(params[1].oracle) : ghostPrice(params[2].oracle); + +definition getLltv(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = + collateralIndex == 0 ? params[0].lltv : collateralIndex == 1 ? params[1].lltv : params[2].lltv; + +definition getMaxLif(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = + collateralIndex == 0 ? params[0].maxLif : collateralIndex == 1 ? params[1].maxLif : params[2].maxLif; + + // Assume the market is already created. function summaryToId(Midnight.Market market) returns bytes32 { return Utils.hashMarket(market); @@ -151,7 +162,7 @@ function seizablePreamble(env e, Midnight.Market market, bytes32 id, address bor threeCollatSetup(e, market, id, borrower); require collateralIndex == 0 || collateralIndex == 1 || collateralIndex == 2, "seized index in {0,1,2} (<= loop_iter)"; require summaryGetBit(collateralBitmap(id, borrower), collateralIndex), "the seized collateral is active"; - require (collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle)) > 0, "the seized collateral is priced (LIVENESS)"; + require getPrice(collateralIndex, market.collateralParams) > 0, "the seized collateral is priced (LIVENESS)"; } /// maxDebt = sum over all collaterals of collat * price * lltv (down-rounded). @@ -194,15 +205,15 @@ function lowLltvScaffolding(Midnight.Market market, bytes32 id, address borrower uint128 collat2 = collateral(id, borrower, 2); // recovery_i >= maxDebtContrib_i for every collateral - require ghostMulDivUp(ghostMulDivUp(collat0, price0, ORACLE_PRICE_SCALE()), WAD(), maxLif0) >= ghostMulDivDown(ghostMulDivDown(collat0, price0, ORACLE_PRICE_SCALE()), lltv0, WAD()), "recovery0 >= maxDebtContrib0 (any valid collateral, incl. inactive)"; - require ghostMulDivUp(ghostMulDivUp(collat1, price1, ORACLE_PRICE_SCALE()), WAD(), maxLif1) >= ghostMulDivDown(ghostMulDivDown(collat1, price1, ORACLE_PRICE_SCALE()), lltv1, WAD()), "recovery1 >= maxDebtContrib1 (any valid collateral, incl. inactive)"; - require ghostMulDivUp(ghostMulDivUp(collat2, price2, ORACLE_PRICE_SCALE()), WAD(), maxLif2) >= ghostMulDivDown(ghostMulDivDown(collat2, price2, ORACLE_PRICE_SCALE()), lltv2, WAD()), "recovery2 >= maxDebtContrib2 (any valid collateral, incl. inactive)"; + assert ghostMulDivUp(ghostMulDivUp(collat0, price0, ORACLE_PRICE_SCALE()), WAD(), maxLif0) >= ghostMulDivDown(ghostMulDivDown(collat0, price0, ORACLE_PRICE_SCALE()), lltv0, WAD()), "recovery0 >= maxDebtContrib0 (any valid collateral, incl. inactive)"; + assert ghostMulDivUp(ghostMulDivUp(collat1, price1, ORACLE_PRICE_SCALE()), WAD(), maxLif1) >= ghostMulDivDown(ghostMulDivDown(collat1, price1, ORACLE_PRICE_SCALE()), lltv1, WAD()), "recovery1 >= maxDebtContrib1 (any valid collateral, incl. inactive)"; + assert ghostMulDivUp(ghostMulDivUp(collat2, price2, ORACLE_PRICE_SCALE()), WAD(), maxLif2) >= ghostMulDivDown(ghostMulDivDown(collat2, price2, ORACLE_PRICE_SCALE()), lltv2, WAD()), "recovery2 >= maxDebtContrib2 (any valid collateral, incl. inactive)"; // Seized collateral: ExactMath denominator bound (=> WAD*WAD - maxLif*lltv >= WAD >= 1) and strict // recovery > maxDebtContrib (=> debtAfter > maxDebt, so maxRepaid >= 1; needs collatJ*priceJ >= ORACLE_PRICE_SCALE). - uint256 lltvJ = collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv; - uint256 maxLifJ = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif; - uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle); + uint256 lltvJ = getLltv(collateralIndex, market.collateralParams); + uint256 maxLifJ = getMaxLif(collateralIndex, market.collateralParams); + uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint128 collatJ = collateral(id, borrower, collateralIndex); require maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; require ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)"; @@ -216,11 +227,11 @@ rule unhealthyLltvFullLiquidatableForAnySafeAmount(env e, Midnight.Market market bytes32 id = summaryToId(market); seizablePreamble(e, market, id, borrower, collateralIndex); - uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif; - require (collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)"; + uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams); + require getLltv(collateralIndex, market.collateralParams) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)"; uint128 collatJ = collateral(id, borrower, collateralIndex); - uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle); + uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint256 _debt = debtOf(id, borrower); mathint debtAfter = debtAfterBadDebt(market, id, borrower); require _debt > maxDebtSum(market, id, borrower), "unhealthy: debt > maxDebt"; @@ -240,12 +251,12 @@ rule unhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market market, bytes32 id = summaryToId(market); seizablePreamble(e, market, id, borrower, collateralIndex); - uint256 lltv = collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv; - uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif; + uint256 lltv = getLltv(collateralIndex, market.collateralParams); + uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams); require lltv < WAD(), "lltv < WAD partition"; uint128 collatJ = collateral(id, borrower, collateralIndex); - uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle); + uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint256 _debt = debtOf(id, borrower); mathint maxDebt = maxDebtSum(market, id, borrower); mathint debtAfter = debtAfterBadDebt(market, id, borrower); @@ -276,9 +287,9 @@ rule postMaturityLiquidatableForAnySafeAmount(env e, Midnight.Market market, add require e.block.timestamp > market.maturity, "post-maturity partition (liquidatable by expiry)"; - uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif; + uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams); uint128 collatJ = collateral(id, borrower, collateralIndex); - uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle); + uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint256 _debt = debtOf(id, borrower); mathint debtAfter = debtAfterBadDebt(market, id, borrower); @@ -292,19 +303,19 @@ rule postMaturityLiquidatableForAnySafeAmount(env e, Midnight.Market market, add assert debtOf(id, borrower) < _debt; } -/// SEIZE PATH (seizedAssets > 0, repaidUnits = 0): contract derives repaidUnits = mulDivUp(mulDivUp(seizedAssets, price0, ORACLE_PRICE_SCALE), WAD, lif). -/// Collateral guard is a direct `seizedAssets <= collateral[0]`; debt-underflow / RCF apply to the derived repaidUnits, which is >= 1 (seizedAssets > 0, price0 > 0) so progress holds. +/// SEIZE PATH (seizedAssets > 0, repaidUnits = 0): contract derives repaidUnits = mulDivUp(mulDivUp(seizedAssets, price, ORACLE_PRICE_SCALE), WAD, lif). +/// Collateral guard is a direct `seizedAssets <= collateral`; debt-underflow / RCF apply to the derived repaidUnits, which is >= 1 (seizedAssets > 0, price > 0) so progress holds. /// Seize path, unhealthy, lltv == WAD: maxRepaid = uint256.max (RCF auto-passes), lif = maxLif. rule seizeUnhealthyLltvFullLiquidatableForAnySafeAmount(env e, Midnight.Market market, address borrower, address receiver, uint256 collateralIndex, uint256 seizedAssets) { bytes32 id = summaryToId(market); seizablePreamble(e, market, id, borrower, collateralIndex); - uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif; - require (collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)"; + uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams); + require getLltv(collateralIndex, market.collateralParams) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)"; uint128 collatJ = collateral(id, borrower, collateralIndex); - uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle); + uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint256 _debt = debtOf(id, borrower); mathint debtAfter = debtAfterBadDebt(market, id, borrower); require _debt > maxDebtSum(market, id, borrower), "unhealthy: debt > maxDebt"; @@ -326,12 +337,12 @@ rule seizeUnhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market ma bytes32 id = summaryToId(market); seizablePreamble(e, market, id, borrower, collateralIndex); - uint256 lltv = collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv; - uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif; + uint256 lltv = getLltv(collateralIndex, market.collateralParams); + uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams); require lltv < WAD(), "lltv < WAD partition"; uint128 collatJ = collateral(id, borrower, collateralIndex); - uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle); + uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint256 _debt = debtOf(id, borrower); mathint maxDebt = maxDebtSum(market, id, borrower); mathint debtAfter = debtAfterBadDebt(market, id, borrower); @@ -365,7 +376,7 @@ rule seizePostMaturityLiquidatableForAnySafeAmount(env e, Midnight.Market market require e.block.timestamp > market.maturity, "post-maturity partition (liquidatable by expiry)"; uint128 collatJ = collateral(id, borrower, collateralIndex); - uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle); + uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint256 _debt = debtOf(id, borrower); mathint debtAfter = debtAfterBadDebt(market, id, borrower); From 4877102620f712b97b1e078638ff4a0bd3a9ac29 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 23 Jun 2026 15:14:07 +0200 Subject: [PATCH 2/5] Replaced some require with assert. --- certora/specs/LiquidateLiveness.spec | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/certora/specs/LiquidateLiveness.spec b/certora/specs/LiquidateLiveness.spec index 7268ad37..dde5b6c1 100644 --- a/certora/specs/LiquidateLiveness.spec +++ b/certora/specs/LiquidateLiveness.spec @@ -215,8 +215,8 @@ function lowLltvScaffolding(Midnight.Market market, bytes32 id, address borrower uint256 maxLifJ = getMaxLif(collateralIndex, market.collateralParams); uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint128 collatJ = collateral(id, borrower, collateralIndex); - require maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; - require ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)"; + assert maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; + assert ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)"; } /// REPAY PATH (repaidUnits > 0, seizedAssets = 0) /// @@ -267,6 +267,7 @@ rule unhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market market, // maxRepaid (RCF check) = mulDivUp(debtAfter - maxDebt, WAD*WAD, WAD*WAD - lif*lltv), lif = maxLif here. // Reconstructed bit-for-bit so the bound matches the RCF check exactly; denominator > 0 and debtAfter >= maxDebt from lowLltvScaffolding. mathint maxRepaid = ghostMulDivUp(assert_uint256(debtAfter - maxDebt), assert_uint256(WAD() * WAD()), assert_uint256(WAD() * WAD() - maxLif * lltv)); + assert maxRepaid > 0, "it's possible to repay at least one unit"; require repaidUnits > 0; require repaidUnits <= maxRepaid, "RCF check passes"; @@ -353,6 +354,7 @@ rule seizeUnhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market ma // maxRepaid (RCF check) = mulDivUp(debtAfter - maxDebt, WAD*WAD, WAD*WAD - lif*lltv), // lif = maxLif here. Reconstructed bit-for-bit so the bound matches the contract's RCF check exactly. mathint maxRepaid = ghostMulDivUp(assert_uint256(debtAfter - maxDebt), assert_uint256(WAD() * WAD()), assert_uint256(WAD() * WAD() - maxLif * lltv)); + assert maxRepaid > 0, "it's possible to repay at least one unit"; mathint repaidUnits = ghostMulDivUp(ghostMulDivUp(seizedAssets, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLif); From 9e0d0411d85f905a599bfc53f2fbb77453ab4834 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 23 Jun 2026 18:53:27 +0200 Subject: [PATCH 3/5] reverted one require/assert change This leads to timeouts --- certora/specs/LiquidateLiveness.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/LiquidateLiveness.spec b/certora/specs/LiquidateLiveness.spec index dde5b6c1..16d1c86a 100644 --- a/certora/specs/LiquidateLiveness.spec +++ b/certora/specs/LiquidateLiveness.spec @@ -215,8 +215,8 @@ function lowLltvScaffolding(Midnight.Market market, bytes32 id, address borrower uint256 maxLifJ = getMaxLif(collateralIndex, market.collateralParams); uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint128 collatJ = collateral(id, borrower, collateralIndex); - assert maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; - assert ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)"; + require maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; + require ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)"; } /// REPAY PATH (repaidUnits > 0, seizedAssets = 0) /// From f00014c68c314691d635de3d4af53cf92a9e7575 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 23 Jun 2026 19:02:15 +0200 Subject: [PATCH 4/5] Lint definitions --- certora/specs/LiquidateLiveness.spec | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/certora/specs/LiquidateLiveness.spec b/certora/specs/LiquidateLiveness.spec index 16d1c86a..551cfd62 100644 --- a/certora/specs/LiquidateLiveness.spec +++ b/certora/specs/LiquidateLiveness.spec @@ -54,16 +54,11 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; +definition getPrice(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = collateralIndex == 0 ? ghostPrice(params[0].oracle) : collateralIndex == 1 ? ghostPrice(params[1].oracle) : ghostPrice(params[2].oracle); -definition getPrice(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = - collateralIndex == 0 ? ghostPrice(params[0].oracle) : collateralIndex == 1 ? ghostPrice(params[1].oracle) : ghostPrice(params[2].oracle); - -definition getLltv(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = - collateralIndex == 0 ? params[0].lltv : collateralIndex == 1 ? params[1].lltv : params[2].lltv; - -definition getMaxLif(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = - collateralIndex == 0 ? params[0].maxLif : collateralIndex == 1 ? params[1].maxLif : params[2].maxLif; +definition getLltv(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = collateralIndex == 0 ? params[0].lltv : collateralIndex == 1 ? params[1].lltv : params[2].lltv; +definition getMaxLif(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = collateralIndex == 0 ? params[0].maxLif : collateralIndex == 1 ? params[1].maxLif : params[2].maxLif; // Assume the market is already created. function summaryToId(Midnight.Market market) returns bytes32 { From fb17b6e593681010f4007bc351e3e316925c5af2 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 23 Jun 2026 20:51:36 +0200 Subject: [PATCH 5/5] Replace one require with assert. --- certora/specs/LiquidateLiveness.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/LiquidateLiveness.spec b/certora/specs/LiquidateLiveness.spec index 551cfd62..53baaeaf 100644 --- a/certora/specs/LiquidateLiveness.spec +++ b/certora/specs/LiquidateLiveness.spec @@ -210,7 +210,7 @@ function lowLltvScaffolding(Midnight.Market market, bytes32 id, address borrower uint256 maxLifJ = getMaxLif(collateralIndex, market.collateralParams); uint256 priceJ = getPrice(collateralIndex, market.collateralParams); uint128 collatJ = collateral(id, borrower, collateralIndex); - require maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; + assert maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; require ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)"; }