diff --git a/certora/specs/NoMultiplicationOverflow.spec b/certora/specs/NoMultiplicationOverflow.spec index a3cd69a4c..be76b3399 100644 --- a/certora/specs/NoMultiplicationOverflow.spec +++ b/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 { + uint256 result; mathint product = to_mathint(x) * y; if (d != 0 && x * y >= 2 ^ 256) { - 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 { + uint256 result; mathint product = x * y; if (d != 0 && x * y + d - 1 >= 2 ^ 256) { - 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);