From f3480008d0a889989719ab8dea611008e374907b Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 21 Jul 2026 23:14:27 +0200 Subject: [PATCH 1/4] Improved multiplication overflow check Allow mulDiv(position.collateral, oracle.price(), ORACLE_PRICE_SCALE) to overflow. Every other mulDiv is checked that the overflow does not cause a revert. We no longer restrict price to uint128, instead only reverts due to position.collateral*oracle.price() >= 2^256 are not checked. --- certora/specs/NoMultiplicationOverflow.spec | 96 +++++++++++++++++---- 1 file changed, 81 insertions(+), 15 deletions(-) diff --git a/certora/specs/NoMultiplicationOverflow.spec b/certora/specs/NoMultiplicationOverflow.spec index 9986cb327..5194ff020 100644 --- a/certora/specs/NoMultiplicationOverflow.spec +++ b/certora/specs/NoMultiplicationOverflow.spec @@ -1,7 +1,15 @@ // 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 onlye 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 +// a documented limitation. + +// Strictly speaking, other mulDivDown/mulDivUp may revert due to overflow. 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 +18,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 +41,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 +61,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 +81,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()) { + // we explicitly allow the revert when some user's collateral is priced at too many debt units + // this asserts double-checks that this only happens in this case. + // gap: here we assume that collateral and oracle price match. + 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 +107,25 @@ 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()) { + // we explicitly allow the revert when some user's collateral is priced at too many debt units + // this asserts double-checks that this only happens in this case. + // gap: here we assume that collateral and oracle price match. + 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; + assert false; + 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 +136,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); @@ -113,3 +156,26 @@ rule noMultiplicationOverflowUpdatePositionView(env e, Midnight.Market market, b updatePositionView(e, market, id, user); assert !mulOverflow; } + +rule noMultiplicationOverflowTake(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes takerCallbackData) { + require !mulOverflow, "prestate: no overflow before call"; + require units < 2^129, "ensured by the toUint128 casts on units - buyerCreditIncrease and buyerCreditIncrease"; + take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); + assert !mulOverflow; +} + +rule noMultiplicationOverflowWithdraw(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver) { + require !mulOverflow, "prestate: no overflow before call"; + require units < 2^128, "ensured by the toUint128 casts on units"; + withdraw(e, market, units, onBehalf, receiver); + assert !mulOverflow; +} + +rule noMultiplicationOverflowLiquidate(env e, bytes32 id, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { + require !mulOverflow, "prestate: no overflow before call"; + require id == summaryToId(market), "id corresponds to market"; + require repaidUnits < 2^128, "ensured by cast"; + require seizedAssets * oraclePriceGhost(market.collateralParams[collateralIndex].oracle) / ORACLE_PRICE_SCALE() < 2^128, "ensured by subtracting seizedAssets from collateral"; + liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + assert !mulOverflow; +} From e55214a55063bcccc6bd84fb4c9c3e4bd032da4d Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 21 Jul 2026 23:20:24 +0200 Subject: [PATCH 2/4] Remove investigation of all reverting mulDiv --- certora/specs/NoMultiplicationOverflow.spec | 24 --------------------- 1 file changed, 24 deletions(-) diff --git a/certora/specs/NoMultiplicationOverflow.spec b/certora/specs/NoMultiplicationOverflow.spec index 5194ff020..6f207d50f 100644 --- a/certora/specs/NoMultiplicationOverflow.spec +++ b/certora/specs/NoMultiplicationOverflow.spec @@ -120,7 +120,6 @@ function mulDivUpSummary(uint256 x, uint256 y, uint256 d) returns uint256 { } else { // other overflows are checked at the end that they didn't cause a revert. mulOverflow = true; - assert false; return result; } } @@ -156,26 +155,3 @@ rule noMultiplicationOverflowUpdatePositionView(env e, Midnight.Market market, b updatePositionView(e, market, id, user); assert !mulOverflow; } - -rule noMultiplicationOverflowTake(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes takerCallbackData) { - require !mulOverflow, "prestate: no overflow before call"; - require units < 2^129, "ensured by the toUint128 casts on units - buyerCreditIncrease and buyerCreditIncrease"; - take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); - assert !mulOverflow; -} - -rule noMultiplicationOverflowWithdraw(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver) { - require !mulOverflow, "prestate: no overflow before call"; - require units < 2^128, "ensured by the toUint128 casts on units"; - withdraw(e, market, units, onBehalf, receiver); - assert !mulOverflow; -} - -rule noMultiplicationOverflowLiquidate(env e, bytes32 id, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { - require !mulOverflow, "prestate: no overflow before call"; - require id == summaryToId(market), "id corresponds to market"; - require repaidUnits < 2^128, "ensured by cast"; - require seizedAssets * oraclePriceGhost(market.collateralParams[collateralIndex].oracle) / ORACLE_PRICE_SCALE() < 2^128, "ensured by subtracting seizedAssets from collateral"; - liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - assert !mulOverflow; -} From b2bd90718629e5122eb952daff610126ddbfb823 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 21 Jul 2026 23:36:38 +0200 Subject: [PATCH 3/4] Rewording of comments --- certora/specs/NoMultiplicationOverflow.spec | 24 +++++++++++---------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/certora/specs/NoMultiplicationOverflow.spec b/certora/specs/NoMultiplicationOverflow.spec index 6f207d50f..1e96efe4b 100644 --- a/certora/specs/NoMultiplicationOverflow.spec +++ b/certora/specs/NoMultiplicationOverflow.spec @@ -1,15 +1,17 @@ // SPDX-License-Identifier: GPL-2.0-or-later // Copyright (c) 2026 Morpho Association -// Proves that the onlye 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 -// a documented limitation. - -// Strictly speaking, other mulDivDown/mulDivUp may revert due to overflow. 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. +// 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; @@ -88,7 +90,7 @@ function mulDivDownSummary(uint256 x, uint256 y, uint256 d) returns uint256 { if (x == lastCollateralAmount && y == lastOraclePrice && d == ORACLE_PRICE_SCALE()) { // we explicitly allow the revert when some user's collateral is priced at too many debt units // this asserts double-checks that this only happens in this case. - // gap: here we assume that collateral and oracle price match. + // 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 { @@ -114,7 +116,7 @@ function mulDivUpSummary(uint256 x, uint256 y, uint256 d) returns uint256 { if (x == lastCollateralAmount && y == lastOraclePrice && d == ORACLE_PRICE_SCALE()) { // we explicitly allow the revert when some user's collateral is priced at too many debt units // this asserts double-checks that this only happens in this case. - // gap: here we assume that collateral and oracle price match. + // 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 { From 9148c5734fd5b8d4fc8e7b3461f59654831e618f Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 21 Jul 2026 23:42:09 +0200 Subject: [PATCH 4/4] More comment refinement --- certora/specs/NoMultiplicationOverflow.spec | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/certora/specs/NoMultiplicationOverflow.spec b/certora/specs/NoMultiplicationOverflow.spec index 1e96efe4b..27b310920 100644 --- a/certora/specs/NoMultiplicationOverflow.spec +++ b/certora/specs/NoMultiplicationOverflow.spec @@ -11,7 +11,7 @@ // 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. +// Thus, the mulDiv did not singlehandedly cause the revert. using Utils as Utils; @@ -88,9 +88,9 @@ function mulDivDownSummary(uint256 x, uint256 y, uint256 d) returns uint256 { if (product > max_uint256) { // overflow in mulDivDown if (x == lastCollateralAmount && y == lastOraclePrice && d == ORACLE_PRICE_SCALE()) { - // we explicitly allow the revert when some user's collateral is priced at too many debt units - // this asserts double-checks that this 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. + // 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 { @@ -114,9 +114,9 @@ function mulDivUpSummary(uint256 x, uint256 y, uint256 d) returns uint256 { if (product > max_uint256 || (d > 0 && product + d - 1 > max_uint256)) { // overflow in mulDivUp if (x == lastCollateralAmount && y == lastOraclePrice && d == ORACLE_PRICE_SCALE()) { - // we explicitly allow the revert when some user's collateral is priced at too many debt units - // this asserts double-checks that this 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. + // 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 {