From 659c2679962816f6fe6bdd721c9f8cb367369f08 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 17 Jun 2026 09:46:22 +0200 Subject: [PATCH 1/6] Prove that take has no new reverts due to continous fees Compare a run of take with zero fees with a run of take with arbitrary fee. Show that if the first does not revert, the second doesn't as well. Requires a deterministic setting (all external gates are modeled by a deterministic ghost). --- certora/confs/ContinuousFeeReverts.conf | 19 +++ certora/specs/ContinuousFeeReverts.spec | 184 ++++++++++++++++++++++++ 2 files changed, 203 insertions(+) create mode 100644 certora/confs/ContinuousFeeReverts.conf create mode 100644 certora/specs/ContinuousFeeReverts.spec diff --git a/certora/confs/ContinuousFeeReverts.conf b/certora/confs/ContinuousFeeReverts.conf new file mode 100644 index 000000000..827517600 --- /dev/null +++ b/certora/confs/ContinuousFeeReverts.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "certora/helpers/Utils.sol", + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/ContinuousFeeReverts.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": 2048, + "smt_timeout": 7200, + "prover_args": [ + "-destructiveOptimizations twostage" + ], + "msg": "Midnight Continuous Fee Reverts" +} diff --git a/certora/specs/ContinuousFeeReverts.spec b/certora/specs/ContinuousFeeReverts.spec new file mode 100644 index 000000000..33d7f028e --- /dev/null +++ b/certora/specs/ContinuousFeeReverts.spec @@ -0,0 +1,184 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// EQUIVALENCE OF REVERTS: activating the continuous fee never makes `take` revert in new ways. +// +// The continuous-fee *rate* (marketState[id].continuousFee) is read in exactly one function, take, and its +// value propagates to only three places: +// - Midnight.sol:393-394 buyerPendingFeeIncrease = toUint128(buyerCreditIncrease.mulDivDown(continuousFee * ttm, WAD)) +// - Midnight.sol:416 buyerPos.pendingFee += buyerPendingFeeIncrease +// - Midnight.sol:458 buyerPendingFeeIncrease is passed to the onBuy callback +// Everything else in take (prices, settlementFee, buyer/seller assets, consumed checks, gates, the seller +// side, _updatePosition, transfers, the final isHealthy check) is byte-identical between a run with the rate +// at its configured value and a run with the rate forced to 0. Hence the only NEW revert opportunities the +// enabled run has are the toUint128 cast (394) and the += (416); the callback is assumed to succeed. +// +// We prove this relationally: run take twice from the same pre-state, differing only in the market's fee rate. +// +// Determinism requirement (why this is a separate spec): in a two-run rule every rate-independent helper must +// return identical results across both runs, otherwise the prover could manufacture a spurious revert +// difference. So all helpers are summarized by *deterministic* persistent ghosts (same args => same result), +// not NONDET. None of these summaries needs non-linear reasoning; they only need to cancel between the runs. +// The single piece of non-linear reasoning is the mulDivDown argument bound (axiomMulDivDownArgLeDenom, +// proved in MulDiv.spec) together with the assumption fee*ttm <= WAD (from the fee-rate and TTM caps). + +using Utils as Utils; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function creditOf(bytes32 id, address user) external returns (uint128) envfree; + function pendingFee(bytes32 id, address user) external returns (uint128) envfree; + function continuousFee(bytes32 id) external returns (uint32) envfree; + function tickSpacing(bytes32 id) external returns (uint8) envfree; + function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; + function Utils.callbackSuccess() external returns (bytes32) envfree; + + // Deterministic id: links the market argument to stored state, identical across both runs. + function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market); + function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET; + + // Deterministic ghost summaries of the rate-independent helpers (see header). + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDownWithRevert(x, y, d); + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUpWithRevert(x, y, d); + function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => ghostTickToPrice(tick); + function settlementFee(bytes32 id, uint256 ttm) internal returns (uint256) => ghostSettlementFee(id, ttm); + function isHealthy(Midnight.Market memory market, bytes32 id, address user) internal returns (bool) => ghostIsHealthy(id, user); + function UtilsLib.tExchange(uint256 slot, bytes32 id, address user, bool val) internal returns (bool) => ghostTExchange(slot, id, user, val); + function UtilsLib.tGet(uint256 slot, bytes32 id, address user) internal returns (bool) => ghostTGet(slot, id, user); + + // Enter/liquidator gates: deterministic per (gate, user) so the rate-independent gate decision is + // identical across both runs. Without this they get an AUTO summary that havocs (and can revert) + // independently per run, producing a spurious revert difference. + function _.canIncreaseCredit(address user) external => ghostCanIncreaseCredit(calledContract, user) expect(bool); + function _.canIncreaseDebt(address user) external => ghostCanIncreaseDebt(calledContract, user) expect(bool); + function _.canLiquidate(address user) external => ghostCanLiquidate(calledContract, user) expect(bool); + + // Callbacks and ratifier: assumed to succeed deterministically. We verify take's own body, not the + // behavior of untrusted callbacks, and this spec (like ContinuousFee.spec) assumes no reentrancy. + function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => deterministicSuccess() expect(bytes32); + function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => deterministicSuccess() expect(bytes32); + function _.isRatified(Midnight.Offer, bytes) external => deterministicSuccess() expect(bytes32); + + // Token transfers: deterministic no-op (void => no havoc); identical across both runs. + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; +} + +/// CONSTANTS /// + +definition WAD() returns uint256 = 10 ^ 18; + +/// DETERMINISTIC GHOST SUMMARIES /// + +function summaryToId(Midnight.Market market) returns (bytes32) { + return Utils.hashMarket(market); +} + +// mulDivDown: deterministic, reverts on d == 0 and on x*y overflow (see mulOverflow below). +// The axiom mulDivArgumentLesserThanDenominator, proved in MulDiv.spec, is needed: +// y <= d => result <= x. +// This bounds the enabled-run fee increase by buyerCreditIncrease. +// Every other mulDivDown call is rate-independent and cancels between the two runs, so it +// needs no axiom (the ghost being deterministic suffices). +persistent ghost summaryMulDivDownGhost(mathint, mathint, mathint) returns mathint { + axiom forall mathint x. forall mathint y. forall mathint d. (d > 0 && 0 <= y && y <= d) => summaryMulDivDownGhost(x, y, d) <= x; +} + +// mulDivUp: deterministic, reverts on d == 0 and on x*y overflow. It needs NO value axioms: every mulDivUp +// call is either rate-independent (so it cancels between the runs) or inside updatePositionView (where a +// revert just prunes the path, since we require its post-update bound directly rather than proving it). +persistent ghost summaryMulDivUpGhost(mathint, mathint, mathint) returns mathint; + +// mulDiv reverts when x*y overflows 256 bits. We model that overflow as a deterministic uninterpreted +// predicate rather than the literal nonlinear `x * y >= 2^256`, for two reasons: +// - The many rate-independent mulDiv calls have identical (x,y) across both runs, so they share the same +// overflow outcome by congruence (an uninterpreted function), with no nonlinear arithmetic to discharge. +// - The one rate-dependent fee mulDiv (x = buyerCreditIncrease, y = continuousFee*ttm) is provably +// non-overflowing via the LINEAR safe-region axiom below instead of a product-of-bounds NIA argument. +// Soundness: the axiom only asserts no-overflow where it genuinely holds (x,y <= max_uint128 => x*y < 2^256), +// so it never hides a real overflow revert. Outside that region the predicate is free, but in every such case +// both runs revert anyway (e.g. the rate-independent toUint128(buyerCreditIncrease) at Midnight.sol:417). +persistent ghost mulOverflow(mathint, mathint) returns bool { + axiom forall mathint x. forall mathint y. (0 <= x && x <= max_uint128 && 0 <= y && y <= max_uint128) => !mulOverflow(x, y); +} + +function summaryMulDivDownWithRevert(uint256 x, uint256 y, uint256 d) returns uint256 { + if (d == 0 || mulOverflow(x, y)) { + revert(); + } + return require_uint256(summaryMulDivDownGhost(x, y, d)); +} + +function summaryMulDivUpWithRevert(uint256 x, uint256 y, uint256 d) returns uint256 { + if (d == 0 || mulOverflow(x, y)) { + revert(); + } + return require_uint256(summaryMulDivUpGhost(x, y, d)); +} + +persistent ghost ghostCanIncreaseCredit(address, address) returns bool; + +persistent ghost ghostCanIncreaseDebt(address, address) returns bool; + +persistent ghost ghostCanLiquidate(address, address) returns bool; + +persistent ghost ghostTickToPrice(uint256) returns uint256; + +persistent ghost ghostSettlementFee(bytes32, uint256) returns uint256; + +persistent ghost ghostIsHealthy(bytes32, address) returns bool; + +persistent ghost ghostTExchange(uint256, bytes32, address, bool) returns bool; + +persistent ghost ghostTGet(uint256, bytes32, address) returns bool; + +function deterministicSuccess() returns bytes32 { + return Utils.callbackSuccess(); +} + +/// RULE /// + +rule continuousFeeActivationAddsNoReverts(env e, env eSetter, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { + bytes32 id = summaryToId(offer.market); + address buyer = offer.buy ? offer.maker : taker; + address seller = offer.buy ? taker : offer.maker; + + // timeToMaturity exactly as take computes it: zeroFloorSub(maturity, block.timestamp). + mathint ttm = offer.market.maturity > e.block.timestamp ? offer.market.maturity - e.block.timestamp : 0; + + // fee*ttm <= WAD follows from continuousFee <= MAX_CONTINUOUS_FEE, ttm <= MAX_TTM, and + // MAX_CONTINUOUS_FEE * MAX_TTM < WAD. With the mulDivDown argument axiom this bounds the buyer fee + // increase by the credit increase. + require to_mathint(continuousFee(id)) * ttm <= WAD(), "fee*ttm <= WAD: fee-rate cap + TTM cap, see Midnight.spec"; + + // updatePosition preserves pendingFee <= credit (pendingContinuousFeeBoundedByCredit). Because the + // mulDiv ghosts are deterministic, this view call computes exactly the post-slash/post-accrual buyer + // credit and pendingFee that take's _updatePosition writes before the fee addition at Midnight.sol:416. + // Requiring the bound here excludes states where the slash result has pendingFee > credit, which saves + // reproving that known invariant via extra mulDiv axioms. This is what makes the += at 416 provably + // non-overflowing in the enabled run whenever the disabled run's credit += creditIncrease at 417 succeeds. + // If updatePositionView reverts, that path is pruned, but on it take's identical + // _updatePosition reverts too, so both takes revert and the assert holds trivially. + uint128 postCreditBuyer; + uint128 postPendingBuyer; + postCreditBuyer, postPendingBuyer, _ = updatePositionView(e, offer.market, id, buyer); + require postPendingBuyer <= postCreditBuyer, "pendingContinuousFeeBoundedByCredit, preserved by updatePosition"; + + // Setter preconditions so the disabled pre-state differs from the enabled one only in the fee rate. + require eSetter.msg.value == 0 && eSetter.msg.sender == currentContract.feeSetter, "valid fee setter call"; + require tickSpacing(id) > 0, "market is created"; + + storage initState = lastStorage; + + // Enabled run: take with the arbitrary configured rate. + take@withrevert(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + bool revertedEnabled = lastReverted; + + // Disabled pre-state: restore initState and force the rate to 0 via the real setter (writes only + // continuousFee), so the only delta versus initState is the rate. Then run the same take. + setMarketContinuousFee(eSetter, id, 0) at initState; + take@withrevert(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + bool revertedDisabled = lastReverted; + + assert !revertedDisabled => !revertedEnabled, "activating the continuous fee must not add reverts to take"; +} From 158ad4329f261c5bec1cfb428b6e24d65b6e18d8 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 4 Aug 2026 12:16:01 +0200 Subject: [PATCH 2/6] Updated to main branch --- certora/specs/ContinuousFeeReverts.spec | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/certora/specs/ContinuousFeeReverts.spec b/certora/specs/ContinuousFeeReverts.spec index 33d7f028e..cb991c183 100644 --- a/certora/specs/ContinuousFeeReverts.spec +++ b/certora/specs/ContinuousFeeReverts.spec @@ -26,16 +26,14 @@ using Utils as Utils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; - function pendingFee(bytes32 id, address user) external returns (uint128) envfree; function continuousFee(bytes32 id) external returns (uint32) envfree; function tickSpacing(bytes32 id) external returns (uint8) envfree; function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; function Utils.callbackSuccess() external returns (bytes32) envfree; // Deterministic id: links the market argument to stored state, identical across both runs. - function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market); - function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET; + function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market); + function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; // Deterministic ghost summaries of the rate-independent helpers (see header). function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDownWithRevert(x, y, d); From 0c15c795ae81a28b036015c174ec4b3705306007 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 4 Aug 2026 15:08:23 +0200 Subject: [PATCH 3/6] Fix isRatified API --- certora/specs/ContinuousFeeReverts.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/ContinuousFeeReverts.spec b/certora/specs/ContinuousFeeReverts.spec index cb991c183..5e2c41e18 100644 --- a/certora/specs/ContinuousFeeReverts.spec +++ b/certora/specs/ContinuousFeeReverts.spec @@ -55,7 +55,7 @@ methods { // behavior of untrusted callbacks, and this spec (like ContinuousFee.spec) assumes no reentrancy. function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => deterministicSuccess() expect(bytes32); function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => deterministicSuccess() expect(bytes32); - function _.isRatified(Midnight.Offer, bytes) external => deterministicSuccess() expect(bytes32); + function _.isRatified(Midnight.Offer, bytes, address) external => deterministicSuccess() expect(bytes32); // Token transfers: deterministic no-op (void => no havoc); identical across both runs. function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; From 3a6205d6f20b3b9466bd8a8536a31173a93e739a Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 4 Aug 2026 15:41:39 +0200 Subject: [PATCH 4/6] Assume continuousFee doesn't exceed offer's cap. --- certora/specs/ContinuousFeeReverts.spec | 41 +++++++++---------------- 1 file changed, 14 insertions(+), 27 deletions(-) diff --git a/certora/specs/ContinuousFeeReverts.spec b/certora/specs/ContinuousFeeReverts.spec index 5e2c41e18..fdb764652 100644 --- a/certora/specs/ContinuousFeeReverts.spec +++ b/certora/specs/ContinuousFeeReverts.spec @@ -1,25 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// EQUIVALENCE OF REVERTS: activating the continuous fee never makes `take` revert in new ways. -// -// The continuous-fee *rate* (marketState[id].continuousFee) is read in exactly one function, take, and its -// value propagates to only three places: -// - Midnight.sol:393-394 buyerPendingFeeIncrease = toUint128(buyerCreditIncrease.mulDivDown(continuousFee * ttm, WAD)) -// - Midnight.sol:416 buyerPos.pendingFee += buyerPendingFeeIncrease -// - Midnight.sol:458 buyerPendingFeeIncrease is passed to the onBuy callback -// Everything else in take (prices, settlementFee, buyer/seller assets, consumed checks, gates, the seller -// side, _updatePosition, transfers, the final isHealthy check) is byte-identical between a run with the rate -// at its configured value and a run with the rate forced to 0. Hence the only NEW revert opportunities the -// enabled run has are the toUint128 cast (394) and the += (416); the callback is assumed to succeed. -// -// We prove this relationally: run take twice from the same pre-state, differing only in the market's fee rate. -// -// Determinism requirement (why this is a separate spec): in a two-run rule every rate-independent helper must -// return identical results across both runs, otherwise the prover could manufacture a spurious revert -// difference. So all helpers are summarized by *deterministic* persistent ghosts (same args => same result), -// not NONDET. None of these summaries needs non-linear reasoning; they only need to cancel between the runs. -// The single piece of non-linear reasoning is the mulDivDown argument bound (axiomMulDivDownArgLeDenom, -// proved in MulDiv.spec) together with the assumption fee*ttm <= WAD (from the fee-rate and TTM caps). +// EQUIVALENCE OF REVERTS: activating the continuous fee never makes `take` revert in new ways, provided +// the fee doesn't exceed the offer's continuousFeeCap. using Utils as Utils; @@ -101,14 +83,14 @@ persistent ghost mulOverflow(mathint, mathint) returns bool { } function summaryMulDivDownWithRevert(uint256 x, uint256 y, uint256 d) returns uint256 { - if (d == 0 || mulOverflow(x, y)) { + if (d == 0 || x * y >= 2^256) { revert(); } return require_uint256(summaryMulDivDownGhost(x, y, d)); } function summaryMulDivUpWithRevert(uint256 x, uint256 y, uint256 d) returns uint256 { - if (d == 0 || mulOverflow(x, y)) { + if (d == 0 || x * y + d - 1 >= 2^256) { revert(); } return require_uint256(summaryMulDivUpGhost(x, y, d)); @@ -136,6 +118,10 @@ function deterministicSuccess() returns bytes32 { /// RULE /// +// Activating the continuous fee never makes `take` revert in new ways, provided the fee doesn't +// exceed the offer's continuousFeeCap. +// +// We prove this relationally: run take twice from the same pre-state, differing only in the market's fee rate. rule continuousFeeActivationAddsNoReverts(env e, env eSetter, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { bytes32 id = summaryToId(offer.market); address buyer = offer.buy ? offer.maker : taker; @@ -144,11 +130,6 @@ rule continuousFeeActivationAddsNoReverts(env e, env eSetter, Midnight.Offer off // timeToMaturity exactly as take computes it: zeroFloorSub(maturity, block.timestamp). mathint ttm = offer.market.maturity > e.block.timestamp ? offer.market.maturity - e.block.timestamp : 0; - // fee*ttm <= WAD follows from continuousFee <= MAX_CONTINUOUS_FEE, ttm <= MAX_TTM, and - // MAX_CONTINUOUS_FEE * MAX_TTM < WAD. With the mulDivDown argument axiom this bounds the buyer fee - // increase by the credit increase. - require to_mathint(continuousFee(id)) * ttm <= WAD(), "fee*ttm <= WAD: fee-rate cap + TTM cap, see Midnight.spec"; - // updatePosition preserves pendingFee <= credit (pendingContinuousFeeBoundedByCredit). Because the // mulDiv ghosts are deterministic, this view call computes exactly the post-slash/post-accrual buyer // credit and pendingFee that take's _updatePosition writes before the fee addition at Midnight.sol:416. @@ -166,6 +147,11 @@ rule continuousFeeActivationAddsNoReverts(env e, env eSetter, Midnight.Offer off require eSetter.msg.value == 0 && eSetter.msg.sender == currentContract.feeSetter, "valid fee setter call"; require tickSpacing(id) > 0, "market is created"; + require continuousFee(id) * ttm <= WAD(), "fee*ttm <= WAD: fee-rate cap + TTM cap, see Midnight.spec"; + + // The offer can intentionally reject the continuous fee if it exceeds the cap. + require continuousFee(id) <= offer.continuousFeeCap, "assume offer is compatible with market's fee"; + storage initState = lastStorage; // Enabled run: take with the arbitrary configured rate. @@ -175,6 +161,7 @@ rule continuousFeeActivationAddsNoReverts(env e, env eSetter, Midnight.Offer off // Disabled pre-state: restore initState and force the rate to 0 via the real setter (writes only // continuousFee), so the only delta versus initState is the rate. Then run the same take. setMarketContinuousFee(eSetter, id, 0) at initState; + take@withrevert(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); bool revertedDisabled = lastReverted; From e671ba57a5723ed8bdcabd0fdc815934862c8d12 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 4 Aug 2026 17:57:19 +0200 Subject: [PATCH 5/6] Clean up rule Also set the continuousfee in the second scenario to a new non-zero value. We don't have to require it was zero before and prove an even stronger property that changing the value will not cause new reverts. --- certora/specs/ContinuousFeeReverts.spec | 42 ++++++++++--------------- 1 file changed, 16 insertions(+), 26 deletions(-) diff --git a/certora/specs/ContinuousFeeReverts.spec b/certora/specs/ContinuousFeeReverts.spec index fdb764652..4bb0d7e63 100644 --- a/certora/specs/ContinuousFeeReverts.spec +++ b/certora/specs/ContinuousFeeReverts.spec @@ -48,6 +48,8 @@ methods { definition WAD() returns uint256 = 10 ^ 18; +definition MAX_TTM() returns mathint = 100 * 365 * 86400; + /// DETERMINISTIC GHOST SUMMARIES /// function summaryToId(Midnight.Market market) returns (bytes32) { @@ -122,48 +124,36 @@ function deterministicSuccess() returns bytes32 { // exceed the offer's continuousFeeCap. // // We prove this relationally: run take twice from the same pre-state, differing only in the market's fee rate. -rule continuousFeeActivationAddsNoReverts(env e, env eSetter, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { +rule continuousFeeActivationAddsNoReverts(env e, env eSetter, uint256 newContinuousFee, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { bytes32 id = summaryToId(offer.market); - address buyer = offer.buy ? offer.maker : taker; - address seller = offer.buy ? taker : offer.maker; + + // The offer can intentionally reject the continuous fee if it exceeds the cap. + require newContinuousFee <= offer.continuousFeeCap, "assume offer is compatible with new continuous fee"; // timeToMaturity exactly as take computes it: zeroFloorSub(maturity, block.timestamp). mathint ttm = offer.market.maturity > e.block.timestamp ? offer.market.maturity - e.block.timestamp : 0; + require ttm <= MAX_TTM(), "maturity less than MAX_TTM() in the future, see Midnight.spec"; - // updatePosition preserves pendingFee <= credit (pendingContinuousFeeBoundedByCredit). Because the - // mulDiv ghosts are deterministic, this view call computes exactly the post-slash/post-accrual buyer - // credit and pendingFee that take's _updatePosition writes before the fee addition at Midnight.sol:416. - // Requiring the bound here excludes states where the slash result has pendingFee > credit, which saves - // reproving that known invariant via extra mulDiv axioms. This is what makes the += at 416 provably - // non-overflowing in the enabled run whenever the disabled run's credit += creditIncrease at 417 succeeds. - // If updatePositionView reverts, that path is pruned, but on it take's identical - // _updatePosition reverts too, so both takes revert and the assert holds trivially. + // updatePosition preserves pendingFee <= credit + // proved as pendingContinuousFeeBoundedByCredit in Midnight.spec. + address buyer = offer.buy ? offer.maker : taker; uint128 postCreditBuyer; uint128 postPendingBuyer; postCreditBuyer, postPendingBuyer, _ = updatePositionView(e, offer.market, id, buyer); require postPendingBuyer <= postCreditBuyer, "pendingContinuousFeeBoundedByCredit, preserved by updatePosition"; - // Setter preconditions so the disabled pre-state differs from the enabled one only in the fee rate. - require eSetter.msg.value == 0 && eSetter.msg.sender == currentContract.feeSetter, "valid fee setter call"; - require tickSpacing(id) > 0, "market is created"; - - require continuousFee(id) * ttm <= WAD(), "fee*ttm <= WAD: fee-rate cap + TTM cap, see Midnight.spec"; - - // The offer can intentionally reject the continuous fee if it exceeds the cap. - require continuousFee(id) <= offer.continuousFeeCap, "assume offer is compatible with market's fee"; - storage initState = lastStorage; - // Enabled run: take with the arbitrary configured rate. + // arbitrary pre-state before continuous fee is set. Record its revert status. take@withrevert(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - bool revertedEnabled = lastReverted; + bool revertedDisabled = lastReverted; - // Disabled pre-state: restore initState and force the rate to 0 via the real setter (writes only - // continuousFee), so the only delta versus initState is the rate. Then run the same take. - setMarketContinuousFee(eSetter, id, 0) at initState; + // now set the new continuous fee and check again. + setMarketContinuousFee(eSetter, id, newContinuousFee) at initState; + // Enabled run: take with the arbitrary configured rate. take@withrevert(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - bool revertedDisabled = lastReverted; + bool revertedEnabled = lastReverted; assert !revertedDisabled => !revertedEnabled, "activating the continuous fee must not add reverts to take"; } From 43262ab25d403b2dabc6d60c59559b5a13034f3c Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 4 Aug 2026 18:24:31 +0200 Subject: [PATCH 6/6] ran linter --- certora/specs/ContinuousFeeReverts.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/ContinuousFeeReverts.spec b/certora/specs/ContinuousFeeReverts.spec index 4bb0d7e63..3e1a8ba99 100644 --- a/certora/specs/ContinuousFeeReverts.spec +++ b/certora/specs/ContinuousFeeReverts.spec @@ -85,14 +85,14 @@ persistent ghost mulOverflow(mathint, mathint) returns bool { } function summaryMulDivDownWithRevert(uint256 x, uint256 y, uint256 d) returns uint256 { - if (d == 0 || x * y >= 2^256) { + if (d == 0 || x * y >= 2 ^ 256) { revert(); } return require_uint256(summaryMulDivDownGhost(x, y, d)); } function summaryMulDivUpWithRevert(uint256 x, uint256 y, uint256 d) returns uint256 { - if (d == 0 || x * y + d - 1 >= 2^256) { + if (d == 0 || x * y + d - 1 >= 2 ^ 256) { revert(); } return require_uint256(summaryMulDivUpGhost(x, y, d));