From 38e9e984b147298cd96ccaf89f7368b4fbe6472a Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 21:19:29 +0200 Subject: [PATCH 1/7] remove no reentrancy assumption --- certora/confs/SettlementFeeSpread.conf | 1 + certora/specs/SettlementFeeSpread.spec | 2 -- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/certora/confs/SettlementFeeSpread.conf b/certora/confs/SettlementFeeSpread.conf index 73424d39d..e00080264 100644 --- a/certora/confs/SettlementFeeSpread.conf +++ b/certora/confs/SettlementFeeSpread.conf @@ -13,6 +13,7 @@ "loop_iter": 2, "rule_sanity": "basic", "prover_args": [ + "-havocAllByDefault true", "-depth 5", "-mediumTimeout 60", "-timeout 3600" diff --git a/certora/specs/SettlementFeeSpread.spec b/certora/specs/SettlementFeeSpread.spec index dba07ea3a..a348c3ac3 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -19,8 +19,6 @@ 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. } function summaryToId(Midnight.Market market) returns (bytes32) { From 96d6eecbe94065986265ef2db9a96e0d05981f29 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 19:29:18 +0200 Subject: [PATCH 2/7] add touchMarketRevertCausesTakeRevert mention --- certora/confs/SettlementFeeSpread.conf | 1 - certora/specs/OnlyExplicitPayerCanLoseTokens.spec | 2 +- certora/specs/SettlementFeeSpread.spec | 6 +++++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/certora/confs/SettlementFeeSpread.conf b/certora/confs/SettlementFeeSpread.conf index e00080264..73424d39d 100644 --- a/certora/confs/SettlementFeeSpread.conf +++ b/certora/confs/SettlementFeeSpread.conf @@ -13,7 +13,6 @@ "loop_iter": 2, "rule_sanity": "basic", "prover_args": [ - "-havocAllByDefault true", "-depth 5", "-mediumTimeout 60", "-timeout 3600" diff --git a/certora/specs/OnlyExplicitPayerCanLoseTokens.spec b/certora/specs/OnlyExplicitPayerCanLoseTokens.spec index f989e746d..fc0bc32cc 100644 --- a/certora/specs/OnlyExplicitPayerCanLoseTokens.spec +++ b/certora/specs/OnlyExplicitPayerCanLoseTokens.spec @@ -10,7 +10,7 @@ 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 + // 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); diff --git a/certora/specs/SettlementFeeSpread.spec b/certora/specs/SettlementFeeSpread.spec index a348c3ac3..f42dbd6d7 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -48,8 +48,12 @@ rule makerFavorableRounding(env e, Midnight.Offer offer, bytes ratifierData, uin rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0; + // See rule touchMarketRevertCausesTakeRevert for why calling touchMarket doesn't prune meaningful take paths. + touchMarket(e, offer.market); + bytes32 id = summaryToId(offer.market); - uint256 fee = settlementFee(id, timeToMaturity); + uint256 fee = settlementFee@withrevert(id, timeToMaturity); + assert !lastReverted; uint256 buyerAssets; uint256 sellerAssets; From cf20f51914ab00cd990e022642fe3aaf5af8e2e3 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 20:02:49 +0200 Subject: [PATCH 3/7] TouchMarketIsCalled --- certora/confs/SettlementFeeSpread.conf | 1 + certora/confs/TouchMarketIsCalled.conf | 21 +++++++ certora/specs/SettlementFeeSpread.spec | 3 +- certora/specs/TouchMarketIsCalled.spec | 87 ++++++++++++++++++++++++++ 4 files changed, 111 insertions(+), 1 deletion(-) create mode 100644 certora/confs/TouchMarketIsCalled.conf create mode 100644 certora/specs/TouchMarketIsCalled.spec diff --git a/certora/confs/SettlementFeeSpread.conf b/certora/confs/SettlementFeeSpread.conf index 73424d39d..813802787 100644 --- a/certora/confs/SettlementFeeSpread.conf +++ b/certora/confs/SettlementFeeSpread.conf @@ -12,6 +12,7 @@ "optimistic_loop": true, "loop_iter": 2, "rule_sanity": "basic", + "multi_assert_check": true, "prover_args": [ "-depth 5", "-mediumTimeout 60", diff --git a/certora/confs/TouchMarketIsCalled.conf b/certora/confs/TouchMarketIsCalled.conf new file mode 100644 index 000000000..24ac16be3 --- /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/specs/SettlementFeeSpread.spec b/certora/specs/SettlementFeeSpread.spec index f42dbd6d7..27817cf2d 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -48,7 +48,8 @@ rule makerFavorableRounding(env e, Midnight.Offer offer, bytes ratifierData, uin rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0; - // See rule touchMarketRevertCausesTakeRevert for why calling touchMarket doesn't prune meaningful take paths. + // take calls touchMarket (see rule takeCallsTouchMarket), so a reverting touchMarket reverts take too. + // Calling touchMarket here therefore only prunes take paths that revert anyway. touchMarket(e, offer.market); bytes32 id = summaryToId(offer.market); diff --git a/certora/specs/TouchMarketIsCalled.spec b/certora/specs/TouchMarketIsCalled.spec new file mode 100644 index 000000000..ed2144a4e --- /dev/null +++ b/certora/specs/TouchMarketIsCalled.spec @@ -0,0 +1,87 @@ +// 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. The `internal` entry catches the + // same-contract calls made by take/withdraw/repay/supplyCollateral/withdrawCollateral/liquidate. + // Summarizing touchMarket is sound for the property proved here (that it is called): we only observe whether + // the call happens, not its effects. Solidity propagates reverts out of internal calls, so proving that each + // interaction calls touchMarket(market) shows that a reverting touchMarket forces the interaction to revert. + function touchMarket(Midnight.Market memory market) internal returns (bytes32) => recordTouchMarket(market); +} + +/// 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 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); +} From 15690f620ab1a6b865aec40c241cc95bbecc56fe Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 20:04:32 +0200 Subject: [PATCH 4/7] add summaries --- certora/specs/TouchMarketIsCalled.spec | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/certora/specs/TouchMarketIsCalled.spec b/certora/specs/TouchMarketIsCalled.spec index ed2144a4e..5587cf1fa 100644 --- a/certora/specs/TouchMarketIsCalled.spec +++ b/certora/specs/TouchMarketIsCalled.spec @@ -7,12 +7,20 @@ methods { function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; - // Record every call to touchMarket and the market it is called with. The `internal` entry catches the - // same-contract calls made by take/withdraw/repay/supplyCollateral/withdrawCollateral/liquidate. - // Summarizing touchMarket is sound for the property proved here (that it is called): we only observe whether - // the call happens, not its effects. Solidity propagates reverts out of internal calls, so proving that each - // interaction calls touchMarket(market) shows that a reverting touchMarket forces the interaction to revert. + // 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 settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; + 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 /// From 0ceede8c6be069fcba4ee9b565ba5a7a67ed1d15 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 21:16:22 +0200 Subject: [PATCH 5/7] revert to no withrevert on settlement fee --- certora/confs/SettlementFeeSpread.conf | 1 - certora/specs/SettlementFeeSpread.spec | 10 +++------- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/certora/confs/SettlementFeeSpread.conf b/certora/confs/SettlementFeeSpread.conf index 813802787..73424d39d 100644 --- a/certora/confs/SettlementFeeSpread.conf +++ b/certora/confs/SettlementFeeSpread.conf @@ -12,7 +12,6 @@ "optimistic_loop": true, "loop_iter": 2, "rule_sanity": "basic", - "multi_assert_check": true, "prover_args": [ "-depth 5", "-mediumTimeout 60", diff --git a/certora/specs/SettlementFeeSpread.spec b/certora/specs/SettlementFeeSpread.spec index 27817cf2d..780536a89 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -47,14 +47,10 @@ 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). rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) { uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0; - - // take calls touchMarket (see rule takeCallsTouchMarket), so a reverting touchMarket reverts take too. - // Calling touchMarket here therefore only prunes take paths that revert anyway. - touchMarket(e, offer.market); - bytes32 id = summaryToId(offer.market); - uint256 fee = settlementFee@withrevert(id, timeToMaturity); - assert !lastReverted; + + // take calls touchMarket, so calling settlementFee (in particular checking if the market is touched) doesn't prune meaningful take paths. + uint256 fee = settlementFee(id, timeToMaturity); uint256 buyerAssets; uint256 sellerAssets; From 82398a49377fb717aa6331cd5c83e12c547ced7d Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 21:21:17 +0200 Subject: [PATCH 6/7] improve comments --- certora/specs/OnlyExplicitPayerCanLoseTokens.spec | 4 ++-- certora/specs/SettlementFeeSpread.spec | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/certora/specs/OnlyExplicitPayerCanLoseTokens.spec b/certora/specs/OnlyExplicitPayerCanLoseTokens.spec index fc0bc32cc..2cd7caea6 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. 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 780536a89..a2ffe8012 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -49,7 +49,8 @@ rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0; bytes32 id = summaryToId(offer.market); - // take calls touchMarket, so calling settlementFee (in particular checking if the market is touched) doesn't prune meaningful take paths. + // take calls touchMarket see rule takeCallsTouchMarket. + // Thus calling settlementFee (in particular checking if the market is touched) doesn't prune meaningful take paths. uint256 fee = settlementFee(id, timeToMaturity); uint256 buyerAssets; From 4413199158184c70533ac4bbb69616d0f1fd4253 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 21:22:08 +0200 Subject: [PATCH 7/7] add havoc by default --- certora/confs/SettlementFeeSpread.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/SettlementFeeSpread.conf b/certora/confs/SettlementFeeSpread.conf index 73424d39d..e00080264 100644 --- a/certora/confs/SettlementFeeSpread.conf +++ b/certora/confs/SettlementFeeSpread.conf @@ -13,6 +13,7 @@ "loop_iter": 2, "rule_sanity": "basic", "prover_args": [ + "-havocAllByDefault true", "-depth 5", "-mediumTimeout 60", "-timeout 3600"