modular lif

certora/README.md

@@ -13,11 +13,11 @@ Global invariants on positions, markets and accounting.
   Total units always equal the sum of debt plus withdrawable, a user never holds both credit and debt, and a position's pending continuous fee never exceeds its credit.
   Continuous fees stay below `MAX_CONTINUOUS_FEE` at both the default and the market level, and loss factors only ever increase, with each user's bounded by its market's.
   Rules also pin down `take`/`liquidate` input-output consistency: zero inputs give zero outputs, and `take` raises the claimable settlement fee by exactly the buyer/seller spread.
-  It also shows that neither credit nor debt can grow once a market's loss factor is maxed out.
+  It also shows that neither credit nor debt can grow once a market's loss factor is maxed out, and that every enabled `LLTV` tier and liquidation cursor is at most `WAD`.
 - [`BalanceEffects.spec`](specs/BalanceEffects.spec) pins down the exact credit, debt and collateral effect of every entry point.
 - [`WithdrawableMonotonicity.spec`](specs/WithdrawableMonotonicity.spec) checks how withdrawable assets move: up on `repay` and `liquidate`, down by exactly the amount on `withdraw` and `claimContinuousFee`, and unchanged otherwise.
   It checks the claimable settlement fee the same way: up on `take`, down on `claimSettlementFee`, and unchanged otherwise.
-- [`CreatedMarkets.spec`](specs/CreatedMarkets.spec) checks the well-formedness invariants of a created market: a non-empty collateral list, strictly sorted by token, with no zero token, and every entry with an `LLTV <= WAD` from an allowed tier and an allowed `maxLif`.
+- [`CreatedMarkets.spec`](specs/CreatedMarkets.spec) checks the well-formedness invariants of a created market: a non-empty collateral list, strictly sorted by token, with no zero token, and every entry with an enabled `LLTV` tier, an enabled liquidation cursor, and a `maxLif <= 2 * WAD`.
   Rules add that a market is created by the first interaction of each entry point, can only be created that way, and can never be deleted.
 - [`NotCreatedMarket.spec`](specs/NotCreatedMarket.spec) checks the converse: every state field of a market that was never created is empty.
 - [`LossFactor.spec`](specs/LossFactor.spec) checks that only `liquidate` changes a market's loss factor, and only when bad debt is realized (total units decrease), and that `updatePosition` syncs the user's `lastLossFactor` to the market's.

certora/confs/CreatedMarkets.conf

@@ -24,8 +24,9 @@
     "-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}]"
   ],
   "split_rules": [
-    "createdMarketsHaveAllowedMaxLif",
-    "createdMarketsHaveAllowedLltv"
+    "createdMarketsHaveEnabledLltv",
+    "createdMarketsHaveEnabledLiquidationCursor",
+    "createdMarketsHaveMaxLifAtMostTwoWad"
   ],
   "msg": "CreatedMarkets"
 }

certora/confs/TakeAmountsLibInvertibility.conf

@@ -13,9 +13,10 @@
   "optimistic_loop": true,
   "loop_iter": 2,
   "prover_args": [
-    "-depth 5",
-    "-mediumTimeout 60",
-    "-timeout 3600"
+    "-destructiveOptimizations twostage",
+    "-splitParallel true",
+    "-splitParallelInitialDepth 4",
+    "-splitParallelTimelimit 7200"
   ],
   "msg": "Midnight TakeAmountsLib Invertibility"
 }

certora/helpers/Utils.sol

