diff --git a/certora/confs/NoSubtractionUnderflow.conf b/certora/confs/NoSubtractionUnderflow.conf new file mode 100644 index 00000000..41ef354f --- /dev/null +++ b/certora/confs/NoSubtractionUnderflow.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "certora/helpers/Utils.sol", + "src/Midnight.sol" + ], + "parametric_contracts": [ + "Midnight" + ], + "verify": "Midnight:certora/specs/NoSubtractionUnderflow.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, + "prover_args": [ + "-depth 5", + "-mediumTimeout 20", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]" + ], + "msg": "No Subtraction Underflow" +} diff --git a/certora/specs/NoSubtractionUnderflow.spec b/certora/specs/NoSubtractionUnderflow.spec new file mode 100644 index 00000000..a4adf16d --- /dev/null +++ b/certora/specs/NoSubtractionUnderflow.spec @@ -0,0 +1,163 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// Proves that successful calls do not underflow in any subtraction, given that every subtraction in Midnight and its +// dependencies is routed through UtilsLib.sub, and given the oracle price is bounded. + +using Utils as Utils; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; + function pendingFee(bytes32 id, address user) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) 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 toId: links call-site markets to validated state from touchMarket. + function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market); + + // Sound return bound: tickToPrice <= WAD for non-reverting calls. + function TickLib.tickToPrice(uint256) internal returns (uint256) => boundedTickPrice(); + + // Summarize mulDivDown and mulDivUp with their proven bounds (their internal subtraction is therefore not analyzed + // here; it is the `d - 1` in mulDivUp, which underflows only when d == 0, i.e. when the original code reverts too). + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => mulDivDownSummary(x, y, d); + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => mulDivUpSummary(x, y, d); + + // Summarize sub to track underflow. + function UtilsLib.sub(uint256 x, uint256 y) internal returns (uint256) => subSummary(x, y); +} + +/// HELPERS /// + +persistent ghost bool subUnderflow; + +definition WAD() returns uint256 = 10 ^ 18; + +definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; + +// Proven in CreatedMarkets.spec (createdMarketsHaveLltvLessThanOrEqualToOne) +// and ExactMath.spec (maxLifIsAtLeastWad, maxLifIsAtMostTwoWad). +// Maturity is bounded to uint64 as a realistic timestamp assumption for underflow analysis. +function summaryToId(Midnight.Market market) returns (bytes32) { + require forall uint256 i. i < market.collateralParams.length => market.collateralParams[i].lltv <= WAD(), "proven in CreatedMarkets.spec"; + require forall uint256 i. i < market.collateralParams.length => market.collateralParams[i].maxLif >= WAD() && market.collateralParams[i].maxLif <= 2 * WAD(), "proven in ExactMath.spec"; + require market.maturity <= max_uint64, "maturity fits in uint64: realistic timestamp assumption"; + 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"; + return price; +} + +// Sound: tickToPrice = 1e36 / (1e18 + wExp(...)) and wExp(x) >= 0, so result <= WAD. +function boundedTickPrice() returns uint256 { + uint256 price; + require price <= WAD(), "Proven in TickToPrice.spec"; + return price; +} + +function mulDivDownSummary(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + require d > 0 => to_mathint(result) * d <= to_mathint(x) * y, "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)"; + return result; +} + +function mulDivUpSummary(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + require d > 0 => to_mathint(result) * d >= to_mathint(x) * y, "proven in MulDiv.spec (mulDivUpRoundsUp)"; + require d > 0 => to_mathint(result) * d <= to_mathint(x) * y + 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)"; + return result; +} + +// Records an underflow when x < y, and returns the exact difference otherwise. On underflow the result is left +// unconstrained so that execution can continue: this maximizes the prover's freedom to reach a reverting-free +// counterexample, exactly as the multiplication summary does for overflow. +function subSummary(uint256 x, uint256 y) returns uint256 { + uint256 result; + if (x < y) { + subUnderflow = true; + } else { + require to_mathint(result) == x - y, "exact subtraction when no underflow"; + } + return result; +} + +/// RULES /// + +// Unlike multiplication overflow (which is never intended and is ruled out purely by magnitude bounds), several of +// Midnight's subtractions underflow *by design*: the underflow is the revert that rejects an out-of-range input. These +// input-guarded entry points are excluded from the parametric rule below and listed here with where their revert +// behavior is already proven: +// - repay : `debt -= units` rejects repaying more than owed (Reverts.spec) +// - withdraw : `credit/withdrawable/totalUnits -= units` rejects over-withdrawal (Reverts.spec) +// - withdrawCollateral : `collateral -= assets` rejects withdrawing absent collateral (Reverts.spec) +// - claimSettlementFee : `claimableSettlementFee -= amount` rejects over-claiming (Role.spec) +// - claimContinuousFee : `continuousFeeCredit/totalUnits/withdrawable -= amount` rejects over-claiming (Role.spec) +// - take : `offerPrice - settlementFee` rejects buy offers priced below the fee (Reverts.spec) +// The functions that thread through _updatePosition (take/withdraw/updatePosition) or the liquidation math (liquidate) +// have their non-reverting (hence underflow-free) behavior established under explicit preconditions by +// updatePositionDoesNotRevert and liquidateLossFactorDoesNotRevert in LossFactor.spec; updatePosition(View) is proven +// underflow-free directly below under those same preconditions. + +rule noSubtractionUnderflow(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 + && f.selector != sig:updatePosition(Midnight.Market, address).selector + && f.selector != sig:take(Midnight.Offer, bytes, uint256, address, address, address, bytes).selector + && f.selector != sig:repay(Midnight.Market, uint256, address, address, bytes).selector + && f.selector != sig:withdraw(Midnight.Market, uint256, address, address).selector + && f.selector != sig:withdrawCollateral(Midnight.Market, uint256, uint256, address, address).selector + && f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector + && f.selector != sig:claimSettlementFee(address, uint256, address).selector + && f.selector != sig:claimContinuousFee(Midnight.Market, uint256, address).selector +} { + require !subUnderflow, "prestate: no underflow before call"; + f(e, args); + assert !subUnderflow; +} + +// isHealthy contains no subtraction, so this holds trivially; kept for parity with NoMultiplicationOverflow. +rule noSubtractionUnderflowIsHealthy(env e, Midnight.Market market, bytes32 id, address borrower) { + require !subUnderflow, "prestate: no underflow before call"; + require id == summaryToId(market), "id corresponds to market"; + isHealthy(e, market, id, borrower); + assert !subUnderflow; +} + +// Preconditions are exactly those of updatePositionDoesNotRevert in LossFactor.spec. +rule noSubtractionUnderflowUpdatePositionView(env e, Midnight.Market market, bytes32 id, address user) { + require !subUnderflow, "prestate: no underflow before call"; + require id == summaryToId(market), "id corresponds to market"; + require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "proven in Midnight.spec (lastLossFactorLeqMarketLossFactor)"; + require pendingFee(id, user) <= credit(id, user), "proven in Midnight.spec (pendingContinuousFeeBoundedByCredit)"; + require currentContract.position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity"; + require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; + updatePositionView(e, market, id, user); + assert !subUnderflow; +} + +// updatePosition wraps updatePositionView (same subtractions) and additionally subtracts newCredit/newPendingFee from +// the stored credit/pendingFee, both bounded by the post-slash values. Same preconditions as above. +rule noSubtractionUnderflowUpdatePosition(env e, Midnight.Market market, address user) { + bytes32 id = summaryToId(market); + require !subUnderflow, "prestate: no underflow before call"; + require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "proven in Midnight.spec (lastLossFactorLeqMarketLossFactor)"; + require pendingFee(id, user) <= credit(id, user), "proven in Midnight.spec (pendingContinuousFeeBoundedByCredit)"; + require currentContract.position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity"; + require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; + updatePosition(e, market, user); + assert !subUnderflow; +} diff --git a/src/Midnight.sol b/src/Midnight.sol index 2f6fc6e7..f89134be 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -323,7 +323,7 @@ contract Midnight is IMidnight { function claimSettlementFee(address token, uint256 amount, address receiver) external { require(msg.sender == feeClaimer, OnlyFeeClaimer()); - claimableSettlementFee[token] -= amount; + claimableSettlementFee[token] = UtilsLib.sub(claimableSettlementFee[token], amount); emit EventsLib.ClaimSettlementFee(msg.sender, token, amount, receiver); SafeTransferLib.safeTransfer(token, receiver, amount); } @@ -334,9 +334,11 @@ contract Midnight is IMidnight { require(msg.sender == feeClaimer, OnlyFeeClaimer()); require(_marketState.tickSpacing > 0, MarketNotCreated()); - _marketState.continuousFeeCredit -= UtilsLib.toUint128(amount); - _marketState.totalUnits -= UtilsLib.toUint128(amount); - _marketState.withdrawable -= UtilsLib.toUint128(amount); + _marketState.continuousFeeCredit = + UtilsLib.toUint128(UtilsLib.sub(_marketState.continuousFeeCredit, UtilsLib.toUint128(amount))); + _marketState.totalUnits = UtilsLib.toUint128(UtilsLib.sub(_marketState.totalUnits, UtilsLib.toUint128(amount))); + _marketState.withdrawable = + UtilsLib.toUint128(UtilsLib.sub(_marketState.withdrawable, UtilsLib.toUint128(amount))); emit EventsLib.ClaimContinuousFee(msg.sender, id, amount, receiver); @@ -382,7 +384,7 @@ contract Midnight is IMidnight { uint256 offerPrice = TickLib.tickToPrice(offer.tick); uint256 timeToMaturity = UtilsLib.zeroFloorSub(offer.market.maturity, block.timestamp); uint256 _settlementFee = settlementFee(id, timeToMaturity); - uint256 sellerPrice = offer.buy ? offerPrice - _settlementFee : offerPrice; + uint256 sellerPrice = offer.buy ? UtilsLib.sub(offerPrice, _settlementFee) : offerPrice; uint256 buyerPrice = sellerPrice + _settlementFee; uint256 buyerAssets = offer.buy ? units.mulDivDown(buyerPrice, WAD) : units.mulDivUp(buyerPrice, WAD); uint256 sellerAssets = offer.buy ? units.mulDivDown(sellerPrice, WAD) : units.mulDivUp(sellerPrice, WAD); @@ -405,7 +407,7 @@ contract Midnight is IMidnight { uint256 buyerCreditIncrease = UtilsLib.zeroFloorSub(units, buyerPos.debt); uint256 sellerCreditDecrease = UtilsLib.min(units, sellerPos.credit); - uint256 sellerDebtIncrease = units - sellerCreditDecrease; + uint256 sellerDebtIncrease = UtilsLib.sub(units, sellerCreditDecrease); uint128 buyerPendingFeeIncrease = UtilsLib.toUint128(buyerCreditIncrease.mulDivDown(_marketState.continuousFee * timeToMaturity, WAD)); uint128 sellerPendingFeeDecrease = sellerPos.credit > 0 @@ -428,17 +430,19 @@ contract Midnight is IMidnight { SellerGatedFromIncreasingDebt() ); - buyerPos.debt -= UtilsLib.toUint128(units - buyerCreditIncrease); + buyerPos.debt = UtilsLib.toUint128( + UtilsLib.sub(buyerPos.debt, UtilsLib.toUint128(UtilsLib.sub(units, buyerCreditIncrease))) + ); buyerPos.pendingFee += buyerPendingFeeIncrease; buyerPos.credit += UtilsLib.toUint128(buyerCreditIncrease); - sellerPos.pendingFee -= sellerPendingFeeDecrease; - sellerPos.credit -= UtilsLib.toUint128(sellerCreditDecrease); + sellerPos.pendingFee = UtilsLib.toUint128(UtilsLib.sub(sellerPos.pendingFee, sellerPendingFeeDecrease)); + sellerPos.credit = UtilsLib.toUint128(UtilsLib.sub(sellerPos.credit, UtilsLib.toUint128(sellerCreditDecrease))); sellerPos.debt += UtilsLib.toUint128(sellerDebtIncrease); _marketState.totalUnits = - UtilsLib.toUint128(_marketState.totalUnits + buyerCreditIncrease - sellerCreditDecrease); - claimableSettlementFee[offer.market.loanToken] += buyerAssets - sellerAssets; + UtilsLib.toUint128(UtilsLib.sub(_marketState.totalUnits + buyerCreditIncrease, sellerCreditDecrease)); + claimableSettlementFee[offer.market.loanToken] += UtilsLib.sub(buyerAssets, sellerAssets); consumed[offer.maker][offer.group] = newConsumed; @@ -477,7 +481,9 @@ contract Midnight is IMidnight { ); } - SafeTransferLib.safeTransferFrom(offer.market.loanToken, payer, address(this), buyerAssets - sellerAssets); + SafeTransferLib.safeTransferFrom( + offer.market.loanToken, payer, address(this), UtilsLib.sub(buyerAssets, sellerAssets) + ); SafeTransferLib.safeTransferFrom(offer.market.loanToken, payer, receiver, sellerAssets); if (sellerCallback != address(0)) { @@ -513,11 +519,12 @@ contract Midnight is IMidnight { uint128 pendingFeeDecrease; if (_position.credit > 0) { pendingFeeDecrease = UtilsLib.toUint128(_position.pendingFee.mulDivUp(units, _position.credit)); - _position.pendingFee -= pendingFeeDecrease; + _position.pendingFee = UtilsLib.toUint128(UtilsLib.sub(_position.pendingFee, pendingFeeDecrease)); } - _position.credit -= UtilsLib.toUint128(units); - _marketState.withdrawable -= UtilsLib.toUint128(units); - _marketState.totalUnits -= UtilsLib.toUint128(units); + _position.credit = UtilsLib.toUint128(UtilsLib.sub(_position.credit, UtilsLib.toUint128(units))); + _marketState.withdrawable = + UtilsLib.toUint128(UtilsLib.sub(_marketState.withdrawable, UtilsLib.toUint128(units))); + _marketState.totalUnits = UtilsLib.toUint128(UtilsLib.sub(_marketState.totalUnits, UtilsLib.toUint128(units))); emit EventsLib.Withdraw(msg.sender, id, units, onBehalf, receiver, pendingFeeDecrease); @@ -530,7 +537,8 @@ contract Midnight is IMidnight { require(onBehalf == msg.sender || isAuthorized[onBehalf][msg.sender], Unauthorized()); bytes32 id = touchMarket(market); - position[id][onBehalf].debt -= UtilsLib.toUint128(units); + position[id][onBehalf].debt = + UtilsLib.toUint128(UtilsLib.sub(position[id][onBehalf].debt, UtilsLib.toUint128(units))); marketState[id].withdrawable += UtilsLib.toUint128(units); address payer = callback != address(0) ? callback : msg.sender; @@ -583,7 +591,7 @@ contract Midnight is IMidnight { address collateralToken = market.collateralParams[collateralIndex].token; Position storage _position = position[id][onBehalf]; - uint256 newCollateral = _position.collateral[collateralIndex] - assets; + uint256 newCollateral = UtilsLib.sub(_position.collateral[collateralIndex], assets); _position.collateral[collateralIndex] = UtilsLib.toUint128(newCollateral); if (newCollateral == 0 && assets > 0) { @@ -650,17 +658,25 @@ contract Midnight is IMidnight { if (badDebt > 0) { // forge-lint: disable-next-item(unsafe-typecast) as badDebt <= _position.debt - _position.debt -= uint128(badDebt); + _position.debt = UtilsLib.toUint128(UtilsLib.sub(_position.debt, uint128(badDebt))); uint256 _totalUnits = _marketState.totalUnits; uint256 _lossFactor = _marketState.lossFactor; _marketState.lossFactor = UtilsLib.toUint128( - type(uint128).max - (type(uint128).max - _lossFactor).mulDivDown(_totalUnits - badDebt, _totalUnits) + UtilsLib.sub( + type(uint128).max, + UtilsLib.sub(type(uint128).max, _lossFactor) + .mulDivDown(UtilsLib.sub(_totalUnits, badDebt), _totalUnits) + ) ); - _marketState.totalUnits -= UtilsLib.toUint128(badDebt); + _marketState.totalUnits = + UtilsLib.toUint128(UtilsLib.sub(_marketState.totalUnits, UtilsLib.toUint128(badDebt))); _marketState.continuousFeeCredit = _lossFactor < type(uint128).max ? UtilsLib.toUint128( _marketState.continuousFeeCredit - .mulDivDown(type(uint128).max - _marketState.lossFactor, type(uint128).max - _lossFactor) + .mulDivDown( + UtilsLib.sub(type(uint128).max, _marketState.lossFactor), + UtilsLib.sub(type(uint128).max, _lossFactor) + ) ) : 0; } @@ -668,7 +684,10 @@ contract Midnight is IMidnight { if (repaidUnits > 0 || seizedAssets > 0) { uint256 _maxLif = market.collateralParams[collateralIndex].maxLif; uint256 lif = postMaturityMode - ? UtilsLib.min(_maxLif, WAD + (_maxLif - WAD) * (block.timestamp - market.maturity) / TIME_TO_MAX_LIF) + ? UtilsLib.min( + _maxLif, + WAD + UtilsLib.sub(_maxLif, WAD) * UtilsLib.sub(block.timestamp, market.maturity) / TIME_TO_MAX_LIF + ) : _maxLif; if (seizedAssets > 0) { @@ -682,7 +701,7 @@ contract Midnight is IMidnight { // Note that debt >= maxDebt in this branch. // The imprecision in this computation is at most a few hundred collateral or loan token assets. uint256 maxRepaid = lltv < WAD - ? (_position.debt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lif * lltv) + ? UtilsLib.sub(_position.debt, maxDebt).mulDivUp(WAD * WAD, UtilsLib.sub(WAD * WAD, lif * lltv)) : type(uint256).max; require( repaidUnits <= maxRepaid @@ -692,13 +711,15 @@ contract Midnight is IMidnight { ); } - uint128 newCollateral = _position.collateral[collateralIndex] - UtilsLib.toUint128(seizedAssets); + uint128 newCollateral = UtilsLib.toUint128( + UtilsLib.sub(_position.collateral[collateralIndex], UtilsLib.toUint128(seizedAssets)) + ); _position.collateral[collateralIndex] = newCollateral; if (newCollateral == 0 && seizedAssets > 0) { _position.collateralBitmap = _position.collateralBitmap.clearBit(collateralIndex); } _marketState.withdrawable += UtilsLib.toUint128(repaidUnits); - _position.debt -= UtilsLib.toUint128(repaidUnits); + _position.debt = UtilsLib.toUint128(UtilsLib.sub(_position.debt, UtilsLib.toUint128(repaidUnits))); } address payer = callback != address(0) ? callback : msg.sender; @@ -828,19 +849,31 @@ contract Midnight is IMidnight { uint128 _credit = _position.credit; uint128 _lastLossFactor = _position.lastLossFactor; uint256 postSlashCredit = _lastLossFactor < type(uint128).max - ? _credit.mulDivDown(type(uint128).max - marketState[id].lossFactor, type(uint128).max - _lastLossFactor) + ? _credit.mulDivDown( + UtilsLib.sub(type(uint128).max, marketState[id].lossFactor), + UtilsLib.sub(type(uint128).max, _lastLossFactor) + ) : 0; uint128 _pendingFee = _position.pendingFee; - uint256 postSlashPendingFee = - _credit > 0 ? _pendingFee - _pendingFee.mulDivUp(_credit - postSlashCredit, _credit) : 0; + uint256 postSlashPendingFee = _credit > 0 + ? UtilsLib.sub(_pendingFee, _pendingFee.mulDivUp(UtilsLib.sub(_credit, postSlashCredit), _credit)) + : 0; uint256 accrualEnd = UtilsLib.min(block.timestamp, market.maturity); uint128 _lastAccrual = _position.lastAccrual; // forge-lint: disable-next-item(unsafe-typecast) as fee <= pending <= credit which are uint128 position fields uint128 fee = _lastAccrual < market.maturity - ? uint128(postSlashPendingFee.mulDivDown(accrualEnd - _lastAccrual, market.maturity - _lastAccrual)) + ? uint128( + postSlashPendingFee.mulDivDown( + UtilsLib.sub(accrualEnd, _lastAccrual), UtilsLib.sub(market.maturity, _lastAccrual) + ) + ) : 0; // forge-lint: disable-next-item(unsafe-typecast) as credit and pending are <= uint128 position fields - return (uint128(postSlashCredit) - fee, uint128(postSlashPendingFee) - fee, fee); + return ( + UtilsLib.toUint128(UtilsLib.sub(uint128(postSlashCredit), fee)), + UtilsLib.toUint128(UtilsLib.sub(uint128(postSlashPendingFee), fee)), + fee + ); } /// @dev Slashes the position and accrues the continuous fee. @@ -861,8 +894,8 @@ contract Midnight is IMidnight { Position storage _position = position[id][user]; (uint128 newCredit, uint128 newPendingFee, uint128 accruedFee) = updatePositionView(market, id, user); - uint128 creditDecrease = _position.credit - newCredit; - uint128 pendingFeeDecrease = _position.pendingFee - newPendingFee; + uint128 creditDecrease = UtilsLib.toUint128(UtilsLib.sub(_position.credit, newCredit)); + uint128 pendingFeeDecrease = UtilsLib.toUint128(UtilsLib.sub(_position.pendingFee, newPendingFee)); _position.credit = newCredit; _position.lastLossFactor = marketState[id].lossFactor; @@ -1001,6 +1034,7 @@ contract Midnight is IMidnight { (180 days, 360 days, _marketState.settlementFeeCbp5 * CBP, _marketState.settlementFeeCbp6 * CBP); // forgefmt: disable-end - return (feeLower * (end - timeToMaturity) + feeUpper * (timeToMaturity - start)) / (end - start); + return (feeLower * UtilsLib.sub(end, timeToMaturity) + feeUpper * UtilsLib.sub(timeToMaturity, start)) + / UtilsLib.sub(end, start); } } diff --git a/src/libraries/ConstantsLib.sol b/src/libraries/ConstantsLib.sol index e86817d6..6e30207e 100644 --- a/src/libraries/ConstantsLib.sol +++ b/src/libraries/ConstantsLib.sol @@ -32,6 +32,6 @@ function maxSettlementFee(uint256 index) pure returns (uint256) { /// @dev Returns the max LIF for the given lltv and cursor. function maxLif(uint256 lltv, uint256 cursor) pure returns (uint256) { - return UtilsLib.mulDivDown(WAD, WAD, WAD - UtilsLib.mulDivDown(cursor, WAD - lltv, WAD)); + return UtilsLib.mulDivDown(WAD, WAD, UtilsLib.sub(WAD, UtilsLib.mulDivDown(cursor, UtilsLib.sub(WAD, lltv), WAD))); } // forgefmt: disable-end diff --git a/src/libraries/TickLib.sol b/src/libraries/TickLib.sol index 635de316..6a09a091 100644 --- a/src/libraries/TickLib.sol +++ b/src/libraries/TickLib.sol @@ -2,6 +2,8 @@ // Copyright (c) 2025 Morpho Association pragma solidity ^0.8.0; +import {UtilsLib} from "./UtilsLib.sol"; + int256 constant LN_ONE_PLUS_DELTA = 0.004987541511039073e18; // floor(ln(1.005) * 1e18) uint256 constant MAX_TICK = 6744; // Minimum representable price increment in WAD (1e-7 WAD). Tick prices are rounded to multiples of this value. @@ -16,7 +18,7 @@ library TickLib { /// @dev Returns x / d rounded to the nearest integer with ties rounded down, without checking for overflow. function divHalfDownUnchecked(uint256 x, uint256 d) internal pure returns (uint256) { unchecked { - return (x + (d - 1) / 2) / d; + return (x + UtilsLib.sub(d, 1) / 2) / d; } } @@ -64,6 +66,6 @@ library TickLib { else high = mid; } } - return (low + spacing - 1) / spacing * spacing; + return UtilsLib.sub(low + spacing, 1) / spacing * spacing; } } diff --git a/src/libraries/UtilsLib.sol b/src/libraries/UtilsLib.sol index dcd1d32a..df176837 100644 --- a/src/libraries/UtilsLib.sol +++ b/src/libraries/UtilsLib.sol @@ -18,6 +18,11 @@ library UtilsLib { } } + /// @dev Returns x - y. + function sub(uint256 x, uint256 y) internal pure returns (uint256) { + return x - y; + } + /// @dev Returns (x * y) / d rounded down. function mulDivDown(uint256 x, uint256 y, uint256 d) internal pure returns (uint256) { return (x * y) / d; @@ -25,7 +30,7 @@ library UtilsLib { /// @dev Returns (x * y) / d rounded up. function mulDivUp(uint256 x, uint256 y, uint256 d) internal pure returns (uint256) { - return (x * y + (d - 1)) / d; + return (x * y + sub(d, 1)) / d; } function toUint128(uint256 x) internal pure returns (uint128) { @@ -36,7 +41,7 @@ library UtilsLib { function countBits(uint128 x) internal pure returns (uint256) { unchecked { - x = x - ((x >> 1) & 0x55555555555555555555555555555555); + x = toUint128(sub(x, (x >> 1) & 0x55555555555555555555555555555555)); x = (x & 0x33333333333333333333333333333333) + ((x >> 2) & 0x33333333333333333333333333333333); x = (x + (x >> 4)) & 0x0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f; return (x * 0x01010101010101010101010101010101) >> 120;