[Certora] settlement fee spread assumption

certora/confs/SettlementFeeSpread.conf

@@ -13,6 +13,7 @@
   "loop_iter": 2,
   "rule_sanity": "basic",
   "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/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

@@ -19,8 +19,6 @@ 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.
 }
 
 function summaryToId(Midnight.Market market) returns (bytes32) {
@@ -49,8 +47,10 @@ 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).
 rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) {
     uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0;
-
     bytes32 id = summaryToId(offer.market);
+
+    // take calls touchMarket see rule takeCallsTouchMarket.
+    // Thus calling settlementFee (in particular checking if the market is touched) doesn't prune meaningful take paths.
     uint256 fee = settlementFee(id, timeToMaturity);
 
     uint256 buyerAssets;

certora/specs/TouchMarketIsCalled.spec

@@ -0,0 +1,95 @@
+// 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 settlementFee(bytes32, uint256) internal returns (uint256) => NONDET;
+    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 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);
+}