add chainId and midnight to Market

certora/confs/BalanceEffects.conf

@@ -1,7 +1,11 @@
 {
   "files": [
+    "certora/helpers/Utils.sol",
     "src/Midnight.sol"
   ],
+  "parametric_contracts": [
+    "Midnight"
+  ],
   "verify": "Midnight:certora/specs/BalanceEffects.spec",
   "solc": "solc-0.8.34",
   "solc_via_ir": true,

certora/confs/Solvency.conf

@@ -1,6 +1,7 @@
 {
   "files": [
     "src/Midnight.sol",
+    "certora/helpers/Utils.sol",
     "certora/helpers/FlashLiquidateCallback.sol"
   ],
   "parametric_contracts": [

certora/confs/WithdrawableMonotonicity.conf

@@ -1,7 +1,11 @@
 {
   "files": [
+    "certora/helpers/Utils.sol",
     "src/Midnight.sol"
   ],
+  "parametric_contracts": [
+    "Midnight"
+  ],
   "verify": "Midnight:certora/specs/WithdrawableMonotonicity.spec",
   "solc": "solc-0.8.34",
   "solc_via_ir": true,

certora/helpers/Utils.sol

@@ -4,6 +4,7 @@ pragma solidity ^0.8.0;
 
 import {Offer, Market} from "../../src/interfaces/IMidnight.sol";
 import {UtilsLib} from "../../src/libraries/UtilsLib.sol";
+import {IdLib} from "../../src/libraries/IdLib.sol";
 import {
     CALLBACK_SUCCESS,
     LIQUIDATION_CURSOR_LOW,
@@ -14,6 +15,10 @@ import {
 } from "../../src/libraries/ConstantsLib.sol";
 
 contract Utils {
+    function toId(Market memory market) external pure returns (bytes32) {
+        return IdLib.toId(market);
+    }
+
     function hashMarket(Market memory market) external pure returns (bytes32) {
         return keccak256(abi.encode(market));
     }

certora/specs/BalanceEffects.spec

@@ -1,6 +1,9 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+using Utils as Utils;
+
 methods {
+    function Utils.toId(Midnight.Market) external returns (bytes32) envfree;
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
     function credit(bytes32 id, address user) external returns (uint128) envfree;
@@ -12,7 +15,7 @@ methods {
     function continuousFeeCredit(bytes32 id) external returns (uint128) envfree;
 
     // Summarize internals irrelevant to credit and debt tracking.
-    function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET;
+    function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET;
     function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET;
     function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
     function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;
@@ -34,7 +37,7 @@ methods {
 /// sets it to the post-update value, only changes credit of user at the market id,
 /// and accrues fee to continuousFeeCredit.
 rule updatePositionEffects(env e, Midnight.Market market, address user, bytes32 anyId, address anyUser) {
-    bytes32 id = toId(e, market);
+    bytes32 id = Utils.toId(market);
 
     uint256 creditBefore = credit(id, user);
     uint128 updatedUserCredit;
@@ -61,7 +64,7 @@ rule updatePositionEffects(env e, Midnight.Market market, address user, bytes32
 /// withdraw decreases onBehalf's post-update credit by exactly units
 /// and only changes credit of onBehalf at the market id.
 rule withdrawEffects(env e, Midnight.Market market, uint256 units, address onBehalf, address receiver, bytes32 anyId, address anyUser) {
-    bytes32 id = toId(e, market);
+    bytes32 id = Utils.toId(market);
 
     uint128 updatedUserCredit;
     uint128 userFee;
@@ -84,7 +87,7 @@ rule withdrawEffects(env e, Midnight.Market market, uint256 units, address onBeh
 /// take changes maker's and taker's net credit-debt by +/- units relative to their post-update values
 /// and only changes credit of maker and taker and debt of maker and taker at the market id.
 rule takeEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData, bytes32 anyId, address anyUser) {
-    bytes32 id = toId(e, offer.market);
+    bytes32 id = Utils.toId(offer.market);
 
     uint128 makerCreditBefore;
     makerCreditBefore, _, _ = updatePositionView(e, offer.market, id, offer.maker);
@@ -112,7 +115,7 @@ rule takeEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 units,
 /// Buyer's credit is non-decreasing relative to its post-update value and can increase by at most take units.
 /// Buyer's debt is non-increasing and can decrease by at most take units.
 rule takeBuyerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) {
-    bytes32 id = toId(e, offer.market);
+    bytes32 id = Utils.toId(offer.market);
 
     address buyer = offer.buy ? offer.maker : taker;
     uint256 buyerDebtBefore = debt(id, buyer);
@@ -132,7 +135,7 @@ rule takeBuyerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 u
 /// Seller's debt is non-decreasing, and can increase by at most take units.
 /// Seller's credit is non-increasing relative to its post-update value and can decrease by at most take units.
 rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, address taker, address receiver, address takerCallback, bytes takerCallbackData) {
-    bytes32 id = toId(e, offer.market);
+    bytes32 id = Utils.toId(offer.market);
 
     address seller = offer.buy ? taker : offer.maker;
     uint256 sellerDebtBefore = debt(id, seller);
@@ -152,7 +155,7 @@ rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256
 
 /// Repay decreases onBehalf's debt by exactly units and only changes position[id][onBehalf].debt
 rule repayEffects(env e, Midnight.Market market, uint256 units, address onBehalf, address callback, bytes data, bytes32 anyId, address anyUser) {
-    bytes32 id = toId(e, market);
+    bytes32 id = Utils.toId(market);
 
     uint256 debtBefore = debt(id, onBehalf);
     uint256 otherCreditBefore = credit(anyId, anyUser);
@@ -170,7 +173,7 @@ rule repayEffects(env e, Midnight.Market market, uint256 units, address onBehalf
 /// Liquidate decreases the borrower's debt by at least repaidUnits,
 /// and only changes position[id][borrower].debt.
 rule liquidateEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bytes32 anyId, address anyUser, bool postMaturityMode) {
-    bytes32 id = toId(e, market);
+    bytes32 id = Utils.toId(market);
 
     uint256 debtBefore = debt(id, borrower);
     uint256 otherCreditBefore = credit(anyId, anyUser);
@@ -209,7 +212,7 @@ filtered {
 /// supplyCollateral increases onBehalf's collateral by exactly assets,
 /// and only changes position[id][onBehalf].collateral[collateralIndex].
 rule supplyCollateralEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf, bytes32 anyId, address anyUser, uint256 anyIndex) {
-    bytes32 id = toId(e, market);
+    bytes32 id = Utils.toId(market);
 
     uint256 collateralBefore = collateral(id, onBehalf, collateralIndex);
     uint256 otherCollateralBefore = collateral(anyId, anyUser, anyIndex);
@@ -225,7 +228,7 @@ rule supplyCollateralEffects(env e, Midnight.Market market, uint256 collateralIn
 /// withdrawCollateral decreases onBehalf's collateral by exactly assets,
 /// and only changes position[id][onBehalf].collateral[collateralIndex].
 rule withdrawCollateralCollateralEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 assets, address onBehalf, address receiver, bytes32 anyId, address anyUser, uint256 anyIndex) {
-    bytes32 id = toId(e, market);
+    bytes32 id = Utils.toId(market);
 
     uint256 collateralBefore = collateral(id, onBehalf, collateralIndex);
     uint256 otherCollateralBefore = collateral(anyId, anyUser, anyIndex);
@@ -241,7 +244,7 @@ rule withdrawCollateralCollateralEffects(env e, Midnight.Market market, uint256
 /// liquidate decreases the borrower's collateral at collateralIndex by exactly seizedResult,
 /// and only changes position[id][borrower].collateral[collateralIndex].
 rule liquidateCollateralEffects(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bytes32 anyId, address anyUser, uint256 anyIndex, bool postMaturityMode) {
-    bytes32 id = toId(e, market);
+    bytes32 id = Utils.toId(market);
 
     uint256 collateralBefore = collateral(id, borrower, collateralIndex);
     uint256 otherCollateralBefore = collateral(anyId, anyUser, anyIndex);

certora/specs/BundlerRepayInvertibility.spec

@@ -10,7 +10,7 @@ methods {
     function midnight.tickSpacing(bytes32 id) external returns (uint8) envfree;
 
     // Deterministic market id (same pattern as Midnight.spec / TakeAmountsLibInvertibility.spec).
-    function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market);
+    function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
 
     // Deterministic mulDivDown.
     function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d);

certora/specs/CollateralBitmap.spec

@@ -18,7 +18,7 @@ methods {
      */
     function _.price() external => PER_CALLEE_CONSTANT;
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
-    function IdLib.toId(Midnight.Market memory market, uint256 chainId, address midnight) internal returns (bytes32) => NONDET;
+    function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => NONDET;
 
     /* Simplify mulDiv reasoning for the solver.  We summarize these by ghost functions, i.e.,
      * arbitrary deterministic functions and axiomatize the axioms we need.

certora/specs/Consume.spec

@@ -7,7 +7,7 @@ methods {
     function totalUnits(bytes32 id) external returns (uint128) envfree;
 
     // Summaries for complex internals irrelevant to consumed-mapping properties.
-    function IdLib.toId(Midnight.Market memory, uint256, address) internal returns (bytes32) => NONDET;
+    function IdLib.toId(Midnight.Market memory) internal returns (bytes32) => NONDET;
     function UtilsLib.mulDivDown(uint256, uint256, uint256) internal returns (uint256) => NONDET;
     function UtilsLib.mulDivUp(uint256, uint256, uint256) internal returns (uint256) => NONDET;
     function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;

certora/specs/ContinuousFee.spec

@@ -3,15 +3,15 @@
 methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
-    function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => CVL_toId(market);
+    function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => CVL_toId(market);
 
     function credit(bytes32 id, address user) external returns (uint128) 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 (uint128) envfree;
 
     // Summarize internals irrelevant to continuous fee tracking.
-    function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET;
+    function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET;
     function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
 

certora/specs/CreatedMarkets.spec

@@ -25,10 +25,10 @@ methods {
     function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => ghostMulDivDown(x, y, d);
 
     // Summary is required because abi.encodePacked doesn't ensure injectivity of the hash function in CVL, for an unknown reason.
-    function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market);
+    function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
 
     // Sound because the protocol doesn't use toMarket.
-    function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET;
+    function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET;
 
     // Tokens are assumed to not reenter, for performance reasons.
     function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
@@ -130,7 +130,17 @@ rule marketIsCreatedAfterLiquidate(env e, Midnight.Market market, uint256 collat
     assert marketIsCreated(market);
 }
 
-// Markets can only be created by: touchMarket, take, withdraw, repay, supplyCollateral, withdrawCollateral or liquidate.
+rule marketIsCreatedAfterClaimContinuousFee(env e, Midnight.Market market, uint256 amount, address receiver) {
+    claimContinuousFee(e, market, amount, receiver);
+    assert marketIsCreated(market);
+}
+
+rule marketIsCreatedAfterUpdatePosition(env e, Midnight.Market market, address user) {
+    updatePosition(e, market, user);
+    assert marketIsCreated(market);
+}
+
+// Markets can only be created by: touchMarket, take, withdraw, repay, supplyCollateral, withdrawCollateral, liquidate, claimContinuousFee or updatePosition.
 rule onlyTouchMarketCreatesMarket(env e, method f, calldataarg args, Midnight.Market market)
 filtered {
     f -> f.selector != sig:touchMarket(Midnight.Market).selector
@@ -140,6 +150,8 @@ filtered {
         && f.selector != sig:supplyCollateral(Midnight.Market, uint256, uint256, address).selector
         && f.selector != sig:withdrawCollateral(Midnight.Market, uint256, uint256, address, address).selector
         && f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector
+        && f.selector != sig:claimContinuousFee(Midnight.Market, uint256, address).selector
+        && f.selector != sig:updatePosition(Midnight.Market, address).selector
 } {
     require !marketIsCreated(market), "Assume that the market is not created";
     f(e, args);

certora/specs/EmptyOffer.spec

@@ -7,7 +7,7 @@ methods {
     function Utils.emptyOffer() external returns (Midnight.Offer) envfree;
 
     // Summarize internals, which is sound since it would only remove revert reasons.
-    function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET;
+    function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET;
     function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET;
     function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
     function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;

certora/specs/Healthiness.spec

@@ -16,7 +16,7 @@ methods {
     // Under this assumption we can prove that a healthy borrower cannot get unhealthy by any action on the contract.
     function _.price() external => summaryPrice(calledContract) expect(uint256);
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
-    function IdLib.toId(Midnight.Market memory market, uint256 chainId, address midnight) internal returns (bytes32) => summaryToId(market, chainId, midnight);
+    function IdLib.toId(Midnight.Market memory market) 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.
@@ -25,7 +25,7 @@ methods {
     function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d);
     function _.havocAll() external => HAVOC_ALL;
 
-    function IdLib.storeInCode(Midnight.Market memory, uint256) internal returns (address) => NONDET;
+    function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET;
 
     function SafeTransferLib.safeTransfer(address, address, uint256) internal => transferCallback();
     function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => transferCallback();
@@ -102,6 +102,8 @@ persistent ghost bool healthyOrLockedBeforeCallbacks;
 // global variable to track which market and borrower we're testing.
 persistent ghost address globalMarketLoanToken;
 
+persistent ghost uint256 globalMarketChainId;
+
 persistent ghost uint256 globalMarketCollateralLength;
 
 persistent ghost mapping(uint256 => address) globalMarketCollateralOracle;
@@ -129,7 +131,7 @@ persistent ghost address globalBorrower;
 definition collateralMatches(Midnight.Market market, uint256 index) returns bool = (index < globalMarketCollateralLength => market.collateralParams[index].oracle == globalMarketCollateralOracle[index] && market.collateralParams[index].token == globalMarketCollateralToken[index] && market.collateralParams[index].lltv == globalMarketCollateralLLTV[index] && market.collateralParams[index].maxLif == globalMarketCollateralMaxLif[index]);
 
 function equalsGlobalMarket(Midnight.Market market) returns (bool) {
-    return market.loanToken == globalMarketLoanToken && market.collateralParams.length == globalMarketCollateralLength && collateralMatches(market, 0) && collateralMatches(market, 1) && collateralMatches(market, 2) && market.maturity == globalMarketMaturity && market.rcfThreshold == globalMarketRcfThreshold && market.enterGate == globalMarketEnterGate && market.liquidatorGate == globalMarketLiquidatorGate;
+    return market.chainId == globalMarketChainId && market.midnight == currentContract && market.loanToken == globalMarketLoanToken && market.collateralParams.length == globalMarketCollateralLength && collateralMatches(market, 0) && collateralMatches(market, 1) && collateralMatches(market, 2) && market.maturity == globalMarketMaturity && market.rcfThreshold == globalMarketRcfThreshold && market.enterGate == globalMarketEnterGate && market.liquidatorGate == globalMarketLiquidatorGate;
 }
 
 function getGlobalMarket() returns (Midnight.Market) {
@@ -138,9 +140,9 @@ function getGlobalMarket() returns (Midnight.Market) {
     return market;
 }
 
-function summaryToId(Midnight.Market market, uint256 chainId, address midnight) returns (bytes32) {
+function summaryToId(Midnight.Market market) returns (bytes32) {
     bytes32 id;
-    if (equalsGlobalMarket(market) && midnight == currentContract) {
+    if (equalsGlobalMarket(market)) {
         require id == globalId, "toId() is deterministic";
     } else {
         require id != globalId, "toId() is injective";

certora/specs/Liquidate.spec

@@ -18,14 +18,14 @@ methods {
     function UtilsLib.mulDivUp(uint256 a, uint256 b, uint256 denominator) internal returns (uint256) => summaryMulDivUp(a, b, denominator);
 
     // IdLib summary: remember the last id returned by toId.
-    function IdLib.toId(Midnight.Market memory market, uint256 chainId, address midnight) internal returns (bytes32) => summaryToId(market, chainId, midnight);
+    function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
 }
 
 /// HELPERS ///
 
 persistent ghost bytes32 liqId;
 
-function summaryToId(Midnight.Market market, uint256 chainId, address midnight) returns bytes32 {
+function summaryToId(Midnight.Market market) returns bytes32 {
     bytes32 id;
     liqId = id;
     return id;

certora/specs/LiquidationBoundedByLIF.spec

@@ -14,10 +14,10 @@ methods {
     function _.price() external => summaryPrice(calledContract) expect(uint256);
 
     // Deterministic toId summary using a wrapper that extracts all scalar Market fields.
-    function IdLib.toId(Midnight.Market memory market, uint256 chainId, address midnight) internal returns (bytes32) => summaryToId(market);
+    function IdLib.toId(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
 
-    // Skip market creation logic: removes the collateral-validation loop.
-    function touchMarket(Midnight.Market memory market) internal returns (bytes32) => summaryToId(market);
+    // Sound because the protocol doesn't use toMarket.
+    function IdLib.storeInCode(Midnight.Market memory) internal returns (address) => NONDET;
 
     // Token transfers happen after return values are computed; irrelevant to the assertion.
     function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET;