From 2d1a0435f5fb08c34a6c7af1031dc6a68069c5d1 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 15 Jun 2026 17:30:31 +0200 Subject: [PATCH 01/11] Rules for netCredit is not decreasing. The netCredit is the credit after updatePendingView minus all future pending fees. This value should never decrease as long as the user is not actively trading on the market or withdrawing the funds. The only notable exception is a liquidate that causes bad debt, so the rule for liquidate assumes no bad debt. --- certora/confs/CreditNondecreasing.conf | 19 ++++++ certora/specs/CreditNondecreasing.spec | 82 ++++++++++++++++++++++++++ 2 files changed, 101 insertions(+) create mode 100644 certora/confs/CreditNondecreasing.conf create mode 100644 certora/specs/CreditNondecreasing.spec diff --git a/certora/confs/CreditNondecreasing.conf b/certora/confs/CreditNondecreasing.conf new file mode 100644 index 00000000..139d4d35 --- /dev/null +++ b/certora/confs/CreditNondecreasing.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/CreditNondecreasing.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", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "msg": "CreditNondecreasing" +} diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec new file mode 100644 index 00000000..7ca9f7ef --- /dev/null +++ b/certora/specs/CreditNondecreasing.spec @@ -0,0 +1,82 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function lossFactor(bytes32 id) external returns (uint128) envfree; + function toId(Midnight.Market) external returns (bytes32) envfree; +} + +/// The up-to-date face value of a lender's position: credit - pendingFee after slashing and fee accrual. +/// The continuous fee cancels out (it is subtracted from both credit and pendingFee), so this only +/// reflects withdrawals, take transfers, and bad-debt slashing via the market loss factor. +function netCredit(env e, Midnight.Market market, address user) returns mathint { + bytes32 id = toId(market); + uint128 credit; + uint128 pending; + uint128 accruedFee; + credit, pending, accruedFee = updatePositionView(e, market, id, user); + return credit - pending; +} + +/// The up-to-date face value of a lender's position (credit - pendingFee) can only decrease by +/// withdrawing, taking, or liquidating. Every other function leaves it unchanged or increases it. +rule creditNondecreasing(env e, method f, calldataarg args, Midnight.Market market, address user) +filtered { + f -> !f.isView + && f.selector != sig:withdraw(Midnight.Market, uint256, address, address).selector + && f.selector != sig:take(Midnight.Offer, bytes, uint256, address, address, address, bytes).selector + && f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector +} { + mathint creditBefore = netCredit(e, market, user); + + f(e, args); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter >= creditBefore; +} + +/// Withdrawing on behalf of another account does not decrease an unrelated user's net credit. +rule withdrawDoesNotDecreaseOtherCredit(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver, address user) { + require user != onBehalf; + + mathint creditBefore = netCredit(e, market, user); + + withdraw(e, market, units, onBehalf, receiver); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter >= creditBefore; +} + +/// Taking does not decrease the net credit of a user that is neither the taker nor the offer's maker. +rule takeDoesNotDecreaseUninvolvedCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { + require user != taker && user != offer.maker; + + mathint creditBefore = netCredit(e, offer.market, user); + + take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + + mathint creditAfter = netCredit(e, offer.market, user); + + assert creditAfter >= creditBefore; +} + +/// Liquidating does not decrease any user's net credit as long as no bad debt is realized, +/// i.e. the market loss factor is unchanged by the liquidation. +rule liquidateWithoutBadDebtDoesNotDecreaseCredit(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, address user) { + bytes32 id = toId(market); + uint128 lossFactorBefore = lossFactor(id); + + mathint creditBefore = netCredit(e, market, user); + + liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + // Restrict to executions in which no bad debt was realized. + require lossFactor(id) == lossFactorBefore; + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter >= creditBefore; +} From 99076fb8e806a5b98b49278fa486eb4e9e6b1ad5 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 15 Jun 2026 17:53:19 +0200 Subject: [PATCH 02/11] Strenghthened property to ==, added pending==0 after maturity --- certora/specs/CreditNondecreasing.spec | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec index 7ca9f7ef..75200027 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/CreditNondecreasing.spec @@ -4,9 +4,16 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function lossFactor(bytes32 id) external returns (uint128) envfree; + function pendingFee(bytes32 id, address user) external returns (uint128) envfree; + function lastAccrual(bytes32 id, address user) external returns (uint128) envfree; function toId(Midnight.Market) external returns (bytes32) envfree; } +/// Once a position has been accrued at or after maturity, its pending fee is fully realized and stays +/// at zero: the continuous fee only accrues up to maturity, so there is nothing left to accrue. +invariant pendingFeeZeroAfterMaturity(Midnight.Market market, address user) + lastAccrual(toId(market), user) >= market.maturity => pendingFee(toId(market), user) == 0; + /// The up-to-date face value of a lender's position: credit - pendingFee after slashing and fee accrual. /// The continuous fee cancels out (it is subtracted from both credit and pendingFee), so this only /// reflects withdrawals, take transfers, and bad-debt slashing via the market loss factor. @@ -34,7 +41,7 @@ filtered { mathint creditAfter = netCredit(e, market, user); - assert creditAfter >= creditBefore; + assert creditAfter == creditBefore; } /// Withdrawing on behalf of another account does not decrease an unrelated user's net credit. @@ -47,7 +54,7 @@ rule withdrawDoesNotDecreaseOtherCredit(env e, Midnight.Market market, uint256 u mathint creditAfter = netCredit(e, market, user); - assert creditAfter >= creditBefore; + assert creditAfter == creditBefore; } /// Taking does not decrease the net credit of a user that is neither the taker nor the offer's maker. @@ -60,7 +67,7 @@ rule takeDoesNotDecreaseUninvolvedCredit(env e, Midnight.Offer offer, bytes rati mathint creditAfter = netCredit(e, offer.market, user); - assert creditAfter >= creditBefore; + assert creditAfter == creditBefore; } /// Liquidating does not decrease any user's net credit as long as no bad debt is realized, @@ -78,5 +85,5 @@ rule liquidateWithoutBadDebtDoesNotDecreaseCredit(env e, Midnight.Market market, mathint creditAfter = netCredit(e, market, user); - assert creditAfter >= creditBefore; + assert creditAfter == creditBefore; } From 5e5c7d9969f444027b2c32dfbe7e8ed25e7e472c Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 15 Jun 2026 18:19:37 +0200 Subject: [PATCH 03/11] Added toId() summary and one missing require --- certora/confs/CreditNondecreasing.conf | 1 + certora/specs/CreditNondecreasing.spec | 25 +++++++++++++++++++++---- 2 files changed, 22 insertions(+), 4 deletions(-) diff --git a/certora/confs/CreditNondecreasing.conf b/certora/confs/CreditNondecreasing.conf index 139d4d35..482db9ec 100644 --- a/certora/confs/CreditNondecreasing.conf +++ b/certora/confs/CreditNondecreasing.conf @@ -1,5 +1,6 @@ { "files": [ + "certora/helpers/Utils.sol", "src/Midnight.sol" ], "verify": "Midnight:certora/specs/CreditNondecreasing.spec", diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec index 75200027..55f41f8b 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/CreditNondecreasing.spec @@ -1,18 +1,25 @@ // SPDX-License-Identifier: GPL-2.0-or-later +using Utils as Utils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function lossFactor(bytes32 id) external returns (uint128) envfree; function pendingFee(bytes32 id, address user) external returns (uint128) envfree; + function creditOf(bytes32 id, address user) external returns (uint128) envfree; function lastAccrual(bytes32 id, address user) external returns (uint128) envfree; function toId(Midnight.Market) external returns (bytes32) envfree; + function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; + + // Deterministic hash preserves market-to-id relationship without adding assumptions. + function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market); } -/// Once a position has been accrued at or after maturity, its pending fee is fully realized and stays -/// at zero: the continuous fee only accrues up to maturity, so there is nothing left to accrue. -invariant pendingFeeZeroAfterMaturity(Midnight.Market market, address user) - lastAccrual(toId(market), user) >= market.maturity => pendingFee(toId(market), user) == 0; +/// SUMMARY FUNCTIONS /// + +function summaryToId(Midnight.Market market) returns (bytes32) { + return Utils.hashMarket(market); +} /// The up-to-date face value of a lender's position: credit - pendingFee after slashing and fee accrual. /// The continuous fee cancels out (it is subtracted from both credit and pendingFee), so this only @@ -22,10 +29,20 @@ function netCredit(env e, Midnight.Market market, address user) returns mathint uint128 credit; uint128 pending; uint128 accruedFee; + require pendingFee(id, user) <= creditOf(id, user), "See pendingContinuousFeeBoundedByCredit in Midnight.spec"; credit, pending, accruedFee = updatePositionView(e, market, id, user); return credit - pending; } +/// INVARIANTS /// + +/// Once a position has been accrued at or after maturity, its pending fee is fully realized and stays +/// at zero: the continuous fee only accrues up to maturity, so there is nothing left to accrue. +invariant pendingFeeZeroAfterMaturity(Midnight.Market market, address user) + lastAccrual(toId(market), user) >= market.maturity => pendingFee(toId(market), user) == 0; + +/// RULES /// + /// The up-to-date face value of a lender's position (credit - pendingFee) can only decrease by /// withdrawing, taking, or liquidating. Every other function leaves it unchanged or increases it. rule creditNondecreasing(env e, method f, calldataarg args, Midnight.Market market, address user) From c42533d800287c3c9775e43d2f46ef67bdccc74d Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 16 Jun 2026 12:27:52 +0200 Subject: [PATCH 04/11] axiomatized mulDiv --- certora/confs/CreditNondecreasing.conf | 3 +- certora/specs/CreditNondecreasing.spec | 58 ++++++++++++++++++++++++-- 2 files changed, 55 insertions(+), 6 deletions(-) diff --git a/certora/confs/CreditNondecreasing.conf b/certora/confs/CreditNondecreasing.conf index 482db9ec..85c137e7 100644 --- a/certora/confs/CreditNondecreasing.conf +++ b/certora/confs/CreditNondecreasing.conf @@ -13,8 +13,7 @@ "hashing_length_bound": 2048, "smt_timeout": 7200, "prover_args": [ - "-destructiveOptimizations twostage", - "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + "-destructiveOptimizations twostage" ], "msg": "CreditNondecreasing" } diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec index 55f41f8b..3abbc48d 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/CreditNondecreasing.spec @@ -13,10 +13,49 @@ methods { // Deterministic hash preserves market-to-id relationship without adding assumptions. function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market); + + // Summarize mulDivDown and mulDivUp to simplify the verification task. + // Use a ghost function that ensures mulDivDown/Up behaves deterministically and add only the axioms about mulDiv that are needed to prove the desired property. + // The axioms are proved in MulDiv.spec. + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); } /// SUMMARY FUNCTIONS /// +persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; + +persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; + +/* Axioms that are proved by MulDiv.spec */ +definition WAD() returns uint256 = 10 ^ 18; + +/* proved in mulDivZero in MulDiv.spec */ +definition axiomDownZero(mathint b, mathint d) returns bool = d > 0 => ghostMulDivDown(0, b, d) == 0; + +definition axiomDownZero2(mathint a, mathint d) returns bool = d > 0 => ghostMulDivDown(a, 0, d) == 0; + +definition axiomUpZero2(mathint a, mathint d) returns bool = d > 0 => ghostMulDivUp(a, 0, d) == 0; + +/* proved in mulDivIdentity in MulDiv.spec */ +definition axiomDownIdentity(mathint a, mathint b) returns bool = b > 0 => ghostMulDivDown(a, b, b) == a; + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(ghostMulDivDown(a, b, d)); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(ghostMulDivUp(a, b, d)); +} + function summaryToId(Midnight.Market market) returns (bytes32) { return Utils.hashMarket(market); } @@ -39,7 +78,14 @@ function netCredit(env e, Midnight.Market market, address user) returns mathint /// Once a position has been accrued at or after maturity, its pending fee is fully realized and stays /// at zero: the continuous fee only accrues up to maturity, so there is nothing left to accrue. invariant pendingFeeZeroAfterMaturity(Midnight.Market market, address user) - lastAccrual(toId(market), user) >= market.maturity => pendingFee(toId(market), user) == 0; + lastAccrual(toId(market), user) >= market.maturity => pendingFee(toId(market), user) == 0 + { + preserved with (env e) { + require(forall mathint b. forall mathint d. axiomDownZero(b, d)), "axiom"; + require(forall mathint a. forall mathint d. axiomDownZero2(a, d)), "axiom"; + require(forall mathint a. forall mathint b. axiomDownIdentity(a, b)), "axiom"; + } + } /// RULES /// @@ -54,6 +100,10 @@ filtered { } { mathint creditBefore = netCredit(e, market, user); + require(forall mathint a. forall mathint d. axiomDownZero2(a, d)), "axiom"; + require(forall mathint a. forall mathint d. axiomUpZero2(a, d)), "axiom"; + require(forall mathint a. forall mathint b. axiomDownIdentity(a, b)), "axiom"; + f(e, args); mathint creditAfter = netCredit(e, market, user); @@ -63,7 +113,7 @@ filtered { /// Withdrawing on behalf of another account does not decrease an unrelated user's net credit. rule withdrawDoesNotDecreaseOtherCredit(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver, address user) { - require user != onBehalf; + require user != onBehalf, "withdrawing for someone else"; mathint creditBefore = netCredit(e, market, user); @@ -76,7 +126,7 @@ rule withdrawDoesNotDecreaseOtherCredit(env e, Midnight.Market market, uint256 u /// Taking does not decrease the net credit of a user that is neither the taker nor the offer's maker. rule takeDoesNotDecreaseUninvolvedCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { - require user != taker && user != offer.maker; + require user != taker && user != offer.maker, "user is not involved in the take"; mathint creditBefore = netCredit(e, offer.market, user); @@ -98,7 +148,7 @@ rule liquidateWithoutBadDebtDoesNotDecreaseCredit(env e, Midnight.Market market, liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); // Restrict to executions in which no bad debt was realized. - require lossFactor(id) == lossFactorBefore; + require lossFactor(id) == lossFactorBefore, "no bad debt realized"; mathint creditAfter = netCredit(e, market, user); From 28d3ddde70c7597fe7f9f6f326f358d643aa3211 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 16 Jun 2026 13:05:46 +0200 Subject: [PATCH 05/11] remove non-linear bottleneck --- certora/specs/CreditNondecreasing.spec | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec index 3abbc48d..16fd4383 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/CreditNondecreasing.spec @@ -19,6 +19,15 @@ methods { // The axioms are proved in MulDiv.spec. function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); + + // Price/fee/health helpers are non-linear (wExp, fee interpolation, oracle math) but only feed + // take()'s prices, settlement fees, and the maker/taker positions. The rules that exercise take + // (takeDoesNotDecreaseUninvolvedCredit) only look at an uninvolved user's position and never the + // market loss factor, so these are irrelevant to the asserted property. NONDET removes the + // non-linearity without weakening what we prove. + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; + function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; } /// SUMMARY FUNCTIONS /// From 18981c0f6c83c3bc3e915427d3c7b4e248f6ef02 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 16 Jun 2026 13:40:43 +0200 Subject: [PATCH 06/11] avoid calling toId twice --- certora/specs/CreditNondecreasing.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec index 16fd4383..e56c9b77 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/CreditNondecreasing.spec @@ -86,8 +86,8 @@ function netCredit(env e, Midnight.Market market, address user) returns mathint /// Once a position has been accrued at or after maturity, its pending fee is fully realized and stays /// at zero: the continuous fee only accrues up to maturity, so there is nothing left to accrue. -invariant pendingFeeZeroAfterMaturity(Midnight.Market market, address user) - lastAccrual(toId(market), user) >= market.maturity => pendingFee(toId(market), user) == 0 +invariant pendingFeeZeroAfterMaturity(Midnight.Market market, bytes32 id, address user) + toId(market) == id && lastAccrual(id, user) >= market.maturity => pendingFee(id, user) == 0 { preserved with (env e) { require(forall mathint b. forall mathint d. axiomDownZero(b, d)), "axiom"; From 9ffc55dbbb3b6caa6a6297b71594c76ec2bd549d Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 18 Jun 2026 14:52:03 +0200 Subject: [PATCH 07/11] Apply suggestions from code review Co-authored-by: Quentin Garchery Signed-off-by: Jochen Hoenicke --- certora/specs/CreditNondecreasing.spec | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec index e56c9b77..7a18d8b1 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/CreditNondecreasing.spec @@ -20,11 +20,7 @@ methods { function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); - // Price/fee/health helpers are non-linear (wExp, fee interpolation, oracle math) but only feed - // take()'s prices, settlement fees, and the maker/taker positions. The rules that exercise take - // (takeDoesNotDecreaseUninvolvedCredit) only look at an uninvolved user's position and never the - // market loss factor, so these are irrelevant to the asserted property. NONDET removes the - // non-linearity without weakening what we prove. + // Over-approximate view functions. function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; @@ -70,8 +66,6 @@ function summaryToId(Midnight.Market market) returns (bytes32) { } /// The up-to-date face value of a lender's position: credit - pendingFee after slashing and fee accrual. -/// The continuous fee cancels out (it is subtracted from both credit and pendingFee), so this only -/// reflects withdrawals, take transfers, and bad-debt slashing via the market loss factor. function netCredit(env e, Midnight.Market market, address user) returns mathint { bytes32 id = toId(market); uint128 credit; @@ -99,7 +93,7 @@ invariant pendingFeeZeroAfterMaturity(Midnight.Market market, bytes32 id, addres /// RULES /// /// The up-to-date face value of a lender's position (credit - pendingFee) can only decrease by -/// withdrawing, taking, or liquidating. Every other function leaves it unchanged or increases it. +/// withdrawing, taking, or liquidating. Every other function leaves it unchanged. rule creditNondecreasing(env e, method f, calldataarg args, Midnight.Market market, address user) filtered { f -> !f.isView From 15c9c0cdcb651ef5dad7240a8657fdc7acd0a707 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 19 Jun 2026 12:50:09 +0200 Subject: [PATCH 08/11] Review comments - use uint256 instead of mathint for ghost function. - allow different market - seller and buyer case for take --- certora/specs/CreditNondecreasing.spec | 114 +++++++++++++++++++------ 1 file changed, 86 insertions(+), 28 deletions(-) diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/CreditNondecreasing.spec index 7a18d8b1..a3d227e9 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/CreditNondecreasing.spec @@ -8,6 +8,8 @@ methods { function pendingFee(bytes32 id, address user) external returns (uint128) envfree; function creditOf(bytes32 id, address user) external returns (uint128) envfree; function lastAccrual(bytes32 id, address user) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; + function continuousFee(bytes32 id) external returns (uint32) envfree; function toId(Midnight.Market) external returns (bytes32) envfree; function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; @@ -28,29 +30,38 @@ methods { /// SUMMARY FUNCTIONS /// -persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint; +persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256; -persistent ghost ghostMulDivUp(mathint, mathint, mathint) returns mathint; +persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; /* Axioms that are proved by MulDiv.spec */ definition WAD() returns uint256 = 10 ^ 18; /* proved in mulDivZero in MulDiv.spec */ -definition axiomDownZero(mathint b, mathint d) returns bool = d > 0 => ghostMulDivDown(0, b, d) == 0; +definition axiomDownZero(uint256 b, uint256 d) returns bool = d > 0 => ghostMulDivDown(0, b, d) == 0; -definition axiomDownZero2(mathint a, mathint d) returns bool = d > 0 => ghostMulDivDown(a, 0, d) == 0; +definition axiomDownZero2(uint256 a, uint256 d) returns bool = d > 0 => ghostMulDivDown(a, 0, d) == 0; -definition axiomUpZero2(mathint a, mathint d) returns bool = d > 0 => ghostMulDivUp(a, 0, d) == 0; +definition axiomUpZero2(uint256 a, uint256 d) returns bool = d > 0 => ghostMulDivUp(a, 0, d) == 0; /* proved in mulDivIdentity in MulDiv.spec */ -definition axiomDownIdentity(mathint a, mathint b) returns bool = b > 0 => ghostMulDivDown(a, b, b) == a; +definition axiomDownIdentity(uint256 a, uint256 b) returns bool = b > 0 => ghostMulDivDown(a, b, b) == a; + +/* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ +definition axiomDownArgLeqDen(uint256 a, uint256 b, uint256 d) returns bool = d > 0 && b <= d => ghostMulDivDown(a, b, d) <= a; + +/* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ +definition axiomUpArgLeqDen(uint256 a, uint256 b, uint256 d) returns bool = d > 0 && a <= d => ghostMulDivUp(a, b, d) <= b; + +/* proved in mulDivResidualBound in MulDiv.spec */ +definition axiomUpResidual(uint256 a, uint256 b, uint256 d) returns bool = a <= d && b <= d => a - ghostMulDivUp(a, b, d) <= d - b; function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { revert(); } - return require_uint256(ghostMulDivDown(a, b, d)); + return ghostMulDivDown(a, b, d); } function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { @@ -58,7 +69,7 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { if (overflow || d == 0) { revert(); } - return require_uint256(ghostMulDivUp(a, b, d)); + return ghostMulDivUp(a, b, d); } function summaryToId(Midnight.Market market) returns (bytes32) { @@ -72,6 +83,7 @@ function netCredit(env e, Midnight.Market market, address user) returns mathint uint128 pending; uint128 accruedFee; require pendingFee(id, user) <= creditOf(id, user), "See pendingContinuousFeeBoundedByCredit in Midnight.spec"; + require lastLossFactor(id, user) <= lossFactor(id), "See lastLossFactorLeqMarketLossFactor in Midnight.spec"; credit, pending, accruedFee = updatePositionView(e, market, id, user); return credit - pending; } @@ -84,17 +96,17 @@ invariant pendingFeeZeroAfterMaturity(Midnight.Market market, bytes32 id, addres toId(market) == id && lastAccrual(id, user) >= market.maturity => pendingFee(id, user) == 0 { preserved with (env e) { - require(forall mathint b. forall mathint d. axiomDownZero(b, d)), "axiom"; - require(forall mathint a. forall mathint d. axiomDownZero2(a, d)), "axiom"; - require(forall mathint a. forall mathint b. axiomDownIdentity(a, b)), "axiom"; + require(forall uint256 b. forall uint256 d. axiomDownZero(b, d)), "axiom"; + require(forall uint256 a. forall uint256 d. axiomDownZero2(a, d)), "axiom"; + require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; } } /// RULES /// -/// The up-to-date face value of a lender's position (credit - pendingFee) can only decrease by +/// The up-to-date face value of a lender's position (credit - pendingFee) can only change by /// withdrawing, taking, or liquidating. Every other function leaves it unchanged. -rule creditNondecreasing(env e, method f, calldataarg args, Midnight.Market market, address user) +rule creditUnaffected(env e, method f, calldataarg args, Midnight.Market market, address user) filtered { f -> !f.isView && f.selector != sig:withdraw(Midnight.Market, uint256, address, address).selector @@ -103,9 +115,9 @@ filtered { } { mathint creditBefore = netCredit(e, market, user); - require(forall mathint a. forall mathint d. axiomDownZero2(a, d)), "axiom"; - require(forall mathint a. forall mathint d. axiomUpZero2(a, d)), "axiom"; - require(forall mathint a. forall mathint b. axiomDownIdentity(a, b)), "axiom"; + require(forall uint256 a. forall uint256 d. axiomDownZero2(a, d)), "axiom"; + require(forall uint256 a. forall uint256 d. axiomUpZero2(a, d)), "axiom"; + require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; f(e, args); @@ -114,44 +126,90 @@ filtered { assert creditAfter == creditBefore; } -/// Withdrawing on behalf of another account does not decrease an unrelated user's net credit. -rule withdrawDoesNotDecreaseOtherCredit(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver, address user) { - require user != onBehalf, "withdrawing for someone else"; +/// Withdrawing on behalf of another account does not change an unrelated user's net credit. +rule withdrawDoesNotChangeOtherCredit(env e, Midnight.Market withdrawMarket, uint256 units, address onBehalf, address receiver, Midnight.Market market, address user) { + require user != onBehalf || toId(withdrawMarket) != toId(market), "withdrawing for someone else or on another market"; + + mathint creditBefore = netCredit(e, market, user); + + withdraw(e, withdrawMarket, units, onBehalf, receiver); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter == creditBefore; +} + +/// Taking does not change the net credit of a user that is neither the taker nor the offer's maker. +rule takeDoesNotChangeUninvolvedCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, Midnight.Market market, address user) { + require (user != taker && user != offer.maker) || toId(offer.market) != toId(market), "user is not involved in the take or another market"; mathint creditBefore = netCredit(e, market, user); - withdraw(e, market, units, onBehalf, receiver); + take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); mathint creditAfter = netCredit(e, market, user); assert creditAfter == creditBefore; } -/// Taking does not decrease the net credit of a user that is neither the taker nor the offer's maker. -rule takeDoesNotDecreaseUninvolvedCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { - require user != taker && user != offer.maker, "user is not involved in the take"; +/// Taking does not decrease the net credit of a buyer in a take. +rule takeDoesNotDecreaseBuyerCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { + require offer.buy ? (user == offer.maker) : (user == taker), "user is the buyer in the take"; + + require(forall uint256 b. forall uint256 d. axiomDownZero(b, d)), "axiom"; + require(forall uint256 a. forall uint256 d. axiomDownZero2(a, d)), "axiom"; + require(forall uint256 a. forall uint256 d. axiomUpZero2(a, d)), "axiom"; + require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; + require(forall uint256 a. forall uint256 b. forall uint256 d. axiomDownArgLeqDen(a, b, d)), "axiom"; + + mathint timeToMaturity = offer.market.maturity > e.block.timestamp ? offer.market.maturity - e.block.timestamp : 0; mathint creditBefore = netCredit(e, offer.market, user); take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + // This follows from continuousFeeBounded in Midnight.sol under the asssumption + // that maturity is not more than 100 years in the future. + // We require it after `take`, because `take` may initialize the market first. + require continuousFee(toId(offer.market)) * timeToMaturity <= WAD(), "continuousFee * timeToMaturity bounded by WAD"; + mathint creditAfter = netCredit(e, offer.market, user); - assert creditAfter == creditBefore; + assert creditAfter >= creditBefore; +} + +/// Taking does not increase the net credit of a seller in a take: the seller is the borrower, who sheds lender +/// credit and takes on debt. +rule takeDoesNotIncreaseSellerCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { + require offer.buy ? (user == taker) : (user == offer.maker), "user is the seller in the take"; + + require(forall uint256 b. forall uint256 d. axiomDownZero(b, d)), "axiom"; + require(forall uint256 a. forall uint256 d. axiomUpZero2(a, d)), "axiom"; + require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; + require(forall uint256 a. forall uint256 b. forall uint256 d. axiomUpArgLeqDen(a, b, d)), "axiom"; + require(forall uint256 a. forall uint256 b. forall uint256 d. axiomUpResidual(a, b, d)), "axiom"; + + mathint creditBefore = netCredit(e, offer.market, user); + + take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + + mathint creditAfter = netCredit(e, offer.market, user); + + assert creditAfter <= creditBefore; } -/// Liquidating does not decrease any user's net credit as long as no bad debt is realized, +/// Liquidating does not change any user's net credit as long as no bad debt is realized, /// i.e. the market loss factor is unchanged by the liquidation. -rule liquidateWithoutBadDebtDoesNotDecreaseCredit(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, address user) { +rule liquidateWithoutBadDebtDoesNotChangeCredit(env e, Midnight.Market liquidateMarket, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, Midnight.Market market, address user) { bytes32 id = toId(market); uint128 lossFactorBefore = lossFactor(id); mathint creditBefore = netCredit(e, market, user); - liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + liquidate(e, liquidateMarket, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); // Restrict to executions in which no bad debt was realized. - require lossFactor(id) == lossFactorBefore, "no bad debt realized"; + require lossFactor(id) == lossFactorBefore || toId(liquidateMarket) != toId(market), "no bad debt realized or on different market"; mathint creditAfter = netCredit(e, market, user); From c9aabd6ffe025fa98d83af7ad791d8909bfc46a2 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 19 Jun 2026 18:00:54 +0200 Subject: [PATCH 09/11] [Certora] net credit refactor (#1001) Signed-off-by: Quentin Garchery --- ...reditNondecreasing.conf => NetCredit.conf} | 5 +- certora/specs/MulDiv.spec | 12 ++ ...reditNondecreasing.spec => NetCredit.spec} | 125 +++++++++--------- 3 files changed, 74 insertions(+), 68 deletions(-) rename certora/confs/{CreditNondecreasing.conf => NetCredit.conf} (77%) rename certora/specs/{CreditNondecreasing.spec => NetCredit.spec} (61%) diff --git a/certora/confs/CreditNondecreasing.conf b/certora/confs/NetCredit.conf similarity index 77% rename from certora/confs/CreditNondecreasing.conf rename to certora/confs/NetCredit.conf index 85c137e7..10f2b302 100644 --- a/certora/confs/CreditNondecreasing.conf +++ b/certora/confs/NetCredit.conf @@ -3,7 +3,7 @@ "certora/helpers/Utils.sol", "src/Midnight.sol" ], - "verify": "Midnight:certora/specs/CreditNondecreasing.spec", + "verify": "Midnight:certora/specs/NetCredit.spec", "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", @@ -12,8 +12,9 @@ "optimistic_hashing": true, "hashing_length_bound": 2048, "smt_timeout": 7200, + "multi_assert_check": true, "prover_args": [ "-destructiveOptimizations twostage" ], - "msg": "CreditNondecreasing" + "msg": "NetCredit" } diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index 16f6c483..1463d792 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -29,6 +29,18 @@ rule mulDivMonotoneD(uint256 a, uint256 b, uint256 d1, uint256 d2) { assert d1 <= d2 => mulDivUp(a, b, d1) >= mulDivUp(a, b, d2); } +// 1-Lipschitz in the first argument when b <= d: the result cannot grow faster than the numerator a. +rule mulDivLipschitzA(uint256 a1, uint256 a2, uint256 b, uint256 d) { + assert b <= d && a1 <= a2 => mulDivDown(a2, b, d) - mulDivDown(a1, b, d) <= a2 - a1; + assert b <= d && a1 <= a2 => mulDivUp(a2, b, d) - mulDivUp(a1, b, d) <= a2 - a1; +} + +// 1-Lipschitz in the second argument when a <= d: the result cannot grow faster than the numerator b. +rule mulDivLipschitzB(uint256 a, uint256 b1, uint256 b2, uint256 d) { + assert a <= d && b1 <= b2 => mulDivDown(a, b2, d) - mulDivDown(a, b1, d) <= b2 - b1; + assert a <= d && b1 <= b2 => mulDivUp(a, b2, d) - mulDivUp(a, b1, d) <= b2 - b1; +} + rule mulDivAddDownDown(uint256 a1, uint256 a2, uint256 b, uint256 d) { uint256 a1plusa2 = require_uint256(a1 + a2); assert mulDivDown(a1, b, d) + mulDivDown(a2, b, d) <= mulDivDown(a1plusa2, b, d); diff --git a/certora/specs/CreditNondecreasing.spec b/certora/specs/NetCredit.spec similarity index 61% rename from certora/specs/CreditNondecreasing.spec rename to certora/specs/NetCredit.spec index a3d227e9..81c1a3e9 100644 --- a/certora/specs/CreditNondecreasing.spec +++ b/certora/specs/NetCredit.spec @@ -18,7 +18,6 @@ methods { // Summarize mulDivDown and mulDivUp to simplify the verification task. // Use a ghost function that ensures mulDivDown/Up behaves deterministically and add only the axioms about mulDiv that are needed to prove the desired property. - // The axioms are proved in MulDiv.spec. function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); @@ -30,31 +29,30 @@ methods { /// SUMMARY FUNCTIONS /// -persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256; +persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256 { + /* proved in mulDivZero in MulDiv.spec */ + axiom forall uint256 b. forall uint256 d. d > 0 => ghostMulDivDown(0, b, d) == 0; + axiom forall uint256 a. forall uint256 d. d > 0 => ghostMulDivDown(a, 0, d) == 0; -persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; + /* proved in mulDivIdentity in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. b > 0 => ghostMulDivDown(a, b, b) == a; -/* Axioms that are proved by MulDiv.spec */ -definition WAD() returns uint256 = 10 ^ 18; - -/* proved in mulDivZero in MulDiv.spec */ -definition axiomDownZero(uint256 b, uint256 d) returns bool = d > 0 => ghostMulDivDown(0, b, d) == 0; - -definition axiomDownZero2(uint256 a, uint256 d) returns bool = d > 0 => ghostMulDivDown(a, 0, d) == 0; - -definition axiomUpZero2(uint256 a, uint256 d) returns bool = d > 0 => ghostMulDivUp(a, 0, d) == 0; + /* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && b <= d => ghostMulDivDown(a, b, d) <= a; +} -/* proved in mulDivIdentity in MulDiv.spec */ -definition axiomDownIdentity(uint256 a, uint256 b) returns bool = b > 0 => ghostMulDivDown(a, b, b) == a; +persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256 { + /* proved in mulDivZero in MulDiv.spec */ + axiom forall uint256 a. forall uint256 d. d > 0 => ghostMulDivUp(a, 0, d) == 0; -/* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ -definition axiomDownArgLeqDen(uint256 a, uint256 b, uint256 d) returns bool = d > 0 && b <= d => ghostMulDivDown(a, b, d) <= a; + /* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && a <= d => ghostMulDivUp(a, b, d) <= b; -/* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ -definition axiomUpArgLeqDen(uint256 a, uint256 b, uint256 d) returns bool = d > 0 && a <= d => ghostMulDivUp(a, b, d) <= b; + /* proved in mulDivResidualBound in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. a <= d && b <= d => a - ghostMulDivUp(a, b, d) <= d - b; +} -/* proved in mulDivResidualBound in MulDiv.spec */ -definition axiomUpResidual(uint256 a, uint256 b, uint256 d) returns bool = a <= d && b <= d => a - ghostMulDivUp(a, b, d) <= d - b; +definition WAD() returns uint256 = 10 ^ 18; function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; @@ -92,21 +90,15 @@ function netCredit(env e, Midnight.Market market, address user) returns mathint /// Once a position has been accrued at or after maturity, its pending fee is fully realized and stays /// at zero: the continuous fee only accrues up to maturity, so there is nothing left to accrue. +/// This implies that the net credit is equal to the credit once a position has been accrued at or after maturity. invariant pendingFeeZeroAfterMaturity(Midnight.Market market, bytes32 id, address user) - toId(market) == id && lastAccrual(id, user) >= market.maturity => pendingFee(id, user) == 0 - { - preserved with (env e) { - require(forall uint256 b. forall uint256 d. axiomDownZero(b, d)), "axiom"; - require(forall uint256 a. forall uint256 d. axiomDownZero2(a, d)), "axiom"; - require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; - } - } + toId(market) == id && lastAccrual(id, user) >= market.maturity => pendingFee(id, user) == 0; /// RULES /// /// The up-to-date face value of a lender's position (credit - pendingFee) can only change by /// withdrawing, taking, or liquidating. Every other function leaves it unchanged. -rule creditUnaffected(env e, method f, calldataarg args, Midnight.Market market, address user) +rule netCreditUnaffected(env e, method f, calldataarg args, Midnight.Market market, address user) filtered { f -> !f.isView && f.selector != sig:withdraw(Midnight.Market, uint256, address, address).selector @@ -115,10 +107,6 @@ filtered { } { mathint creditBefore = netCredit(e, market, user); - require(forall uint256 a. forall uint256 d. axiomDownZero2(a, d)), "axiom"; - require(forall uint256 a. forall uint256 d. axiomUpZero2(a, d)), "axiom"; - require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; - f(e, args); mathint creditAfter = netCredit(e, market, user); @@ -127,7 +115,7 @@ filtered { } /// Withdrawing on behalf of another account does not change an unrelated user's net credit. -rule withdrawDoesNotChangeOtherCredit(env e, Midnight.Market withdrawMarket, uint256 units, address onBehalf, address receiver, Midnight.Market market, address user) { +rule withdrawDoesNotChangeOtherNetCredit(env e, Midnight.Market withdrawMarket, uint256 units, address onBehalf, address receiver, Midnight.Market market, address user) { require user != onBehalf || toId(withdrawMarket) != toId(market), "withdrawing for someone else or on another market"; mathint creditBefore = netCredit(e, market, user); @@ -139,8 +127,19 @@ rule withdrawDoesNotChangeOtherCredit(env e, Midnight.Market withdrawMarket, uin assert creditAfter == creditBefore; } +/// Withdrawing cannot increase net credit. +rule withdrawNetCreditNonIncreasing(env e, Midnight.Market withdrawMarket, uint256 units, address onBehalf, address receiver, Midnight.Market market, address user) { + mathint creditBefore = netCredit(e, market, user); + + withdraw(e, withdrawMarket, units, onBehalf, receiver); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter <= creditBefore; +} + /// Taking does not change the net credit of a user that is neither the taker nor the offer's maker. -rule takeDoesNotChangeUninvolvedCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, Midnight.Market market, address user) { +rule takeDoesNotChangeOtherNetCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, Midnight.Market market, address user) { require (user != taker && user != offer.maker) || toId(offer.market) != toId(market), "user is not involved in the take or another market"; mathint creditBefore = netCredit(e, market, user); @@ -152,16 +151,8 @@ rule takeDoesNotChangeUninvolvedCredit(env e, Midnight.Offer offer, bytes ratifi assert creditAfter == creditBefore; } -/// Taking does not decrease the net credit of a buyer in a take. -rule takeDoesNotDecreaseBuyerCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { - require offer.buy ? (user == offer.maker) : (user == taker), "user is the buyer in the take"; - - require(forall uint256 b. forall uint256 d. axiomDownZero(b, d)), "axiom"; - require(forall uint256 a. forall uint256 d. axiomDownZero2(a, d)), "axiom"; - require(forall uint256 a. forall uint256 d. axiomUpZero2(a, d)), "axiom"; - require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; - require(forall uint256 a. forall uint256 b. forall uint256 d. axiomDownArgLeqDen(a, b, d)), "axiom"; - +/// Taking does not decrease the net credit of a buyer in a take, and does not increase the net credit of a seller in a take. +rule takeNetCreditChangeForBuyerAndSeller(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { mathint timeToMaturity = offer.market.maturity > e.block.timestamp ? offer.market.maturity - e.block.timestamp : 0; mathint creditBefore = netCredit(e, offer.market, user); @@ -175,27 +166,10 @@ rule takeDoesNotDecreaseBuyerCredit(env e, Midnight.Offer offer, bytes ratifierD mathint creditAfter = netCredit(e, offer.market, user); - assert creditAfter >= creditBefore; -} - -/// Taking does not increase the net credit of a seller in a take: the seller is the borrower, who sheds lender -/// credit and takes on debt. -rule takeDoesNotIncreaseSellerCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { - require offer.buy ? (user == taker) : (user == offer.maker), "user is the seller in the take"; - - require(forall uint256 b. forall uint256 d. axiomDownZero(b, d)), "axiom"; - require(forall uint256 a. forall uint256 d. axiomUpZero2(a, d)), "axiom"; - require(forall uint256 a. forall uint256 b. axiomDownIdentity(a, b)), "axiom"; - require(forall uint256 a. forall uint256 b. forall uint256 d. axiomUpArgLeqDen(a, b, d)), "axiom"; - require(forall uint256 a. forall uint256 b. forall uint256 d. axiomUpResidual(a, b, d)), "axiom"; - - mathint creditBefore = netCredit(e, offer.market, user); - - take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - - mathint creditAfter = netCredit(e, offer.market, user); - - assert creditAfter <= creditBefore; + address buyer = offer.buy ? offer.maker : taker; + address seller = offer.buy ? taker : offer.maker; + assert user == buyer => creditAfter >= creditBefore; + assert user == seller => creditAfter <= creditBefore; } /// Liquidating does not change any user's net credit as long as no bad debt is realized, @@ -215,3 +189,22 @@ rule liquidateWithoutBadDebtDoesNotChangeCredit(env e, Midnight.Market liquidate assert creditAfter == creditBefore; } + +/// Liquidation cannot increase net credit. +rule liquidateNetCreditNonIncreasing(env e, Midnight.Market liquidateMarket, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, Midnight.Market market, address user) { + mathint creditBefore = netCredit(e, market, user); + + require forall uint256 a. forall uint256 b1. forall uint256 b2. forall uint256 d. d > 0 => b1 <= b2 => ghostMulDivUp(a, b1, d) <= ghostMulDivUp(a, b2, d), "See mulDivMonotoneB in MulDiv.spec"; + require forall uint256 a. forall uint256 b1. forall uint256 b2. forall uint256 d. d > 0 => a <= d => b2 <= b1 => ghostMulDivUp(a, b1, d) - ghostMulDivUp(a, b2, d) <= b1 - b2, "See mulDivLipschitzB in MulDiv.spec"; + require forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => b <= d => ghostMulDivUp(a, b, d) <= a, "See mulDivArgumentLesserThanDenominator in MulDiv.spec"; + + require forall uint256 a. forall uint256 b1. forall uint256 b2. forall uint256 d. d > 0 => b1 <= b2 => ghostMulDivDown(a, b1, d) <= ghostMulDivDown(a, b2, d), "See mulDivMonotoneB in MulDiv.spec"; + require forall uint256 a1. forall uint256 a2. forall uint256 b. forall uint256 d. d > 0 => a1 <= a2 => ghostMulDivDown(a1, b, d) <= ghostMulDivDown(a2, b, d), "See mulDivMonotoneA in MulDiv.spec"; + require forall uint256 a1. forall uint256 a2. forall uint256 b. forall uint256 d. d > 0 => b <= d => a1 <= a2 => ghostMulDivDown(a2, b, d) - ghostMulDivDown(a1, b, d) <= a2 - a1, "See mulDivLipschitzA in MulDiv.spec"; + + liquidate(e, liquidateMarket, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter <= creditBefore; +} From 088ced4d9b14af9dabc2ff4aaf26b00475e7ddb8 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 19 Jun 2026 18:04:07 +0200 Subject: [PATCH 10/11] Apply suggestions from code review Co-authored-by: Jochen Hoenicke Signed-off-by: Jochen Hoenicke --- certora/specs/NetCredit.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/NetCredit.spec b/certora/specs/NetCredit.spec index 81c1a3e9..0b3ff386 100644 --- a/certora/specs/NetCredit.spec +++ b/certora/specs/NetCredit.spec @@ -172,7 +172,7 @@ rule takeNetCreditChangeForBuyerAndSeller(env e, Midnight.Offer offer, bytes rat assert user == seller => creditAfter <= creditBefore; } -/// Liquidating does not change any user's net credit as long as no bad debt is realized, +/// Liquidating does not change any user's net credit as long as no bad debt is realized on the same market, /// i.e. the market loss factor is unchanged by the liquidation. rule liquidateWithoutBadDebtDoesNotChangeCredit(env e, Midnight.Market liquidateMarket, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, Midnight.Market market, address user) { bytes32 id = toId(market); @@ -182,7 +182,7 @@ rule liquidateWithoutBadDebtDoesNotChangeCredit(env e, Midnight.Market liquidate liquidate(e, liquidateMarket, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - // Restrict to executions in which no bad debt was realized. + // Restrict to executions in which no bad debt was realized or that are on other markets. require lossFactor(id) == lossFactorBefore || toId(liquidateMarket) != toId(market), "no bad debt realized or on different market"; mathint creditAfter = netCredit(e, market, user); From 64da25e7d9b3be3296d663689bee1d882ea0994e Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 19 Jun 2026 20:27:30 +0200 Subject: [PATCH 11/11] Require MAX_CONTINUOUS_FEE and MAX_TTM separately --- certora/specs/NetCredit.spec | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/certora/specs/NetCredit.spec b/certora/specs/NetCredit.spec index 0b3ff386..bba6916b 100644 --- a/certora/specs/NetCredit.spec +++ b/certora/specs/NetCredit.spec @@ -27,6 +27,16 @@ methods { function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; } +/// HELPERS /// + +definition MAX_CONTINUOUS_FEE() returns uint256 = 317097919; + +definition MAX_TTM() returns mathint = 100 * 365 * 86400; + +definition WAD() returns uint256 = 10 ^ 18; + +definition zeroFloorSub(uint256 a, uint256 b) returns mathint = a >= b ? a - b : 0; + /// SUMMARY FUNCTIONS /// persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256 { @@ -52,8 +62,6 @@ persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256 { axiom forall uint256 a. forall uint256 b. forall uint256 d. a <= d && b <= d => a - ghostMulDivUp(a, b, d) <= d - b; } -definition WAD() returns uint256 = 10 ^ 18; - function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; if (overflow || d == 0) { @@ -153,16 +161,14 @@ rule takeDoesNotChangeOtherNetCredit(env e, Midnight.Offer offer, bytes ratifier /// Taking does not decrease the net credit of a buyer in a take, and does not increase the net credit of a seller in a take. rule takeNetCreditChangeForBuyerAndSeller(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { - mathint timeToMaturity = offer.market.maturity > e.block.timestamp ? offer.market.maturity - e.block.timestamp : 0; - mathint creditBefore = netCredit(e, offer.market, user); take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - // This follows from continuousFeeBounded in Midnight.sol under the asssumption - // that maturity is not more than 100 years in the future. // We require it after `take`, because `take` may initialize the market first. - require continuousFee(toId(offer.market)) * timeToMaturity <= WAD(), "continuousFee * timeToMaturity bounded by WAD"; + require continuousFee(toId(offer.market)) <= MAX_CONTINUOUS_FEE(), "See continuousFeeBounded in Midnight.sol"; + require offer.market.maturity <= e.block.timestamp + MAX_TTM(), "Maturity not too far in the future"; + assert continuousFee(toId(offer.market)) * zeroFloorSub(offer.market.maturity, e.block.timestamp) <= WAD(), "interest <= 100%"; mathint creditAfter = netCredit(e, offer.market, user);