diff --git a/certora/confs/SettlementFeeSpread.conf b/certora/confs/SettlementFeeSpread.conf index 73424d39..ef758b2d 100644 --- a/certora/confs/SettlementFeeSpread.conf +++ b/certora/confs/SettlementFeeSpread.conf @@ -1,18 +1,23 @@ { "files": [ "certora/helpers/Utils.sol", + "certora/helpers/SettlementFeeUtils.sol", "src/Midnight.sol" ], + "split_rules": [ + "*" + ], "verify": "Midnight:certora/specs/SettlementFeeSpread.spec", "solc": "solc-0.8.34", "solc_evm_version": "osaka", + "solc_via_ir": true, "optimistic_hashing": true, "hashing_length_bound": 2048, - "solc_via_ir": true, "optimistic_loop": true, "loop_iter": 2, - "rule_sanity": "basic", + "multi_assert_check": true, "prover_args": [ + "-havocAllByDefault true", "-depth 5", "-mediumTimeout 60", "-timeout 3600" diff --git a/certora/confs/TouchMarketIsCalled.conf b/certora/confs/TouchMarketIsCalled.conf new file mode 100644 index 00000000..24ac16be --- /dev/null +++ b/certora/confs/TouchMarketIsCalled.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "certora/helpers/Utils.sol", + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/TouchMarketIsCalled.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, + "rule_sanity": "basic", + "prover_args": [ + "-depth 5", + "-mediumTimeout 60", + "-timeout 3600" + ], + "msg": "TouchMarket Is Called" +} diff --git a/certora/helpers/SettlementFeeUtils.sol b/certora/helpers/SettlementFeeUtils.sol new file mode 100644 index 00000000..c81e90db --- /dev/null +++ b/certora/helpers/SettlementFeeUtils.sol @@ -0,0 +1,40 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2025 Morpho Association +pragma solidity ^0.8.0; + +import {IMidnight} from "../../src/interfaces/IMidnight.sol"; +import {CBP} from "../../src/libraries/ConstantsLib.sol"; + +contract SettlementFeeUtils { + /// @dev Mirrors Midnight.settlementFee but reads the loan token's default settlement fee cbps (in Solidity) instead + /// of the market state. This is the fee a freshly created market applies, since touchMarket copies these defaults + /// into the market state. + function defaultSettlementFee(IMidnight midnight, address loanToken, uint256 timeToMaturity) + external + view + returns (uint256) + { + uint16[7] memory settlementFeeCbp; + settlementFeeCbp[0] = midnight.defaultSettlementFeeCbp(loanToken, 0); + settlementFeeCbp[1] = midnight.defaultSettlementFeeCbp(loanToken, 1); + settlementFeeCbp[2] = midnight.defaultSettlementFeeCbp(loanToken, 2); + settlementFeeCbp[3] = midnight.defaultSettlementFeeCbp(loanToken, 3); + settlementFeeCbp[4] = midnight.defaultSettlementFeeCbp(loanToken, 4); + settlementFeeCbp[5] = midnight.defaultSettlementFeeCbp(loanToken, 5); + settlementFeeCbp[6] = midnight.defaultSettlementFeeCbp(loanToken, 6); + + if (timeToMaturity >= 360 days) return settlementFeeCbp[6] * CBP; + + // forgefmt: disable-start + (uint256 start, uint256 end, uint256 feeLower, uint256 feeUpper) = + timeToMaturity < 1 days ? ( 0 days, 1 days, settlementFeeCbp[0] * CBP, settlementFeeCbp[1] * CBP) : + timeToMaturity < 7 days ? ( 1 days, 7 days, settlementFeeCbp[1] * CBP, settlementFeeCbp[2] * CBP) : + timeToMaturity < 30 days ? ( 7 days, 30 days, settlementFeeCbp[2] * CBP, settlementFeeCbp[3] * CBP) : + timeToMaturity < 90 days ? ( 30 days, 90 days, settlementFeeCbp[3] * CBP, settlementFeeCbp[4] * CBP) : + timeToMaturity < 180 days ? ( 90 days, 180 days, settlementFeeCbp[4] * CBP, settlementFeeCbp[5] * CBP) : + (180 days, 360 days, settlementFeeCbp[5] * CBP, settlementFeeCbp[6] * CBP); + // forgefmt: disable-end + + return (feeLower * (end - timeToMaturity) + feeUpper * (timeToMaturity - start)) / (end - start); + } +} diff --git a/certora/specs/OnlyExplicitPayerCanLoseTokens.spec b/certora/specs/OnlyExplicitPayerCanLoseTokens.spec index f989e746..2cd7caea 100644 --- a/certora/specs/OnlyExplicitPayerCanLoseTokens.spec +++ b/certora/specs/OnlyExplicitPayerCanLoseTokens.spec @@ -10,8 +10,8 @@ methods { // Callbacks can modify the whole state arbitrarily, and can only modify the ghost variables to allow // themselves as payer. Callbacks are checked to only be called by their corresponding function, - // eg onLiquidate is only called by liquidate. onRatify and onSell cannot authorize a payer, so we - // model them with a plain HAVOC_ALL. + // eg onLiquidate is only called by liquidate. onSell cannot authorize a payer, so we model them + // with a plain HAVOC_ALL. function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => onCallBackSummary(calledContract, buyCallbackAllowed) expect(bytes32); function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => onCallBackSummary(calledContract, liquidateCallbackAllowed) expect(bytes32); function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => onCallBackSummary(calledContract, repayCallbackAllowed) expect(bytes32); diff --git a/certora/specs/SettlementFeeSpread.spec b/certora/specs/SettlementFeeSpread.spec index 2eb7e8b5..6debe502 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -1,14 +1,16 @@ // SPDX-License-Identifier: GPL-2.0-or-later -using Utils as Utils; +using SettlementFeeUtils as SettlementFeeUtils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; function settlementFee(bytes32, uint256) external returns (uint256) envfree; + function tickSpacing(bytes32) external returns (uint8) envfree; + function SettlementFeeUtils.defaultSettlementFee(address, address, uint256) external returns (uint256) envfree; - // Summary is required because abi.encodePacked doesn't ensure injectivity of the hash function in CVL, for an unknown reason. + // Summarize the id as a deterministic ghost over the market, removing the collateral params array. + // This is sound because the rules only use a single market. function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); // Deterministic TickLib.tickToPrice summary to be able to reference the price in the rules. @@ -20,11 +22,17 @@ methods { // Over-approximate view functions for prover performance. function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; - // Assume no reentrancy, because we need to know that the settlement fee won't change in the onRatify callback. This allows to reference the settlement fee in the rule settlementFeeSpreadBounds. + // SettlementFeeUtils reads the defaults through the IMidnight interface; dispatch the call to Midnight's getter so + // it reads currentContract's storage instead of being havoc'd to an arbitrary value. + function _.defaultSettlementFeeCbp(address, uint256) external => DISPATCHER(true); + + // function _updatePosition(Midnight.Market memory, bytes32, address) internal returns (uint128, uint128, uint128) => NONDET; } +persistent ghost ghostToId(uint256, address, address, uint256, uint256, address, address) returns bytes32; + function summaryToId(Midnight.Market market) returns (bytes32) { - return Utils.hashMarket(market); + return ghostToId(market.chainId, market.midnight, market.loanToken, market.maturity, market.rcfThreshold, market.enterGate, market.liquidatorGate); } persistent ghost summaryTickToPrice(uint256) returns uint256; @@ -47,11 +55,32 @@ rule makerFavorableRounding(env e, Midnight.Offer offer, bytes ratifierData, uin } // The spread between what the buyer pays and what the seller receives is at least floor(units * fee / WAD) and at most ceil(units * fee / WAD). +// Assume that the market is created. rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { + bytes32 id = summaryToId(offer.market); + require tickSpacing(id) > 0; + uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0; + uint256 fee = settlementFee@withrevert(id, timeToMaturity); + assert !lastReverted; + + uint256 buyerAssets; + uint256 sellerAssets; + buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + + assert buyerAssets - sellerAssets >= (units * fee) / WAD(); + assert buyerAssets - sellerAssets <= (units * fee + WAD() - 1) / WAD(); +} + +// Twin rule of settlementFeeSpreadBounds for a market that is not created yet at the start. +rule settlementFeeSpreadBoundsNotCreatedMarket(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { bytes32 id = summaryToId(offer.market); - uint256 fee = settlementFee(id, timeToMaturity); + require tickSpacing(id) == 0; + + 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); uint256 buyerAssets; uint256 sellerAssets; diff --git a/certora/specs/TouchMarketIsCalled.spec b/certora/specs/TouchMarketIsCalled.spec new file mode 100644 index 00000000..d2686954 --- /dev/null +++ b/certora/specs/TouchMarketIsCalled.spec @@ -0,0 +1,111 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +using Utils as Utils; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; + + // Record every call to touchMarket and the market it is called with. + function touchMarket(Midnight.Market memory market) internal returns (bytes32) => recordTouchMarket(market); + + // Over-approximate the heavy functions for prover performance. + // This is safe here: the worst they could do is fail to record a touchMarket call, which would make a rule fail rather than pass unsoundly. + function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function UtilsLib.countBits(uint128) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function UtilsLib.mulDivUp(uint256, uint256, uint256) internal returns (uint256) => NONDET; + function UtilsLib.mulDivDown(uint256, uint256, uint256) internal returns (uint256) => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; +} + +/// HELPERS /// + +persistent ghost bool touchMarketCalled; + +persistent ghost bytes32 touchedMarketId; + +function recordTouchMarket(Midnight.Market market) returns bytes32 { + touchMarketCalled = true; + touchedMarketId = Utils.hashMarket(market); + return Utils.hashMarket(market); +} + +/// RULES /// + +// Each rule shows that a successful interaction calls touchMarket with its own market, which in turn implies that a reverting touchMarket forces the interaction to revert. + +rule claimContinuousFeeCallsTouchMarket(env e, Midnight.Market market, uint256 amount, address receiver) { + require !touchMarketCalled, "reset call tracking"; + + claimContinuousFee(e, market, amount, receiver); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(market); +} + +rule takeCallsTouchMarket(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { + require !touchMarketCalled, "reset call tracking"; + + take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(offer.market); +} + +rule withdrawCallsTouchMarket(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver) { + require !touchMarketCalled, "reset call tracking"; + + withdraw(e, market, units, onBehalf, receiver); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(market); +} + +rule repayCallsTouchMarket(env e, Midnight.Market market, uint256 units, address onBehalf, address callback, bytes data) { + require !touchMarketCalled, "reset call tracking"; + + repay(e, market, units, onBehalf, callback, data); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(market); +} + +rule supplyCollateralCallsTouchMarket(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf) { + require !touchMarketCalled, "reset call tracking"; + + supplyCollateral(e, market, collateralIndex, assets, onBehalf); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(market); +} + +rule withdrawCollateralCallsTouchMarket(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf, address receiver) { + require !touchMarketCalled, "reset call tracking"; + + withdrawCollateral(e, market, collateralIndex, assets, onBehalf, receiver); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(market); +} + +rule liquidateCallsTouchMarket(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) { + require !touchMarketCalled, "reset call tracking"; + + liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(market); +} + +rule updatePositionCallsTouchMarket(env e, Midnight.Market market, address user) { + require !touchMarketCalled, "reset call tracking"; + + updatePosition(e, market, user); + + assert touchMarketCalled; + assert touchedMarketId == Utils.hashMarket(market); +}