diff --git a/certora/confs/ContinuousFee.conf b/certora/confs/ContinuousFee.conf new file mode 100644 index 000000000..55a0c3e53 --- /dev/null +++ b/certora/confs/ContinuousFee.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/ContinuousFee.spec", + "solc": "solc-0.8.34", + "solc_evm_version": "osaka", + "optimistic_hashing": true, + "hashing_length_bound": 2048, + "solc_via_ir": true, + "optimistic_loop": true, + "loop_iter": 2, + "prover_args": [ + "-depth 5", + "-timeout 3600", + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true", + "-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": "Midnight Continuous Fee" +} diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec new file mode 100644 index 000000000..6c2891a6c --- /dev/null +++ b/certora/specs/ContinuousFee.spec @@ -0,0 +1,154 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight); + + function creditOf(bytes32 id, address user) external returns (uint256) envfree; + function pendingFee(bytes32 id, address user) external returns (uint128) envfree; + function continuousFee(bytes32 id) external returns (uint32) envfree; + function continuousFeeCredit(bytes32 id) external returns (uint256) envfree; + + // Summarize internals irrelevant to continuous fee tracking. + function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; + function UtilsLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET; + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; + function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; + + // summaries over-approximating the behavior of transient storage. + function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET; + function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET; + + // Assume no reentrancy: callbacks and transfers do not re-enter Midnight. +} + +/// HELPERS /// + +// IdLib summary: remember the last id returned by toId. + +persistent ghost bytes32 lastId; + +function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 { + // non-deterministic id + bytes32 id; + lastId = id; + return id; +} + +definition WAD() returns uint256 = 10 ^ 18; + +// The buyer's pendingFee increases by floor(creditIncrease * continuousFee * timeToMaturity / WAD). +rule continuousFeeNotOverchargedForBuyer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { + address buyer = offer.buy ? offer.maker : taker; + + bytes32 id; + uint128 postUpdateCredit; + uint128 postUpdatePendingFee; + + postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, buyer); + + take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof); + + require id == lastId, "id should be derived from obligation"; + + uint256 contFee = continuousFee(id); + uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0; + + mathint creditDelta = creditOf(id, buyer) - postUpdateCredit; + + assert pendingFee(id, buyer) == postUpdatePendingFee + (creditDelta * contFee * timeToMaturity) / WAD(); +} + +// When a seller's credit decreases via a take, their pendingFee decreases by ceil(PendingFee * creditDelta / postUpdateCredit). +rule pendingFeeDecreasesProportionallyForSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { + address seller = offer.buy ? taker : offer.maker; + + bytes32 id; + uint128 postUpdateCredit; + uint128 postUpdatePendingFee; + + postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, seller); + + require postUpdateCredit > 0 || postUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec"; + + take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof); + + require id == lastId, "id should be derived from obligation"; + + uint256 creditAfter = creditOf(id, seller); + uint256 pendingFeeAfter = pendingFee(id, seller); + + require creditAfter > 0 || pendingFeeAfter == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec"; + + mathint creditDelta = postUpdateCredit - creditAfter; + + // When postUpdateCredit == 0: noRemainingContinuousFeeWithoutCredit gives postUpdatePendingFee == 0; credit is non-increasing for a seller, therefore creditAfter == 0; + // noRemainingContinuousFeeWithoutCredit gives pendingFeeAfter == 0; hence pendingFeeDelta == 0. + assert postUpdateCredit == 0 ? postUpdatePendingFee == pendingFeeAfter : postUpdatePendingFee == pendingFeeAfter + (postUpdatePendingFee * creditDelta + postUpdateCredit - 1) / postUpdateCredit; +} + +// When credit decreases via withdraw, pendingFee decreases by ceil(pendingFee * units / postUpdateCredit). +rule pendingFeeDecreasesProportionallyOnWithdraw(env e, Midnight.Obligation obligation, uint256 units, address onBehalf, address receiver) { + bytes32 id; + uint128 postUpdateCredit; + uint128 postUpdatePendingFee; + + postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, obligation, id, onBehalf); + + withdraw(e, obligation, units, onBehalf, receiver); + + require id == lastId, "id should be derived from obligation"; + + // When postUpdateCredit == 0, pendingFee(id, onBehalf) is unchanged on withdraw. + assert postUpdateCredit == 0 ? pendingFee(id, onBehalf) == postUpdatePendingFee : pendingFee(id, onBehalf) == postUpdatePendingFee - (postUpdatePendingFee * units + postUpdateCredit - 1) / postUpdateCredit; +} + +// take() increases continuousFeeCredit by exactly the sum of the accrued fees of the buyer and seller. +rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) { + address buyer = offer.buy ? offer.maker : taker; + address seller = offer.buy ? taker : offer.maker; + + bytes32 id; + uint128 buyerAccruedFee; + uint128 sellerAccruedFee; + + _, _, buyerAccruedFee = updatePositionView(e, offer.obligation, id, buyer); + _, _, sellerAccruedFee = updatePositionView(e, offer.obligation, id, seller); + + uint256 continuousFeeCreditBefore = continuousFeeCredit(id); + + take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof); + + require id == lastId, "id should be derived from obligation"; + + assert continuousFeeCredit(id) == continuousFeeCreditBefore + buyerAccruedFee + sellerAccruedFee; +} + +// take should not change the return values of updatePositionView (i.e., post-update credit, pending fee, and accrued fee) of a third party. +rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof, address user) { + address buyer = offer.buy ? offer.maker : taker; + address seller = offer.buy ? taker : offer.maker; + + require user != buyer && user != seller, "user is different from buyer and seller"; + + bytes32 id; + uint256 postUpdateCreditBefore; + uint256 postUpdatePendingFeeBefore; + uint256 userAccruedFeeBefore; + postUpdateCreditBefore, postUpdatePendingFeeBefore, userAccruedFeeBefore = updatePositionView(e, offer.obligation, id, user); + + take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof); + + require id == lastId, "id should be derived from obligation"; + + uint256 postUpdateCreditAfter; + uint256 postUpdatePendingFeeAfter; + uint256 userAccruedFeeAfter; + postUpdateCreditAfter, postUpdatePendingFeeAfter, userAccruedFeeAfter = updatePositionView(e, offer.obligation, id, user); + + assert postUpdateCreditBefore == postUpdateCreditAfter; + assert postUpdatePendingFeeBefore == postUpdatePendingFeeAfter; + assert userAccruedFeeBefore == userAccruedFeeAfter; +}