diff --git a/certora/confs/NetCredit.conf b/certora/confs/NetCredit.conf new file mode 100644 index 00000000..10f2b302 --- /dev/null +++ b/certora/confs/NetCredit.conf @@ -0,0 +1,20 @@ +{ + "files": [ + "certora/helpers/Utils.sol", + "src/Midnight.sol" + ], + "verify": "Midnight:certora/specs/NetCredit.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": 2048, + "smt_timeout": 7200, + "multi_assert_check": true, + "prover_args": [ + "-destructiveOptimizations twostage" + ], + "msg": "NetCredit" +} diff --git a/certora/specs/MulDiv.spec b/certora/specs/MulDiv.spec index 16f6c483..1463d792 100644 --- a/certora/specs/MulDiv.spec +++ b/certora/specs/MulDiv.spec @@ -29,6 +29,18 @@ rule mulDivMonotoneD(uint256 a, uint256 b, uint256 d1, uint256 d2) { assert d1 <= d2 => mulDivUp(a, b, d1) >= mulDivUp(a, b, d2); } +// 1-Lipschitz in the first argument when b <= d: the result cannot grow faster than the numerator a. +rule mulDivLipschitzA(uint256 a1, uint256 a2, uint256 b, uint256 d) { + assert b <= d && a1 <= a2 => mulDivDown(a2, b, d) - mulDivDown(a1, b, d) <= a2 - a1; + assert b <= d && a1 <= a2 => mulDivUp(a2, b, d) - mulDivUp(a1, b, d) <= a2 - a1; +} + +// 1-Lipschitz in the second argument when a <= d: the result cannot grow faster than the numerator b. +rule mulDivLipschitzB(uint256 a, uint256 b1, uint256 b2, uint256 d) { + assert a <= d && b1 <= b2 => mulDivDown(a, b2, d) - mulDivDown(a, b1, d) <= b2 - b1; + assert a <= d && b1 <= b2 => mulDivUp(a, b2, d) - mulDivUp(a, b1, d) <= b2 - b1; +} + rule mulDivAddDownDown(uint256 a1, uint256 a2, uint256 b, uint256 d) { uint256 a1plusa2 = require_uint256(a1 + a2); assert mulDivDown(a1, b, d) + mulDivDown(a2, b, d) <= mulDivDown(a1plusa2, b, d); diff --git a/certora/specs/NetCredit.spec b/certora/specs/NetCredit.spec new file mode 100644 index 00000000..bba6916b --- /dev/null +++ b/certora/specs/NetCredit.spec @@ -0,0 +1,216 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +using Utils as Utils; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function lossFactor(bytes32 id) external returns (uint128) envfree; + function pendingFee(bytes32 id, address user) external returns (uint128) envfree; + function creditOf(bytes32 id, address user) external returns (uint128) envfree; + function lastAccrual(bytes32 id, address user) external returns (uint128) envfree; + function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; + function continuousFee(bytes32 id) external returns (uint32) envfree; + function toId(Midnight.Market) external returns (bytes32) envfree; + function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; + + // Deterministic hash preserves market-to-id relationship without adding assumptions. + function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market); + + // Summarize mulDivDown and mulDivUp to simplify the verification task. + // Use a ghost function that ensures mulDivDown/Up behaves deterministically and add only the axioms about mulDiv that are needed to prove the desired property. + 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); + + // Over-approximate view functions. + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function settlementFee(bytes32, uint256) internal returns (uint256) => NONDET; + function isHealthy(Midnight.Market memory, bytes32, address) internal returns (bool) => NONDET; +} + +/// HELPERS /// + +definition MAX_CONTINUOUS_FEE() returns uint256 = 317097919; + +definition MAX_TTM() returns mathint = 100 * 365 * 86400; + +definition WAD() returns uint256 = 10 ^ 18; + +definition zeroFloorSub(uint256 a, uint256 b) returns mathint = a >= b ? a - b : 0; + +/// SUMMARY FUNCTIONS /// + +persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256 { + /* proved in mulDivZero in MulDiv.spec */ + axiom forall uint256 b. forall uint256 d. d > 0 => ghostMulDivDown(0, b, d) == 0; + axiom forall uint256 a. forall uint256 d. d > 0 => ghostMulDivDown(a, 0, d) == 0; + + /* proved in mulDivIdentity in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. b > 0 => ghostMulDivDown(a, b, b) == a; + + /* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && b <= d => ghostMulDivDown(a, b, d) <= a; +} + +persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256 { + /* proved in mulDivZero in MulDiv.spec */ + axiom forall uint256 a. forall uint256 d. d > 0 => ghostMulDivUp(a, 0, d) == 0; + + /* proved in mulDivArgumentLesserThanDenominator in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && a <= d => ghostMulDivUp(a, b, d) <= b; + + /* proved in mulDivResidualBound in MulDiv.spec */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. a <= d && b <= d => a - ghostMulDivUp(a, b, d) <= d - b; +} + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return ghostMulDivDown(a, b, d); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return ghostMulDivUp(a, b, d); +} + +function summaryToId(Midnight.Market market) returns (bytes32) { + return Utils.hashMarket(market); +} + +/// The up-to-date face value of a lender's position: credit - pendingFee after slashing and fee accrual. +function netCredit(env e, Midnight.Market market, address user) returns mathint { + bytes32 id = toId(market); + uint128 credit; + uint128 pending; + uint128 accruedFee; + require pendingFee(id, user) <= creditOf(id, user), "See pendingContinuousFeeBoundedByCredit in Midnight.spec"; + require lastLossFactor(id, user) <= lossFactor(id), "See lastLossFactorLeqMarketLossFactor in Midnight.spec"; + credit, pending, accruedFee = updatePositionView(e, market, id, user); + return credit - pending; +} + +/// INVARIANTS /// + +/// Once a position has been accrued at or after maturity, its pending fee is fully realized and stays +/// at zero: the continuous fee only accrues up to maturity, so there is nothing left to accrue. +/// This implies that the net credit is equal to the credit once a position has been accrued at or after maturity. +invariant pendingFeeZeroAfterMaturity(Midnight.Market market, bytes32 id, address user) + toId(market) == id && lastAccrual(id, user) >= market.maturity => pendingFee(id, user) == 0; + +/// RULES /// + +/// The up-to-date face value of a lender's position (credit - pendingFee) can only change by +/// withdrawing, taking, or liquidating. Every other function leaves it unchanged. +rule netCreditUnaffected(env e, method f, calldataarg args, Midnight.Market market, address user) +filtered { + f -> !f.isView + && f.selector != sig:withdraw(Midnight.Market, uint256, address, address).selector + && 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 +} { + mathint creditBefore = netCredit(e, market, user); + + f(e, args); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter == creditBefore; +} + +/// Withdrawing on behalf of another account does not change an unrelated user's net credit. +rule withdrawDoesNotChangeOtherNetCredit(env e, Midnight.Market withdrawMarket, uint256 units, address onBehalf, address receiver, Midnight.Market market, address user) { + require user != onBehalf || toId(withdrawMarket) != toId(market), "withdrawing for someone else or on another market"; + + mathint creditBefore = netCredit(e, market, user); + + withdraw(e, withdrawMarket, units, onBehalf, receiver); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter == creditBefore; +} + +/// Withdrawing cannot increase net credit. +rule withdrawNetCreditNonIncreasing(env e, Midnight.Market withdrawMarket, uint256 units, address onBehalf, address receiver, Midnight.Market market, address user) { + mathint creditBefore = netCredit(e, market, user); + + withdraw(e, withdrawMarket, units, onBehalf, receiver); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter <= creditBefore; +} + +/// Taking does not change the net credit of a user that is neither the taker nor the offer's maker. +rule takeDoesNotChangeOtherNetCredit(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, Midnight.Market market, address user) { + require (user != taker && user != offer.maker) || toId(offer.market) != toId(market), "user is not involved in the take or another market"; + + mathint creditBefore = netCredit(e, market, user); + + take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter == creditBefore; +} + +/// Taking does not decrease the net credit of a buyer in a take, and does not increase the net credit of a seller in a take. +rule takeNetCreditChangeForBuyerAndSeller(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, address user) { + mathint creditBefore = netCredit(e, offer.market, user); + + take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + + // We require it after `take`, because `take` may initialize the market first. + require continuousFee(toId(offer.market)) <= MAX_CONTINUOUS_FEE(), "See continuousFeeBounded in Midnight.sol"; + require offer.market.maturity <= e.block.timestamp + MAX_TTM(), "Maturity not too far in the future"; + assert continuousFee(toId(offer.market)) * zeroFloorSub(offer.market.maturity, e.block.timestamp) <= WAD(), "interest <= 100%"; + + mathint creditAfter = netCredit(e, offer.market, user); + + address buyer = offer.buy ? offer.maker : taker; + address seller = offer.buy ? taker : offer.maker; + assert user == buyer => creditAfter >= creditBefore; + assert user == seller => creditAfter <= creditBefore; +} + +/// Liquidating does not change any user's net credit as long as no bad debt is realized on the same market, +/// i.e. the market loss factor is unchanged by the liquidation. +rule liquidateWithoutBadDebtDoesNotChangeCredit(env e, Midnight.Market liquidateMarket, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, Midnight.Market market, address user) { + bytes32 id = toId(market); + uint128 lossFactorBefore = lossFactor(id); + + mathint creditBefore = netCredit(e, market, user); + + liquidate(e, liquidateMarket, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + // Restrict to executions in which no bad debt was realized or that are on other markets. + require lossFactor(id) == lossFactorBefore || toId(liquidateMarket) != toId(market), "no bad debt realized or on different market"; + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter == creditBefore; +} + +/// Liquidation cannot increase net credit. +rule liquidateNetCreditNonIncreasing(env e, Midnight.Market liquidateMarket, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data, Midnight.Market market, address user) { + mathint creditBefore = netCredit(e, market, user); + + require forall uint256 a. forall uint256 b1. forall uint256 b2. forall uint256 d. d > 0 => b1 <= b2 => ghostMulDivUp(a, b1, d) <= ghostMulDivUp(a, b2, d), "See mulDivMonotoneB in MulDiv.spec"; + require forall uint256 a. forall uint256 b1. forall uint256 b2. forall uint256 d. d > 0 => a <= d => b2 <= b1 => ghostMulDivUp(a, b1, d) - ghostMulDivUp(a, b2, d) <= b1 - b2, "See mulDivLipschitzB in MulDiv.spec"; + require forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => b <= d => ghostMulDivUp(a, b, d) <= a, "See mulDivArgumentLesserThanDenominator in MulDiv.spec"; + + require forall uint256 a. forall uint256 b1. forall uint256 b2. forall uint256 d. d > 0 => b1 <= b2 => ghostMulDivDown(a, b1, d) <= ghostMulDivDown(a, b2, d), "See mulDivMonotoneB in MulDiv.spec"; + require forall uint256 a1. forall uint256 a2. forall uint256 b. forall uint256 d. d > 0 => a1 <= a2 => ghostMulDivDown(a1, b, d) <= ghostMulDivDown(a2, b, d), "See mulDivMonotoneA in MulDiv.spec"; + require forall uint256 a1. forall uint256 a2. forall uint256 b. forall uint256 d. d > 0 => b <= d => a1 <= a2 => ghostMulDivDown(a2, b, d) - ghostMulDivDown(a1, b, d) <= a2 - a1, "See mulDivLipschitzA in MulDiv.spec"; + + liquidate(e, liquidateMarket, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); + + mathint creditAfter = netCredit(e, market, user); + + assert creditAfter <= creditBefore; +}