round up collat value in rcf check

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}]",

certora/confs/Reentrancy.conf

@@ -14,5 +14,6 @@
   "loop_iter": 5,
   "optimistic_hashing": true,
   "hashing_length_bound": 2048,
+  "smt_timeout": 7200,
   "msg": "Midnight Reentrancy"
 }

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()
                 );
             }

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), "");
     }