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}]", 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" } diff --git a/src/Midnight.sol b/src/Midnight.sol index 2f6fc6e7..59c79ecf 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -72,10 +72,10 @@ import {IMidnight, Market, Offer, CollateralParams, MarketState, Position} from /// <=> repaidUnits <= (debt-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 Nothing prevents borrowers from opening small positions / liquidators from leaving small positions that might /// not be profitable to liquidate because of gas cost. The RCF deactivation at rcfThreshold just prevents the systemic /// aspect. @@ -684,10 +684,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 09e57f6c..b1de47c3 100644 --- a/test/LiquidationTest.sol +++ b/test/LiquidationTest.sol @@ -548,11 +548,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), ""); @@ -596,32 +600,32 @@ contract LiquidationTest is BaseTest { assertEq(midnight.withdrawable(id), 2 * repaid, "withdrawable after second liquidation"); } - /// @dev When rcfThreshold > remaining debt after max repayment, full liquidation is allowed pre-maturity. + /// @dev When rcfThreshold >= remaining payable 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.debt(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, @@ -630,20 +634,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), ""); }