@@ -6,8 +6,6 @@ import {Offer, Market} from "../../src/interfaces/IMidnight.sol";
 import {UtilsLib} from "../../src/libraries/UtilsLib.sol";
 import {
     CALLBACK_SUCCESS,
-    LIQUIDATION_CURSOR_LOW,
-    LIQUIDATION_CURSOR_HIGH,
     MAX_COLLATERALS_PER_BORROWER,
     maxSettlementFee as _maxSettlementFee,
     maxLif as _maxLif
@@ -51,16 +49,8 @@ contract Utils {
         return _maxSettlementFee(index);
     }
 
-    function maxLif(uint256 lltv, uint256 cursor) external pure returns (uint256) {
-        return _maxLif(lltv, cursor);
-    }
-
-    function liquidationCursorLow() external pure returns (uint256) {
-        return LIQUIDATION_CURSOR_LOW;
-    }
-
-    function liquidationCursorHigh() external pure returns (uint256) {
-        return LIQUIDATION_CURSOR_HIGH;
+    function maxLif(uint256 lltv, uint256 liquidationCursor) external pure returns (uint256) {
+        return _maxLif(lltv, liquidationCursor);
     }
 
     function maxCollateralsPerBorrower() external pure returns (uint256) {

certora/specs/CreatedMarkets.spec

@@ -6,11 +6,9 @@ methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
     function tickSpacing(bytes32) external returns (uint8) envfree;
-    function isLltvAllowed(uint256) external returns (bool) envfree;
+    function isLltvEnabled(uint256) external returns (bool) envfree;
     function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree;
     function Utils.maxLif(uint256, uint256) external returns (uint256) envfree;
-    function Utils.liquidationCursorLow() external returns (uint256) envfree;
-    function Utils.liquidationCursorHigh() external returns (uint256) envfree;
 
     // Over-approximate view functions for prover performance.
     function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET;
@@ -49,8 +47,6 @@ function marketIsCreated(Midnight.Market market) returns (bool) {
     return tickSpacing(summaryToId(market)) > 0;
 }
 
-definition isMaxLifAllowed(uint256 lltv, uint256 maxLif) returns bool = maxLif == Utils.maxLif(lltv, Utils.liquidationCursorLow()) || maxLif == Utils.maxLif(lltv, Utils.liquidationCursorHigh());
-
 /// RULES ///
 
 // Show that a created market has at least one collateral.
@@ -65,26 +61,15 @@ strong invariant createdMarketsHaveSortedCollaterals(Midnight.Market market, uin
 strong invariant createdMarketsHaveNonZeroCollaterals(Midnight.Market market, uint256 i)
     marketIsCreated(market) => i < market.collateralParams.length => market.collateralParams[i].token != 0;
 
-// Show that an allowed LLTV tier is at most WAD, which holds because tiers can only be added with lltv <= WAD.
-strong invariant allowedLltvIsLessThanOrEqualToOne(uint256 lltv)
-    isLltvAllowed(lltv) => lltv <= WAD();
-
-// Show that a created market has lltv <= WAD.
-strong invariant createdMarketsHaveLltvLessThanOrEqualToOne(Midnight.Market market, uint256 i)
-    marketIsCreated(market) => i < market.collateralParams.length => market.collateralParams[i].lltv <= WAD()
-    {
-        preserved {
-            requireInvariant allowedLltvIsLessThanOrEqualToOne(market.collateralParams[i].lltv);
-        }
-    }
-
-// Show that a created market only has allowed LLTV tiers.
-strong invariant createdMarketsHaveAllowedLltv(Midnight.Market market, uint256 i)
-    marketIsCreated(market) => i < market.collateralParams.length => isLltvAllowed(market.collateralParams[i].lltv);
-
-// Show that a created market has maxLif allowed.
-strong invariant createdMarketsHaveAllowedMaxLif(Midnight.Market market, uint256 i)
-    marketIsCreated(market) => i < market.collateralParams.length => isMaxLifAllowed(market.collateralParams[i].lltv, market.collateralParams[i].maxLif);
+// Show that a created market only has enabled LLTV tiers.
+strong invariant createdMarketsHaveEnabledLltv(Midnight.Market market, uint256 i)
+    marketIsCreated(market) => i < market.collateralParams.length => isLltvEnabled(market.collateralParams[i].lltv);
+
+strong invariant createdMarketsHaveEnabledLiquidationCursor(Midnight.Market market, uint256 i)
+    marketIsCreated(market) => i < market.collateralParams.length => currentContract.isLiquidationCursorEnabled[market.collateralParams[i].liquidationCursor];
+
+strong invariant createdMarketsHaveMaxLifAtMostTwoWad(Midnight.Market market, uint256 i)
+    marketIsCreated(market) => i < market.collateralParams.length => Utils.maxLif(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD();
 
 // Show that a created market cannot be deleted.
 rule marketCannotBeDeleted(env e, method f, calldataarg args, Midnight.Market market) {

certora/specs/ExactMath.spec

@@ -9,28 +9,14 @@ methods {
 
 definition WAD() returns uint256 = 10 ^ 18;
 
-rule lifTimesLltvIsLessThanOrEqualToOne(uint256 lltv, uint256 cursor) {
-    require lltv <= WAD(), "see rule createdMarketsHaveLltvLessThanOrEqualToOne";
-    require cursor < WAD(), "see the definition of LIQUIDATION_CURSOR_LOW and LIQUIDATION_CURSOR_HIGH";
-    assert lltv * maxLif(lltv, cursor) <= WAD() * WAD();
+rule lifTimesLltvIsLessThanOrEqualToOne(uint256 lltv, uint256 liquidationCursor) {
+    require lltv <= WAD(), "see rule createdMarketsHaveEnabledLltv";
+    require liquidationCursor <= WAD(), "enabled liquidationCursors are at most WAD, see addLiquidationCursor";
+    assert lltv * maxLif(lltv, liquidationCursor) <= WAD() * WAD();
 }
 
-/// Check that maxLif >= WAD
-rule maxLifIsAtLeastWad(uint256 lltv, uint256 cursor) {
-    assert maxLif(lltv, cursor) >= WAD();
-}
-
-/// Check that maxLif <= 2*WAD for valid cursor values
-rule maxLifIsAtMostTwoWad(uint256 lltv, uint256 cursor) {
-    require lltv <= WAD(), "see rule createdMarketsHaveLltvLessThanOrEqualToOne";
-    require cursor <= WAD() / 2, "see LIQUIDATION_CURSOR_HIGH in ConstantsLib";
-    assert maxLif(lltv, cursor) <= 2 * WAD();
-}
-
-/// Check that maxLif * lltv <= WAD * (WAD - 1) for valid cursor values
-rule lifTimesLltvStrictBound(uint256 lltv, uint256 cursor) {
-    require cursor < WAD(), "see the definition of LIQUIDATION_CURSOR_LOW and LIQUIDATION_CURSOR_HIGH";
-    assert lltv < WAD() => lltv * maxLif(lltv, cursor) <= WAD() * (WAD() - 1);
+rule maxLifIsAtLeastWad(uint256 lltv, uint256 liquidationCursor) {
+    assert maxLif(lltv, liquidationCursor) >= WAD();
 }
 
 /// Check that mulDivUp(a, lltv, WAD()) <= mulDivUp(a, WAD(), lif)

certora/specs/Healthiness.spec

@@ -23,6 +23,10 @@ methods {
     // The axioms are proved in MulDiv.spec.
     function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d);
     function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d);
+
+    // maxLif is recomputed on the fly from (lltv, liquidationCursor) during liquidate. Summarize it by a deterministic ghost; its
+    // lltv * maxLif <= WAD * WAD bound is assumed below (see lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec).
+    function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor);
     function _.havocAll() external => HAVOC_ALL;
 
     function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET;
@@ -110,7 +114,9 @@ persistent ghost mapping(uint256 => address) globalMarketCollateralToken;
 
 persistent ghost mapping(uint256 => uint256) globalMarketCollateralLLTV;
 
-persistent ghost mapping(uint256 => uint256) globalMarketCollateralMaxLif;
+persistent ghost mapping(uint256 => uint256) globalMarketCollateralLiquidationCursor;
+
+persistent ghost maxLifGhost(uint256, uint256) returns uint256;
 
 persistent ghost uint256 globalMarketMaturity;
 
@@ -126,7 +132,7 @@ persistent ghost address globalBorrower;
 
 // helper function to check if one of the collateralParams of a market matches the global variables.
 // It checks for the length and also returns true if the index is out of bounds. This allows us to require this for every index.
-definition collateralMatches(Midnight.Market market, uint256 index) returns bool = (index < globalMarketCollateralLength => market.collateralParams[index].oracle == globalMarketCollateralOracle[index] && market.collateralParams[index].token == globalMarketCollateralToken[index] && market.collateralParams[index].lltv == globalMarketCollateralLLTV[index] && market.collateralParams[index].maxLif == globalMarketCollateralMaxLif[index]);
+definition collateralMatches(Midnight.Market market, uint256 index) returns bool = (index < globalMarketCollateralLength => market.collateralParams[index].oracle == globalMarketCollateralOracle[index] && market.collateralParams[index].token == globalMarketCollateralToken[index] && market.collateralParams[index].lltv == globalMarketCollateralLLTV[index] && market.collateralParams[index].liquidationCursor == globalMarketCollateralLiquidationCursor[index]);
 
 function equalsGlobalMarket(Midnight.Market market) returns (bool) {
     return market.loanToken == globalMarketLoanToken && market.collateralParams.length == globalMarketCollateralLength && collateralMatches(market, 0) && collateralMatches(market, 1) && collateralMatches(market, 2) && market.maturity == globalMarketMaturity && market.rcfThreshold == globalMarketRcfThreshold && market.enterGate == globalMarketEnterGate && market.liquidatorGate == globalMarketLiquidatorGate;
@@ -241,7 +247,7 @@ rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 se
     // This variable is set to false whenever isHealthy() is violated before a callback.  Initially we set it to true to indicate no violations detected.
     healthyOrLockedBeforeCallbacks = true;
 
-    require globalMarketCollateralLLTV[collateralIndex] * globalMarketCollateralMaxLif[collateralIndex] <= WAD() * WAD(), "Proved in lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec: maxLif is at most 1/lltv";
+    require globalMarketCollateralLLTV[collateralIndex] * maxLifGhost(globalMarketCollateralLLTV[collateralIndex], globalMarketCollateralLiquidationCursor[collateralIndex]) <= WAD() * WAD(), "Proved in lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec: maxLif is at most 1/lltv";
 
     require globalMarketCollateralLength <= 2, "too many collateralParams for the spec to handle";
 
@@ -266,9 +272,9 @@ rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 se
     require forall mathint a. forall mathint b. forall mathint d1. forall mathint d2. axiomUpMonotoneD(a, b, d1, d2), "axiom";
     require axiomDownZero(price, ORACLE_PRICE_SCALE()), "axiom";
     require axiomDownZero(globalMarketCollateralLLTV[collateralIndex], WAD()), "axiom";
-    require axiomInverseUpDown(repaidUnitsOut, globalMarketCollateralMaxLif[collateralIndex], WAD()), "axiom";
-    require axiomInverseUpDown(ghostMulDivDown(repaidUnitsOut, globalMarketCollateralMaxLif[collateralIndex], WAD()), ORACLE_PRICE_SCALE(), price), "axiom";
-    require axiomLifLLTV(ghostMulDivUp(seizedAssetsOut, price, ORACLE_PRICE_SCALE()), globalMarketCollateralMaxLif[collateralIndex], globalMarketCollateralLLTV[collateralIndex]), "axiom";
+    require axiomInverseUpDown(repaidUnitsOut, maxLifGhost(globalMarketCollateralLLTV[collateralIndex], globalMarketCollateralLiquidationCursor[collateralIndex]), WAD()), "axiom";
+    require axiomInverseUpDown(ghostMulDivDown(repaidUnitsOut, maxLifGhost(globalMarketCollateralLLTV[collateralIndex], globalMarketCollateralLiquidationCursor[collateralIndex]), WAD()), ORACLE_PRICE_SCALE(), price), "axiom";
+    require axiomLifLLTV(ghostMulDivUp(seizedAssetsOut, price, ORACLE_PRICE_SCALE()), maxLifGhost(globalMarketCollateralLLTV[collateralIndex], globalMarketCollateralLiquidationCursor[collateralIndex]), globalMarketCollateralLLTV[collateralIndex]), "axiom";
     require axiomAddDownUp(collateralAfter, seizedAssetsOut, price, ORACLE_PRICE_SCALE()), "axiom";
     require axiomAddDownUp(ghostMulDivDown(collateralAfter, price, ORACLE_PRICE_SCALE()), ghostMulDivUp(seizedAssetsOut, price, ORACLE_PRICE_SCALE()), globalMarketCollateralLLTV[collateralIndex], WAD()), "axiom";
 

certora/specs/LiquidationBoundedByLIF.spec

@@ -9,6 +9,7 @@ methods {
 
     function collateral(bytes32 id, address user, uint256 index) external returns (uint128) envfree;
     function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree;
+    function Utils.maxLif(uint256, uint256) external returns (uint256) envfree;
 
     // Summary to capture the oracle price so the spec can reference it in assertions.
     function _.price() external => summaryPrice(calledContract) expect(uint256);
@@ -76,7 +77,7 @@ strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint25
 /// Liquidation profit is bounded by maxLif (repaidUnits input).
 /// Unlike the seizedAssets rule, no requireInvariant is needed here: if collateralIndex is not in the bitmap because mulDivDown(..., 0) reverts.
 rule liquidationProfitBoundedInputRepaidUnits(env e, Midnight.Market market, uint256 collateralIndex, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) {
-    mathint maxLif = market.collateralParams[collateralIndex].maxLif;
+    mathint maxLif = Utils.maxLif(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor);
     require data.length == 0, "no callback for prover performance";
     require maxLif >= WAD(), "maxLif must be at least 1x for profit boundedness (see touchMarket validation and ExactMath.spec)";
 
@@ -91,7 +92,7 @@ rule liquidationProfitBoundedInputRepaidUnits(env e, Midnight.Market market, uin
 
 /// Liquidation profit is bounded by maxLif (seizedAssets input)
 rule liquidationProfitBoundedSeizedAssets(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) {
-    mathint maxLif = market.collateralParams[collateralIndex].maxLif;
+    mathint maxLif = Utils.maxLif(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor);
     require data.length == 0, "no callback for prover performance";
     require maxLif >= WAD(), "maxLif must be at least 1x for profit boundedness (see touchMarket validation and ExactMath.spec)";
 

certora/specs/LiquidationProfitability.spec

@@ -6,6 +6,7 @@ methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
     function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree;
+    function Utils.maxLif(uint256, uint256) external returns (uint256) envfree;
 
     // Summary to capture the oracle price so the spec can reference it in assertions.
     function _.price() external => summaryPrice(calledContract) expect(uint256);
@@ -69,7 +70,7 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 {
 
 /// 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;
+    uint256 maxLif = Utils.maxLif(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor);
     require maxLif >= WAD(), "see the rule maxLifIsAtLeastWad";
 
     bool maxLifReached = !postMaturityMode || e.block.timestamp >= require_uint256(market.maturity + TIME_TO_MAX_LIF());
@@ -89,7 +90,7 @@ rule liquidationLifRepaidUnits(env e, Midnight.Market market, uint256 collateral
 
 /// 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;
+    uint256 maxLif = Utils.maxLif(market.collateralParams[collateralIndex].lltv, market.collateralParams[collateralIndex].liquidationCursor);
     require maxLif >= WAD(), "see the rule maxLifIsAtLeastWad";
 
     bool maxLifReached = !postMaturityMode || e.block.timestamp >= require_uint256(market.maturity + TIME_TO_MAX_LIF());