From 7a0340368e6f1b5c52f3632d8a8739dc5dde60b6 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Thu, 4 Jun 2026 17:35:30 +0000 Subject: [PATCH] fix: extend liquidation auction duration --- certora/specs/LiquidationProfitability.spec | 10 +++++----- certora/specs/NoDivisionByZero.spec | 2 +- src/libraries/ConstantsLib.sol | 2 +- test/LiquidationTest.sol | 4 ++++ 4 files changed, 11 insertions(+), 7 deletions(-) diff --git a/certora/specs/LiquidationProfitability.spec b/certora/specs/LiquidationProfitability.spec index 415f70a5d..220e1067d 100644 --- a/certora/specs/LiquidationProfitability.spec +++ b/certora/specs/LiquidationProfitability.spec @@ -31,7 +31,7 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; -definition TIME_TO_MAX_LIF() returns uint256 = 900; // 15 min +definition TIME_TO_MAX_LIF() returns uint256 = 3600; // 60 min persistent ghost summaryPrice(address) returns uint256; @@ -67,7 +67,7 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { /// LIF CHARACTERIZATION /// -/// For repaidUnits input: lif >= WAD (solvency), and lif == maxLif when in normal mode or when the call is >= 15 min post-maturity (profitability). +/// For repaidUnits input: lif >= WAD (solvency), and lif == maxLif when in normal mode or when the call is >= 60 min post-maturity (profitability). rule liquidationLifRepaidUnits(env e, Midnight.Market market, uint256 collateralIndex, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) { uint256 maxLif = market.collateralParams[collateralIndex].maxLif; require maxLif >= WAD(), "see the rule maxLifIsAtLeastWad"; @@ -83,11 +83,11 @@ rule liquidationLifRepaidUnits(env e, Midnight.Market market, uint256 collateral // lif >= WAD: liquidator receives collateral worth at least the repaid debt (up to 1 unit floor rounding on seizedAssets) at the oracle price. assert (seizedResult + 1) * price >= repaidResult * ORACLE_PRICE_SCALE(); - // lif == maxLif when in normal mode or when >= 15 min post-maturity: full liquidation incentive factor applies. + // lif == maxLif when in normal mode or when >= 60 min post-maturity: full liquidation incentive factor applies. assert maxLifReached => (seizedResult + 1) * price * WAD() + ORACLE_PRICE_SCALE() * WAD() > repaidResult * maxLif * ORACLE_PRICE_SCALE(); } -/// For seizedAssets input: lif >= WAD (solvency), and lif == maxLif when in normal mode or when the call is >= 15 min post-maturity (profitability). +/// For seizedAssets input: lif >= WAD (solvency), and lif == maxLif when in normal mode or when the call is >= 60 min post-maturity (profitability). rule liquidationLifSeizedAssets(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) { uint256 maxLif = market.collateralParams[collateralIndex].maxLif; require maxLif >= WAD(), "see the rule maxLifIsAtLeastWad"; @@ -103,6 +103,6 @@ rule liquidationLifSeizedAssets(env e, Midnight.Market market, uint256 collatera // lif >= WAD: liquidator receives collateral worth at least the repaid debt (up to 1 unit ceil rounding on repaidUnits) at the oracle price. assert seizedResult * price > (repaidResult - 1) * ORACLE_PRICE_SCALE(); - // lif == maxLif when in normal mode or when >= 15 min post-maturity: full liquidation incentive factor applies. + // lif == maxLif when in normal mode or when >= 60 min post-maturity: full liquidation incentive factor applies. assert maxLifReached => seizedResult * price * WAD() + ORACLE_PRICE_SCALE() * WAD() > (repaidResult - 1) * maxLif * ORACLE_PRICE_SCALE(); } diff --git a/certora/specs/NoDivisionByZero.spec b/certora/specs/NoDivisionByZero.spec index 16a05df03..1eb8c1c5f 100644 --- a/certora/specs/NoDivisionByZero.spec +++ b/certora/specs/NoDivisionByZero.spec @@ -5,7 +5,7 @@ // All other Solidity divisions in the codebase use non-zero denominators: // - settlementFee: divides by (end - start), always a positive constant from the breakpoint table. // - setMarketSettlementFee / setDefaultSettlementFee: divide by CBP (1e12). -// - liquidate: divides by TIME_TO_MAX_LIF (15 minutes = 900). +// - liquidate: divides by TIME_TO_MAX_LIF (60 minutes = 3600). // - tickToPrice: divides by 5e12 or a value greater than 1e18. // - wExp, used in tickToPrice: divides by non-zero constants. // Therefore, we only look for division by zero in mulDivDown and mulDivUp in this file. diff --git a/src/libraries/ConstantsLib.sol b/src/libraries/ConstantsLib.sol index f91d005c2..bd1894754 100644 --- a/src/libraries/ConstantsLib.sol +++ b/src/libraries/ConstantsLib.sol @@ -16,7 +16,7 @@ uint256 constant MAX_SETTLEMENT_FEE_90_DAYS = 0.00125e18; uint256 constant MAX_SETTLEMENT_FEE_180_DAYS = 0.0025e18; uint256 constant MAX_SETTLEMENT_FEE_360_DAYS = 0.005e18; uint32 constant MAX_CONTINUOUS_FEE = uint32(uint256(0.01e18) / uint256(365 days)); -uint256 constant TIME_TO_MAX_LIF = 15 minutes; +uint256 constant TIME_TO_MAX_LIF = 60 minutes; uint256 constant MAX_COLLATERALS = 128; uint256 constant MAX_COLLATERALS_PER_BORROWER = 16; uint256 constant LIQUIDATION_CURSOR_LOW = 0.25e18; diff --git a/test/LiquidationTest.sol b/test/LiquidationTest.sol index e2800d706..68200b6f8 100644 --- a/test/LiquidationTest.sol +++ b/test/LiquidationTest.sol @@ -73,6 +73,10 @@ contract LiquidationTest is BaseTest { deal(address(loanToken), address(this), type(uint256).max); } + function testTimeToMaxLifIs60Minutes() public pure { + assertEq(TIME_TO_MAX_LIF, 60 minutes); + } + function testLiquidateInvalidCollateralIndex() public { uint256 units = 100e18; collateralize(market, borrower, units);