From 9963194734b86047719cd7f140dd9f15a12c4115 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 13 Jul 2026 13:38:39 +0200 Subject: [PATCH 01/11] Spec: SumOfCredits equals TotalUnits plus Fees. This is the main solvency invariant: the totalUnits equals the correctly scaled sums of all position credit plus fee. Together with the invariant from Midnight.spec that totalUnits equals the sum of all debts plus the withdrawable amount, this shows that all credits are backed by debt. --- certora/confs/SumOfCreditsAxiomatic.conf | 23 ++ certora/confs/UpdatePositionView.conf | 27 ++ certora/specs/SumOfCreditsAxiomatic.spec | 405 +++++++++++++++++++++++ certora/specs/UpdatePositionView.spec | 178 ++++++++++ 4 files changed, 633 insertions(+) create mode 100644 certora/confs/SumOfCreditsAxiomatic.conf create mode 100644 certora/confs/UpdatePositionView.conf create mode 100644 certora/specs/SumOfCreditsAxiomatic.spec create mode 100644 certora/specs/UpdatePositionView.spec diff --git a/certora/confs/SumOfCreditsAxiomatic.conf b/certora/confs/SumOfCreditsAxiomatic.conf new file mode 100644 index 000000000..56d5fb56d --- /dev/null +++ b/certora/confs/SumOfCreditsAxiomatic.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "parametric_contracts": [ + "Midnight" + ], + "verify": "Midnight:certora/specs/SumOfCreditsAxiomatic.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, + "build_cache": true, + "prover_args": [ + "-destructiveOptimizations twostage -depth 2" + ], + "rule_sanity": "basic", + "smt_timeout": 7200, + "msg": "SumOfCredits" +} diff --git a/certora/confs/UpdatePositionView.conf b/certora/confs/UpdatePositionView.conf new file mode 100644 index 000000000..5d723332d --- /dev/null +++ b/certora/confs/UpdatePositionView.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/UpdatePositionView.spec", + "parametric_contracts": ["Midnight"], + "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, + "multi_assert_check": true, + "build_cache": true, + "smt_timeout": 600, + "prover_args": [ + "-destructiveOptimizations twostage", + "-backendStrategy singleRace", + "-smt_useLIA false", + "-smt_useNIA true", + "-depth 0", + "-smt_skipDelayedSolvers false", + "-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": "Update Position View" +} diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec new file mode 100644 index 000000000..efb7a2d15 --- /dev/null +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -0,0 +1,405 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function creditOf(bytes32 id, address user) external returns (uint128) envfree; + function totalUnits(bytes32 id) external returns (uint128) envfree; + function continuousFeeCredit(bytes32 id) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; + function lossFactor(bytes32) external returns (uint128) envfree; + + /// SUMMARY OF updatePositionView -- see file header for soundness argument. /// + function Midnight.updatePositionView(Midnight.Market memory obligation, bytes32 id, address user) internal returns (uint128, uint128, uint128) with(env e) => summaryUpdatePositionView(e, id, user); + + /// PRICE / ORACLE /// + function _.price() external => NONDET; + + /// MUL/DIV — exact mathint summaries (still needed for the parts of + /// withdraw / take outside `updatePositionView`, e.g. the proportional + /// pendingFee adjustment and the take buyer-fee accrual). + 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); + + /// MISC INTERNALS irrelevant to credit / loss-index tracking. /// + function toId(Midnight.Market) external returns (bytes32) => NONDET; + function IdLib.toId(Midnight.Market memory, uint256, address) internal returns (bytes32) => NONDET; + function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET; + function touchMarket(Midnight.Market) external returns (bytes32) => NONDET; + function Midnight.touchMarket(Midnight.Market memory) internal returns (bytes32) => 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 TickLib.wExp(int256) internal returns (uint256) => NONDET; + function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET; + function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET; + function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; + function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; + + /// SAFE TRANSFERS /// + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + + /// EXTERNAL CALLBACKS — prevent havoc of ghosts on unresolved calls in `take` / + /// `liquidate` / `flashLoan`. Signatures MUST match the real callbacks exactly + /// (ICallbacks.sol / IRatifier.sol); a mismatched arg list yields a different + /// selector, so the `_.` summary does NOT apply and the call falls through to + /// AUTO => DEFAULT HAVOC, which havocs the (non-persistent) credit ghosts. + function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; + function _.isRatified(Midnight.Offer, bytes) external => NONDET; + function _.canIncreaseCredit(address) external => NONDET; + function _.canIncreaseDebt(address) external => NONDET; + function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; + function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; + + /// EXTERNAL TOKEN CALLS — defensive, redundant with SafeTransferLib NONDET. /// + function _.transfer(address, uint256) external => NONDET; + function _.transferFrom(address, address, uint256) external => NONDET; +} + +/// MULDIV FUNCTION SUMMARIES — axiomatic (deterministic ghost + rounding bound) instead of the exact +/// `a*b/d`, to avoid a nonlinear division term at every call site. The only invariant-relevant mulDiv is +/// liquidate's loss-index update (Midnight.sol:591) and the continuousFeeCredit slash (Midnight.sol:597), +/// both of which need only the rounds-down bound `result*d <= a*b` (proved in MulDiv.spec:mulDivDownRoundsDown). +/// mulDivUp's calls here feed badDebt / pendingFee, whose exact values are immaterial to sumOfCreditsBody, +/// so it needs no bound (a bare deterministic ghost suffices). +persistent ghost mulDivDownGhost(mathint, mathint, mathint) returns mathint { + axiom forall mathint a. forall mathint b. forall mathint d. mulDivDownGhost(a, b, d) >= 0; + axiom forall mathint a. forall mathint d. d > 0 => mulDivDownGhost(a, 0, d) == 0; + axiom forall mathint b. forall mathint d. d > 0 => mulDivDownGhost(0, b, d) == 0; + + // RAW-arithmetic form only (not also a multiply-wrapped duplicate): liquidate's + // closing argument grounds sum*M and (tu-cf)*PRECISION to real arithmetic (single, + // non-aggregate products -- cheap; see the liquidate rule), and lossFactorLeqLastLossFactor + // compares raw mapIndex values directly, never through `multiply`. Keeping only one + // form avoids giving the solver two redundant bounds to case on at the same call sites. + axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(d, mulDivDownGhost(a, b, d)) <= multiply(b, a); + axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(mulDivDownGhost(a, b, d), d) <= multiply(a, b); +} + +persistent ghost mulDivUpGhost(mathint, mathint, mathint) returns mathint { + axiom forall mathint a. forall mathint b. forall mathint d. mulDivUpGhost(a, b, d) >= 0; +} + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(mulDivDownGhost(a, b, d)); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(mulDivUpGhost(a, b, d)); +} + +/// GHOSTS /// + +persistent ghost mathint PRECISION { + axiom PRECISION > 0; +} + +ghost mapping(bytes32 => mathint) sumPreciseCreditDivIndex { + init_state axiom forall bytes32 id. sumPreciseCreditDivIndex[id] == 0; + axiom forall bytes32 id. sumPreciseCreditDivIndex[id] >= 0; +} + +ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { + init_state axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] == 0; + axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] >= 0; +} + +// `multiply(a, b)` IS the product `a * b` declared as an uninterpreted function. +persistent ghost multiply(mathint, mathint) returns mathint { + axiom forall mathint a. forall mathint b. (a > 0 && b > 0) => multiply(a, b) > 0; + axiom forall mathint a. multiply(a, 0) == 0; + axiom forall mathint b. multiply(0, b) == 0; +} + +// Distributivity axiom. +definition axiomDistributivity(mathint a, mathint b, mathint c) returns bool = multiply(a + b, c) == multiply(a, c) + multiply(b, c); + +// Symmetry axiom over associativity. +definition axiomAssocComm(mathint a, mathint b, mathint c) returns bool = multiply(multiply(a, b), c) == multiply(multiply(a, c), b); + +// Linear order axiom for multiplication with nonnegative constants. +definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c >= 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); + +/// HELPER DEFINITIONS /// + +definition mapIndex(mathint index) returns mathint = 2 ^ 128 - 1 - index; + +definition cvlCreditOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; + +definition cvlLastLossFactor(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastLossFactor; + +definition cvlPendingFeeOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].pendingFee; + +definition cvlLastAccrualOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastAccrual; + +// Body of the strong invariant. The aggregate product is routed through the +// uninterpreted `multiply` (== sumPreciseCreditDivIndex[id] * mapIndex(...)). +definition sumOfCreditsBody(bytes32 id) returns bool = multiply(sumPreciseCreditDivIndex[id], mapIndex(lossFactor(id))) <= multiply(totalUnits(id), PRECISION) - multiply(continuousFeeCredit(id), PRECISION); + +/// HOOKS /// + +function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint128 newIndex) { + mathint ownerLossIndex = mapIndex(newIndex); + mathint oldD = preciseCreditDivIndex[id][owner]; + mathint value; + + // We require there is a value such that + // value * ownerLossIndex == newCredit * PRECISION. + // This is sound because we can assume PRECISION to be large enough to + // be divisible by ownerLossIndex. + require multiply(value, ownerLossIndex) == multiply(newCredit, PRECISION), "PRECISION is divisible by ownerLossIndex"; + + mathint newD = (ownerLossIndex == 0 || newCredit == 0) ? 0 : value; + preciseCreditDivIndex[id][owner] = newD; + mathint oldSum = sumPreciseCreditDivIndex[id]; + sumPreciseCreditDivIndex[id] = oldSum + newD - oldD; + + // require distributivity axioms to help prover + mathint lossIndex = mapIndex(lossFactor(id)); + require axiomDistributivity(oldSum, newD, lossIndex), "axiom"; + require axiomDistributivity(oldSum + newD - oldD, oldD, lossIndex), "axiom"; +} + +function checkCreditDivInvariant(bytes32 id, address owner) returns bool { + uint128 credit = cvlCreditOf(id, owner); + uint128 userIndex = cvlLastLossFactor(id, owner); + mathint mappedIndex = mapIndex(userIndex); + + // Per-user invariant stays in REAL-product form: it is per-user (cheap) and + // the hook's division-exactness genuinely needs real arithmetic. Abstracting + // it to multiply weakened this ASSUMED invariant enough to make a + // fully-slashed store (mapIndex==0, credit!=0) reachable, breaking the hook + // assert. Only the AGGREGATE (sumOfCreditsBody) is abstracted. + return mappedIndex == 0 || credit == 0 ? preciseCreditDivIndex[id][owner] == 0 : multiply(preciseCreditDivIndex[id][owner], mappedIndex) == multiply(credit, PRECISION); +} + +hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit (uint128 oldCredit) { + updateCreditDivIndex(id, owner, newCredit, cvlLastLossFactor(id, owner)); + if (newCredit > oldCredit) { + require axiomDistributivity(oldCredit, newCredit - oldCredit, PRECISION), "axiom"; + } else { + require axiomDistributivity(newCredit, oldCredit - newCredit, PRECISION), "axiom"; + } +} + +hook Sstore position[KEY bytes32 id][KEY address owner].lastLossFactor uint128 newIndex (uint128 oldIndex) { + updateCreditDivIndex(id, owner, cvlCreditOf(id, owner), newIndex); +} + +hook Sstore marketState[KEY bytes32 id].totalUnits uint128 newTotal (uint128 oldTotal) { + if (newTotal > oldTotal) { + require axiomDistributivity(oldTotal, newTotal - oldTotal, PRECISION), "axiom"; + } else { + require axiomDistributivity(newTotal, oldTotal - newTotal, PRECISION), "axiom"; + } +} + +/// SUMMARY OF updatePositionView /// +// +// Returns nondet (newCredit, newPendingFee, fee) constrained by the +// inequalities proved in UpdatePositionView.spec +// (rule `updatePositionViewReflectedByIndex`). +function summaryUpdatePositionView(env e, bytes32 id, address user) returns (uint128, uint128, uint128) { + uint128 oldCredit = cvlCreditOf(id, user); + uint128 oldPendingFee = cvlPendingFeeOf(id, user); + uint128 oldLastAccrual = cvlLastAccrualOf(id, user); + + require to_mathint(e.block.timestamp) >= to_mathint(oldLastAccrual), "time is non-decreasing"; + + uint128 newCredit; + uint128 newPendingFee; + uint128 fee; + + require newCredit <= oldCredit, "slashing only decreases credit"; + require newPendingFee <= oldPendingFee, "fee deduction only decreases pending"; + require fee <= oldPendingFee, "fee bounded by pending (UpdatePositionView.spec)"; + + // The touched user's pre-term lower bound (updatePositionView slashing bound). + // Kept in REAL-product form (per-user, cheap); the rule grounds the matching + // multiply(Dpre, M) to this same product. + //require (newCredit + fee) * PRECISION <= preciseCreditDivIndex[id][user] * mapIndex(lossFactor(id)), "newCredit (with fees) bounded by precise credit (UpdatePositionView.spec)"; + require multiply(newCredit, PRECISION) + multiply(fee, PRECISION) <= multiply(preciseCreditDivIndex[id][user], mapIndex(lossFactor(id))), "newCredit (with fees) bounded by precise credit (UpdatePositionView.spec)"; + + // A fully-slashed user (lossIndex == max, mapIndex == 0) gets credit and fee 0: updatePositionView's + // postSlashCredit ternary returns 0 when _lossIndex == max (Midnight.sol:752), and postSlashPending/fee + // then collapse to 0 too. Without this the summary admits newCredit > 0 for a fully-slashed user, which + // breaks the "division is exact" hook (0 == newCredit * PRECISION). + require mapIndex(cvlLastLossFactor(id, user)) == 0 => (newCredit == 0 && fee == 0), "fully-slashed user gets 0 credit/fee (updatePositionView _lossIndex == max guard)"; + + // Fully-slashed OBLIGATION also forces 0, independent of whether this user's own + // lastLossFactor has synced yet: postSlashCredit = credit.mulDivDown(mapIndex(lossFactor(id)), + // mapIndex(_lastLossFactor)) (Midnight.sol:820-821) has a ZERO NUMERATOR whenever + // mapIndex(lossFactor(id)) == 0, so mulDivDown returns exactly 0 regardless of the + // (nonzero) divisor -- and postSlashPendingFee/fee then cascade to 0 too (L824-830). + // Without this, a "stale" user (obligation fully slashed, user not yet synced) can + // leak nonzero newCredit/fee through the summary. + require mapIndex(lossFactor(id)) == 0 => (newCredit == 0 && fee == 0), "fully-slashed obligation gets 0 credit/fee regardless of user sync (mulDivDown zero-numerator)"; + + // help solver to reason about fee and distributivity. + require axiomDistributivity(fee, continuousFeeCredit(id), PRECISION), "axiom"; + + return (newCredit, newPendingFee, fee); +} + +/// INVARIANTS /// + +strong invariant preciseCreditCorrect(bytes32 id, address owner) + checkCreditDivInvariant(id, owner); + +strong invariant lossFactorLeqLastLossFactor(bytes32 id, address owner) + mapIndex(lossFactor(id)) <= mapIndex(cvlLastLossFactor(id, owner)) + { + preserved liquidate(Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) with (env e) { + require forall mathint a. forall mathint b. forall mathint d. b <= d => mulDivDownGhost(a, b, d) <= a, "see mulDivArgumentLesserThanDenominator in MulDiv.spec"; + } + } + +// Parametric coverage of the sum invariant for all methods EXCEPT withdraw and +// take, which are handled by their dedicated rules (sumOfCreditsLeTotalUnits_withdraw +// here, and the SumOfCreditsSummaryTake.spec split for take). +strong invariant sumOfCreditsLeTotalUnits(bytes32 id) + sumOfCreditsBody(id) + filtered { f -> 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 } { + preserved claimContinuousFee(Midnight.Market market, uint256 amount, address receiver) with (env e) { + require axiomDistributivity(continuousFeeCredit(id) - amount, amount, PRECISION); + require axiomDistributivity(totalUnits(id) - amount, amount, PRECISION); + } + + preserved updatePosition(Midnight.Market market, address user) with (env e) { + requireInvariant preciseCreditCorrect(id, user); + requireInvariant lossFactorLeqLastLossFactor(id, user); + } + + preserved withdraw(Midnight.Market market, uint256 units, address onBehalf, address receiver) with (env e) { + requireInvariant preciseCreditCorrect(id, onBehalf); + requireInvariant lossFactorLeqLastLossFactor(id, onBehalf); + } + } + +// LIQUIDATE — the OPPOSITE of withdraw/take for multiply. Liquidate never +// calls _updatePosition or touches any user's credit (it writes the *obligation* +// lossFactor, not per-user position.lastLossFactor), so no hook fires and `sum` is +// UNCHANGED. Instead the obligation factor M rescales: +// mapIndex(new) = mulDivDown(mapIndex(old), tu - badDebt, tu) (Midnight.sol:589) +// continuousFeeCredit_new = mulDivDown(cf_old, mapIndex(new), mapIndex(old)) (L594) +// tu_new = tu_old - badDebt (L593) +// The aggregate `multiply(sum, M)` therefore changes via its 2ND argument, +// which additivity cannot express. So here we do the inverse of withdraw/take: +// GROUND the aggregate back to a real product (pre and post). That re-exposes +// sum*M_old and sum*M_new, but liquidate ALREADY discharges those via the +// mulDivDownGhost rounds-down bound (it verifies in the parametric invariant), +// and `sum` is a single snapshot here (not the touched-user delta), so the +// withdraw-style NIA divergence does not occur. +rule sumOfCreditsLeTotalUnits_liquidate(bytes32 id, env e, Midnight.Market obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { + require sumOfCreditsBody(id); + requireInvariant preciseCreditCorrect(id, borrower); + requireInvariant lossFactorLeqLastLossFactor(id, borrower); + + mathint sumPre = sumPreciseCreditDivIndex[id]; + mathint indexPre = mapIndex(lossFactor(id)); + mathint tuPre = totalUnits(id); + mathint cfPre = continuousFeeCredit(id); + + liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + mathint indexPost = mapIndex(lossFactor(id)); + mathint tuPost = totalUnits(id); + mathint cfPost = continuousFeeCredit(id); + + // Real fact (Midnight.sol:649): tuPost==tuPre-badDebt whenever liquidate's update block + // ran (badDebt>0); when badDebt==0 the block is skipped entirely and tuPost==tuPre, so + // this identity still gives badDebt==0 correctly either way. + mathint badDebt = tuPre - tuPost; + + // (C): linear combination of (A) and rearranged (B) (add (A) to -1*(B), i.e. + // cfPre*indexPost-cfPost*indexPre>=0), then factor via subtraction-distributivity -- both terms + // on each side share the SAME second argument (indexPost for the tuPre/cfPre pair, indexPre for + // tuPost/cfPost), which is exactly the shape multiply(a,m)-multiply(b,m)==multiply(a-b,m) + // needs, so this needs no cancellation, only the additivity already established. + require axiomDistributivity(cfPre, tuPre - cfPre, indexPost); + require axiomDistributivity(cfPost, tuPost - cfPost, indexPre); + require axiomDistributivity(tuPre - cfPre, cfPre, PRECISION); + require axiomDistributivity(tuPost - cfPost, cfPost, PRECISION); + + // The proof requires several steps: + + // From mulDiv axioms for indexPost = indexPre.mulDivDown(tuPost, tuPre): + // tuPre * indexPost <= tuPost * indexPre + // From mulDiv axiom for cfPost = cfPre.mulDivDown(indexPost, indexPre): + // cfPost * indexPre <= cfPre * indexPost + // Using distributivity above: + // (tuPre - cfPre) * indexPost <= (tuPost - cfPost) * indexPre (A) + + // Then the main proof is: + // sumPre * indexPre <= (tuPre - cfPre) * PRECISION (sumOfCreditBody Pre) + // <=> { indexPost >= 0} + // sumPre * indexPre * indexPost <= (tuPre - cfPre) * PRECISION * indexPost + // <=> { 2x associative commutative } + // sumPre * indexPost * indexPre <= (tuPre - cfPre) * indexPost * PRECISION + // <=> { (A) multiplied with PRECISION >= 0 } + // sumPre * indexPost * indexPre <= (tuPost - cfPost) * indexPre * PRECISION + // <=> { associative, commutative } + // sumPre * indexPost * indexPre <= (tuPost - cfPost) * PRECISION * indexPre + // <=> { divide by indexPre >= 0} + // sumPre * indexPost <= (tuPost - cfPost) * PRECISION (sumOfCreditBody Post) + + // These are the axioms used in the proof above + require axiomLeMulPos(multiply(sumPre, indexPre), multiply(tuPre - cfPre, PRECISION), indexPost); + require axiomAssocComm(sumPre, indexPre, indexPost); + require axiomAssocComm(tuPre - cfPre, PRECISION, indexPost); + require axiomLeMulPos(multiply(tuPre - cfPre, indexPost), multiply(tuPost - cfPost, indexPre), PRECISION); + require axiomAssocComm(tuPost - cfPost, indexPre, PRECISION); + require axiomLeMulPos(multiply(sumPre, indexPost), multiply(tuPost - cfPost, PRECISION), indexPre); + + assert sumOfCreditsBody(id); +} + +rule sumOfCreditsLeTotalUnits_take(bytes32 id, env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { + require sumOfCreditsBody(id); + + // Determine buyer and seller + address buyer = offer.buy ? offer.maker : taker; + address seller = offer.buy ? taker : offer.maker; + + requireInvariant preciseCreditCorrect(id, taker); + requireInvariant lossFactorLeqLastLossFactor(id, taker); + requireInvariant preciseCreditCorrect(id, offer.maker); + requireInvariant lossFactorLeqLastLossFactor(id, offer.maker); + + mathint tuPre = totalUnits(id); + mathint debtPre_b = currentContract.position[id][buyer].debt; + + take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); + mathint creditPost_b = currentContract.position[id][buyer].credit; + mathint creditPost_s = currentContract.position[id][seller].credit; + mathint tuPost = totalUnits(id); + + // Compute the buyer credit increase. Note that updatePosition does + // not touch debt, so we can use this formula from Midnight. + mathint buyerCreditIncrease = units > debtPre_b ? units - debtPre_b : 0; + + // We do not have the credit of seller after updatePosition before take, + // but we can compute sellerCreditDecrease from totalUnits change. + mathint sellerCreditDecrease = tuPre + buyerCreditIncrease - tuPost; + + // These distributivity axiom is needed because Midnight adds buyer and + // seller credit at the same time. + if (buyerCreditIncrease > sellerCreditDecrease) { + require axiomDistributivity(buyerCreditIncrease - sellerCreditDecrease, sellerCreditDecrease, PRECISION), "axiom"; + } else { + require axiomDistributivity(sellerCreditDecrease - buyerCreditIncrease, buyerCreditIncrease, PRECISION), "axiom"; + } + assert sumOfCreditsBody(id); +} diff --git a/certora/specs/UpdatePositionView.spec b/certora/specs/UpdatePositionView.spec new file mode 100644 index 000000000..afb35503c --- /dev/null +++ b/certora/specs/UpdatePositionView.spec @@ -0,0 +1,178 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function creditOf(bytes32 id, address user) external returns (uint128) envfree; + function totalUnits(bytes32 id) external returns (uint128) envfree; + function continuousFeeCredit(bytes32 id) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; + function lossFactor(bytes32) external returns (uint128) envfree; + + function updatePositionView(Midnight.Market, bytes32, address) external returns (uint128, uint128, uint128) optional; + + /// PRICE / ORACLE /// + function _.price() external => NONDET; + + /// SAFE TRANSFERS /// + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + + /// MUL/DIV — function summaries that compute the exact value in mathint. + 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); + + /// MISC INTERNALS irrelevant to credit / loss-factor tracking /// + function toId(Midnight.Market) external returns (bytes32) => NONDET; + function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function TickLib.wExp(int256) internal returns (uint256) => NONDET; + function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; + function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; + + /// EXTERNAL CALLBACKS — collapse path explosion for strong invariants. /// + function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; + function _.isRatified(Midnight.Offer, bytes) external => NONDET; + function _.canIncreaseCredit(address) external => NONDET; + function _.canIncreaseDebt(address) external => NONDET; + function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; + function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; + function _.canLiquidate(address) external => NONDET; +} + +/// MULDIV FUNCTION SUMMARIES /// +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(a * b / d); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256((a * b + (d - 1)) / d); +} + +/// GHOSTS /// + +persistent ghost mathint PRECISION { + axiom PRECISION > 0; +} + +ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivFactor { + init_state axiom forall bytes32 id. forall address user. preciseCreditDivFactor[id][user] == 0; +} + +ghost mapping(bytes32 => mapping(address => mathint)) pendingFeeMirror { + init_state axiom forall bytes32 id. forall address user. pendingFeeMirror[id][user] == 0; +} + +ghost mapping(bytes32 => mapping(address => mathint)) lastAccrualMirror { + init_state axiom forall bytes32 id. forall address user. lastAccrualMirror[id][user] == 0; +} + +/// HELPER FUNCTIONS /// + +// Map factor to 1 - factor, for easier math. +definition mapFactor(mathint factor) returns mathint = 2 ^ 128 - 1 - factor; + +definition cvlCreditOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; + +definition cvlLastLossFactor(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastLossFactor; + +/// HOOKS /// + +function updateCreditDivFactor(bytes32 id, address owner, uint128 newCredit, uint128 newFactor) { + mathint ownerLossFactor = mapFactor(newFactor); + require ownerLossFactor > 0 => PRECISION * newCredit % ownerLossFactor == 0, "PRECISION is 2^128!"; + preciseCreditDivFactor[id][owner] = ownerLossFactor == 0 ? 0 : PRECISION * newCredit / ownerLossFactor; +} + +function checkCreditDivInvariant(bytes32 id, address owner) returns bool { + uint128 credit = cvlCreditOf(id, owner); + uint128 userFactor = cvlLastLossFactor(id, owner); + mathint mappedFactor = mapFactor(userFactor); + return mappedFactor == 0 ? preciseCreditDivFactor[id][owner] == 0 : preciseCreditDivFactor[id][owner] * mappedFactor == PRECISION * credit; +} + +hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit (uint128 oldCredit) { + updateCreditDivFactor(id, owner, newCredit, cvlLastLossFactor(id, owner)); +} + +hook Sstore position[KEY bytes32 id][KEY address owner].lastLossFactor uint128 newFactor (uint128 oldFactor) { + updateCreditDivFactor(id, owner, cvlCreditOf(id, owner), newFactor); +} + +hook Sload uint128 value position[KEY bytes32 id][KEY address owner].pendingFee { + require pendingFeeMirror[id][owner] == value, "ghost mirror"; +} + +hook Sload uint128 value position[KEY bytes32 id][KEY address owner].lastAccrual { + require lastAccrualMirror[id][owner] == value, "ghost mirror"; +} + +hook Sstore position[KEY bytes32 id][KEY address owner].pendingFee uint128 newPending (uint128 oldPending) { + pendingFeeMirror[id][owner] = newPending; +} + +hook Sstore position[KEY bytes32 id][KEY address owner].lastAccrual uint128 newLast (uint128 oldLast) { + lastAccrualMirror[id][owner] = newLast; +} + +/// INVARIANTS /// + +strong invariant preciseCreditCorrect(bytes32 id, address owner) + checkCreditDivInvariant(id, owner); + +// The obligation loss factor cannot be larger than the user loss factor. +strong invariant lossFactorLeqLastLossFactor(bytes32 id, address owner) + mapFactor(lossFactor(id)) <= mapFactor(cvlLastLossFactor(id, owner)); + +/// RULES /// + +rule updatePositionViewReflectedByFactor(env e, Midnight.Market obligation, bytes32 id, address owner) { + requireInvariant preciseCreditCorrect(id, owner); + requireInvariant lossFactorLeqLastLossFactor(id, owner); + + uint128 newCredit; + uint128 newPending; + uint128 fee; + + uint128 creditBefore = cvlCreditOf(id, owner); + mathint preciseCreditBefore = preciseCreditDivFactor[id][owner] * mapFactor(lossFactor(id)); + mathint pendingBefore = pendingFeeMirror[id][owner]; + mathint lastAccrualBefore = lastAccrualMirror[id][owner]; + + require e.block.timestamp >= lastAccrualBefore, "Time is increasing"; + + newCredit, newPending, fee = updatePositionView(e, obligation, id, owner); + + assert fee <= pendingBefore, "Cannot take more fee than pending"; + assert (newCredit + fee) * PRECISION <= preciseCreditBefore, "newCredit (with fees) is at most precise credit after slashing"; + // The two monotonicity facts the SumOfCredits summaries assume about + // `updatePositionView`. `newCredit <= creditBefore` holds because + // postSlashCredit = credit * mapFactor(lossFactor) / mapFactor(lastLossFactor) + // <= credit under `lossFactorLeqLastLossFactor`, and newCredit = + // postSlashCredit - fee. Proving them here means the summaries no longer + // rely on the indirect underflow-revert argument in `_updatePosition`. + assert newCredit <= creditBefore, "slashing and fee accrual only decrease credit"; + assert newPending <= pendingBefore, "fee deduction only decreases pending"; +} + +rule updatePositionZero(env e, Midnight.Market obligation, bytes32 id, address owner) { + require currentContract.position[id][owner].credit == 0, "Assume no credit"; + + uint128 newCredit; + uint128 newPending; + uint128 fee; + newCredit, newPending, fee = updatePositionView(e, obligation, id, owner); + + assert newCredit == 0 && newPending == 0 && fee == 0; +} From 5345d1b52aa97924d43003032908ac62fafa1084 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 13 Jul 2026 14:23:47 +0200 Subject: [PATCH 02/11] Ran formatter --- certora/specs/UpdatePositionView.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/specs/UpdatePositionView.spec b/certora/specs/UpdatePositionView.spec index afb35503c..137efbd2c 100644 --- a/certora/specs/UpdatePositionView.spec +++ b/certora/specs/UpdatePositionView.spec @@ -156,6 +156,7 @@ rule updatePositionViewReflectedByFactor(env e, Midnight.Market obligation, byte assert fee <= pendingBefore, "Cannot take more fee than pending"; assert (newCredit + fee) * PRECISION <= preciseCreditBefore, "newCredit (with fees) is at most precise credit after slashing"; + // The two monotonicity facts the SumOfCredits summaries assume about // `updatePositionView`. `newCredit <= creditBefore` holds because // postSlashCredit = credit * mapFactor(lossFactor) / mapFactor(lastLossFactor) From dcdd4c8d529d81774f9fe779b3d0a1bb0fc44fd0 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 13 Jul 2026 14:37:52 +0200 Subject: [PATCH 03/11] Don't filter withdraw, lint configs --- certora/confs/SumOfCreditsAxiomatic.conf | 4 ++-- certora/confs/UpdatePositionView.conf | 4 +++- certora/specs/SumOfCreditsAxiomatic.spec | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/certora/confs/SumOfCreditsAxiomatic.conf b/certora/confs/SumOfCreditsAxiomatic.conf index 56d5fb56d..89ccb797e 100644 --- a/certora/confs/SumOfCreditsAxiomatic.conf +++ b/certora/confs/SumOfCreditsAxiomatic.conf @@ -15,8 +15,8 @@ "hashing_length_bound": 1024, "build_cache": true, "prover_args": [ - "-destructiveOptimizations twostage -depth 2" - ], + "-destructiveOptimizations twostage -depth 2" + ], "rule_sanity": "basic", "smt_timeout": 7200, "msg": "SumOfCredits" diff --git a/certora/confs/UpdatePositionView.conf b/certora/confs/UpdatePositionView.conf index 5d723332d..38dcc3f2c 100644 --- a/certora/confs/UpdatePositionView.conf +++ b/certora/confs/UpdatePositionView.conf @@ -3,7 +3,9 @@ "src/Midnight.sol" ], "verify": "Midnight:certora/specs/UpdatePositionView.spec", - "parametric_contracts": ["Midnight"], + "parametric_contracts": [ + "Midnight" + ], "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index efb7a2d15..39eff1942 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -271,7 +271,7 @@ strong invariant lossFactorLeqLastLossFactor(bytes32 id, address owner) // here, and the SumOfCreditsSummaryTake.spec split for take). strong invariant sumOfCreditsLeTotalUnits(bytes32 id) sumOfCreditsBody(id) - filtered { f -> 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 } { + filtered { f -> 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 } { preserved claimContinuousFee(Midnight.Market market, uint256 amount, address receiver) with (env e) { require axiomDistributivity(continuousFeeCredit(id) - amount, amount, PRECISION); require axiomDistributivity(totalUnits(id) - amount, amount, PRECISION); From dd5df1dabd46f8a9bea8117a08885b0f7eb9c587 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 13 Jul 2026 15:10:51 +0200 Subject: [PATCH 04/11] Clean up method block and fix it --- certora/specs/SumOfCreditsAxiomatic.spec | 7 ++----- certora/specs/UpdatePositionView.spec | 10 ++-------- 2 files changed, 4 insertions(+), 13 deletions(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 39eff1942..6e6ad0150 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -4,10 +4,8 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; function totalUnits(bytes32 id) external returns (uint128) envfree; function continuousFeeCredit(bytes32 id) external returns (uint128) envfree; - function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; function lossFactor(bytes32) external returns (uint128) envfree; /// SUMMARY OF updatePositionView -- see file header for soundness argument. /// @@ -23,9 +21,8 @@ methods { function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); /// MISC INTERNALS irrelevant to credit / loss-index tracking. /// - function toId(Midnight.Market) external returns (bytes32) => NONDET; - function IdLib.toId(Midnight.Market memory, uint256, address) internal returns (bytes32) => NONDET; - function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET; + function IdLib.toId(Midnight.Market memory) internal returns (bytes32) => NONDET; + function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; function touchMarket(Midnight.Market) external returns (bytes32) => NONDET; function Midnight.touchMarket(Midnight.Market memory) internal returns (bytes32) => NONDET; function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; diff --git a/certora/specs/UpdatePositionView.spec b/certora/specs/UpdatePositionView.spec index 137efbd2c..1cff75ef8 100644 --- a/certora/specs/UpdatePositionView.spec +++ b/certora/specs/UpdatePositionView.spec @@ -3,14 +3,8 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; - function totalUnits(bytes32 id) external returns (uint128) envfree; - function continuousFeeCredit(bytes32 id) external returns (uint128) envfree; - function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; function lossFactor(bytes32) external returns (uint128) envfree; - function updatePositionView(Midnight.Market, bytes32, address) external returns (uint128, uint128, uint128) optional; - /// PRICE / ORACLE /// function _.price() external => NONDET; @@ -23,8 +17,8 @@ methods { function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); /// MISC INTERNALS irrelevant to credit / loss-factor tracking /// - function toId(Midnight.Market) external returns (bytes32) => NONDET; - function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET; + function IdLib.toId(Midnight.Market memory) internal returns (bytes32) => NONDET; + function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET; function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; function TickLib.wExp(int256) internal returns (uint256) => NONDET; From b47f1387e7a689a699b96cfe641498e1dd8f356d Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 17 Aug 2026 13:58:19 +0200 Subject: [PATCH 05/11] Some changes from code review --- certora/specs/SumOfCreditsAxiomatic.spec | 94 ++++++++++-------------- 1 file changed, 38 insertions(+), 56 deletions(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 6e6ad0150..789965ff3 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -38,63 +38,12 @@ methods { function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; - /// EXTERNAL CALLBACKS — prevent havoc of ghosts on unresolved calls in `take` / - /// `liquidate` / `flashLoan`. Signatures MUST match the real callbacks exactly - /// (ICallbacks.sol / IRatifier.sol); a mismatched arg list yields a different - /// selector, so the `_.` summary does NOT apply and the call falls through to - /// AUTO => DEFAULT HAVOC, which havocs the (non-persistent) credit ghosts. + /// EXTERNAL CALLBACKS — prevent havoc of ghosts and variables in callbacks. function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; - function _.isRatified(Midnight.Offer, bytes) external => NONDET; - function _.canIncreaseCredit(address) external => NONDET; - function _.canIncreaseDebt(address) external => NONDET; function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; - - /// EXTERNAL TOKEN CALLS — defensive, redundant with SafeTransferLib NONDET. /// - function _.transfer(address, uint256) external => NONDET; - function _.transferFrom(address, address, uint256) external => NONDET; -} - -/// MULDIV FUNCTION SUMMARIES — axiomatic (deterministic ghost + rounding bound) instead of the exact -/// `a*b/d`, to avoid a nonlinear division term at every call site. The only invariant-relevant mulDiv is -/// liquidate's loss-index update (Midnight.sol:591) and the continuousFeeCredit slash (Midnight.sol:597), -/// both of which need only the rounds-down bound `result*d <= a*b` (proved in MulDiv.spec:mulDivDownRoundsDown). -/// mulDivUp's calls here feed badDebt / pendingFee, whose exact values are immaterial to sumOfCreditsBody, -/// so it needs no bound (a bare deterministic ghost suffices). -persistent ghost mulDivDownGhost(mathint, mathint, mathint) returns mathint { - axiom forall mathint a. forall mathint b. forall mathint d. mulDivDownGhost(a, b, d) >= 0; - axiom forall mathint a. forall mathint d. d > 0 => mulDivDownGhost(a, 0, d) == 0; - axiom forall mathint b. forall mathint d. d > 0 => mulDivDownGhost(0, b, d) == 0; - - // RAW-arithmetic form only (not also a multiply-wrapped duplicate): liquidate's - // closing argument grounds sum*M and (tu-cf)*PRECISION to real arithmetic (single, - // non-aggregate products -- cheap; see the liquidate rule), and lossFactorLeqLastLossFactor - // compares raw mapIndex values directly, never through `multiply`. Keeping only one - // form avoids giving the solver two redundant bounds to case on at the same call sites. - axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(d, mulDivDownGhost(a, b, d)) <= multiply(b, a); - axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(mulDivDownGhost(a, b, d), d) <= multiply(a, b); -} - -persistent ghost mulDivUpGhost(mathint, mathint, mathint) returns mathint { - axiom forall mathint a. forall mathint b. forall mathint d. mulDivUpGhost(a, b, d) >= 0; -} - -function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { - bool overflow; - if (overflow || d == 0) { - revert(); - } - return require_uint256(mulDivDownGhost(a, b, d)); -} - -function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { - bool overflow; - if (overflow || d == 0) { - revert(); - } - return require_uint256(mulDivUpGhost(a, b, d)); } /// GHOSTS /// @@ -113,6 +62,8 @@ ghost mapping(bytes32 => mapping(address => mathint)) preciseCreditDivIndex { axiom forall bytes32 id. forall address user. preciseCreditDivIndex[id][user] >= 0; } +// Instead of using the builtin `*`, which requires unstable non-linear arithemetic, we +// use the uninterpreted function `multiply` and only instantiate those axioms we need for proving. // `multiply(a, b)` IS the product `a * b` declared as an uninterpreted function. persistent ghost multiply(mathint, mathint) returns mathint { axiom forall mathint a. forall mathint b. (a > 0 && b > 0) => multiply(a, b) > 0; @@ -126,8 +77,39 @@ definition axiomDistributivity(mathint a, mathint b, mathint c) returns bool = m // Symmetry axiom over associativity. definition axiomAssocComm(mathint a, mathint b, mathint c) returns bool = multiply(multiply(a, b), c) == multiply(multiply(a, c), b); -// Linear order axiom for multiplication with nonnegative constants. -definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c >= 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); +// Linear order axiom for multiplication with positive constants. +definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c > 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); + +/// MULDIV FUNCTION SUMMARIES — axiomatic: TODO rebase on mulDivAxiom pull request. +persistent ghost mulDivDownGhost(mathint, mathint, mathint) returns mathint { + axiom forall mathint a. forall mathint b. forall mathint d. mulDivDownGhost(a, b, d) >= 0; + axiom forall mathint a. forall mathint d. d > 0 => mulDivDownGhost(a, 0, d) == 0; + axiom forall mathint b. forall mathint d. d > 0 => mulDivDownGhost(0, b, d) == 0; + + // The following is the mulDivBound axiom stated using the `multiply` function. + axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(d, mulDivDownGhost(a, b, d)) <= multiply(b, a); + axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(mulDivDownGhost(a, b, d), d) <= multiply(a, b); +} + +persistent ghost mulDivUpGhost(mathint, mathint, mathint) returns mathint { + axiom forall mathint a. forall mathint b. forall mathint d. mulDivUpGhost(a, b, d) >= 0; +} + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(mulDivDownGhost(a, b, d)); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(mulDivUpGhost(a, b, d)); +} /// HELPER DEFINITIONS /// @@ -299,7 +281,7 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) // mulDivDownGhost rounds-down bound (it verifies in the parametric invariant), // and `sum` is a single snapshot here (not the touched-user delta), so the // withdraw-style NIA divergence does not occur. -rule sumOfCreditsLeTotalUnits_liquidate(bytes32 id, env e, Midnight.Market obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { +rule sumOfCreditsLeTotalUnitsPreservedByLiquidate(bytes32 id, env e, Midnight.Market obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { require sumOfCreditsBody(id); requireInvariant preciseCreditCorrect(id, borrower); requireInvariant lossFactorLeqLastLossFactor(id, borrower); @@ -363,7 +345,7 @@ rule sumOfCreditsLeTotalUnits_liquidate(bytes32 id, env e, Midnight.Market oblig assert sumOfCreditsBody(id); } -rule sumOfCreditsLeTotalUnits_take(bytes32 id, env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { +rule sumOfCreditsLeTotalUnitsPreservedByTake(bytes32 id, env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { require sumOfCreditsBody(id); // Determine buyer and seller From a3d61a005964d8ed41370574984a4aba341f65f6 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 28 Aug 2026 12:03:44 +0200 Subject: [PATCH 06/11] Clean-up only --- certora/specs/SumOfCreditsAxiomatic.spec | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 789965ff3..181858cbc 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -131,7 +131,7 @@ definition sumOfCreditsBody(bytes32 id) returns bool = multiply(sumPreciseCredit function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint128 newIndex) { mathint ownerLossIndex = mapIndex(newIndex); - mathint oldD = preciseCreditDivIndex[id][owner]; + mathint oldCDI = preciseCreditDivIndex[id][owner]; mathint value; // We require there is a value such that @@ -140,15 +140,15 @@ function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint // be divisible by ownerLossIndex. require multiply(value, ownerLossIndex) == multiply(newCredit, PRECISION), "PRECISION is divisible by ownerLossIndex"; - mathint newD = (ownerLossIndex == 0 || newCredit == 0) ? 0 : value; - preciseCreditDivIndex[id][owner] = newD; + mathint newCDI = (ownerLossIndex == 0 || newCredit == 0) ? 0 : value; + preciseCreditDivIndex[id][owner] = newCDI; mathint oldSum = sumPreciseCreditDivIndex[id]; - sumPreciseCreditDivIndex[id] = oldSum + newD - oldD; + sumPreciseCreditDivIndex[id] = oldSum + newCDI - oldCDI; // require distributivity axioms to help prover mathint lossIndex = mapIndex(lossFactor(id)); - require axiomDistributivity(oldSum, newD, lossIndex), "axiom"; - require axiomDistributivity(oldSum + newD - oldD, oldD, lossIndex), "axiom"; + require axiomDistributivity(oldSum, newCDI, lossIndex), "axiom"; + require axiomDistributivity(oldSum + newCDI - oldCDI, oldCDI, lossIndex), "axiom"; } function checkCreditDivInvariant(bytes32 id, address owner) returns bool { @@ -361,8 +361,6 @@ rule sumOfCreditsLeTotalUnitsPreservedByTake(bytes32 id, env e, uint256 units, a mathint debtPre_b = currentContract.position[id][buyer].debt; take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); - mathint creditPost_b = currentContract.position[id][buyer].credit; - mathint creditPost_s = currentContract.position[id][seller].credit; mathint tuPost = totalUnits(id); // Compute the buyer credit increase. Note that updatePosition does From f4db2d150d74353b2a60c5854d058e1aa4e75caa Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 28 Aug 2026 13:53:42 +0200 Subject: [PATCH 07/11] Use MulDivAxioms. Also instead of requiring some axioms for all values, we require the axioms in summaryMulDivDown only for the used values. --- certora/specs/SumOfCreditsAxiomatic.spec | 59 +++++++++++------------- 1 file changed, 27 insertions(+), 32 deletions(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 181858cbc..3fba78624 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -1,6 +1,8 @@ // SPDX-License-Identifier: GPL-2.0-or-later // +import "MulDivAxioms.spec"; + methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -80,35 +82,28 @@ definition axiomAssocComm(mathint a, mathint b, mathint c) returns bool = multip // Linear order axiom for multiplication with positive constants. definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c > 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); -/// MULDIV FUNCTION SUMMARIES — axiomatic: TODO rebase on mulDivAxiom pull request. -persistent ghost mulDivDownGhost(mathint, mathint, mathint) returns mathint { - axiom forall mathint a. forall mathint b. forall mathint d. mulDivDownGhost(a, b, d) >= 0; - axiom forall mathint a. forall mathint d. d > 0 => mulDivDownGhost(a, 0, d) == 0; - axiom forall mathint b. forall mathint d. d > 0 => mulDivDownGhost(0, b, d) == 0; +// The following is RoundsDown axiom stated using the `multiply` function. +definition axiomMathMulDivDownRoundsDownMultiply(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 => multiply(mathMulDivDown(a, b, d), d) <= multiply(a, b); - // The following is the mulDivBound axiom stated using the `multiply` function. - axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(d, mulDivDownGhost(a, b, d)) <= multiply(b, a); - axiom forall mathint a. forall mathint b. forall mathint d. d > 0 => multiply(mulDivDownGhost(a, b, d), d) <= multiply(a, b); -} - -persistent ghost mulDivUpGhost(mathint, mathint, mathint) returns mathint { - axiom forall mathint a. forall mathint b. forall mathint d. mulDivUpGhost(a, b, d) >= 0; -} +definition axiomMathMulDivDownRoundsDownMultiplySymm(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 => multiply(d, mathMulDivDown(a, b, d)) <= multiply(b, a); function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { - bool overflow; - if (overflow || d == 0) { + if (d == 0 || a * b >= 2 ^ 256) { revert(); } - return require_uint256(mulDivDownGhost(a, b, d)); + require axiomMathMulDivDownZeroA(b, d), "axiom"; + require axiomMathMulDivDownZeroB(a, d), "axiom"; + require axiomMathMulDivDownRoundsDownMultiply(a, b, d), "axiom"; + require axiomMathMulDivDownRoundsDownMultiplySymm(a, b, d), "axiom"; + return require_uint256(ghostMulDivDown(a, b, d)); } function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { bool overflow; - if (overflow || d == 0) { + if (d == 0 || a * b + d - 1 >= 2 ^ 256) { revert(); } - return require_uint256(mulDivUpGhost(a, b, d)); + return require_uint256(ghostMulDivUp(a, b, d)); } /// HELPER DEFINITIONS /// @@ -241,7 +236,7 @@ strong invariant lossFactorLeqLastLossFactor(bytes32 id, address owner) mapIndex(lossFactor(id)) <= mapIndex(cvlLastLossFactor(id, owner)) { preserved liquidate(Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) with (env e) { - require forall mathint a. forall mathint b. forall mathint d. b <= d => mulDivDownGhost(a, b, d) <= a, "see mulDivArgumentLesserThanDenominator in MulDiv.spec"; + require forall mathint a. forall mathint b. forall mathint d. axiomMathMulDivDownArgumentLesserThanDenominatorB(a, b, d), "axiom"; } } @@ -252,8 +247,8 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) sumOfCreditsBody(id) filtered { f -> 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 } { preserved claimContinuousFee(Midnight.Market market, uint256 amount, address receiver) with (env e) { - require axiomDistributivity(continuousFeeCredit(id) - amount, amount, PRECISION); - require axiomDistributivity(totalUnits(id) - amount, amount, PRECISION); + require axiomDistributivity(continuousFeeCredit(id) - amount, amount, PRECISION), "axiom"; + require axiomDistributivity(totalUnits(id) - amount, amount, PRECISION), "axiom"; } preserved updatePosition(Midnight.Market market, address user) with (env e) { @@ -278,7 +273,7 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) // which additivity cannot express. So here we do the inverse of withdraw/take: // GROUND the aggregate back to a real product (pre and post). That re-exposes // sum*M_old and sum*M_new, but liquidate ALREADY discharges those via the -// mulDivDownGhost rounds-down bound (it verifies in the parametric invariant), +// ghostMulDivDown rounds-down bound (it verifies in the parametric invariant), // and `sum` is a single snapshot here (not the touched-user delta), so the // withdraw-style NIA divergence does not occur. rule sumOfCreditsLeTotalUnitsPreservedByLiquidate(bytes32 id, env e, Midnight.Market obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { @@ -307,10 +302,10 @@ rule sumOfCreditsLeTotalUnitsPreservedByLiquidate(bytes32 id, env e, Midnight.Ma // on each side share the SAME second argument (indexPost for the tuPre/cfPre pair, indexPre for // tuPost/cfPost), which is exactly the shape multiply(a,m)-multiply(b,m)==multiply(a-b,m) // needs, so this needs no cancellation, only the additivity already established. - require axiomDistributivity(cfPre, tuPre - cfPre, indexPost); - require axiomDistributivity(cfPost, tuPost - cfPost, indexPre); - require axiomDistributivity(tuPre - cfPre, cfPre, PRECISION); - require axiomDistributivity(tuPost - cfPost, cfPost, PRECISION); + require axiomDistributivity(cfPre, tuPre - cfPre, indexPost), "axiom"; + require axiomDistributivity(cfPost, tuPost - cfPost, indexPre), "axiom"; + require axiomDistributivity(tuPre - cfPre, cfPre, PRECISION), "axiom"; + require axiomDistributivity(tuPost - cfPost, cfPost, PRECISION), "axiom"; // The proof requires several steps: @@ -335,12 +330,12 @@ rule sumOfCreditsLeTotalUnitsPreservedByLiquidate(bytes32 id, env e, Midnight.Ma // sumPre * indexPost <= (tuPost - cfPost) * PRECISION (sumOfCreditBody Post) // These are the axioms used in the proof above - require axiomLeMulPos(multiply(sumPre, indexPre), multiply(tuPre - cfPre, PRECISION), indexPost); - require axiomAssocComm(sumPre, indexPre, indexPost); - require axiomAssocComm(tuPre - cfPre, PRECISION, indexPost); - require axiomLeMulPos(multiply(tuPre - cfPre, indexPost), multiply(tuPost - cfPost, indexPre), PRECISION); - require axiomAssocComm(tuPost - cfPost, indexPre, PRECISION); - require axiomLeMulPos(multiply(sumPre, indexPost), multiply(tuPost - cfPost, PRECISION), indexPre); + require axiomLeMulPos(multiply(sumPre, indexPre), multiply(tuPre - cfPre, PRECISION), indexPost), "axiom"; + require axiomAssocComm(sumPre, indexPre, indexPost), "axiom"; + require axiomAssocComm(tuPre - cfPre, PRECISION, indexPost), "axiom"; + require axiomLeMulPos(multiply(tuPre - cfPre, indexPost), multiply(tuPost - cfPost, indexPre), PRECISION), "axiom"; + require axiomAssocComm(tuPost - cfPost, indexPre, PRECISION), "axiom"; + require axiomLeMulPos(multiply(sumPre, indexPost), multiply(tuPost - cfPost, PRECISION), indexPre), "axiom"; assert sumOfCreditsBody(id); } From 5cc00d27db4362fdad64b4c7cfd8f8476ef6052b Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 28 Aug 2026 14:02:55 +0200 Subject: [PATCH 08/11] Apply suggestion from @QGarchery Co-authored-by: Quentin Garchery Signed-off-by: Jochen Hoenicke --- certora/specs/SumOfCreditsAxiomatic.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 3fba78624..9cc2f7133 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -133,7 +133,7 @@ function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint // value * ownerLossIndex == newCredit * PRECISION. // This is sound because we can assume PRECISION to be large enough to // be divisible by ownerLossIndex. - require multiply(value, ownerLossIndex) == multiply(newCredit, PRECISION), "PRECISION is divisible by ownerLossIndex"; + require ownerLossIndex > 0 => multiply(value, ownerLossIndex) == multiply(newCredit, PRECISION), "PRECISION is divisible by ownerLossIndex"; mathint newCDI = (ownerLossIndex == 0 || newCredit == 0) ? 0 : value; preciseCreditDivIndex[id][owner] = newCDI; From 0be12e82251f796066902fba64cae0fdcca9f3fd Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 28 Aug 2026 14:15:34 +0200 Subject: [PATCH 09/11] Applied changes from CodeReview Rename cvl*Of functions. Use invariant from Midnight.spec --- certora/specs/SumOfCreditsAxiomatic.spec | 35 ++++++++++-------------- certora/specs/UpdatePositionView.spec | 15 ++++------ 2 files changed, 20 insertions(+), 30 deletions(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 9cc2f7133..94ed587b3 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -9,6 +9,7 @@ methods { function totalUnits(bytes32 id) external returns (uint128) envfree; function continuousFeeCredit(bytes32 id) external returns (uint128) envfree; function lossFactor(bytes32) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; /// SUMMARY OF updatePositionView -- see file header for soundness argument. /// function Midnight.updatePositionView(Midnight.Market memory obligation, bytes32 id, address user) internal returns (uint128, uint128, uint128) with(env e) => summaryUpdatePositionView(e, id, user); @@ -110,13 +111,13 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { definition mapIndex(mathint index) returns mathint = 2 ^ 128 - 1 - index; -definition cvlCreditOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; +definition cvlCredit(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; definition cvlLastLossFactor(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastLossFactor; -definition cvlPendingFeeOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].pendingFee; +definition cvlPendingFee(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].pendingFee; -definition cvlLastAccrualOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastAccrual; +definition cvlLastAccrual(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastAccrual; // Body of the strong invariant. The aggregate product is routed through the // uninterpreted `multiply` (== sumPreciseCreditDivIndex[id] * mapIndex(...)). @@ -147,7 +148,7 @@ function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint } function checkCreditDivInvariant(bytes32 id, address owner) returns bool { - uint128 credit = cvlCreditOf(id, owner); + uint128 credit = cvlCredit(id, owner); uint128 userIndex = cvlLastLossFactor(id, owner); mathint mappedIndex = mapIndex(userIndex); @@ -169,7 +170,7 @@ hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit } hook Sstore position[KEY bytes32 id][KEY address owner].lastLossFactor uint128 newIndex (uint128 oldIndex) { - updateCreditDivIndex(id, owner, cvlCreditOf(id, owner), newIndex); + updateCreditDivIndex(id, owner, cvlCredit(id, owner), newIndex); } hook Sstore marketState[KEY bytes32 id].totalUnits uint128 newTotal (uint128 oldTotal) { @@ -186,9 +187,9 @@ hook Sstore marketState[KEY bytes32 id].totalUnits uint128 newTotal (uint128 old // inequalities proved in UpdatePositionView.spec // (rule `updatePositionViewReflectedByIndex`). function summaryUpdatePositionView(env e, bytes32 id, address user) returns (uint128, uint128, uint128) { - uint128 oldCredit = cvlCreditOf(id, user); - uint128 oldPendingFee = cvlPendingFeeOf(id, user); - uint128 oldLastAccrual = cvlLastAccrualOf(id, user); + uint128 oldCredit = cvlCredit(id, user); + uint128 oldPendingFee = cvlPendingFee(id, user); + uint128 oldLastAccrual = cvlLastAccrual(id, user); require to_mathint(e.block.timestamp) >= to_mathint(oldLastAccrual), "time is non-decreasing"; @@ -232,14 +233,6 @@ function summaryUpdatePositionView(env e, bytes32 id, address user) returns (uin strong invariant preciseCreditCorrect(bytes32 id, address owner) checkCreditDivInvariant(id, owner); -strong invariant lossFactorLeqLastLossFactor(bytes32 id, address owner) - mapIndex(lossFactor(id)) <= mapIndex(cvlLastLossFactor(id, owner)) - { - preserved liquidate(Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) with (env e) { - require forall mathint a. forall mathint b. forall mathint d. axiomMathMulDivDownArgumentLesserThanDenominatorB(a, b, d), "axiom"; - } - } - // Parametric coverage of the sum invariant for all methods EXCEPT withdraw and // take, which are handled by their dedicated rules (sumOfCreditsLeTotalUnits_withdraw // here, and the SumOfCreditsSummaryTake.spec split for take). @@ -253,12 +246,12 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) preserved updatePosition(Midnight.Market market, address user) with (env e) { requireInvariant preciseCreditCorrect(id, user); - requireInvariant lossFactorLeqLastLossFactor(id, user); + require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; } preserved withdraw(Midnight.Market market, uint256 units, address onBehalf, address receiver) with (env e) { requireInvariant preciseCreditCorrect(id, onBehalf); - requireInvariant lossFactorLeqLastLossFactor(id, onBehalf); + require lastLossFactor(id, onBehalf) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; } } @@ -279,7 +272,7 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) rule sumOfCreditsLeTotalUnitsPreservedByLiquidate(bytes32 id, env e, Midnight.Market obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { require sumOfCreditsBody(id); requireInvariant preciseCreditCorrect(id, borrower); - requireInvariant lossFactorLeqLastLossFactor(id, borrower); + require lastLossFactor(id, borrower) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; mathint sumPre = sumPreciseCreditDivIndex[id]; mathint indexPre = mapIndex(lossFactor(id)); @@ -348,9 +341,9 @@ rule sumOfCreditsLeTotalUnitsPreservedByTake(bytes32 id, env e, uint256 units, a address seller = offer.buy ? taker : offer.maker; requireInvariant preciseCreditCorrect(id, taker); - requireInvariant lossFactorLeqLastLossFactor(id, taker); + require lastLossFactor(id, taker) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; requireInvariant preciseCreditCorrect(id, offer.maker); - requireInvariant lossFactorLeqLastLossFactor(id, offer.maker); + require lastLossFactor(id, offer.maker) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; mathint tuPre = totalUnits(id); mathint debtPre_b = currentContract.position[id][buyer].debt; diff --git a/certora/specs/UpdatePositionView.spec b/certora/specs/UpdatePositionView.spec index 1cff75ef8..fb98d9505 100644 --- a/certora/specs/UpdatePositionView.spec +++ b/certora/specs/UpdatePositionView.spec @@ -4,6 +4,7 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function lossFactor(bytes32) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; /// PRICE / ORACLE /// function _.price() external => NONDET; @@ -77,7 +78,7 @@ ghost mapping(bytes32 => mapping(address => mathint)) lastAccrualMirror { // Map factor to 1 - factor, for easier math. definition mapFactor(mathint factor) returns mathint = 2 ^ 128 - 1 - factor; -definition cvlCreditOf(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; +definition cvlCredit(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; definition cvlLastLossFactor(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastLossFactor; @@ -90,7 +91,7 @@ function updateCreditDivFactor(bytes32 id, address owner, uint128 newCredit, uin } function checkCreditDivInvariant(bytes32 id, address owner) returns bool { - uint128 credit = cvlCreditOf(id, owner); + uint128 credit = cvlCredit(id, owner); uint128 userFactor = cvlLastLossFactor(id, owner); mathint mappedFactor = mapFactor(userFactor); return mappedFactor == 0 ? preciseCreditDivFactor[id][owner] == 0 : preciseCreditDivFactor[id][owner] * mappedFactor == PRECISION * credit; @@ -101,7 +102,7 @@ hook Sstore position[KEY bytes32 id][KEY address owner].credit uint128 newCredit } hook Sstore position[KEY bytes32 id][KEY address owner].lastLossFactor uint128 newFactor (uint128 oldFactor) { - updateCreditDivFactor(id, owner, cvlCreditOf(id, owner), newFactor); + updateCreditDivFactor(id, owner, cvlCredit(id, owner), newFactor); } hook Sload uint128 value position[KEY bytes32 id][KEY address owner].pendingFee { @@ -125,21 +126,17 @@ hook Sstore position[KEY bytes32 id][KEY address owner].lastAccrual uint128 newL strong invariant preciseCreditCorrect(bytes32 id, address owner) checkCreditDivInvariant(id, owner); -// The obligation loss factor cannot be larger than the user loss factor. -strong invariant lossFactorLeqLastLossFactor(bytes32 id, address owner) - mapFactor(lossFactor(id)) <= mapFactor(cvlLastLossFactor(id, owner)); - /// RULES /// rule updatePositionViewReflectedByFactor(env e, Midnight.Market obligation, bytes32 id, address owner) { requireInvariant preciseCreditCorrect(id, owner); - requireInvariant lossFactorLeqLastLossFactor(id, owner); + require lastLossFactor(id, owner) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; uint128 newCredit; uint128 newPending; uint128 fee; - uint128 creditBefore = cvlCreditOf(id, owner); + uint128 creditBefore = cvlCredit(id, owner); mathint preciseCreditBefore = preciseCreditDivFactor[id][owner] * mapFactor(lossFactor(id)); mathint pendingBefore = pendingFeeMirror[id][owner]; mathint lastAccrualBefore = lastAccrualMirror[id][owner]; From 1908960daa520bf4482bd72f54ac9c9cceca80d4 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 28 Aug 2026 15:08:38 +0200 Subject: [PATCH 10/11] Ensure summary of UpdatePosition matches proved properties Made the specs more similar to each other (adapted variable names). Use "proved in UpdatePositionView" as explanation for require. --- certora/specs/SumOfCreditsAxiomatic.spec | 102 ++++++++--------------- certora/specs/UpdatePositionView.spec | 55 ++++-------- 2 files changed, 54 insertions(+), 103 deletions(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 94ed587b3..4c9d8fd75 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -81,7 +81,7 @@ definition axiomDistributivity(mathint a, mathint b, mathint c) returns bool = m definition axiomAssocComm(mathint a, mathint b, mathint c) returns bool = multiply(multiply(a, b), c) == multiply(multiply(a, c), b); // Linear order axiom for multiplication with positive constants. -definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c > 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); +definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c >= 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); // The following is RoundsDown axiom stated using the `multiply` function. definition axiomMathMulDivDownRoundsDownMultiply(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 => multiply(mathMulDivDown(a, b, d), d) <= multiply(a, b); @@ -109,7 +109,7 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { /// HELPER DEFINITIONS /// -definition mapIndex(mathint index) returns mathint = 2 ^ 128 - 1 - index; +definition mapFactor(mathint index) returns mathint = 2 ^ 128 - 1 - index; definition cvlCredit(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].credit; @@ -120,13 +120,13 @@ definition cvlPendingFee(bytes32 id, address owner) returns uint128 = currentCon definition cvlLastAccrual(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].lastAccrual; // Body of the strong invariant. The aggregate product is routed through the -// uninterpreted `multiply` (== sumPreciseCreditDivIndex[id] * mapIndex(...)). -definition sumOfCreditsBody(bytes32 id) returns bool = multiply(sumPreciseCreditDivIndex[id], mapIndex(lossFactor(id))) <= multiply(totalUnits(id), PRECISION) - multiply(continuousFeeCredit(id), PRECISION); +// uninterpreted `multiply` (== sumPreciseCreditDivIndex[id] * mapFactor(...)). +definition sumOfCreditsBody(bytes32 id) returns bool = multiply(sumPreciseCreditDivIndex[id], mapFactor(lossFactor(id))) <= multiply(totalUnits(id), PRECISION) - multiply(continuousFeeCredit(id), PRECISION); /// HOOKS /// function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint128 newIndex) { - mathint ownerLossIndex = mapIndex(newIndex); + mathint ownerLossIndex = mapFactor(newIndex); mathint oldCDI = preciseCreditDivIndex[id][owner]; mathint value; @@ -142,7 +142,7 @@ function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint sumPreciseCreditDivIndex[id] = oldSum + newCDI - oldCDI; // require distributivity axioms to help prover - mathint lossIndex = mapIndex(lossFactor(id)); + mathint lossIndex = mapFactor(lossFactor(id)); require axiomDistributivity(oldSum, newCDI, lossIndex), "axiom"; require axiomDistributivity(oldSum + newCDI - oldCDI, oldCDI, lossIndex), "axiom"; } @@ -150,12 +150,12 @@ function updateCreditDivIndex(bytes32 id, address owner, uint128 newCredit, uint function checkCreditDivInvariant(bytes32 id, address owner) returns bool { uint128 credit = cvlCredit(id, owner); uint128 userIndex = cvlLastLossFactor(id, owner); - mathint mappedIndex = mapIndex(userIndex); + mathint mappedIndex = mapFactor(userIndex); // Per-user invariant stays in REAL-product form: it is per-user (cheap) and // the hook's division-exactness genuinely needs real arithmetic. Abstracting // it to multiply weakened this ASSUMED invariant enough to make a - // fully-slashed store (mapIndex==0, credit!=0) reachable, breaking the hook + // fully-slashed store (mapFactor==0, credit!=0) reachable, breaking the hook // assert. Only the AGGREGATE (sumOfCreditsBody) is abstracted. return mappedIndex == 0 || credit == 0 ? preciseCreditDivIndex[id][owner] == 0 : multiply(preciseCreditDivIndex[id][owner], mappedIndex) == multiply(credit, PRECISION); } @@ -183,9 +183,8 @@ hook Sstore marketState[KEY bytes32 id].totalUnits uint128 newTotal (uint128 old /// SUMMARY OF updatePositionView /// // -// Returns nondet (newCredit, newPendingFee, fee) constrained by the -// inequalities proved in UpdatePositionView.spec -// (rule `updatePositionViewReflectedByIndex`). +// Returns nondet (newCredit, newPendingFee, fee) constrained by the inequalities +// proved by rule updatePositionViewReflectedByFactor in UpdatePositionView.spec function summaryUpdatePositionView(env e, bytes32 id, address user) returns (uint128, uint128, uint128) { uint128 oldCredit = cvlCredit(id, user); uint128 oldPendingFee = cvlPendingFee(id, user); @@ -196,31 +195,15 @@ function summaryUpdatePositionView(env e, bytes32 id, address user) returns (uin uint128 newCredit; uint128 newPendingFee; uint128 fee; + mathint preciseCreditBefore = multiply(preciseCreditDivIndex[id][user], mapFactor(lossFactor(id))); - require newCredit <= oldCredit, "slashing only decreases credit"; - require newPendingFee <= oldPendingFee, "fee deduction only decreases pending"; - require fee <= oldPendingFee, "fee bounded by pending (UpdatePositionView.spec)"; - - // The touched user's pre-term lower bound (updatePositionView slashing bound). - // Kept in REAL-product form (per-user, cheap); the rule grounds the matching - // multiply(Dpre, M) to this same product. - //require (newCredit + fee) * PRECISION <= preciseCreditDivIndex[id][user] * mapIndex(lossFactor(id)), "newCredit (with fees) bounded by precise credit (UpdatePositionView.spec)"; - require multiply(newCredit, PRECISION) + multiply(fee, PRECISION) <= multiply(preciseCreditDivIndex[id][user], mapIndex(lossFactor(id))), "newCredit (with fees) bounded by precise credit (UpdatePositionView.spec)"; - - // A fully-slashed user (lossIndex == max, mapIndex == 0) gets credit and fee 0: updatePositionView's - // postSlashCredit ternary returns 0 when _lossIndex == max (Midnight.sol:752), and postSlashPending/fee - // then collapse to 0 too. Without this the summary admits newCredit > 0 for a fully-slashed user, which - // breaks the "division is exact" hook (0 == newCredit * PRECISION). - require mapIndex(cvlLastLossFactor(id, user)) == 0 => (newCredit == 0 && fee == 0), "fully-slashed user gets 0 credit/fee (updatePositionView _lossIndex == max guard)"; - - // Fully-slashed OBLIGATION also forces 0, independent of whether this user's own - // lastLossFactor has synced yet: postSlashCredit = credit.mulDivDown(mapIndex(lossFactor(id)), - // mapIndex(_lastLossFactor)) (Midnight.sol:820-821) has a ZERO NUMERATOR whenever - // mapIndex(lossFactor(id)) == 0, so mulDivDown returns exactly 0 regardless of the - // (nonzero) divisor -- and postSlashPendingFee/fee then cascade to 0 too (L824-830). - // Without this, a "stale" user (obligation fully slashed, user not yet synced) can - // leak nonzero newCredit/fee through the summary. - require mapIndex(lossFactor(id)) == 0 => (newCredit == 0 && fee == 0), "fully-slashed obligation gets 0 credit/fee regardless of user sync (mulDivDown zero-numerator)"; + require newCredit <= oldCredit, "proved in UpdatePositionView"; + require newPendingFee <= oldPendingFee, "proved in UpdatePositionView"; + require fee <= oldPendingFee, "proved in UpdatePositionView"; + require multiply(newCredit + fee, PRECISION) <= preciseCreditBefore, "proved in UpdatePositionView"; + + require axiomDistributivity(newCredit, fee, PRECISION), "axiom"; + require mapFactor(lossFactor(id)) == 0 => (newCredit == 0 && fee == 0), "proved in UpdatePositionView"; // help solver to reason about fee and distributivity. require axiomDistributivity(fee, continuousFeeCredit(id), PRECISION), "axiom"; @@ -255,58 +238,45 @@ strong invariant sumOfCreditsLeTotalUnits(bytes32 id) } } -// LIQUIDATE — the OPPOSITE of withdraw/take for multiply. Liquidate never -// calls _updatePosition or touches any user's credit (it writes the *obligation* -// lossFactor, not per-user position.lastLossFactor), so no hook fires and `sum` is -// UNCHANGED. Instead the obligation factor M rescales: -// mapIndex(new) = mulDivDown(mapIndex(old), tu - badDebt, tu) (Midnight.sol:589) -// continuousFeeCredit_new = mulDivDown(cf_old, mapIndex(new), mapIndex(old)) (L594) -// tu_new = tu_old - badDebt (L593) -// The aggregate `multiply(sum, M)` therefore changes via its 2ND argument, -// which additivity cannot express. So here we do the inverse of withdraw/take: -// GROUND the aggregate back to a real product (pre and post). That re-exposes -// sum*M_old and sum*M_new, but liquidate ALREADY discharges those via the -// ghostMulDivDown rounds-down bound (it verifies in the parametric invariant), -// and `sum` is a single snapshot here (not the touched-user delta), so the -// withdraw-style NIA divergence does not occur. rule sumOfCreditsLeTotalUnitsPreservedByLiquidate(bytes32 id, env e, Midnight.Market obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) { require sumOfCreditsBody(id); requireInvariant preciseCreditCorrect(id, borrower); require lastLossFactor(id, borrower) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; mathint sumPre = sumPreciseCreditDivIndex[id]; - mathint indexPre = mapIndex(lossFactor(id)); + mathint indexPre = mapFactor(lossFactor(id)); mathint tuPre = totalUnits(id); mathint cfPre = continuousFeeCredit(id); liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - mathint indexPost = mapIndex(lossFactor(id)); + // Liquidate never calls _updatePosition or touches any user's credit; `sum` is unchanged. + // Instead the lossFactor rescales: + // lossFactor = mapLossFactor(mulDivDown(mapFactor(lossFactor), totalUnits - badDebt, totalUnits)) + // continuousFeeCredit = mulDivDown(contnuousFeeCredit, mapFactor(new), mapFactor(old)) + // totalUnits = totalUnits - badDebt + + mathint indexPost = mapFactor(lossFactor(id)); mathint tuPost = totalUnits(id); mathint cfPost = continuousFeeCredit(id); - // Real fact (Midnight.sol:649): tuPost==tuPre-badDebt whenever liquidate's update block - // ran (badDebt>0); when badDebt==0 the block is skipped entirely and tuPost==tuPre, so - // this identity still gives badDebt==0 correctly either way. + // bad debt can be computed from the change of totalUnits. mathint badDebt = tuPre - tuPost; - // (C): linear combination of (A) and rearranged (B) (add (A) to -1*(B), i.e. - // cfPre*indexPost-cfPost*indexPre>=0), then factor via subtraction-distributivity -- both terms - // on each side share the SAME second argument (indexPost for the tuPre/cfPre pair, indexPre for - // tuPost/cfPost), which is exactly the shape multiply(a,m)-multiply(b,m)==multiply(a-b,m) - // needs, so this needs no cancellation, only the additivity already established. + // The proof requires several steps: + + // From mulDivDownRoundsDown for indexPost = indexPre.mulDivDown(tuPost, tuPre): + // tuPre * indexPost <= tuPost * indexPre + // From mulDivDownRoundsDown for cfPost = cfPre.mulDivDown(indexPost, indexPre): + // cfPost * indexPre <= cfPre * indexPost + + // Use the following distributivity rules: require axiomDistributivity(cfPre, tuPre - cfPre, indexPost), "axiom"; require axiomDistributivity(cfPost, tuPost - cfPost, indexPre), "axiom"; require axiomDistributivity(tuPre - cfPre, cfPre, PRECISION), "axiom"; require axiomDistributivity(tuPost - cfPost, cfPost, PRECISION), "axiom"; - // The proof requires several steps: - - // From mulDiv axioms for indexPost = indexPre.mulDivDown(tuPost, tuPre): - // tuPre * indexPost <= tuPost * indexPre - // From mulDiv axiom for cfPost = cfPre.mulDivDown(indexPost, indexPre): - // cfPost * indexPre <= cfPre * indexPost - // Using distributivity above: + // this yields // (tuPre - cfPre) * indexPost <= (tuPost - cfPost) * indexPre (A) // Then the main proof is: diff --git a/certora/specs/UpdatePositionView.spec b/certora/specs/UpdatePositionView.spec index fb98d9505..120c69b6d 100644 --- a/certora/specs/UpdatePositionView.spec +++ b/certora/specs/UpdatePositionView.spec @@ -29,13 +29,9 @@ methods { /// EXTERNAL CALLBACKS — collapse path explosion for strong invariants. /// function _.onBuy(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; function _.onSell(bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes) external => NONDET; - function _.isRatified(Midnight.Offer, bytes) external => NONDET; - function _.canIncreaseCredit(address) external => NONDET; - function _.canIncreaseDebt(address) external => NONDET; function _.onLiquidate(address, bytes32, Midnight.Market, uint256, uint256, uint256, address, address, bytes, uint256) external => NONDET; function _.onFlashLoan(address, address[], uint256[], bytes) external => NONDET; function _.onRepay(bytes32, Midnight.Market, uint256, address, bytes) external => NONDET; - function _.canLiquidate(address) external => NONDET; } /// MULDIV FUNCTION SUMMARIES /// @@ -113,8 +109,8 @@ hook Sload uint128 value position[KEY bytes32 id][KEY address owner].lastAccrual require lastAccrualMirror[id][owner] == value, "ghost mirror"; } -hook Sstore position[KEY bytes32 id][KEY address owner].pendingFee uint128 newPending (uint128 oldPending) { - pendingFeeMirror[id][owner] = newPending; +hook Sstore position[KEY bytes32 id][KEY address owner].pendingFee uint128 newPendingFee (uint128 oldPendingFee) { + pendingFeeMirror[id][owner] = newPendingFee; } hook Sstore position[KEY bytes32 id][KEY address owner].lastAccrual uint128 newLast (uint128 oldLast) { @@ -128,43 +124,28 @@ strong invariant preciseCreditCorrect(bytes32 id, address owner) /// RULES /// -rule updatePositionViewReflectedByFactor(env e, Midnight.Market obligation, bytes32 id, address owner) { - requireInvariant preciseCreditCorrect(id, owner); - require lastLossFactor(id, owner) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; +rule updatePositionViewProperties(env e, Midnight.Market obligation, bytes32 id, address user) { + requireInvariant preciseCreditCorrect(id, user); + require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight"; uint128 newCredit; - uint128 newPending; + uint128 newPendingFee; uint128 fee; - uint128 creditBefore = cvlCredit(id, owner); - mathint preciseCreditBefore = preciseCreditDivFactor[id][owner] * mapFactor(lossFactor(id)); - mathint pendingBefore = pendingFeeMirror[id][owner]; - mathint lastAccrualBefore = lastAccrualMirror[id][owner]; + uint128 oldCredit = cvlCredit(id, user); + mathint preciseCreditBefore = preciseCreditDivFactor[id][user] * mapFactor(lossFactor(id)); + mathint oldPendingFee = pendingFeeMirror[id][user]; + mathint oldLastAccrual = lastAccrualMirror[id][user]; - require e.block.timestamp >= lastAccrualBefore, "Time is increasing"; + require e.block.timestamp >= oldLastAccrual, "Time is increasing"; - newCredit, newPending, fee = updatePositionView(e, obligation, id, owner); + newCredit, newPendingFee, fee = updatePositionView(e, obligation, id, user); - assert fee <= pendingBefore, "Cannot take more fee than pending"; - assert (newCredit + fee) * PRECISION <= preciseCreditBefore, "newCredit (with fees) is at most precise credit after slashing"; - - // The two monotonicity facts the SumOfCredits summaries assume about - // `updatePositionView`. `newCredit <= creditBefore` holds because - // postSlashCredit = credit * mapFactor(lossFactor) / mapFactor(lastLossFactor) - // <= credit under `lossFactorLeqLastLossFactor`, and newCredit = - // postSlashCredit - fee. Proving them here means the summaries no longer - // rely on the indirect underflow-revert argument in `_updatePosition`. - assert newCredit <= creditBefore, "slashing and fee accrual only decrease credit"; - assert newPending <= pendingBefore, "fee deduction only decreases pending"; -} - -rule updatePositionZero(env e, Midnight.Market obligation, bytes32 id, address owner) { - require currentContract.position[id][owner].credit == 0, "Assume no credit"; + // These are the properties updatePositionView guarantees - uint128 newCredit; - uint128 newPending; - uint128 fee; - newCredit, newPending, fee = updatePositionView(e, obligation, id, owner); - - assert newCredit == 0 && newPending == 0 && fee == 0; + assert fee <= oldPendingFee, "Cannot take more fee than pending"; + assert (newCredit + fee) * PRECISION <= preciseCreditBefore, "newCredit (with fees) is at most precise credit after slashing"; + assert newCredit <= oldCredit, "slashing and fee accrual only decrease credit"; + assert newPendingFee <= oldPendingFee, "fee deduction only decreases pending"; + assert mapFactor(currentContract.marketState[id].lossFactor) == 0 => newCredit == 0 && fee == 0, "no credit/fee on total loss factor"; } From 1a38e115d5dac603f359ee10ea296223d96b8026 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 28 Aug 2026 16:16:57 +0200 Subject: [PATCH 11/11] Fix accidental revert of bugfix --- certora/specs/SumOfCreditsAxiomatic.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/SumOfCreditsAxiomatic.spec b/certora/specs/SumOfCreditsAxiomatic.spec index 4c9d8fd75..6263a84a8 100644 --- a/certora/specs/SumOfCreditsAxiomatic.spec +++ b/certora/specs/SumOfCreditsAxiomatic.spec @@ -81,7 +81,7 @@ definition axiomDistributivity(mathint a, mathint b, mathint c) returns bool = m definition axiomAssocComm(mathint a, mathint b, mathint c) returns bool = multiply(multiply(a, b), c) == multiply(multiply(a, c), b); // Linear order axiom for multiplication with positive constants. -definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c >= 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); +definition axiomLeMulPos(mathint a, mathint b, mathint c) returns bool = c > 0 => ((a <= b) <=> (multiply(a, c) <= multiply(b, c))); // The following is RoundsDown axiom stated using the `multiply` function. definition axiomMathMulDivDownRoundsDownMultiply(mathint a, mathint b, mathint d) returns bool = a >= 0 && b >= 0 => multiply(mathMulDivDown(a, b, d), d) <= multiply(a, b);