From 46c2871686d60748b62bab9536ab6ee7127269ba Mon Sep 17 00:00:00 2001 From: Bhargav Date: Sun, 12 Apr 2026 22:18:48 +0200 Subject: [PATCH 1/3] initial draft --- certora/confs/ContinuousFeeConserved.conf | 23 ++ certora/specs/ContinuousFeeConserved.spec | 292 ++++++++++++++++++++++ 2 files changed, 315 insertions(+) create mode 100644 certora/confs/ContinuousFeeConserved.conf create mode 100644 certora/specs/ContinuousFeeConserved.spec diff --git a/certora/confs/ContinuousFeeConserved.conf b/certora/confs/ContinuousFeeConserved.conf new file mode 100644 index 000000000..7363ec78c --- /dev/null +++ b/certora/confs/ContinuousFeeConserved.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "certora/helpers/Utils.sol", + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/ContinuousFeeConserved.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 1024, + "rule_sanity": "basic", + "multi_assert_check": true, + "smt_timeout": 7200, + "prover_args": [ + "-s", + "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]", + "-splitParallel true" + ], + "msg": "Continuous Fee Conserved" +} diff --git a/certora/specs/ContinuousFeeConserved.spec b/certora/specs/ContinuousFeeConserved.spec new file mode 100644 index 000000000..1ebcb75c1 --- /dev/null +++ b/certora/specs/ContinuousFeeConserved.spec @@ -0,0 +1,292 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// Continuous Fee Conservation +// +// The central property: the total fee still live in the system — pending (minted but not yet +// accrued) plus credited (accrued but not yet claimed) — can never exceed the total fee that +// was ever legitimately minted. +// +// totalPendingFeeMinted[id] +// = Σ buyerPendingFeeIncrease over every take() that increased a buyer's credit +// = the only source of new continuous fee in the protocol +// +// sumPendingFee[id] + continuousFeeCredit[id] ≤ totalPendingFeeMinted[id] +// +// The gap is fee that has been legitimately removed from the system: +// - accrued from pendingFee into continuousFeeCredit then claimed (buckets 1→2→3) +// - accrued then slashed by bad debt (buckets 1→2→4) +// - cancelled when a seller exits credit in take() +// - cancelled when credit is withdrawn in withdraw() +// - lost to lazy-slash realisation when _updatePosition is called after a lossIndex increase +// +// How the invariant closes the loop the per-function rules leave open: +// The per-function rules below constrain each function's effect on continuousFeeCredit in +// isolation, but they say nothing about the aggregate of pendingFee across all users. A bug +// that inflated continuousFeeCredit without a corresponding pendingFee minting event in take() +// would not be caught by the directional rules alone. The invariant catches exactly that: +// every unit still live in the system must be traceable to a buyerPendingFeeIncrease event. +// +// Why strong invariant holds at every intermediate Sstore: +// In _updatePosition the two writes are ordered: +// (1) position[id][user].pendingFee = newPendingFee -- sumPendingFee drops by accrued+slash +// (2) obligationState[id].continuousFeeCredit += accrued -- credit rises by accrued +// Between (1) and (2) the LHS has dipped by (accrued+slash), so LHS ≤ prior LHS ≤ RHS. ✓ +// After (2) LHS rises by accrued only, net LHS change = -slash ≤ 0. ✓ +// In take(), buyerPos.pendingFee += buyerPendingFeeIncrease triggers both sumPendingFee and +// totalPendingFeeMinted to increase by the same amount, keeping equality on the margin. ✓ + +using Utils as Utils; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function creditOf(bytes32 id, address user) external returns (uint256) envfree; + function debtOf(bytes32 id, address user) external returns (uint256) envfree; + function pendingFee(bytes32 id, address user) external returns (uint128) envfree; + function continuousFeeCredit(bytes32 id) external returns (uint256) envfree; + function lossIndex(bytes32 id) external returns (uint128) envfree; + function totalUnits(bytes32 id) external returns (uint256) envfree; + function withdrawable(bytes32 id) external returns (uint256) envfree; + function obligationCreated(bytes32 id) external returns (bool) envfree; + function _.price() external => NONDET; + + function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + + // Assume no reentrancy. + function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET; + function _.onLiquidate(bytes32, Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Obligation, uint256, address, bytes) external => NONDET; + function _.onFlashLoan(address, uint256, bytes) external => NONDET; + function _.transfer(address, uint256) external => NONDET; +} + +/// GHOSTS AND HOOKS /// + +// Running sum of position[id][user].pendingFee over every user for a given obligation id. +ghost mapping(bytes32 => mathint) sumPendingFee { + init_state axiom (forall bytes32 id. sumPendingFee[id] == 0); +} + +// Cumulative total of every increase to position[id][user].pendingFee. +// Increases only in take() via buyerPendingFeeIncrease — the sole source of new continuous fee. +ghost mapping(bytes32 => mathint) totalPendingFeeMinted { + init_state axiom (forall bytes32 id. totalPendingFeeMinted[id] == 0); +} + +// Cumulative total of every decrease to position[id][user].pendingFee (all causes combined: +// accrual, lazy-slash, seller exit in take(), proportional reduction in withdraw()). +ghost mapping(bytes32 => mathint) sumPendingFeeDecreased { + init_state axiom (forall bytes32 id. sumPendingFeeDecreased[id] == 0); +} + +// Cumulative total of every increase to obligationState[id].continuousFeeCredit (accrual only). +ghost mapping(bytes32 => mathint) continuousFeeCreditIncreased { + init_state axiom (forall bytes32 id. continuousFeeCreditIncreased[id] == 0); +} + +// Cumulative total of every decrease to obligationState[id].continuousFeeCredit (claims + bad-debt slash). +ghost mapping(bytes32 => mathint) continuousFeeCreditDecreased { + init_state axiom (forall bytes32 id. continuousFeeCreditDecreased[id] == 0); +} + +// Total fee that has permanently left the system through any channel: +// = (pendingFee decreases not offset by a continuousFeeCredit increase) [cancel + lazy-slash] +// + continuousFeeCredit decreases [claimed + bad-debt slashed] +// +// Derivation: every decrease to pendingFee either (a) moves to continuousFeeCredit (accrual) or +// (b) exits the system (cancel/lazy-slash). Subtracting (a) leaves only (b). Adding the +// decreases to continuousFeeCredit gives the full set of permanent exits. +definition totalExited(bytes32 id) returns mathint = + sumPendingFeeDecreased[id] - continuousFeeCreditIncreased[id] + continuousFeeCreditDecreased[id]; + +// Hook on position[id][user].pendingFee: maintains sumPendingFee, totalPendingFeeMinted, +// and sumPendingFeeDecreased. +hook Sstore position[KEY bytes32 id][KEY address user].pendingFee + uint128 newVal (uint128 oldVal) { + sumPendingFee[id] = sumPendingFee[id] + newVal - oldVal; + if (newVal > oldVal) { + totalPendingFeeMinted[id] = totalPendingFeeMinted[id] + (newVal - oldVal); + } + if (newVal < oldVal) { + sumPendingFeeDecreased[id] = sumPendingFeeDecreased[id] + (oldVal - newVal); + } +} + +// Hook on obligationState[id].continuousFeeCredit: maintains continuousFeeCreditIncreased +// and continuousFeeCreditDecreased. +hook Sstore obligationState[KEY bytes32 id].continuousFeeCredit + uint128 newVal (uint128 oldVal) { + if (newVal > oldVal) { + continuousFeeCreditIncreased[id] = continuousFeeCreditIncreased[id] + (newVal - oldVal); + } + if (newVal < oldVal) { + continuousFeeCreditDecreased[id] = continuousFeeCreditDecreased[id] + (oldVal - newVal); + } +} + +/// CONSERVATION INVARIANT /// + +// Total live fee (pending + credited) never exceeds total fee ever minted into pending. +// +// Preserved at every intermediate Sstore (strong invariant) because: +// - Decreases to sumPendingFee never increase the LHS beyond the prior value. +// - Increases to sumPendingFee (buyer minting) are matched one-for-one by increases to RHS. +// - Increases to continuousFeeCredit (accrual by amount `fee`) are always ≤ the preceding +// pendingFee decrease, because: +// pendingFeeDecrease = (oldPendingFee − postSlashPending) + fee ≥ fee = accrued +// since oldPendingFee ≥ postSlashPending (slashing only reduces pending). +// Net LHS change across both Sstores = accrued − pendingFeeDecrease = −slash ≤ 0. ✓ +// - Decreases to continuousFeeCredit (claims, slashing) only shrink the LHS. +// The upper-bound half: live fee never exceeds total minted. +// Implied by feeConservedExactly below (since totalExited >= 0), but kept as a standalone +// check because it is cheaper to prove and gives a cleaner counterexample when violated. +strong invariant feeInSystemBoundedByMinted(bytes32 id) + sumPendingFee[id] + to_mathint(continuousFeeCredit(id)) <= totalPendingFeeMinted[id] + { + preserved with (env e) { + require e.msg.sender != currentContract; + } + } + +// The lower-bound half: live fee plus all tracked exits equals total minted exactly. +// Together with feeInSystemBoundedByMinted this closes the conservation proof: +// fee can neither be created out of nothing nor disappear unexpectedly. +// +// totalExited accounts for every channel through which fee leaves the live system: +// (a) sumPendingFeeDecreased − continuousFeeCreditIncreased +// = fee that left pendingFee without going to continuousFeeCredit +// = lazy-slash (lossIndex increase in _updatePosition) + seller cancellation in take() +// + proportional reduction in withdraw() +// (b) continuousFeeCreditDecreased +// = fee that left continuousFeeCredit +// = claimed via claimContinuousFee + bad-debt slashed in liquidate() +// +// Preserved at every intermediate Sstore because each hook updates exactly one ghost, +// keeping the algebraic identity intact (verified case-by-case in the file header). +strong invariant feeConservedExactly(bytes32 id) + sumPendingFee[id] + to_mathint(continuousFeeCredit(id)) + totalExited(id) == totalPendingFeeMinted[id] + { + preserved with (env e) { + require e.msg.sender != currentContract; + } + } + +/// PER-FUNCTION SUPPORTING RULES /// + +rule updatePositionAccruesFeeCredit(env e, Midnight.Obligation obligation, address user) { + bytes32 id = toId(e, obligation); + + uint128 accrued; + _, _, accrued = updatePositionView(e, obligation, id, user); + uint256 feeCreditBefore = continuousFeeCredit(id); + + updatePosition(e, obligation, user); + + assert continuousFeeCredit(id) == feeCreditBefore + accrued; +} + +rule updatePositionSetsPendingFee(env e, Midnight.Obligation obligation, address user) { + bytes32 id = toId(e, obligation); + + uint128 newPending; + _, newPending, _ = updatePositionView(e, obligation, id, user); + + updatePosition(e, obligation, user); + + assert pendingFee(id, user) == newPending; +} + +/// BUCKET 1 → BUCKET 2 : withdraw /// + +rule withdrawAccruesFeeCredit(env e, Midnight.Obligation obligation, uint256 units, address onBehalf, address receiver) { + bytes32 id = toId(e, obligation); + + uint128 accrued; + _, _, accrued = updatePositionView(e, obligation, id, onBehalf); + uint256 feeCreditBefore = continuousFeeCredit(id); + + withdraw(e, obligation, units, onBehalf, receiver); + + assert continuousFeeCredit(id) == feeCreditBefore + accrued; +} + +/// BUCKET 1 (mint) + BUCKET 1 → BUCKET 2 (accrual) : take /// + +rule takeOnlyIncreasesFeeCredit(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { + bytes32 id = toId(e, offer.obligation); + uint256 feeCreditBefore = continuousFeeCredit(id); + + take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof); + + assert continuousFeeCredit(id) >= feeCreditBefore; +} + +rule takeMintsPendingFeeForBuyer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { + bytes32 id = toId(e, offer.obligation); + address buyer = offer.buy ? offer.maker : taker; + + uint128 newPendingBefore; + _, newPendingBefore, _ = updatePositionView(e, offer.obligation, id, buyer); + + take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof); + + assert pendingFee(id, buyer) >= newPendingBefore; +} + +/// BUCKET 2 → BUCKET 3 : claimContinuousFee /// + +rule claimReducesFeeCredit(env e, Midnight.Obligation obligation, uint256 amount, address receiver) { + bytes32 id = toId(e, obligation); + uint256 feeCreditBefore = continuousFeeCredit(id); + + claimContinuousFee(e, obligation, amount, receiver); + + assert continuousFeeCredit(id) == feeCreditBefore - amount; +} + +/// BUCKET 2 → BUCKET 4 : liquidate bad debt /// + +rule liquidateDoesNotIncreaseFeeCredit(env e, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { + bytes32 id = toId(e, obligation); + uint256 feeCreditBefore = continuousFeeCredit(id); + + liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + + assert continuousFeeCredit(id) <= feeCreditBefore; +} + +// Uses totalUnits as the proxy for "no bad debt" rather than lossIndex: when lossIndex is +// already saturated at type(uint128).max it stays at max even as bad debt is realized, yet +// continuousFeeCredit is still zeroed. totalUnits always decreases by badDebt regardless. +rule liquidateWithoutBadDebtPreservesFeeCredit(env e, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { + bytes32 id = toId(e, obligation); + uint256 totalUnitsBefore = totalUnits(id); + uint256 feeCreditBefore = continuousFeeCredit(id); + + liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + + assert totalUnits(id) == totalUnitsBefore => continuousFeeCredit(id) == feeCreditBefore; +} + +/// GLOBAL CONSERVATION : no other function touches continuousFeeCredit /// + +rule onlyExpectedFunctionsChangeFeeCredit(method f, env e, calldataarg args, bytes32 id) +filtered { + f -> !f.isView + && f.selector != sig:updatePosition(Midnight.Obligation, address).selector + && f.selector != sig:withdraw(Midnight.Obligation, uint256, address, address).selector + && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, bytes, bytes32, bytes32[]).selector + && f.selector != sig:claimContinuousFee(Midnight.Obligation, uint256, address).selector + && f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector +} { + uint256 feeCreditBefore = continuousFeeCredit(id); + f(e, args); + assert continuousFeeCredit(id) == feeCreditBefore; +} From 3101daa80eef4244ae268cd98728b66dcbe5e1d1 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Sun, 12 Apr 2026 22:45:48 +0200 Subject: [PATCH 2/3] removed equality invariant --- certora/specs/ContinuousFeeConserved.spec | 67 +---------------------- 1 file changed, 1 insertion(+), 66 deletions(-) diff --git a/certora/specs/ContinuousFeeConserved.spec b/certora/specs/ContinuousFeeConserved.spec index 1ebcb75c1..5207c5dcf 100644 --- a/certora/specs/ContinuousFeeConserved.spec +++ b/certora/specs/ContinuousFeeConserved.spec @@ -80,55 +80,13 @@ ghost mapping(bytes32 => mathint) totalPendingFeeMinted { init_state axiom (forall bytes32 id. totalPendingFeeMinted[id] == 0); } -// Cumulative total of every decrease to position[id][user].pendingFee (all causes combined: -// accrual, lazy-slash, seller exit in take(), proportional reduction in withdraw()). -ghost mapping(bytes32 => mathint) sumPendingFeeDecreased { - init_state axiom (forall bytes32 id. sumPendingFeeDecreased[id] == 0); -} - -// Cumulative total of every increase to obligationState[id].continuousFeeCredit (accrual only). -ghost mapping(bytes32 => mathint) continuousFeeCreditIncreased { - init_state axiom (forall bytes32 id. continuousFeeCreditIncreased[id] == 0); -} - -// Cumulative total of every decrease to obligationState[id].continuousFeeCredit (claims + bad-debt slash). -ghost mapping(bytes32 => mathint) continuousFeeCreditDecreased { - init_state axiom (forall bytes32 id. continuousFeeCreditDecreased[id] == 0); -} - -// Total fee that has permanently left the system through any channel: -// = (pendingFee decreases not offset by a continuousFeeCredit increase) [cancel + lazy-slash] -// + continuousFeeCredit decreases [claimed + bad-debt slashed] -// -// Derivation: every decrease to pendingFee either (a) moves to continuousFeeCredit (accrual) or -// (b) exits the system (cancel/lazy-slash). Subtracting (a) leaves only (b). Adding the -// decreases to continuousFeeCredit gives the full set of permanent exits. -definition totalExited(bytes32 id) returns mathint = - sumPendingFeeDecreased[id] - continuousFeeCreditIncreased[id] + continuousFeeCreditDecreased[id]; - -// Hook on position[id][user].pendingFee: maintains sumPendingFee, totalPendingFeeMinted, -// and sumPendingFeeDecreased. +// Hook on position[id][user].pendingFee: maintains sumPendingFee and totalPendingFeeMinted. hook Sstore position[KEY bytes32 id][KEY address user].pendingFee uint128 newVal (uint128 oldVal) { sumPendingFee[id] = sumPendingFee[id] + newVal - oldVal; if (newVal > oldVal) { totalPendingFeeMinted[id] = totalPendingFeeMinted[id] + (newVal - oldVal); } - if (newVal < oldVal) { - sumPendingFeeDecreased[id] = sumPendingFeeDecreased[id] + (oldVal - newVal); - } -} - -// Hook on obligationState[id].continuousFeeCredit: maintains continuousFeeCreditIncreased -// and continuousFeeCreditDecreased. -hook Sstore obligationState[KEY bytes32 id].continuousFeeCredit - uint128 newVal (uint128 oldVal) { - if (newVal > oldVal) { - continuousFeeCreditIncreased[id] = continuousFeeCreditIncreased[id] + (newVal - oldVal); - } - if (newVal < oldVal) { - continuousFeeCreditDecreased[id] = continuousFeeCreditDecreased[id] + (oldVal - newVal); - } } /// CONSERVATION INVARIANT /// @@ -155,29 +113,6 @@ strong invariant feeInSystemBoundedByMinted(bytes32 id) } } -// The lower-bound half: live fee plus all tracked exits equals total minted exactly. -// Together with feeInSystemBoundedByMinted this closes the conservation proof: -// fee can neither be created out of nothing nor disappear unexpectedly. -// -// totalExited accounts for every channel through which fee leaves the live system: -// (a) sumPendingFeeDecreased − continuousFeeCreditIncreased -// = fee that left pendingFee without going to continuousFeeCredit -// = lazy-slash (lossIndex increase in _updatePosition) + seller cancellation in take() -// + proportional reduction in withdraw() -// (b) continuousFeeCreditDecreased -// = fee that left continuousFeeCredit -// = claimed via claimContinuousFee + bad-debt slashed in liquidate() -// -// Preserved at every intermediate Sstore because each hook updates exactly one ghost, -// keeping the algebraic identity intact (verified case-by-case in the file header). -strong invariant feeConservedExactly(bytes32 id) - sumPendingFee[id] + to_mathint(continuousFeeCredit(id)) + totalExited(id) == totalPendingFeeMinted[id] - { - preserved with (env e) { - require e.msg.sender != currentContract; - } - } - /// PER-FUNCTION SUPPORTING RULES /// rule updatePositionAccruesFeeCredit(env e, Midnight.Obligation obligation, address user) { From 63f692965a5fab45fae7479ae9abd6ed4474a30e Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 13 Apr 2026 16:28:07 +0200 Subject: [PATCH 3/3] cleaned up comments --- certora/specs/ContinuousFeeConserved.spec | 47 ++++++++--------------- 1 file changed, 17 insertions(+), 30 deletions(-) diff --git a/certora/specs/ContinuousFeeConserved.spec b/certora/specs/ContinuousFeeConserved.spec index 5207c5dcf..37365740e 100644 --- a/certora/specs/ContinuousFeeConserved.spec +++ b/certora/specs/ContinuousFeeConserved.spec @@ -19,21 +19,6 @@ // - cancelled when credit is withdrawn in withdraw() // - lost to lazy-slash realisation when _updatePosition is called after a lossIndex increase // -// How the invariant closes the loop the per-function rules leave open: -// The per-function rules below constrain each function's effect on continuousFeeCredit in -// isolation, but they say nothing about the aggregate of pendingFee across all users. A bug -// that inflated continuousFeeCredit without a corresponding pendingFee minting event in take() -// would not be caught by the directional rules alone. The invariant catches exactly that: -// every unit still live in the system must be traceable to a buyerPendingFeeIncrease event. -// -// Why strong invariant holds at every intermediate Sstore: -// In _updatePosition the two writes are ordered: -// (1) position[id][user].pendingFee = newPendingFee -- sumPendingFee drops by accrued+slash -// (2) obligationState[id].continuousFeeCredit += accrued -- credit rises by accrued -// Between (1) and (2) the LHS has dipped by (accrued+slash), so LHS ≤ prior LHS ≤ RHS. ✓ -// After (2) LHS rises by accrued only, net LHS change = -slash ≤ 0. ✓ -// In take(), buyerPos.pendingFee += buyerPendingFeeIncrease triggers both sumPendingFee and -// totalPendingFeeMinted to increase by the same amount, keeping equality on the margin. ✓ using Utils as Utils; @@ -81,8 +66,7 @@ ghost mapping(bytes32 => mathint) totalPendingFeeMinted { } // Hook on position[id][user].pendingFee: maintains sumPendingFee and totalPendingFeeMinted. -hook Sstore position[KEY bytes32 id][KEY address user].pendingFee - uint128 newVal (uint128 oldVal) { +hook Sstore position[KEY bytes32 id][KEY address user].pendingFee uint128 newVal (uint128 oldVal) { sumPendingFee[id] = sumPendingFee[id] + newVal - oldVal; if (newVal > oldVal) { totalPendingFeeMinted[id] = totalPendingFeeMinted[id] + (newVal - oldVal); @@ -92,19 +76,6 @@ hook Sstore position[KEY bytes32 id][KEY address user].pendingFee /// CONSERVATION INVARIANT /// // Total live fee (pending + credited) never exceeds total fee ever minted into pending. -// -// Preserved at every intermediate Sstore (strong invariant) because: -// - Decreases to sumPendingFee never increase the LHS beyond the prior value. -// - Increases to sumPendingFee (buyer minting) are matched one-for-one by increases to RHS. -// - Increases to continuousFeeCredit (accrual by amount `fee`) are always ≤ the preceding -// pendingFee decrease, because: -// pendingFeeDecrease = (oldPendingFee − postSlashPending) + fee ≥ fee = accrued -// since oldPendingFee ≥ postSlashPending (slashing only reduces pending). -// Net LHS change across both Sstores = accrued − pendingFeeDecrease = −slash ≤ 0. ✓ -// - Decreases to continuousFeeCredit (claims, slashing) only shrink the LHS. -// The upper-bound half: live fee never exceeds total minted. -// Implied by feeConservedExactly below (since totalExited >= 0), but kept as a standalone -// check because it is cheaper to prove and gives a cleaner counterexample when violated. strong invariant feeInSystemBoundedByMinted(bytes32 id) sumPendingFee[id] + to_mathint(continuousFeeCredit(id)) <= totalPendingFeeMinted[id] { @@ -212,6 +183,8 @@ rule liquidateWithoutBadDebtPreservesFeeCredit(env e, Midnight.Obligation obliga /// GLOBAL CONSERVATION : no other function touches continuousFeeCredit /// +// continuousFeeCredit can only be modified by the five functions with explicit per-function rules. +// Together with those rules this closes the continuousFeeCredit side of the bypass argument. rule onlyExpectedFunctionsChangeFeeCredit(method f, env e, calldataarg args, bytes32 id) filtered { f -> !f.isView @@ -225,3 +198,17 @@ filtered { f(e, args); assert continuousFeeCredit(id) == feeCreditBefore; } + +/// GLOBAL CONSERVATION : no other function touches pendingFee /// + +rule onlyExpectedFunctionsChangePendingFee(method f, env e, calldataarg args, bytes32 id, address user) +filtered { + f -> !f.isView + && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, bytes, bytes32, bytes32[]).selector + && f.selector != sig:updatePosition(Midnight.Obligation, address).selector + && f.selector != sig:withdraw(Midnight.Obligation, uint256, address, address).selector +} { + uint128 pendingFeeBefore = pendingFee(id, user); + f(e, args); + assert pendingFee(id, user) == pendingFeeBefore; +}