[Certora] SumOfCredits equals TotalUnits plus Fees.

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

certora/confs/UpdatePositionView.conf

@@ -0,0 +1,29 @@
+{
+  "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"
+}

certora/specs/SumOfCreditsAxiomatic.spec

@@ -0,0 +1,340 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+//
+
+import "MulDivAxioms.spec";
+
+methods {
+    function multicall(bytes[]) external => HAVOC_ALL DELETE;
+
+    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);
+
+    /// 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 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;
+    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 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 _.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;
+}
+
+/// 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;
+}
+
+// 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;
+    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 positive constants.
+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);
+
+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 {
+    if (d == 0 || a * b >= 2 ^ 256) {
+        revert();
+    }
+    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 (d == 0 || a * b + d - 1 >= 2 ^ 256) {
+        revert();
+    }
+    return require_uint256(ghostMulDivUp(a, b, d));
+}
+
+/// HELPER DEFINITIONS ///
+
+definition mapFactor(mathint index) returns mathint = 2 ^ 128 - 1 - index;
+
+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 cvlPendingFee(bytes32 id, address owner) returns uint128 = currentContract.position[id][owner].pendingFee;
+
+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] * 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 = mapFactor(newIndex);
+    mathint oldCDI = 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 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;
+    mathint oldSum = sumPreciseCreditDivIndex[id];
+    sumPreciseCreditDivIndex[id] = oldSum + newCDI - oldCDI;
+
+    // require distributivity axioms to help prover
+    mathint lossIndex = mapFactor(lossFactor(id));
+    require axiomDistributivity(oldSum, newCDI, lossIndex), "axiom";
+    require axiomDistributivity(oldSum + newCDI - oldCDI, oldCDI, lossIndex), "axiom";
+}
+
+function checkCreditDivInvariant(bytes32 id, address owner) returns bool {
+    uint128 credit = cvlCredit(id, owner);
+    uint128 userIndex = cvlLastLossFactor(id, owner);
+    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 (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);
+}
+
+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, cvlCredit(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 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);
+    uint128 oldLastAccrual = cvlLastAccrual(id, user);
+
+    require to_mathint(e.block.timestamp) >= to_mathint(oldLastAccrual), "time is non-decreasing";
+
+    uint128 newCredit;
+    uint128 newPendingFee;
+    uint128 fee;
+    mathint preciseCreditBefore = multiply(preciseCreditDivIndex[id][user], mapFactor(lossFactor(id)));
+
+    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";
+
+    return (newCredit, newPendingFee, fee);
+}
+
+/// INVARIANTS ///
+
+strong invariant preciseCreditCorrect(bytes32 id, address owner)
+    checkCreditDivInvariant(id, owner);
+
+// 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: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), "axiom";
+            require axiomDistributivity(totalUnits(id) - amount, amount, PRECISION), "axiom";
+        }
+
+        preserved updatePosition(Midnight.Market market, address user) with (env e) {
+            requireInvariant preciseCreditCorrect(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);
+            require lastLossFactor(id, onBehalf) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight";
+        }
+    }
+
+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 = mapFactor(lossFactor(id));
+    mathint tuPre = totalUnits(id);
+    mathint cfPre = continuousFeeCredit(id);
+
+    liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data);
+
+    // 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);
+
+    // bad debt can be computed from the change of totalUnits.
+    mathint badDebt = tuPre - tuPost;
+
+    // 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";
+
+    // this yields
+    // (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), "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);
+}
+
+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
+    address buyer = offer.buy ? offer.maker : taker;
+    address seller = offer.buy ? taker : offer.maker;
+
+    requireInvariant preciseCreditCorrect(id, taker);
+    require lastLossFactor(id, taker) <= currentContract.marketState[id].lossFactor, "lastLossFactorLeqMarketLossFactor in Midnight";
+    requireInvariant preciseCreditCorrect(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;
+
+    take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData);
+    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);
+}