[Certora] settlement fee spread assumption

certora/confs/SettlementFeeSpread.conf

@@ -1,18 +1,23 @@
 {
   "files": [
     "certora/helpers/Utils.sol",
+    "certora/helpers/SettlementFeeUtils.sol",
     "src/Midnight.sol"
   ],
+  "split_rules": [
+    "*"
+  ],
   "verify": "Midnight:certora/specs/SettlementFeeSpread.spec",
   "solc": "solc-0.8.34",
   "solc_evm_version": "osaka",
+  "solc_via_ir": true,
   "optimistic_hashing": true,
   "hashing_length_bound": 2048,
-  "solc_via_ir": true,
   "optimistic_loop": true,
   "loop_iter": 2,
-  "rule_sanity": "basic",
+  "multi_assert_check": true,
   "prover_args": [
+    "-havocAllByDefault true",
     "-depth 5",
     "-mediumTimeout 60",
     "-timeout 3600"

certora/confs/TouchMarketIsCalled.conf

@@ -0,0 +1,21 @@
+{
+  "files": [
+    "certora/helpers/Utils.sol",
+    "src/Midnight.sol"
+  ],
+  "verify": "Midnight:certora/specs/TouchMarketIsCalled.spec",
+  "solc": "solc-0.8.34",
+  "solc_via_ir": true,
+  "solc_evm_version": "osaka",
+  "optimistic_loop": true,
+  "loop_iter": 2,
+  "optimistic_hashing": true,
+  "hashing_length_bound": 1024,
+  "rule_sanity": "basic",
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 60",
+    "-timeout 3600"
+  ],
+  "msg": "TouchMarket Is Called"
+}

certora/helpers/SettlementFeeUtils.sol

@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+// Copyright (c) 2025 Morpho Association
+pragma solidity ^0.8.0;
+
+import {IMidnight} from "../../src/interfaces/IMidnight.sol";
+import {CBP} from "../../src/libraries/ConstantsLib.sol";
+
+contract SettlementFeeUtils {
+    /// @dev Mirrors Midnight.settlementFee but reads the loan token's default settlement fee cbps (in Solidity) instead
+    /// of the market state. This is the fee a freshly created market applies, since touchMarket copies these defaults
+    /// into the market state.
+    function defaultSettlementFee(IMidnight midnight, address loanToken, uint256 timeToMaturity)
+        external
+        view
+        returns (uint256)
+    {
+        uint16[7] memory settlementFeeCbp;
+        settlementFeeCbp[0] = midnight.defaultSettlementFeeCbp(loanToken, 0);
+        settlementFeeCbp[1] = midnight.defaultSettlementFeeCbp(loanToken, 1);
+        settlementFeeCbp[2] = midnight.defaultSettlementFeeCbp(loanToken, 2);
+        settlementFeeCbp[3] = midnight.defaultSettlementFeeCbp(loanToken, 3);
+        settlementFeeCbp[4] = midnight.defaultSettlementFeeCbp(loanToken, 4);
+        settlementFeeCbp[5] = midnight.defaultSettlementFeeCbp(loanToken, 5);
+        settlementFeeCbp[6] = midnight.defaultSettlementFeeCbp(loanToken, 6);
+
+        if (timeToMaturity >= 360 days) return settlementFeeCbp[6] * CBP;
+
+        // forgefmt: disable-start
+        (uint256 start, uint256 end, uint256 feeLower, uint256 feeUpper) =
+            timeToMaturity < 1 days   ? (  0 days,   1 days, settlementFeeCbp[0] * CBP, settlementFeeCbp[1] * CBP) :
+            timeToMaturity < 7 days   ? (  1 days,   7 days, settlementFeeCbp[1] * CBP, settlementFeeCbp[2] * CBP) :
+            timeToMaturity < 30 days  ? (  7 days,  30 days, settlementFeeCbp[2] * CBP, settlementFeeCbp[3] * CBP) :
+            timeToMaturity < 90 days  ? ( 30 days,  90 days, settlementFeeCbp[3] * CBP, settlementFeeCbp[4] * CBP) :
+            timeToMaturity < 180 days ? ( 90 days, 180 days, settlementFeeCbp[4] * CBP, settlementFeeCbp[5] * CBP) :
+                                        (180 days, 360 days, settlementFeeCbp[5] * CBP, settlementFeeCbp[6] * CBP);
+        // forgefmt: disable-end
+
+        return (feeLower * (end - timeToMaturity) + feeUpper * (timeToMaturity - start)) / (end - start);
+    }
+}

certora/specs/OnlyExplicitPayerCanLoseTokens.spec

@@ -10,8 +10,8 @@ methods {
 
     // Callbacks can modify the whole state arbitrarily, and can only modify the ghost variables to allow
     // themselves as payer. Callbacks are checked to only be called by their corresponding function,
-    // eg onLiquidate is only called by liquidate. onRatify and onSell cannot authorize a payer, so we
-    // model them with a plain HAVOC_ALL.
+    // eg onLiquidate is only called by liquidate. onSell cannot authorize a payer, so we model them
+    // with a plain HAVOC_ALL.
     function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => onCallBackSummary(calledContract, buyCallbackAllowed) expect(bytes32);
     function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => onCallBackSummary(calledContract, liquidateCallbackAllowed) expect(bytes32);
     function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => onCallBackSummary(calledContract, repayCallbackAllowed) expect(bytes32);

certora/specs/SettlementFeeSpread.spec

@@ -1,14 +1,16 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-using Utils as Utils;
+using SettlementFeeUtils as SettlementFeeUtils;
 
 methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
-    function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree;
     function settlementFee(bytes32, uint256) external returns (uint256) envfree;
+    function tickSpacing(bytes32) external returns (uint8) envfree;
+    function SettlementFeeUtils.defaultSettlementFee(address, address, uint256) external returns (uint256) envfree;
 
-    // Summary is required because abi.encodePacked doesn't ensure injectivity of the hash function in CVL, for an unknown reason.
+    // Summarize the id as a deterministic ghost over the market, removing the collateral params array.
+    // This is sound because the rules only use a single market.
     function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
 
     // Deterministic TickLib.tickToPrice summary to be able to reference the price in the rules.
@@ -20,11 +22,17 @@ methods {
     // Over-approximate view functions for prover performance.
     function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET;
 
-    // Assume no reentrancy, because we need to know that the settlement fee won't change in the onRatify callback. This allows to reference the settlement fee in the rule settlementFeeSpreadBounds.
+    // SettlementFeeUtils reads the defaults through the IMidnight interface; dispatch the call to Midnight's getter so
+    // it reads currentContract's storage instead of being havoc'd to an arbitrary value.
+    function _.defaultSettlementFeeCbp(address, uint256) external => DISPATCHER(true);
+
+    // function _updatePosition(Midnight.Market memory, bytes32, address) internal returns (uint128, uint128, uint128) => NONDET;
 }
 
+persistent ghost ghostToId(uint256, address, address, uint256, uint256, address, address) returns bytes32;
+
 function summaryToId(Midnight.Market market) returns (bytes32) {
-    return Utils.hashMarket(market);
+    return ghostToId(market.chainId, market.midnight, market.loanToken, market.maturity, market.rcfThreshold, market.enterGate, market.liquidatorGate);
 }
 
 persistent ghost summaryTickToPrice(uint256) returns uint256;
@@ -47,11 +55,32 @@ rule makerFavorableRounding(env e, Midnight.Offer offer, bytes ratifierData, uin
 }
 
 // The spread between what the buyer pays and what the seller receives is at least floor(units * fee / WAD) and at most ceil(units * fee / WAD).
+// Assume that the market is created.
 rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) {
+    bytes32 id = summaryToId(offer.market);
+    require tickSpacing(id) > 0;
+
     uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0;
 
+    uint256 fee = settlementFee@withrevert(id, timeToMaturity);
+    assert !lastReverted;
+
+    uint256 buyerAssets;
+    uint256 sellerAssets;
+    buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData);
+
+    assert buyerAssets - sellerAssets >= (units * fee) / WAD();
+    assert buyerAssets - sellerAssets <= (units * fee + WAD() - 1) / WAD();
+}
+
+// Twin rule of settlementFeeSpreadBounds for a market that is not created yet at the start.
+rule settlementFeeSpreadBoundsNotCreatedMarket(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) {
     bytes32 id = summaryToId(offer.market);
-    uint256 fee = settlementFee(id, timeToMaturity);
+    require tickSpacing(id) == 0;
+
+    uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0;
+
+    uint256 fee = SettlementFeeUtils.defaultSettlementFee(currentContract, offer.market.loanToken, timeToMaturity);
 
     uint256 buyerAssets;
     uint256 sellerAssets;

certora/specs/TouchMarketIsCalled.spec

@@ -0,0 +1,111 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using Utils as Utils;
+
+methods {
+    function multicall(bytes[]) external => HAVOC_ALL DELETE;
+
+    function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree;
+
+    // Record every call to touchMarket and the market it is called with.
+    function touchMarket(Midnight.Market memory market) internal returns (bytes32) => recordTouchMarket(market);
+
+    // Over-approximate the heavy functions for prover performance.
+    // This is safe here: the worst they could do is fail to record a touchMarket call, which would make a rule fail rather than pass unsoundly.
+    function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET;
+    function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;
+    function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET;
+    function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET;
+    function UtilsLib.mulDivUp(uint256, uint256, uint256) internal returns (uint256) => NONDET;
+    function UtilsLib.mulDivDown(uint256, uint256, uint256) internal returns (uint256) => NONDET;
+    function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
+    function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET;
+}
+
+/// HELPERS ///
+
+persistent ghost bool touchMarketCalled;
+
+persistent ghost bytes32 touchedMarketId;
+
+function recordTouchMarket(Midnight.Market market) returns bytes32 {
+    touchMarketCalled = true;
+    touchedMarketId = Utils.hashMarket(market);
+    return Utils.hashMarket(market);
+}
+
+/// RULES ///
+
+// Each rule shows that a successful interaction calls touchMarket with its own market, which in turn implies that a reverting touchMarket forces the interaction to revert.
+
+rule claimContinuousFeeCallsTouchMarket(env e, Midnight.Market market, uint256 amount, address receiver) {
+    require !touchMarketCalled, "reset call tracking";
+
+    claimContinuousFee(e, market, amount, receiver);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(market);
+}
+
+rule takeCallsTouchMarket(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) {
+    require !touchMarketCalled, "reset call tracking";
+
+    take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(offer.market);
+}
+
+rule withdrawCallsTouchMarket(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver) {
+    require !touchMarketCalled, "reset call tracking";
+
+    withdraw(e, market, units, onBehalf, receiver);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(market);
+}
+
+rule repayCallsTouchMarket(env e, Midnight.Market market, uint256 units, address onBehalf, address callback, bytes data) {
+    require !touchMarketCalled, "reset call tracking";
+
+    repay(e, market, units, onBehalf, callback, data);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(market);
+}
+
+rule supplyCollateralCallsTouchMarket(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf) {
+    require !touchMarketCalled, "reset call tracking";
+
+    supplyCollateral(e, market, collateralIndex, assets, onBehalf);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(market);
+}
+
+rule withdrawCollateralCallsTouchMarket(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf, address receiver) {
+    require !touchMarketCalled, "reset call tracking";
+
+    withdrawCollateral(e, market, collateralIndex, assets, onBehalf, receiver);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(market);
+}
+
+rule liquidateCallsTouchMarket(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) {
+    require !touchMarketCalled, "reset call tracking";
+
+    liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(market);
+}
+
+rule updatePositionCallsTouchMarket(env e, Midnight.Market market, address user) {
+    require !touchMarketCalled, "reset call tracking";
+
+    updatePosition(e, market, user);
+
+    assert touchMarketCalled;
+    assert touchedMarketId == Utils.hashMarket(market);
+}