[Certora] SettlementFeeSpread: Fix flakiness by replacing non-linear reasoning by axioms

certora/specs/MulDiv.spec

@@ -86,6 +86,18 @@ rule mulDivAddDownUp(uint256 a1, uint256 a2, uint256 b, uint256 d) {
     assert mulDivDown(a1, b, d) + mulDivUp(a2, b, d) >= mulDivDown(a1plusa2, b, d);
 }
 
+// Super-additivity lower bound for mulDivUp with one term rounded down: ceil(a1*b/d) + floor(a2*b/d) <= ceil((a1+a2)*b/d).
+rule mulDivAddUpDown(uint256 a1, uint256 a2, uint256 b, uint256 d) {
+    uint256 a1plusa2 = require_uint256(a1 + a2);
+    assert mulDivUp(a1, b, d) + mulDivDown(a2, b, d) <= mulDivUp(a1plusa2, b, d);
+}
+
+// The first two arguments can be swapped.
+rule mulDivCommutative(uint256 a, uint256 b, uint256 d) {
+    assert mulDivDown(a, b, d) == mulDivDown(b, a, d);
+    assert mulDivUp(a, b, d) == mulDivUp(b, a, d);
+}
+
 // Rounding down the first scaling step cannot increase the result of a second scaling rounded up.
 rule mulDivDownUpComposition(uint256 a, uint256 b, uint256 c, uint256 d) {
     uint256 bc = require_uint256(b * c);
@@ -210,6 +222,17 @@ rule mathMulDivAddDownUp(mathint a1, mathint a2, mathint b, mathint d) {
     assert a1 >= 0 && a2 >= 0 => mathMulDivDown(a1, b, d) + mathMulDivUp(a2, b, d) >= mathMulDivDown(a1 + a2, b, d);
 }
 
+// Super-additivity lower bound for mathMulDivUp with one term rounded down: ceil(a1*b/d) + floor(a2*b/d) <= ceil((a1+a2)*b/d).
+rule mathMulDivAddUpDown(mathint a1, mathint a2, mathint b, mathint d) {
+    assert a1 >= 0 && a2 >= 0 && b >= 0 && d > 0 => mathMulDivUp(a1, b, d) + mathMulDivDown(a2, b, d) <= mathMulDivUp(a1 + a2, b, d);
+}
+
+// The first two arguments can be swapped.
+rule mathMulDivCommutative(mathint a, mathint b, mathint d) {
+    assert mathMulDivDown(a, b, d) == mathMulDivDown(b, a, d);
+    assert mathMulDivUp(a, b, d) == mathMulDivUp(b, a, d);
+}
+
 rule mathMulDivDownUpComposition(mathint a, mathint b, mathint c, mathint d) {
     assert a >= 0 && b >= 0 && c >= 0 && d > 0 => mathMulDivUp(mathMulDivDown(a, b, d), c, d) <= mathMulDivUp(a, b * c, d * d);
 }

certora/specs/MulDivAxioms.spec

@@ -58,6 +58,14 @@ definition axiomMathMulDivAddUpUpTight(mathint a1, mathint a2, mathint b, mathin
 
 definition axiomMathMulDivAddDownUp(mathint a1, mathint a2, mathint b, mathint d) returns bool = a1 >= 0 && a2 >= 0 => mathMulDivDown(a1, b, d) + mathMulDivUp(a2, b, d) >= mathMulDivDown(a1 + a2, b, d);
 
+// Super-additivity lower bound for mathMulDivUp with one term rounded down: ceil(a1*b/d) + floor(a2*b/d) <= ceil((a1+a2)*b/d).
+definition axiomMathMulDivAddUpDown(mathint a1, mathint a2, mathint b, mathint d) returns bool = a1 >= 0 && a2 >= 0 && b >= 0 && d > 0 => mathMulDivUp(a1, b, d) + mathMulDivDown(a2, b, d) <= mathMulDivUp(a1 + a2, b, d);
+
+// The first two arguments can be swapped.
+definition axiomMathMulDivDownCommutative(mathint a, mathint b, mathint d) returns bool = mathMulDivDown(a, b, d) == mathMulDivDown(b, a, d);
+
+definition axiomMathMulDivUpCommutative(mathint a, mathint b, mathint d) returns bool = mathMulDivUp(a, b, d) == mathMulDivUp(b, a, d);
+
 definition axiomMathMulDivDownUpComposition(mathint a, mathint b, mathint c, mathint d) returns bool = a >= 0 && b >= 0 && c >= 0 && d > 0 => mathMulDivUp(mathMulDivDown(a, b, d), c, d) <= mathMulDivUp(a, b * c, d * d);
 
 definition axiomMathMulDivInverseDownUp(mathint a, mathint b, mathint d) returns bool = b > 0 && d > 0 => a <= mathMulDivDown(mathMulDivUp(a, b, d), d, b);

certora/specs/SettlementFeeSpread.spec

@@ -1,6 +1,8 @@
 // SPDX-License-Identifier: MIT
 // Copyright (c) 2026 Morpho Association
 
+import "MulDivAxioms.spec";
+
 using SettlementFeeUtils as SettlementFeeUtils;
 
 methods {
@@ -23,6 +25,11 @@ methods {
     // Over-approximate view functions for prover performance.
     function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET;
 
+    // mulDiv is a deterministic ghost; the rules below assume only the MulDiv.spec facts they need, via MulDivAxioms.spec.
+    // A nondeterministic overflow flag overapproximates reverts.
+    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);
+
     // Dispatch the call to Midnight's getter, because the prover doesn't see that it only calls Midnight.
     function _.defaultSettlementFeeCbp(address, uint256) external => DISPATCHER(true);
 }
@@ -39,12 +46,51 @@ persistent ghost summaryTickToPrice(uint256) returns uint256;
 
 definition WAD() returns uint256 = 10 ^ 18;
 
+function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 {
+    bool overflow;
+    if (overflow || d == 0) {
+        revert();
+    }
+    return require_uint256(ghostMulDivDown(a, b, d));
+}
+
+function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 {
+    bool overflow;
+    if (overflow || d == 0) {
+        revert();
+    }
+    return require_uint256(ghostMulDivUp(a, b, d));
+}
+
+// Facts from MulDiv.spec relating the assets computed by take (units times the buyer or seller price) to units times the fee.
+// Commutativity turns the additivity axioms, stated in the first argument, into additivity in the price.
+function requireSpreadAxioms(mathint units, mathint offerPrice, mathint fee) {
+    require axiomMathMulDivDownCommutative(units, offerPrice, WAD()), "axiom";
+    require axiomMathMulDivDownCommutative(units, offerPrice - fee, WAD()), "axiom";
+    require axiomMathMulDivUpCommutative(units, offerPrice, WAD()), "axiom";
+    require axiomMathMulDivUpCommutative(units, offerPrice + fee, WAD()), "axiom";
+
+    // Buy offer: the buyer pays floor(units * offerPrice / WAD) and the seller receives floor(units * (offerPrice - fee) / WAD).
+    require axiomMathMulDivAddDownDown(offerPrice - fee, fee, units, WAD()), "axiom";
+    require axiomMathMulDivAddDownUp(offerPrice - fee, fee, units, WAD()), "axiom";
+
+    // Sell offer: the buyer pays ceil(units * (offerPrice + fee) / WAD) and the seller receives ceil(units * offerPrice / WAD).
+    require axiomMathMulDivAddUpDown(offerPrice, fee, units, WAD()), "axiom";
+    require axiomMathMulDivAddUpUp(offerPrice, fee, units, WAD()), "axiom";
+
+    // Bound floor and ceil of fee * units / WAD by the exact quotient.
+    require axiomMathMulDivDownTightBound(fee, units, WAD()), "axiom";
+    require axiomMathMulDivUpUpperBound(fee, units, WAD()), "axiom";
+}
+
 // Rounding always favors the maker:
 //   1. buyer-maker pays at most floor(units * offerPrice / WAD).
 //   2. seller-maker receives at least ceil(units * offerPrice / WAD).
 // Note also that this rule ensures that the settlement fee is applied on the taker price, not the maker price.
 rule makerFavorableRounding(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) {
     uint256 offerPrice = summaryTickToPrice(offer.tick);
+    require axiomMathMulDivDownRoundsDown(units, offerPrice, WAD()), "axiom";
+    require axiomMathMulDivUpRoundsUp(units, offerPrice, WAD()), "axiom";
 
     uint256 buyerAssets;
     uint256 sellerAssets;
@@ -64,6 +110,7 @@ rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData,
 
     uint256 fee = settlementFee@withrevert(id, timeToMaturity);
     assert !lastReverted;
+    requireSpreadAxioms(units, summaryTickToPrice(offer.tick), fee);
 
     uint256 buyerAssets;
     uint256 sellerAssets;
@@ -83,6 +130,7 @@ rule settlementFeeSpreadBoundsNotCreatedMarket(env e, Midnight.Offer offer, byte
     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);
+    requireSpreadAxioms(units, summaryTickToPrice(offer.tick), fee);
 
     uint256 buyerAssets;
     uint256 sellerAssets;