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..37365740e --- /dev/null +++ b/certora/specs/ContinuousFeeConserved.spec @@ -0,0 +1,214 @@ +// 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 +// + +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); +} + +// 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); + } +} + +/// CONSERVATION INVARIANT /// + +// Total live fee (pending + credited) never exceeds total fee ever minted into pending. +strong invariant feeInSystemBoundedByMinted(bytes32 id) + sumPendingFee[id] + to_mathint(continuousFeeCredit(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 /// + +// 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 + && 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; +} + +/// 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; +}