[Certora] Improve NoMultiplicationOverflow spec.

certora/specs/NoMultiplicationOverflow.spec

@@ -1,7 +1,17 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 // Copyright (c) 2026 Morpho Association
 
-// Proves that successful calls do not overflow in mulDivDown or mulDivUp, given the oracle price is bounded.
+// Proves that the only overflows in mulDivDown and mulDivUp that can cause a revert are
+// the ones that compute the value of a collateral against the oracle price.
+// These can only overflow if the collateral is priced at more than max_uint128 debt units,
+// which is documented in Midnight.sol.
+
+// Strictly speaking, other mulDivDown/mulDivUp may revert due to overflow, e.g.,
+// for withdraw a mulDiv can revert for very large values of units > 2^128.
+// However, this would result in a different revert, if the mulDiv is never called.
+// This spec checks for overflows at the end, showing that if there is no other reason the
+// call would have reverted the mulDiv didn't overflow.
+// Thus, the mulDiv did not singlehandedly cause the revert.
 
 using Utils as Utils;
 
@@ -10,9 +20,8 @@ methods {
 
     function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree;
 
-    // Oracle integration assumption: every (collateralAmount * oraclePrice) fits in uint256.
-    // Storage collateral is uint128, so boundedPrice enforces the product bound against max_uint128.
-    function _.price() external => boundedPrice(calledContract) expect(uint256);
+    // Deterministic summary for oracle price
+    function _.price() external => getOraclePrice(calledContract) expect(uint256);
 
     // Deterministic toId: links call-site markets to validated state from touchMarket.
     function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
@@ -34,6 +43,12 @@ persistent ghost bool mulOverflow;
 
 persistent ghost maxLifGhost(uint256, uint256) returns uint256;
 
+ghost oraclePriceGhost(address) returns uint256;
+
+ghost uint256 lastOraclePrice;
+
+ghost uint256 lastCollateralAmount;
+
 definition WAD() returns uint256 = 10 ^ 18;
 
 definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36;
@@ -48,10 +63,15 @@ function summaryToId(Midnight.Market market) returns (bytes32) {
     return Utils.hashMarket(market);
 }
 
-// Bound every storage collateral (uint128) * oracle price product.
-function boundedPrice(address oracle) returns uint256 {
-    uint256 price;
-    require to_mathint(price) * max_uint128 + ORACLE_PRICE_SCALE() - 1 <= max_uint256, "same as assuming that collateral * price <= uint256 with mulDivUp rounding headroom";
+// hook to remember the last queried collateral amount.
+hook Sload uint128 value position[KEY bytes32 id][KEY address user].collateral[INDEX uint256 collateralIndex] {
+    lastCollateralAmount = value;
+}
+
+// internal function to remember the last queried oracle price.
+function getOraclePrice(address oracle) returns uint256 {
+    uint256 price = oraclePriceGhost(oracle);
+    lastOraclePrice = price;
     return price;
 }
 
@@ -63,12 +83,24 @@ function boundedTickPrice() returns uint256 {
 }
 
 function mulDivDownSummary(uint256 x, uint256 y, uint256 d) returns uint256 {
-    mathint product = to_mathint(x) * y;
+    uint256 result;
+    mathint product = x * y;
     if (product > max_uint256) {
-        mulOverflow = true;
+        // overflow in mulDivDown
+        if (x == lastCollateralAmount && y == lastOraclePrice && d == ORACLE_PRICE_SCALE()) {
+            // Explicitly allow to revert when some user's collateral is priced at too many debt units
+            // This assert double-checks that a revert only happens in this case.
+            // Gap: here we assume that collateral and oracle price match. A bug where the wrong collateral index is used for the oracle is not detected by this spec.
+            assert lastCollateralAmount * lastOraclePrice / ORACLE_PRICE_SCALE() > max_uint128, "collateral worth more than max_uint128 debt units";
+            revert();
+        } else {
+            // other overflows are checked at the end that they didn't cause a revert.
+            mulOverflow = true;
+            return result;
+        }
     }
 
-    uint256 result;
+    // These requires are proved for the no-overflow case.
     require d > 0 => result * d <= product, "proven in MulDiv.spec (mulDivDownRoundsDown)";
     require d > 0 => y <= d => result <= x, "proven in MulDiv.spec (mulDivArgumentLesserThanDenominator)";
     require d > 0 => x <= d => result <= y, "proven in MulDiv.spec (mulDivArgumentLesserThanDenominator)";
@@ -77,12 +109,24 @@ function mulDivDownSummary(uint256 x, uint256 y, uint256 d) returns uint256 {
 }
 
 function mulDivUpSummary(uint256 x, uint256 y, uint256 d) returns uint256 {
-    mathint product = to_mathint(x) * y;
+    uint256 result;
+    mathint product = x * y;
     if (product > max_uint256 || (d > 0 && product + d - 1 > max_uint256)) {
-        mulOverflow = true;
+        // overflow in mulDivUp
+        if (x == lastCollateralAmount && y == lastOraclePrice && d == ORACLE_PRICE_SCALE()) {
+            // Explicitly allow to revert when some user's collateral is priced at too many debt units
+            // This assert double-checks that a revert only happens in this case.
+            // Gap: here we assume that collateral and oracle price match. A bug where the wrong collateral index is used for the oracle is not detected by this spec.
+            assert lastCollateralAmount * lastOraclePrice / ORACLE_PRICE_SCALE() > max_uint128, "collateral worth more than max_uint128 debt units";
+            revert();
+        } else {
+            // other overflows are checked at the end that they didn't cause a revert.
+            mulOverflow = true;
+            return result;
+        }
     }
 
-    uint256 result;
+    // These requires are proved for the no-overflow case.
     require d > 0 => result * d <= product + d - 1, "proven in MulDiv.spec (mulDivUpUpperBound)";
     require d > 0 => y <= d => result <= x, "proven in MulDiv.spec (mulDivArgumentLesserThanDenominator)";
     require d > 0 => x <= d => result <= y, "proven in MulDiv.spec (mulDivArgumentLesserThanDenominator)";
@@ -93,7 +137,7 @@ function mulDivUpSummary(uint256 x, uint256 y, uint256 d) returns uint256 {
 /// RULES ///
 
 // Normal calls intentionally scope this proof to non-reverting executions.
-// The updatePositionView and isHealthy have dedicated rules.
+// The updatePositionView and isHealthy have dedicated rules to ensure market and id match.
 rule noMultiplicationOverflow(method f, env e, calldataarg args) filtered { f -> f.selector != sig:isHealthy(Midnight.Market, bytes32, address).selector && f.selector != sig:updatePositionView(Midnight.Market, bytes32, address).selector } {
     require !mulOverflow, "prestate: no overflow before call";
     f(e, args);