[Certora] ContinuousFee Protections

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"
+}

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;
+}