From aaf795289b847cb11349f8364d31283eaccf705d Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Thu, 4 Jun 2026 15:49:47 +0200 Subject: [PATCH 1/3] round up collat value in rcf check --- src/Midnight.sol | 14 +++++++------- test/LiquidationTest.sol | 33 +++++++++++++++++++-------------- 2 files changed, 26 insertions(+), 21 deletions(-) diff --git a/src/Midnight.sol b/src/Midnight.sol index a95c455c..c5daae94 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -69,10 +69,10 @@ import {IMidnight, Market, Offer, CollateralParams, MarketState, Position} from /// <=> repaidUnits <= (debtOf-maxDebt) / (1 - LIF*LLTV). /// @dev The RCF is deactivated for small collateral amount, essentially to mitigate issues with liquidations that are /// too small compared to the gas cost. More precisely, it is deactivated if the liquidation could leave a collateral -/// with a value that would not be enough to repay rcfThreshold units. Which means (omitting scaling and roundings): -/// minNewCollateral * liquidatedCollatPrice / LIF < rcfThreshold -/// <=> (collateral - maxRepaid * LIF / liquidatedCollatPrice) * liquidatedCollatPrice / LIF < rcfThreshold -/// <=> collateral * liquidatedCollatPrice / LIF - maxRepaid < rcfThreshold +/// with a value that would repay at most rcfThreshold units. Which means (omitting scaling and roundings): +/// minNewCollateral * liquidatedCollatPrice / LIF <= rcfThreshold +/// <=> (collateral - maxRepaid * LIF / liquidatedCollatPrice) * liquidatedCollatPrice / LIF <= rcfThreshold +/// <=> max(collateral * liquidatedCollatPrice / LIF - maxRepaid, 0) <= rcfThreshold /// @dev In the "post-maturity mode", the LIF (liquidation incentive factor) grows linearly from 1 at maturity to maxLif /// at maturity + TIME_TO_MAX_LIF, and the RCF is deactivated. /// @dev In both modes, maxLif is used to determine if the account has some bad debt, to always assume the worst case. @@ -664,10 +664,10 @@ contract Midnight is IMidnight { uint256 maxRepaid = lltv < WAD ? (_position.debt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lif * lltv) : type(uint256).max; + uint256 repaidIfAllSeized = _position.collateral[collateralIndex] + .mulDivUp(liquidatedCollatPrice, ORACLE_PRICE_SCALE).mulDivUp(WAD, lif); require( - repaidUnits <= maxRepaid - || _position.collateral[collateralIndex].mulDivDown(liquidatedCollatPrice, ORACLE_PRICE_SCALE) - .mulDivDown(WAD, lif).zeroFloorSub(maxRepaid) < market.rcfThreshold, + repaidUnits <= maxRepaid || repaidIfAllSeized.zeroFloorSub(maxRepaid) <= market.rcfThreshold, RecoveryCloseFactorConditionsViolated() ); } diff --git a/test/LiquidationTest.sol b/test/LiquidationTest.sol index e2800d70..4588f93c 100644 --- a/test/LiquidationTest.sol +++ b/test/LiquidationTest.sol @@ -549,11 +549,15 @@ contract LiquidationTest is BaseTest { units = bound(units, 100, MAX_UNITS); liquidationOraclePrice = bound(liquidationOraclePrice, badDebtPriceDown(units) + 1, ORACLE_PRICE_SCALE - 1); - _setupUnhealthy(units, liquidationOraclePrice); + (uint256 collatAmount,) = _setupUnhealthy(units, liquidationOraclePrice); uint256 maxR = _maxRepaid(units, units, liquidationOraclePrice); + uint256 repaidIfAllSeized = collatAmount.mulDivUp(liquidationOraclePrice, ORACLE_PRICE_SCALE) + .mulDivUp(WAD, market.collateralParams[0].maxLif); + vm.assume(maxR < units); + vm.assume(maxR < repaidIfAllSeized); - repaid = bound(repaid, maxR + 1, max(units, maxR + 1)); + repaid = bound(repaid, maxR + 1, units); vm.expectRevert(IMidnight.RecoveryCloseFactorConditionsViolated.selector); midnight.liquidate(market, 0, 0, repaid, borrower, false, address(this), address(0), ""); @@ -579,32 +583,32 @@ contract LiquidationTest is BaseTest { assertLe(remainingDebt, newMaxDebt + 3, "position should be approximately just healthy after max repayment"); } - /// @dev When rcfThreshold > remaining debt after max repayment, full liquidation is allowed pre-maturity. + /// @dev When rcfThreshold >= remaining repayable after max repayment, full liquidation is allowed pre-maturity. function testRcfThresholdAllowsFullLiquidation(uint256 units, uint256 liquidationOraclePrice, uint256 rcfThreshold) public { units = bound(units, 100, MAX_UNITS); liquidationOraclePrice = bound(liquidationOraclePrice, fullRepaymentPrice(units), ORACLE_PRICE_SCALE - 1); - // Compute remaining debt after max repayment from the input parameters. + // Compute remaining repayable after max repayment from the input parameters. uint256 lltv = market.collateralParams[0].lltv; uint256 collatAmount = units.mulDivUp(WAD, lltv); uint256 maxRepaid = _maxRepaid(units, units, liquidationOraclePrice); uint256 lif0 = market.collateralParams[0].maxLif; - uint256 remainingRepayable = collatAmount.mulDivDown(liquidationOraclePrice, ORACLE_PRICE_SCALE) - .mulDivDown(WAD, lif0).zeroFloorSub(maxRepaid); - market.rcfThreshold = bound(rcfThreshold, remainingRepayable + 1, type(uint256).max); + uint256 remainingRepayable = collatAmount.mulDivUp(liquidationOraclePrice, ORACLE_PRICE_SCALE) + .mulDivUp(WAD, lif0).zeroFloorSub(maxRepaid); + market.rcfThreshold = bound(rcfThreshold, remainingRepayable, type(uint256).max); collateralize(market, borrower, units); setupMarket(market, units); Oracle(market.collateralParams[0].oracle).setPrice(liquidationOraclePrice); - // Full liquidation should succeed because remaining debt < rcfThreshold. + // Full liquidation should succeed because remaining repayable <= rcfThreshold. midnight.liquidate(market, 0, 0, units, borrower, false, address(this), address(0), ""); assertEq(midnight.debtOf(toId(market), borrower), 0, "debt should be zero"); } - /// @dev When rcfThreshold <= remaining debt after max repayment, recovery close factor is enforced. + /// @dev When rcfThreshold < remaining repayable after max repayment, recovery close factor is enforced. function testRcfThresholdEnforcesRecoveryCloseFactor( uint256 units, uint256 liquidationOraclePrice, @@ -613,20 +617,21 @@ contract LiquidationTest is BaseTest { units = bound(units, 100, MAX_UNITS); liquidationOraclePrice = bound(liquidationOraclePrice, badDebtPriceDown(units) + 1, ORACLE_PRICE_SCALE - 1); - // Compute remaining debt after max repayment from the input parameters. + // Compute remaining repayable after max repayment from the input parameters. uint256 lltv = market.collateralParams[0].lltv; uint256 collatAmount = units.mulDivUp(WAD, lltv); uint256 maxRepaid = _maxRepaid(units, units, liquidationOraclePrice); vm.assume(maxRepaid < units); // needed because of the round up. - uint256 remainingRepayable = collatAmount.mulDivDown(liquidationOraclePrice, ORACLE_PRICE_SCALE) - .mulDivDown(WAD, market.collateralParams[0].maxLif).zeroFloorSub(maxRepaid); - market.rcfThreshold = bound(rcfThreshold, 0, remainingRepayable); + uint256 remainingRepayable = collatAmount.mulDivUp(liquidationOraclePrice, ORACLE_PRICE_SCALE) + .mulDivUp(WAD, market.collateralParams[0].maxLif).zeroFloorSub(maxRepaid); + vm.assume(remainingRepayable > 0); + market.rcfThreshold = bound(rcfThreshold, 0, remainingRepayable - 1); collateralize(market, borrower, units); setupMarket(market, units); Oracle(market.collateralParams[0].oracle).setPrice(liquidationOraclePrice); - // Full liquidation should revert because remaining debt >= rcfThreshold. + // Full liquidation should revert because remaining repayable > rcfThreshold. vm.expectRevert(IMidnight.RecoveryCloseFactorConditionsViolated.selector); midnight.liquidate(market, 0, 0, units, borrower, false, address(this), address(0), ""); } From 8375bb604de65dc6706856711a2df99cfa7652be Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Tue, 23 Jun 2026 13:01:44 +0200 Subject: [PATCH 2/3] split assert --- certora/confs/LiquidationProfitability.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/LiquidationProfitability.conf b/certora/confs/LiquidationProfitability.conf index 5cdc1af4..c59bbc65 100644 --- a/certora/confs/LiquidationProfitability.conf +++ b/certora/confs/LiquidationProfitability.conf @@ -12,6 +12,7 @@ "optimistic_hashing": true, "hashing_length_bound": 2048, "smt_timeout": 7200, + "multi_assert_check": true, "prover_args": [ "-destructiveOptimizations twostage", "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]", From 6b5fc83acb81dcd2ef97cc665bb8cd3bd2dcba4f Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Tue, 23 Jun 2026 13:31:22 +0200 Subject: [PATCH 3/3] increase timeout --- certora/confs/Reentrancy.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index 1940cfb8..b93b5c9a 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -14,5 +14,6 @@ "loop_iter": 5, "optimistic_hashing": true, "hashing_length_bound": 2048, + "smt_timeout": 7200, "msg": "Midnight Reentrancy" }