diff --git a/certora/confs/BundlerRepayInvertibility.conf b/certora/confs/BundlerRepayInvertibility.conf index a28289b6..e6ec9637 100644 --- a/certora/confs/BundlerRepayInvertibility.conf +++ b/certora/confs/BundlerRepayInvertibility.conf @@ -15,10 +15,10 @@ "solc_via_ir": true, "optimistic_loop": true, "loop_iter": 2, + "smt_timeout": 7200, "prover_args": [ - "-depth 5", - "-mediumTimeout 60", - "-timeout 3600" + "-destructiveOptimizations twostage", + "-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 Bundler Repay Invertibility" } diff --git a/certora/helpers/MidnightWrapper.sol b/certora/helpers/MidnightWrapper.sol index c3c28b9d..8345739b 100644 --- a/certora/helpers/MidnightWrapper.sol +++ b/certora/helpers/MidnightWrapper.sol @@ -15,8 +15,8 @@ contract MidnightWrapper is Midnight { /* This isHealthy function iterates over all collateralParams, it doesn't use the collateral bitmap. */ function isHealthyNoBitmap(Market memory market, bytes32 id, address borrower) public view returns (bool) { - Position storage _position = position[id][borrower]; - uint256 debt = _position.debt; + Position storage userPosition = _position[id][borrower]; + uint256 debt = userPosition.debt; uint256 maxDebt; if (debt > 0) { uint256 len = market.collateralParams.length; @@ -24,7 +24,7 @@ contract MidnightWrapper is Midnight { i--; CollateralParams memory collateralParam = market.collateralParams[i]; uint256 price = IOracle(collateralParam.oracle).price(); - maxDebt += _position.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE) + maxDebt += userPosition.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE) .mulDivDown(collateralParam.lltv, WAD); } } diff --git a/certora/specs/BalanceEffects.spec b/certora/specs/BalanceEffects.spec index 67fe2380..e4e12359 100644 --- a/certora/specs/BalanceEffects.spec +++ b/certora/specs/BalanceEffects.spec @@ -150,7 +150,7 @@ rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 /// REPAY /// -/// Repay decreases onBehalf's debt by exactly units and only changes position[id][onBehalf].debt +/// 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); @@ -168,7 +168,7 @@ rule repayEffects(env e, Midnight.Market market, uint256 units, address onBehalf /// LIQUIDATE /// /// Liquidate decreases the borrower's debt by at least repaidUnits, -/// and only changes position[id][borrower].debt. +/// 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); @@ -207,7 +207,7 @@ filtered { /// SUPPLY COLLATERAL /// /// supplyCollateral increases onBehalf's collateral by exactly assets, -/// and only changes position[id][onBehalf].collateral[collateralIndex]. +/// 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); @@ -223,7 +223,7 @@ rule supplyCollateralEffects(env e, Midnight.Market market, uint256 collateralIn /// WITHDRAW COLLATERAL /// /// withdrawCollateral decreases onBehalf's collateral by exactly assets, -/// and only changes position[id][onBehalf].collateral[collateralIndex]. +/// 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); @@ -239,7 +239,7 @@ rule withdrawCollateralCollateralEffects(env e, Midnight.Market market, uint256 /// LIQUIDATE (COLLATERAL) /// /// liquidate decreases the borrower's collateral at collateralIndex by exactly seizedResult, -/// and only changes position[id][borrower].collateral[collateralIndex]. +/// 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); diff --git a/certora/specs/CollateralBitmap.spec b/certora/specs/CollateralBitmap.spec index 82acdd8d..c9a23a79 100644 --- a/certora/specs/CollateralBitmap.spec +++ b/certora/specs/CollateralBitmap.spec @@ -38,12 +38,12 @@ persistent ghost summaryMulDivUp(uint256, uint256, uint256) returns uint256; // Check that a collateral bit is set exactly when there is collateral for that index. strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint256 collateralIndex) - collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract.position[id][user].collateralBitmap, collateralIndex)); + collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract._position[id][user].collateralBitmap, collateralIndex)); // Check that the number of activated collaterals never exceeds MAX_COLLATERALS_PER_BORROWER. // This bounds the while-loop iterations in isHealthy() and liquidate(). strong invariant atMostMaxCollateralsBitsSet(bytes32 id, address user) - summaryCountBits(currentContract.position[id][user].collateralBitmap) <= Utils.maxCollateralsPerBorrower(); + summaryCountBits(currentContract._position[id][user].collateralBitmap) <= Utils.maxCollateralsPerBorrower(); // This shows that the real isHealthy returns true if and only if the isHealthy function // that does not use collateral bitmap returns true. We also check that the latter function diff --git a/certora/specs/LiquidationBoundedByLIF.spec b/certora/specs/LiquidationBoundedByLIF.spec index efd665e9..86898602 100644 --- a/certora/specs/LiquidationBoundedByLIF.spec +++ b/certora/specs/LiquidationBoundedByLIF.spec @@ -69,7 +69,7 @@ function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { /// Proven in CollateralBitmap.spec; assumed here via requireInvariant (not re-proven in this spec). strong invariant nonZeroCollateralsAreActivated(bytes32 id, address user, uint256 collateralIndex) - collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract.position[id][user].collateralBitmap, collateralIndex)); + collateralIndex < 128 => (collateral(id, user, collateralIndex) != 0 <=> summaryGetBit(currentContract._position[id][user].collateralBitmap, collateralIndex)); /// LIF BOUNDARIES /// diff --git a/certora/specs/LossFactor.spec b/certora/specs/LossFactor.spec index abad19d8..828c235b 100644 --- a/certora/specs/LossFactor.spec +++ b/certora/specs/LossFactor.spec @@ -37,24 +37,24 @@ function marketIsCreated(Midnight.Market market) returns (bool) { /// The market's lossFactor is only modified by liquidate. rule onlyLiquidateChangesMarketLossFactor(bytes32 id, method f, env e, calldataarg args) filtered { f -> !f.isView && f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector } { - uint128 lossFactorBefore = currentContract.marketState[id].lossFactor; + uint128 lossFactorBefore = currentContract._marketState[id].lossFactor; f(e, args); - assert currentContract.marketState[id].lossFactor == lossFactorBefore; + assert currentContract._marketState[id].lossFactor == lossFactorBefore; } /// In liquidate, the market's lossFactor changes if and only if bad debt is realized (totalUnits decreases). rule lossFactorChangesIffBadDebt(env e, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data, bool postMaturityMode) { bytes32 id = summaryToId(market); - uint128 lossFactorBefore = currentContract.marketState[id].lossFactor; + uint128 lossFactorBefore = currentContract._marketState[id].lossFactor; uint256 totalUnitsBefore = totalUnits(id); require lossFactorBefore < max_uint128, "market lossFactor must not be saturated"; liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - bool lossFactorChanged = currentContract.marketState[id].lossFactor != lossFactorBefore; + bool lossFactorChanged = currentContract._marketState[id].lossFactor != lossFactorBefore; bool badDebtOccurred = totalUnits(id) < totalUnitsBefore; assert lossFactorChanged <=> badDebtOccurred; @@ -66,7 +66,7 @@ rule updatePositionSyncsLastLossFactor(env e, Midnight.Market market, address us updatePosition(e, market, user); - assert lastLossFactor(id, user) == currentContract.marketState[id].lossFactor; + assert lastLossFactor(id, user) == currentContract._marketState[id].lossFactor; } /// Assuming that the market is created, the loss factor computation in updatePosition does not revert. @@ -74,11 +74,11 @@ rule updatePositionDoesNotRevert(env e, Midnight.Market market, address user) { bytes32 id = summaryToId(market); require marketIsCreated(market), "market must be created"; - require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec"; + require lastLossFactor(id, user) <= currentContract._marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec"; require pendingFee(id, user) <= credit(id, user), "pending fee bounded by credit, already proved in Midnight.spec"; - require currentContract.position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity"; + require currentContract._position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity"; require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; - require currentContract.marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit"; + require currentContract._marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit"; require e.msg.value == 0, "Midnight is not payable"; updatePosition@withrevert(e, market, user); @@ -90,11 +90,11 @@ rule updatePositionDoesNotRevert(env e, Midnight.Market market, address user) { rule updatePositionViewDoesNotRevert(env e, Midnight.Market market, address user) { bytes32 id = summaryToId(market); - require lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec"; - require pendingFee(id, user) <= creditOf(id, user), "pending fee bounded by credit, already proved in Midnight.spec"; - require currentContract.position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity"; + require lastLossFactor(id, user) <= currentContract._marketState[id].lossFactor, "lastLossFactor bounded by market lossFactor, already proved in Midnight.spec"; + require pendingFee(id, user) <= credit(id, user), "pending fee bounded by credit, already proved in Midnight.spec"; + require currentContract._position[id][user].lastAccrual <= e.block.timestamp, "lastAccrual <= block.timestamp by timestamp monotonicity"; require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; - require currentContract.marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit"; + require currentContract._marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "Total credit should be bounded by 2^128 and an increase of continuous fee credit should corresponds to a similar decrease of credit"; require e.msg.value == 0, "Midnight is not payable"; updatePositionView@withrevert(e, market, id, user); @@ -108,15 +108,15 @@ rule updatePositionIsIdempotent(env e, Midnight.Market market, address user) { require pendingFee(id, user) <= credit(id, user), "see pendingContinuousFeeBoundedByCredit in Midnight.spec"; require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; - require currentContract.marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "see updatePositionDoesNotRevert"; + require currentContract._marketState[id].continuousFeeCredit + pendingFee(id, user) <= max_uint128, "see updatePositionDoesNotRevert"; // Snapshot the relevant position state after a first updatePosition. updatePosition(e, market, user); mathint creditAfterFirst = credit(id, user); mathint pendingFeeAfterFirst = pendingFee(id, user); uint128 lastLossFactorAfterFirst = lastLossFactor(id, user); - uint128 lastAccrualAfterFirst = currentContract.position[id][user].lastAccrual; - uint128 cfcAfterFirst = currentContract.marketState[id].continuousFeeCredit; + uint128 lastAccrualAfterFirst = currentContract._position[id][user].lastAccrual; + uint128 cfcAfterFirst = currentContract._marketState[id].continuousFeeCredit; uint128 newCredit; uint128 newPendingFee; @@ -132,8 +132,8 @@ rule updatePositionIsIdempotent(env e, Midnight.Market market, address user) { assert credit(id, user) == creditAfterFirst; assert pendingFee(id, user) == pendingFeeAfterFirst; assert lastLossFactor(id, user) == lastLossFactorAfterFirst; - assert currentContract.position[id][user].lastAccrual == lastAccrualAfterFirst; - assert currentContract.marketState[id].continuousFeeCredit == cfcAfterFirst; + assert currentContract._position[id][user].lastAccrual == lastAccrualAfterFirst; + assert currentContract._marketState[id].continuousFeeCredit == cfcAfterFirst; } /// When the user's lastLossFactor is in sync with the market's lossFactor (and not saturated), @@ -141,7 +141,7 @@ rule updatePositionIsIdempotent(env e, Midnight.Market market, address user) { rule updatePositionPreservesCreditWhenLossIndexCurrent(env e, Midnight.Market market, address user) { bytes32 id = summaryToId(market); - require lastLossFactor(id, user) == currentContract.marketState[id].lossFactor, "lastLossFactor synced with market"; + require lastLossFactor(id, user) == currentContract._marketState[id].lossFactor, "lastLossFactor synced with market"; require lastLossFactor(id, user) < max_uint128, "lossFactor not saturated"; require pendingFee(id, user) <= credit(id, user), "see pendingContinuousFeeBoundedByCredit in Midnight.spec"; require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; @@ -166,11 +166,11 @@ rule updatePositionPreservesContinuousFeeCreditWhenLastAccrualIsUpToDate(env e, bytes32 id = summaryToId(market); require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; - require currentContract.position[id][user].lastAccrual == e.block.timestamp, "lastAccrual is up to date"; + require currentContract._position[id][user].lastAccrual == e.block.timestamp, "lastAccrual is up to date"; - uint128 continuousFeeCreditBefore = currentContract.marketState[id].continuousFeeCredit; + uint128 continuousFeeCreditBefore = currentContract._marketState[id].continuousFeeCredit; updatePosition(e, market, user); - uint128 continuousFeeCreditAfter = currentContract.marketState[id].continuousFeeCredit; + uint128 continuousFeeCreditAfter = currentContract._marketState[id].continuousFeeCredit; assert continuousFeeCreditAfter == continuousFeeCreditBefore; } @@ -184,9 +184,9 @@ rule liquidateLossFactorDoesNotRevert(env e, Midnight.Market market, address bor require market.liquidatorGate == 0, "Assumption:no liquidator gate"; require market.collateralParams.length > 0, "market has at least one collateral (enforced by touchMarket)"; require !liquidationLocked(id, borrower), "liquidation not locked (transient storage is zero at transaction start)"; - require currentContract.position[id][borrower].collateralBitmap == 0, "Assumption: no active collaterals: skip loop and maximize badDebt"; - require currentContract.position[id][borrower].debt > 0, "borrower must have debt to enter badDebt > 0 block"; - require currentContract.position[id][borrower].debt <= currentContract.marketState[id].totalUnits, "position debt bounded by totalUnits (see totalUnitsEqualsSumNegativeDebtPlusWithdrawable)"; + require currentContract._position[id][borrower].collateralBitmap == 0, "Assumption: no active collaterals: skip loop and maximize badDebt"; + require currentContract._position[id][borrower].debt > 0, "borrower must have debt to enter badDebt > 0 block"; + require currentContract._position[id][borrower].debt <= currentContract._marketState[id].totalUnits, "position debt bounded by totalUnits (see totalUnitsEqualsSumNegativeDebtPlusWithdrawable)"; require e.msg.value == 0, "Midnight is not payable"; address zero = 0; diff --git a/certora/specs/Midnight.spec b/certora/specs/Midnight.spec index a8731d84..b832c55f 100644 --- a/certora/specs/Midnight.spec +++ b/certora/specs/Midnight.spec @@ -48,7 +48,7 @@ persistent ghost mapping(bytes32 => mathint) sumDebt { init_state axiom (forall bytes32 id. sumDebt[id] == 0); } -hook Sstore position[KEY bytes32 id][KEY address owner].debt uint128 newDebt (uint128 oldDebt) { +hook Sstore _position[KEY bytes32 id][KEY address owner].debt uint128 newDebt (uint128 oldDebt) { sumDebt[id] = sumDebt[id] - to_mathint(oldDebt) + to_mathint(newDebt); } @@ -93,9 +93,9 @@ rule liquidateInputOutputConsistency(env e, Midnight.Market market, uint256 coll } rule marketLossFactorMonotonicallyIncreases(bytes32 id, method f, env e, calldataarg args) { - uint128 lossFactorBefore = currentContract.marketState[id].lossFactor; + uint128 lossFactorBefore = currentContract._marketState[id].lossFactor; f(e, args); - uint128 lossFactorAfter = currentContract.marketState[id].lossFactor; + uint128 lossFactorAfter = currentContract._marketState[id].lossFactor; assert lossFactorAfter >= lossFactorBefore; } @@ -108,7 +108,7 @@ rule lastLossFactorMonotonicallyIncreases(bytes32 id, address user, method f, en } rule creditAndDebtCannotIncreaseWhenLossFactorIsMaxed(bytes32 id, address user, method f, env e, calldataarg args) { - require currentContract.marketState[id].lossFactor == max_uint128, "assume loss factor is maxed out"; + require currentContract._marketState[id].lossFactor == max_uint128, "assume loss factor is maxed out"; uint256 creditBefore = credit(id, user); uint256 debtBefore = debt(id, user); @@ -127,7 +127,7 @@ strong invariant defaultContinuousFeeBoundedAll() forall address token. currentContract.defaultContinuousFee[token] <= MAX_CONTINUOUS_FEE(); strong invariant continuousFeeBounded(bytes32 id) - currentContract.marketState[id].continuousFee <= MAX_CONTINUOUS_FEE() + currentContract._marketState[id].continuousFee <= MAX_CONTINUOUS_FEE() { preserved with (env e) { requireInvariant defaultContinuousFeeBoundedAll(); @@ -154,7 +154,7 @@ rule noRemainingContinuousFeeWithoutCredit(bytes32 id, address user) { } strong invariant lastLossFactorLeqMarketLossFactor(bytes32 id, address user) - lastLossFactor(id, user) <= currentContract.marketState[id].lossFactor; + lastLossFactor(id, user) <= currentContract._marketState[id].lossFactor; /// A user cannot have both credit and debt. strong invariant noCreditAndDebt(bytes32 id, address user) diff --git a/certora/specs/NoDebtWithoutCollateral.spec b/certora/specs/NoDebtWithoutCollateral.spec index 57bb86ed..b3949894 100644 --- a/certora/specs/NoDebtWithoutCollateral.spec +++ b/certora/specs/NoDebtWithoutCollateral.spec @@ -1,7 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later /* Proves: a position can never carry debt while having no active collateral bit, i.e.: - * position[id][user].collateralBitmap == 0 => position[id][user].debt == 0 + * _position[id][user].collateralBitmap == 0 => _position[id][user].debt == 0 * * Combined with `nonZeroCollateralsAreActivated` (proved in CollateralBitmap.spec), * this implies the full semantic property: no position can have collateral[i] == 0 for every i while having debt > 0. @@ -64,7 +64,7 @@ persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; /// INVARIANT /// strong invariant lockedOrNoDebtWithoutCollateral(bytes32 id, address user) - liquidationLocked(id, user) || (currentContract.position[id][user].collateralBitmap == 0 => currentContract.position[id][user].debt == 0) + liquidationLocked(id, user) || (currentContract._position[id][user].collateralBitmap == 0 => currentContract._position[id][user].debt == 0) { preserved liquidate(Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes data) with (env e) { // To derive repaidUnits >= debtAfterBadDebt when the last bitmap bit is cleared, the prover requires inverse axioms and mulDiv monotonicity (using lif <= maxLif). diff --git a/certora/specs/NoDivisionByZero.spec b/certora/specs/NoDivisionByZero.spec index 16a05df0..77d71ecb 100644 --- a/certora/specs/NoDivisionByZero.spec +++ b/certora/specs/NoDivisionByZero.spec @@ -58,8 +58,8 @@ persistent ghost bytes32 globalId; /// HOOKS /// // Follows from lastLossFactorLeqMarketLossFactor in Midnight.spec. -hook Sload uint128 value position[KEY bytes32 id][KEY address user].lastLossFactor { - require value <= currentContract.marketState[id].lossFactor; +hook Sload uint128 value _position[KEY bytes32 id][KEY address user].lastLossFactor { + require value <= currentContract._marketState[id].lossFactor; } /// SUMMARIES /// @@ -122,7 +122,7 @@ rule noDivisionByZeroLiquidate(env e, Midnight.Market market, uint256 collateral // Assume that the collateral price is non-zero and the collateral is active. Otherwise, liquidate may revert with div by zero. require ghostPrice(market.collateralParams[collateralIndex].oracle) > 0, "Assumption: the collateral price is not zero"; - require summaryGetBit(currentContract.position[globalId][borrower].collateralBitmap, collateralIndex), "Assumption: liquidated collateral was activated"; + require summaryGetBit(currentContract._position[globalId][borrower].collateralBitmap, collateralIndex), "Assumption: liquidated collateral was activated"; liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); assert true; diff --git a/certora/specs/NotCreatedMarket.spec b/certora/specs/NotCreatedMarket.spec index 9fbf41a5..9e23dc8f 100644 --- a/certora/specs/NotCreatedMarket.spec +++ b/certora/specs/NotCreatedMarket.spec @@ -33,13 +33,13 @@ function noSettlementFeesAreSet(bytes32 id) returns (bool) { return fees[0] == 0 && fees[1] == 0 && fees[2] == 0 && fees[3] == 0 && fees[4] == 0 && fees[5] == 0 && fees[6] == 0; } -definition userHasEmptyCollateralBitmap(bytes32 id, address user) returns bool = currentContract.position[id][user].collateralBitmap == 0; +definition userHasEmptyCollateralBitmap(bytes32 id, address user) returns bool = currentContract._position[id][user].collateralBitmap == 0; definition userHasNoRemainingContinuousFee(bytes32 id, address user) returns bool = pendingFee(id, user) == 0; definition userHasNoLastAccrual(bytes32 id, address user) returns bool = lastAccrual(id, user) == 0; -definition userHasNoCollateral(bytes32 id, address user, uint256 collateralIndex) returns bool = collateralIndex < 128 => currentContract.position[id][user].collateral[collateralIndex] == 0; +definition userHasNoCollateral(bytes32 id, address user, uint256 collateralIndex) returns bool = collateralIndex < 128 => currentContract._position[id][user].collateral[collateralIndex] == 0; /// RULES /// @@ -57,10 +57,10 @@ strong invariant marketContinuousFeeIsEmptyIfNotCreated(bytes32 id) !marketIsCreated(id) => continuousFee(id) == 0; strong invariant marketContinuousFeeCreditIsEmptyIfNotCreated(bytes32 id) - !marketIsCreated(id) => currentContract.marketState[id].continuousFeeCredit == 0; + !marketIsCreated(id) => currentContract._marketState[id].continuousFeeCredit == 0; strong invariant marketLossFactorIsEmptyIfNotCreated(bytes32 id) - !marketIsCreated(id) => currentContract.marketState[id].lossFactor == 0; + !marketIsCreated(id) => currentContract._marketState[id].lossFactor == 0; strong invariant marketCreditIsEmptyIfNotCreated(bytes32 id, address user) !marketIsCreated(id) => credit(id, user) == 0; @@ -81,4 +81,4 @@ strong invariant marketCollateralIsEmptyIfNotCreated(bytes32 id, address user, u !marketIsCreated(id) => userHasNoCollateral(id, user, collateralIndex); strong invariant positionLastLossFactorIsEmptyIfNotCreated(bytes32 id, address user) - !marketIsCreated(id) => currentContract.position[id][user].lastLossFactor == 0; + !marketIsCreated(id) => currentContract._position[id][user].lastLossFactor == 0; diff --git a/certora/specs/Role.spec b/certora/specs/Role.spec index a8206c67..63638042 100644 --- a/certora/specs/Role.spec +++ b/certora/specs/Role.spec @@ -33,7 +33,7 @@ definition CBP() returns uint256 = 10 ^ 12; definition MAX_CONTINUOUS_FEE() returns uint256 = 317097919; -definition marketSettlementFeeCbp(bytes32 id, uint256 index) returns uint16 = index == 0 ? currentContract.marketState[id].settlementFeeCbp0 : index == 1 ? currentContract.marketState[id].settlementFeeCbp1 : index == 2 ? currentContract.marketState[id].settlementFeeCbp2 : index == 3 ? currentContract.marketState[id].settlementFeeCbp3 : index == 4 ? currentContract.marketState[id].settlementFeeCbp4 : index == 5 ? currentContract.marketState[id].settlementFeeCbp5 : currentContract.marketState[id].settlementFeeCbp6; +definition marketSettlementFeeCbp(bytes32 id, uint256 index) returns uint16 = index == 0 ? currentContract._marketState[id].settlementFeeCbp0 : index == 1 ? currentContract._marketState[id].settlementFeeCbp1 : index == 2 ? currentContract._marketState[id].settlementFeeCbp2 : index == 3 ? currentContract._marketState[id].settlementFeeCbp3 : index == 4 ? currentContract._marketState[id].settlementFeeCbp4 : index == 5 ? currentContract._marketState[id].settlementFeeCbp5 : currentContract._marketState[id].settlementFeeCbp6; definition marketSettlementFee(bytes32 id, uint256 index) returns uint256 = assert_uint256(marketSettlementFeeCbp(id, index) * CBP()); @@ -275,7 +275,7 @@ rule feeClaimerCanClaimContinuousFee(env e, Midnight.Market market, uint256 amou bool marketIsCreated = marketIsCreated(id); uint256 withdrawableBefore = withdrawable(id); uint256 totalUnitsBefore = totalUnits(id); - uint128 continuousFeeCreditBefore = currentContract.marketState[id].continuousFeeCredit; + uint128 continuousFeeCreditBefore = currentContract._marketState[id].continuousFeeCredit; mathint midnightBalanceBefore = tokenBalance[market.loanToken][currentContract]; mathint receiverBalanceBefore = tokenBalance[market.loanToken][receiver]; mathint userBalanceBefore = tokenBalance[market.loanToken][user]; @@ -285,7 +285,7 @@ rule feeClaimerCanClaimContinuousFee(env e, Midnight.Market market, uint256 amou assert !reverted <=> e.msg.sender == feeClaimerBefore && e.msg.value == 0 && marketIsCreated && amount <= withdrawableBefore && amount <= totalUnitsBefore && amount <= continuousFeeCreditBefore; assert !reverted => withdrawable(id) == withdrawableBefore - amount; assert !reverted => totalUnits(id) == totalUnitsBefore - amount; - assert !reverted => currentContract.marketState[id].continuousFeeCredit == continuousFeeCreditBefore - amount; + assert !reverted => currentContract._marketState[id].continuousFeeCredit == continuousFeeCreditBefore - amount; assert !reverted => tokenBalance[market.loanToken][currentContract] == midnightBalanceBefore - (receiver == currentContract ? 0 : amount); assert !reverted => tokenBalance[market.loanToken][receiver] == receiverBalanceBefore + (receiver == currentContract ? 0 : amount); assert !reverted => user != currentContract && user != receiver => tokenBalance[market.loanToken][user] == userBalanceBefore; diff --git a/certora/specs/SettlementFeeBoundaries.spec b/certora/specs/SettlementFeeBoundaries.spec index f924bc17..a335c41e 100644 --- a/certora/specs/SettlementFeeBoundaries.spec +++ b/certora/specs/SettlementFeeBoundaries.spec @@ -28,7 +28,7 @@ definition CBP() returns uint256 = 10 ^ 12; definition defaultSettlementFee(address loanToken, uint256 index) returns uint256 = assert_uint256(currentContract.defaultSettlementFeeCbp[loanToken][index] * CBP()); -definition marketSettlementFeeCbp(bytes32 id, uint256 index) returns uint16 = index == 0 ? currentContract.marketState[id].settlementFeeCbp0 : index == 1 ? currentContract.marketState[id].settlementFeeCbp1 : index == 2 ? currentContract.marketState[id].settlementFeeCbp2 : index == 3 ? currentContract.marketState[id].settlementFeeCbp3 : index == 4 ? currentContract.marketState[id].settlementFeeCbp4 : index == 5 ? currentContract.marketState[id].settlementFeeCbp5 : currentContract.marketState[id].settlementFeeCbp6; +definition marketSettlementFeeCbp(bytes32 id, uint256 index) returns uint16 = index == 0 ? currentContract._marketState[id].settlementFeeCbp0 : index == 1 ? currentContract._marketState[id].settlementFeeCbp1 : index == 2 ? currentContract._marketState[id].settlementFeeCbp2 : index == 3 ? currentContract._marketState[id].settlementFeeCbp3 : index == 4 ? currentContract._marketState[id].settlementFeeCbp4 : index == 5 ? currentContract._marketState[id].settlementFeeCbp5 : currentContract._marketState[id].settlementFeeCbp6; definition marketSettlementFee(bytes32 id, uint256 index) returns uint256 = assert_uint256(marketSettlementFeeCbp(id, index) * CBP()); diff --git a/certora/specs/Solvency.spec b/certora/specs/Solvency.spec index 4202619a..3be84240 100644 --- a/certora/specs/Solvency.spec +++ b/certora/specs/Solvency.spec @@ -113,12 +113,12 @@ ghost mapping(bytes32 => mapping(address => mapping(address => mathint))) collat } // Safe require as markets limit the number of collateralParams. -hook Sload uint128 value position[KEY bytes32 id][KEY address owner].collateral[INDEX uint256 collateralIndex] { +hook Sload uint128 value _position[KEY bytes32 id][KEY address owner].collateral[INDEX uint256 collateralIndex] { require value == collateralMirror[id][owner][collateralToken[id][require_uint128(collateralIndex)]], "ghost mirror"; } // Safe require as markets limit the number of collateralParams. -hook Sstore position[KEY bytes32 id][KEY address owner].collateral[INDEX uint256 collateralIndex] uint128 newCollateral (uint128 oldCollateral) { +hook Sstore _position[KEY bytes32 id][KEY address owner].collateral[INDEX uint256 collateralIndex] uint128 newCollateral (uint128 oldCollateral) { collateralMirror[id][owner][collateralToken[id][require_uint128(collateralIndex)]] = newCollateral; } @@ -129,11 +129,11 @@ ghost mapping(bytes32 => mapping(address => mathint)) withdrawableMirror { init_state axiom (forall address token. withdrawableSum(token) == 0); } -hook Sload uint128 value marketState[KEY bytes32 id].withdrawable { +hook Sload uint128 value _marketState[KEY bytes32 id].withdrawable { require value == withdrawableMirror[id][loantoken[id]], "ghost mirror"; } -hook Sstore marketState[KEY bytes32 id].withdrawable uint128 newWithdrawable (uint128 oldWithdrawable) { +hook Sstore _marketState[KEY bytes32 id].withdrawable uint128 newWithdrawable (uint128 oldWithdrawable) { withdrawableMirror[id][loantoken[id]] = newWithdrawable; } diff --git a/certora/specs/SplitPreservesAccounting.spec b/certora/specs/SplitPreservesAccounting.spec index ed268154..037c4f1c 100644 --- a/certora/specs/SplitPreservesAccounting.spec +++ b/certora/specs/SplitPreservesAccounting.spec @@ -71,14 +71,14 @@ rule splitPreservesAccounting(env e, uint256 unitsA, uint256 unitsB, uint256 uni // Path 1: take the full amount A. take(e, offer, ratifierData, unitsA, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); - uint128 creditBuyer1 = credit(id, buyer); - uint128 debtBuyer1 = debt(id, buyer); - uint128 creditSeller1 = credit(id, seller); - uint128 debtSeller1 = debt(id, seller); + uint128 creditOfBuyer1 = credit(id, buyer); + uint128 debtOfBuyer1 = debt(id, buyer); + uint128 creditOfSeller1 = credit(id, seller); + uint128 debtOfSeller1 = debt(id, seller); uint128 totalUnits1 = totalUnits(id); uint128 buyerLossFactor1 = lastLossFactor(id, buyer); uint128 sellerLossFactor1 = lastLossFactor(id, seller); - uint128 continuousFeeCredit1 = currentContract.marketState[id].continuousFeeCredit; + uint128 continuousFeeCredit1 = currentContract._marketState[id].continuousFeeCredit; // lastAccrual is set to block.timestamp by _updatePosition; same env across both paths. uint128 buyerLastAccrual1 = lastAccrual(id, buyer); @@ -89,14 +89,14 @@ rule splitPreservesAccounting(env e, uint256 unitsA, uint256 unitsB, uint256 uni take(e, offer, ratifierData, unitsC, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); - assert creditBuyer1 == credit(id, buyer); - assert debtBuyer1 == debt(id, buyer); - assert creditSeller1 == credit(id, seller); - assert debtSeller1 == debt(id, seller); + assert creditOfBuyer1 == credit(id, buyer); + assert debtOfBuyer1 == debt(id, buyer); + assert creditOfSeller1 == credit(id, seller); + assert debtOfSeller1 == debt(id, seller); assert totalUnits1 == totalUnits(id); assert buyerLossFactor1 == lastLossFactor(id, buyer); assert sellerLossFactor1 == lastLossFactor(id, seller); assert buyerLastAccrual1 == lastAccrual(id, buyer); assert sellerLastAccrual1 == lastAccrual(id, seller); - assert continuousFeeCredit1 == currentContract.marketState[id].continuousFeeCredit; + assert continuousFeeCredit1 == currentContract._marketState[id].continuousFeeCredit; } diff --git a/certora/specs/UpdateBeforeCredit.spec b/certora/specs/UpdateBeforeCredit.spec index 323eeaf6..cd10e160 100644 --- a/certora/specs/UpdateBeforeCredit.spec +++ b/certora/specs/UpdateBeforeCredit.spec @@ -42,18 +42,18 @@ function summaryUpdatePosition(bytes32 id, address user) returns (uint128, uint1 /// Summary for hasCredit: circumvent the load hook for credit checks. function summaryHasCredit(bytes32 id, address user) returns (bool) { - return currentContract.position[id][user].credit > 0; + return currentContract._position[id][user].credit > 0; } /// HOOKS /// -hook Sstore position[KEY bytes32 id][KEY address user].credit uint128 newVal (uint128 oldVal) { +hook Sstore _position[KEY bytes32 id][KEY address user].credit uint128 newVal (uint128 oldVal) { if (!updated[id][user] && newVal != oldVal) { creditStoredBeforeUpdate[id][user] = true; } } -hook Sload uint128 val position[KEY bytes32 id][KEY address user].credit { +hook Sload uint128 val _position[KEY bytes32 id][KEY address user].credit { if (!updated[id][user] && val != 0) { creditLoadedBeforeUpdate[id][user] = true; } diff --git a/foundry.toml b/foundry.toml index 1c268f0f..3ff09008 100644 --- a/foundry.toml +++ b/foundry.toml @@ -1,7 +1,7 @@ [profile.default] via_ir = true optimizer = true -optimizer_runs = 800 +optimizer_runs = 700 bytecode_hash = "none" evm_version = "osaka" fs_permissions = [{ access = "read", path = "test/ticks_exact.json" }] diff --git a/src/Midnight.sol b/src/Midnight.sol index 2f6fc6e7..abf9aa7e 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -196,8 +196,8 @@ contract Midnight is IMidnight { /// STORAGE /// - mapping(bytes32 id => mapping(address user => Position)) public position; - mapping(bytes32 id => MarketState) public marketState; + mapping(bytes32 id => mapping(address user => Position)) internal _position; + mapping(bytes32 id => MarketState) internal _marketState; mapping(address user => mapping(bytes32 group => uint256)) public consumed; mapping(address authorizer => mapping(address authorized => bool)) public isAuthorized; mapping(address loanToken => uint16[7]) public defaultSettlementFeeCbp; @@ -267,29 +267,29 @@ contract Midnight is IMidnight { /// @dev Refines the tick spacing of a market. Can not increase (more ticks become accessible). function setMarketTickSpacing(bytes32 id, uint256 newTickSpacing) external { require(msg.sender == tickSpacingSetter, OnlyTickSpacingSetter()); - require(marketState[id].tickSpacing > 0, MarketNotCreated()); - require(newTickSpacing > 0 && marketState[id].tickSpacing % newTickSpacing == 0, InvalidTickSpacing()); + require(_marketState[id].tickSpacing > 0, MarketNotCreated()); + require(newTickSpacing > 0 && _marketState[id].tickSpacing % newTickSpacing == 0, InvalidTickSpacing()); // forge-lint: disable-next-line(unsafe-typecast) as newTickSpacing <= DEFAULT_TICK_SPACING < type(uint8).max - marketState[id].tickSpacing = uint8(newTickSpacing); + _marketState[id].tickSpacing = uint8(newTickSpacing); emit EventsLib.SetMarketTickSpacing(id, newTickSpacing); } function setMarketSettlementFee(bytes32 id, uint256 index, uint256 newSettlementFee) external { - MarketState storage _marketState = marketState[id]; + MarketState storage state = _marketState[id]; require(msg.sender == feeSetter, OnlyFeeSetter()); require(index <= 6, InvalidFeeIndex()); require(newSettlementFee <= maxSettlementFee(index), SettlementFeeAboveMax()); require(newSettlementFee % CBP == 0, FeeNotMultipleOfFeeCbp()); - require(_marketState.tickSpacing > 0, MarketNotCreated()); + require(state.tickSpacing > 0, MarketNotCreated()); // forge-lint: disable-next-item(unsafe-typecast) as newSettlementFee <= maxSettlementFee <= uint16.max * CBP uint16 newSettlementFeeCbp = uint16(newSettlementFee / CBP); - if (index == 0) _marketState.settlementFeeCbp0 = newSettlementFeeCbp; - else if (index == 1) _marketState.settlementFeeCbp1 = newSettlementFeeCbp; - else if (index == 2) _marketState.settlementFeeCbp2 = newSettlementFeeCbp; - else if (index == 3) _marketState.settlementFeeCbp3 = newSettlementFeeCbp; - else if (index == 4) _marketState.settlementFeeCbp4 = newSettlementFeeCbp; - else if (index == 5) _marketState.settlementFeeCbp5 = newSettlementFeeCbp; - else if (index == 6) _marketState.settlementFeeCbp6 = newSettlementFeeCbp; + if (index == 0) state.settlementFeeCbp0 = newSettlementFeeCbp; + else if (index == 1) state.settlementFeeCbp1 = newSettlementFeeCbp; + else if (index == 2) state.settlementFeeCbp2 = newSettlementFeeCbp; + else if (index == 3) state.settlementFeeCbp3 = newSettlementFeeCbp; + else if (index == 4) state.settlementFeeCbp4 = newSettlementFeeCbp; + else if (index == 5) state.settlementFeeCbp5 = newSettlementFeeCbp; + else if (index == 6) state.settlementFeeCbp6 = newSettlementFeeCbp; emit EventsLib.SetMarketSettlementFee(id, index, newSettlementFee); } @@ -304,12 +304,12 @@ contract Midnight is IMidnight { } function setMarketContinuousFee(bytes32 id, uint256 newContinuousFee) external { - MarketState storage _marketState = marketState[id]; + MarketState storage state = _marketState[id]; require(msg.sender == feeSetter, OnlyFeeSetter()); require(newContinuousFee <= MAX_CONTINUOUS_FEE, ContinuousFeeAboveMax()); - require(_marketState.tickSpacing > 0, MarketNotCreated()); + require(state.tickSpacing > 0, MarketNotCreated()); // forge-lint: disable-next-line(unsafe-typecast) as newContinuousFee <= MAX_CONTINUOUS_FEE < type(uint32).max - _marketState.continuousFee = uint32(newContinuousFee); + state.continuousFee = uint32(newContinuousFee); emit EventsLib.SetMarketContinuousFee(id, newContinuousFee); } @@ -330,13 +330,13 @@ contract Midnight is IMidnight { function claimContinuousFee(Market memory market, uint256 amount, address receiver) external { bytes32 id = toId(market); - MarketState storage _marketState = marketState[id]; + MarketState storage state = _marketState[id]; require(msg.sender == feeClaimer, OnlyFeeClaimer()); - require(_marketState.tickSpacing > 0, MarketNotCreated()); + require(state.tickSpacing > 0, MarketNotCreated()); - _marketState.continuousFeeCredit -= UtilsLib.toUint128(amount); - _marketState.totalUnits -= UtilsLib.toUint128(amount); - _marketState.withdrawable -= UtilsLib.toUint128(amount); + state.continuousFeeCredit -= UtilsLib.toUint128(amount); + state.totalUnits -= UtilsLib.toUint128(amount); + state.withdrawable -= UtilsLib.toUint128(amount); emit EventsLib.ClaimContinuousFee(msg.sender, id, amount, receiver); @@ -364,11 +364,11 @@ contract Midnight is IMidnight { ) external returns (uint256, uint256) { require(taker == msg.sender || isAuthorized[taker][msg.sender], TakerUnauthorized()); bytes32 id = touchMarket(offer.market); - MarketState storage _marketState = marketState[id]; - require(_marketState.lossFactor < type(uint128).max, MarketLossFactorMaxedOut()); + MarketState storage state = _marketState[id]; + require(state.lossFactor < type(uint128).max, MarketLossFactorMaxedOut()); require((offer.maxAssets == 0) != (offer.maxUnits == 0), InvalidOfferCaps()); - require(_marketState.continuousFee <= offer.continuousFeeCap, ContinuousFeeAboveOfferCap()); - require(offer.tick % _marketState.tickSpacing == 0, TickNotAccessible()); + require(state.continuousFee <= offer.continuousFeeCap, ContinuousFeeAboveOfferCap()); + require(offer.tick % state.tickSpacing == 0, TickNotAccessible()); require(block.timestamp >= offer.start, OfferNotStarted()); require(block.timestamp <= offer.expiry, OfferExpired()); require(offer.maker != taker, SelfTake()); @@ -397,8 +397,8 @@ contract Midnight is IMidnight { } (address buyer, address seller) = offer.buy ? (offer.maker, taker) : (taker, offer.maker); - Position storage buyerPos = position[id][buyer]; - Position storage sellerPos = position[id][seller]; + Position storage buyerPos = _position[id][buyer]; + Position storage sellerPos = _position[id][seller]; if (hasCredit(id, buyer) || units > buyerPos.debt) _updatePosition(offer.market, id, buyer); if (hasCredit(id, seller)) _updatePosition(offer.market, id, seller); @@ -407,7 +407,7 @@ contract Midnight is IMidnight { uint256 sellerCreditDecrease = UtilsLib.min(units, sellerPos.credit); uint256 sellerDebtIncrease = units - sellerCreditDecrease; uint128 buyerPendingFeeIncrease = - UtilsLib.toUint128(buyerCreditIncrease.mulDivDown(_marketState.continuousFee * timeToMaturity, WAD)); + UtilsLib.toUint128(buyerCreditIncrease.mulDivDown(state.continuousFee * timeToMaturity, WAD)); uint128 sellerPendingFeeDecrease = sellerPos.credit > 0 ? UtilsLib.toUint128(sellerPos.pendingFee.mulDivUp(sellerCreditDecrease, sellerPos.credit)) : 0; @@ -436,8 +436,7 @@ contract Midnight is IMidnight { sellerPos.credit -= UtilsLib.toUint128(sellerCreditDecrease); sellerPos.debt += UtilsLib.toUint128(sellerDebtIncrease); - _marketState.totalUnits = - UtilsLib.toUint128(_marketState.totalUnits + buyerCreditIncrease - sellerCreditDecrease); + state.totalUnits = UtilsLib.toUint128(state.totalUnits + buyerCreditIncrease - sellerCreditDecrease); claimableSettlementFee[offer.market.loanToken] += buyerAssets - sellerAssets; consumed[offer.maker][offer.group] = newConsumed; @@ -506,18 +505,18 @@ contract Midnight is IMidnight { function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external { require(onBehalf == msg.sender || isAuthorized[onBehalf][msg.sender], Unauthorized()); bytes32 id = touchMarket(market); - MarketState storage _marketState = marketState[id]; + MarketState storage state = _marketState[id]; _updatePosition(market, id, onBehalf); - Position storage _position = position[id][onBehalf]; + Position storage userPosition = _position[id][onBehalf]; uint128 pendingFeeDecrease; - if (_position.credit > 0) { - pendingFeeDecrease = UtilsLib.toUint128(_position.pendingFee.mulDivUp(units, _position.credit)); - _position.pendingFee -= pendingFeeDecrease; + if (userPosition.credit > 0) { + pendingFeeDecrease = UtilsLib.toUint128(userPosition.pendingFee.mulDivUp(units, userPosition.credit)); + userPosition.pendingFee -= pendingFeeDecrease; } - _position.credit -= UtilsLib.toUint128(units); - _marketState.withdrawable -= UtilsLib.toUint128(units); - _marketState.totalUnits -= UtilsLib.toUint128(units); + userPosition.credit -= UtilsLib.toUint128(units); + state.withdrawable -= UtilsLib.toUint128(units); + state.totalUnits -= UtilsLib.toUint128(units); emit EventsLib.Withdraw(msg.sender, id, units, onBehalf, receiver, pendingFeeDecrease); @@ -530,8 +529,8 @@ contract Midnight is IMidnight { require(onBehalf == msg.sender || isAuthorized[onBehalf][msg.sender], Unauthorized()); bytes32 id = touchMarket(market); - position[id][onBehalf].debt -= UtilsLib.toUint128(units); - marketState[id].withdrawable += UtilsLib.toUint128(units); + _position[id][onBehalf].debt -= UtilsLib.toUint128(units); + _marketState[id].withdrawable += UtilsLib.toUint128(units); address payer = callback != address(0) ? callback : msg.sender; emit EventsLib.Repay(msg.sender, id, units, onBehalf, payer); @@ -553,13 +552,13 @@ contract Midnight is IMidnight { bytes32 id = touchMarket(market); address collateralToken = market.collateralParams[collateralIndex].token; - Position storage _position = position[id][onBehalf]; - uint256 oldCollateral = _position.collateral[collateralIndex]; - _position.collateral[collateralIndex] = UtilsLib.toUint128(oldCollateral + assets); + Position storage userPosition = _position[id][onBehalf]; + uint256 oldCollateral = userPosition.collateral[collateralIndex]; + userPosition.collateral[collateralIndex] = UtilsLib.toUint128(oldCollateral + assets); if (oldCollateral == 0 && assets > 0) { - uint128 newCollateralBitmap = _position.collateralBitmap.setBit(collateralIndex); - _position.collateralBitmap = newCollateralBitmap; + uint128 newCollateralBitmap = userPosition.collateralBitmap.setBit(collateralIndex); + userPosition.collateralBitmap = newCollateralBitmap; require( UtilsLib.countBits(newCollateralBitmap) <= MAX_COLLATERALS_PER_BORROWER, TooManyActivatedCollaterals() ); @@ -582,12 +581,12 @@ contract Midnight is IMidnight { bytes32 id = touchMarket(market); address collateralToken = market.collateralParams[collateralIndex].token; - Position storage _position = position[id][onBehalf]; - uint256 newCollateral = _position.collateral[collateralIndex] - assets; - _position.collateral[collateralIndex] = UtilsLib.toUint128(newCollateral); + Position storage userPosition = _position[id][onBehalf]; + uint256 newCollateral = userPosition.collateral[collateralIndex] - assets; + userPosition.collateral[collateralIndex] = UtilsLib.toUint128(newCollateral); if (newCollateral == 0 && assets > 0) { - _position.collateralBitmap = _position.collateralBitmap.clearBit(collateralIndex); + userPosition.collateralBitmap = userPosition.collateralBitmap.clearBit(collateralIndex); } require(isHealthy(market, id, onBehalf), UnhealthyBorrower()); @@ -615,10 +614,10 @@ contract Midnight is IMidnight { bytes calldata data ) external returns (uint256, uint256) { bytes32 id = touchMarket(market); - MarketState storage _marketState = marketState[id]; - Position storage _position = position[id][borrower]; + MarketState storage state = _marketState[id]; + Position storage userPosition = _position[id][borrower]; require(repaidUnits == 0 || seizedAssets == 0, InconsistentInput()); - require(_position.debt > 0, NotBorrower()); // to avoid no-op liquidations of non borrower positions. + require(userPosition.debt > 0, NotBorrower()); // to avoid no-op liquidations of non borrower positions. require( market.liquidatorGate == address(0) || ILiquidatorGate(market.liquidatorGate).canLiquidate(msg.sender), LiquidatorGatedFromLiquidating() @@ -626,15 +625,15 @@ contract Midnight is IMidnight { uint256 maxDebt; uint256 liquidatedCollatPrice; - uint256 originalDebt = _position.debt; + uint256 originalDebt = userPosition.debt; uint256 badDebt = originalDebt; - uint128 _collateralBitmap = _position.collateralBitmap; + uint128 _collateralBitmap = userPosition.collateralBitmap; while (_collateralBitmap != 0) { uint256 i = UtilsLib.msb(_collateralBitmap); CollateralParams memory _collateralParam = market.collateralParams[i]; uint256 price = IOracle(_collateralParam.oracle).price(); if (i == collateralIndex) liquidatedCollatPrice = price; - uint256 _collateral = _position.collateral[i]; + uint256 _collateral = userPosition.collateral[i]; maxDebt += _collateral.mulDivDown(price, ORACLE_PRICE_SCALE).mulDivDown(_collateralParam.lltv, WAD); badDebt = badDebt.zeroFloorSub( _collateral.mulDivUp(price, ORACLE_PRICE_SCALE).mulDivUp(WAD, _collateralParam.maxLif) @@ -649,18 +648,18 @@ contract Midnight is IMidnight { ); if (badDebt > 0) { - // forge-lint: disable-next-item(unsafe-typecast) as badDebt <= _position.debt - _position.debt -= uint128(badDebt); - uint256 _totalUnits = _marketState.totalUnits; - uint256 _lossFactor = _marketState.lossFactor; - _marketState.lossFactor = UtilsLib.toUint128( + // forge-lint: disable-next-item(unsafe-typecast) as badDebt <= userPosition.debt + userPosition.debt -= uint128(badDebt); + uint256 _totalUnits = state.totalUnits; + uint256 _lossFactor = state.lossFactor; + state.lossFactor = UtilsLib.toUint128( type(uint128).max - (type(uint128).max - _lossFactor).mulDivDown(_totalUnits - badDebt, _totalUnits) ); - _marketState.totalUnits -= UtilsLib.toUint128(badDebt); - _marketState.continuousFeeCredit = _lossFactor < type(uint128).max + state.totalUnits -= UtilsLib.toUint128(badDebt); + state.continuousFeeCredit = _lossFactor < type(uint128).max ? UtilsLib.toUint128( - _marketState.continuousFeeCredit - .mulDivDown(type(uint128).max - _marketState.lossFactor, type(uint128).max - _lossFactor) + state.continuousFeeCredit + .mulDivDown(type(uint128).max - state.lossFactor, type(uint128).max - _lossFactor) ) : 0; } @@ -682,23 +681,24 @@ contract Midnight is IMidnight { // Note that debt >= maxDebt in this branch. // The imprecision in this computation is at most a few hundred collateral or loan token assets. uint256 maxRepaid = lltv < WAD - ? (_position.debt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lif * lltv) + ? (userPosition.debt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lif * lltv) : type(uint256).max; require( repaidUnits <= maxRepaid - || _position.collateral[collateralIndex].mulDivDown(liquidatedCollatPrice, ORACLE_PRICE_SCALE) - .mulDivDown(WAD, lif).zeroFloorSub(maxRepaid) < market.rcfThreshold, + || userPosition.collateral[collateralIndex].mulDivDown( + liquidatedCollatPrice, ORACLE_PRICE_SCALE + ).mulDivDown(WAD, lif).zeroFloorSub(maxRepaid) < market.rcfThreshold, RecoveryCloseFactorConditionsViolated() ); } - uint128 newCollateral = _position.collateral[collateralIndex] - UtilsLib.toUint128(seizedAssets); - _position.collateral[collateralIndex] = newCollateral; + uint128 newCollateral = userPosition.collateral[collateralIndex] - UtilsLib.toUint128(seizedAssets); + userPosition.collateral[collateralIndex] = newCollateral; if (newCollateral == 0 && seizedAssets > 0) { - _position.collateralBitmap = _position.collateralBitmap.clearBit(collateralIndex); + userPosition.collateralBitmap = userPosition.collateralBitmap.clearBit(collateralIndex); } - _marketState.withdrawable += UtilsLib.toUint128(repaidUnits); - _position.debt -= UtilsLib.toUint128(repaidUnits); + state.withdrawable += UtilsLib.toUint128(repaidUnits); + userPosition.debt -= UtilsLib.toUint128(repaidUnits); } address payer = callback != address(0) ? callback : msg.sender; @@ -714,8 +714,8 @@ contract Midnight is IMidnight { receiver, payer, badDebt, - _marketState.lossFactor, - _marketState.continuousFeeCredit + state.lossFactor, + state.continuousFeeCredit ); SafeTransferLib.safeTransfer(market.collateralParams[collateralIndex].token, receiver, seizedAssets); @@ -779,7 +779,7 @@ contract Midnight is IMidnight { /// @dev Returns the market id and creates the market if it doesn't exist yet. function touchMarket(Market memory market) public returns (bytes32) { bytes32 id = toId(market); - if (marketState[id].tickSpacing == 0) { + if (_marketState[id].tickSpacing == 0) { require(market.maturity <= block.timestamp + 100 * 365 days, MaturityTooFar()); require(market.collateralParams.length > 0, NoCollateralParams()); require(market.collateralParams.length <= MAX_COLLATERALS, TooManyCollateralParams()); @@ -797,17 +797,17 @@ contract Midnight is IMidnight { previousCollateralToken = collateralToken; } - MarketState storage _marketState = marketState[id]; - _marketState.tickSpacing = DEFAULT_TICK_SPACING; + MarketState storage state = _marketState[id]; + state.tickSpacing = DEFAULT_TICK_SPACING; uint16[7] memory _defaultSettlementFeeCbp = defaultSettlementFeeCbp[market.loanToken]; - _marketState.settlementFeeCbp0 = _defaultSettlementFeeCbp[0]; - _marketState.settlementFeeCbp1 = _defaultSettlementFeeCbp[1]; - _marketState.settlementFeeCbp2 = _defaultSettlementFeeCbp[2]; - _marketState.settlementFeeCbp3 = _defaultSettlementFeeCbp[3]; - _marketState.settlementFeeCbp4 = _defaultSettlementFeeCbp[4]; - _marketState.settlementFeeCbp5 = _defaultSettlementFeeCbp[5]; - _marketState.settlementFeeCbp6 = _defaultSettlementFeeCbp[6]; - _marketState.continuousFee = defaultContinuousFee[market.loanToken]; + state.settlementFeeCbp0 = _defaultSettlementFeeCbp[0]; + state.settlementFeeCbp1 = _defaultSettlementFeeCbp[1]; + state.settlementFeeCbp2 = _defaultSettlementFeeCbp[2]; + state.settlementFeeCbp3 = _defaultSettlementFeeCbp[3]; + state.settlementFeeCbp4 = _defaultSettlementFeeCbp[4]; + state.settlementFeeCbp5 = _defaultSettlementFeeCbp[5]; + state.settlementFeeCbp6 = _defaultSettlementFeeCbp[6]; + state.continuousFee = defaultContinuousFee[market.loanToken]; IdLib.storeInCode(market, INITIAL_CHAIN_ID); emit EventsLib.MarketCreated(market, id); @@ -824,17 +824,17 @@ contract Midnight is IMidnight { view returns (uint128, uint128, uint128) { - Position storage _position = position[id][user]; - uint128 _credit = _position.credit; - uint128 _lastLossFactor = _position.lastLossFactor; + Position storage userPosition = _position[id][user]; + uint128 _credit = userPosition.credit; + uint128 _lastLossFactor = userPosition.lastLossFactor; uint256 postSlashCredit = _lastLossFactor < type(uint128).max - ? _credit.mulDivDown(type(uint128).max - marketState[id].lossFactor, type(uint128).max - _lastLossFactor) + ? _credit.mulDivDown(type(uint128).max - _marketState[id].lossFactor, type(uint128).max - _lastLossFactor) : 0; - uint128 _pendingFee = _position.pendingFee; + uint128 _pendingFee = userPosition.pendingFee; uint256 postSlashPendingFee = _credit > 0 ? _pendingFee - _pendingFee.mulDivUp(_credit - postSlashCredit, _credit) : 0; uint256 accrualEnd = UtilsLib.min(block.timestamp, market.maturity); - uint128 _lastAccrual = _position.lastAccrual; + uint128 _lastAccrual = userPosition.lastAccrual; // forge-lint: disable-next-item(unsafe-typecast) as fee <= pending <= credit which are uint128 position fields uint128 fee = _lastAccrual < market.maturity ? uint128(postSlashPendingFee.mulDivDown(accrualEnd - _lastAccrual, market.maturity - _lastAccrual)) @@ -847,7 +847,7 @@ contract Midnight is IMidnight { /// @dev Returns the new credit, new pending fee, and accrued fee after having updated the position. function updatePosition(Market memory market, address user) external returns (uint128, uint128, uint128) { bytes32 id = toId(market); - require(marketState[id].tickSpacing > 0, MarketNotCreated()); + require(_marketState[id].tickSpacing > 0, MarketNotCreated()); return _updatePosition(market, id, user); } @@ -858,17 +858,17 @@ contract Midnight is IMidnight { internal returns (uint128, uint128, uint128) { - Position storage _position = position[id][user]; + Position storage userPosition = _position[id][user]; (uint128 newCredit, uint128 newPendingFee, uint128 accruedFee) = updatePositionView(market, id, user); - uint128 creditDecrease = _position.credit - newCredit; - uint128 pendingFeeDecrease = _position.pendingFee - newPendingFee; + uint128 creditDecrease = userPosition.credit - newCredit; + uint128 pendingFeeDecrease = userPosition.pendingFee - newPendingFee; - _position.credit = newCredit; - _position.lastLossFactor = marketState[id].lossFactor; - _position.pendingFee = newPendingFee; - _position.lastAccrual = uint128(block.timestamp); - marketState[id].continuousFeeCredit += UtilsLib.toUint128(accruedFee); + userPosition.credit = newCredit; + userPosition.lastLossFactor = _marketState[id].lossFactor; + userPosition.pendingFee = newPendingFee; + userPosition.lastAccrual = uint128(block.timestamp); + _marketState[id].continuousFeeCredit += UtilsLib.toUint128(accruedFee); emit EventsLib.UpdatePosition(id, user, creditDecrease, pendingFeeDecrease, accruedFee); @@ -876,37 +876,45 @@ contract Midnight is IMidnight { } function hasCredit(bytes32 id, address user) internal view returns (bool) { - return position[id][user].credit > 0; + return _position[id][user].credit > 0; } /// OTHER VIEW FUNCTIONS /// + function position(bytes32 id, address user) external view returns (Position memory) { + return _position[id][user]; + } + + function marketState(bytes32 id) external view returns (MarketState memory) { + return _marketState[id]; + } + function credit(bytes32 id, address user) external view returns (uint128) { - return position[id][user].credit; + return _position[id][user].credit; } function pendingFee(bytes32 id, address user) external view returns (uint128) { - return position[id][user].pendingFee; + return _position[id][user].pendingFee; } function lastLossFactor(bytes32 id, address user) external view returns (uint128) { - return position[id][user].lastLossFactor; + return _position[id][user].lastLossFactor; } function lastAccrual(bytes32 id, address user) external view returns (uint128) { - return position[id][user].lastAccrual; + return _position[id][user].lastAccrual; } function debt(bytes32 id, address user) external view returns (uint128) { - return position[id][user].debt; + return _position[id][user].debt; } function collateralBitmap(bytes32 id, address user) external view returns (uint128) { - return position[id][user].collateralBitmap; + return _position[id][user].collateralBitmap; } function collateral(bytes32 id, address user, uint256 index) external view returns (uint128) { - return position[id][user].collateral[index]; + return _position[id][user].collateral[index]; } function toId(Market memory market) public view returns (bytes32) { @@ -916,47 +924,47 @@ contract Midnight is IMidnight { /// @dev Reverts if the id is not a valid id of a touched market. /// @dev Returns the market corresponding to the given id. function toMarket(bytes32 id) external view returns (Market memory) { - require(marketState[id].tickSpacing > 0, MarketNotCreated()); + require(_marketState[id].tickSpacing > 0, MarketNotCreated()); address create2Address = address(uint160(uint256(id))); return abi.decode(create2Address.code, (Market)); } function totalUnits(bytes32 id) external view returns (uint128) { - return marketState[id].totalUnits; + return _marketState[id].totalUnits; } function lossFactor(bytes32 id) external view returns (uint128) { - return marketState[id].lossFactor; + return _marketState[id].lossFactor; } function withdrawable(bytes32 id) external view returns (uint128) { - return marketState[id].withdrawable; + return _marketState[id].withdrawable; } function continuousFeeCredit(bytes32 id) external view returns (uint128) { - return marketState[id].continuousFeeCredit; + return _marketState[id].continuousFeeCredit; } /// @dev The settlement fee cbp values are 0 until the market is created, then set to the default value. function settlementFeeCbps(bytes32 id) external view returns (uint16[7] memory) { return [ - marketState[id].settlementFeeCbp0, - marketState[id].settlementFeeCbp1, - marketState[id].settlementFeeCbp2, - marketState[id].settlementFeeCbp3, - marketState[id].settlementFeeCbp4, - marketState[id].settlementFeeCbp5, - marketState[id].settlementFeeCbp6 + _marketState[id].settlementFeeCbp0, + _marketState[id].settlementFeeCbp1, + _marketState[id].settlementFeeCbp2, + _marketState[id].settlementFeeCbp3, + _marketState[id].settlementFeeCbp4, + _marketState[id].settlementFeeCbp5, + _marketState[id].settlementFeeCbp6 ]; } /// @dev The continuous fee is 0 until the market is created, then set to the default value. function continuousFee(bytes32 id) external view returns (uint32) { - return marketState[id].continuousFee; + return _marketState[id].continuousFee; } function tickSpacing(bytes32 id) external view returns (uint8) { - return marketState[id].tickSpacing; + return _marketState[id].tickSpacing; } function liquidationLocked(bytes32 id, address user) public view returns (bool) { @@ -967,16 +975,16 @@ contract Midnight is IMidnight { /// @dev This function does not call any oracle if debt is 0. /// @dev Expects the id to correspond to the market's id. function isHealthy(Market memory market, bytes32 id, address borrower) public view returns (bool) { - Position storage _position = position[id][borrower]; - uint256 _debt = _position.debt; + Position storage userPosition = _position[id][borrower]; + uint256 _debt = userPosition.debt; uint256 maxDebt; if (_debt > 0) { - uint128 _collateralBitmap = _position.collateralBitmap; + uint128 _collateralBitmap = userPosition.collateralBitmap; while (_collateralBitmap != 0) { uint256 i = UtilsLib.msb(_collateralBitmap); CollateralParams memory collateralParam = market.collateralParams[i]; uint256 price = IOracle(collateralParam.oracle).price(); - maxDebt += _position.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE) + maxDebt += userPosition.collateral[i].mulDivDown(price, ORACLE_PRICE_SCALE) .mulDivDown(collateralParam.lltv, WAD); _collateralBitmap = _collateralBitmap.clearBit(i); } @@ -986,19 +994,19 @@ contract Midnight is IMidnight { /// @dev Returns the settlement fee using piecewise linear interpolation between breakpoints. function settlementFee(bytes32 id, uint256 timeToMaturity) public view returns (uint256) { - MarketState storage _marketState = marketState[id]; - require(_marketState.tickSpacing > 0, MarketNotCreated()); + MarketState storage state = _marketState[id]; + require(state.tickSpacing > 0, MarketNotCreated()); - if (timeToMaturity >= 360 days) return _marketState.settlementFeeCbp6 * CBP; + if (timeToMaturity >= 360 days) return state.settlementFeeCbp6 * CBP; // forgefmt: disable-start (uint256 start, uint256 end, uint256 feeLower, uint256 feeUpper) = - timeToMaturity < 1 days ? ( 0 days, 1 days, _marketState.settlementFeeCbp0 * CBP, _marketState.settlementFeeCbp1 * CBP) : - timeToMaturity < 7 days ? ( 1 days, 7 days, _marketState.settlementFeeCbp1 * CBP, _marketState.settlementFeeCbp2 * CBP) : - timeToMaturity < 30 days ? ( 7 days, 30 days, _marketState.settlementFeeCbp2 * CBP, _marketState.settlementFeeCbp3 * CBP) : - timeToMaturity < 90 days ? ( 30 days, 90 days, _marketState.settlementFeeCbp3 * CBP, _marketState.settlementFeeCbp4 * CBP) : - timeToMaturity < 180 days ? ( 90 days, 180 days, _marketState.settlementFeeCbp4 * CBP, _marketState.settlementFeeCbp5 * CBP) : - (180 days, 360 days, _marketState.settlementFeeCbp5 * CBP, _marketState.settlementFeeCbp6 * CBP); + timeToMaturity < 1 days ? ( 0 days, 1 days, state.settlementFeeCbp0 * CBP, state.settlementFeeCbp1 * CBP) : + timeToMaturity < 7 days ? ( 1 days, 7 days, state.settlementFeeCbp1 * CBP, state.settlementFeeCbp2 * CBP) : + timeToMaturity < 30 days ? ( 7 days, 30 days, state.settlementFeeCbp2 * CBP, state.settlementFeeCbp3 * CBP) : + timeToMaturity < 90 days ? ( 30 days, 90 days, state.settlementFeeCbp3 * CBP, state.settlementFeeCbp4 * CBP) : + timeToMaturity < 180 days ? ( 90 days, 180 days, state.settlementFeeCbp4 * CBP, state.settlementFeeCbp5 * CBP) : + (180 days, 360 days, state.settlementFeeCbp5 * CBP, state.settlementFeeCbp6 * CBP); // forgefmt: disable-end return (feeLower * (end - timeToMaturity) + feeUpper * (timeToMaturity - start)) / (end - start); diff --git a/src/interfaces/IMidnight.sol b/src/interfaces/IMidnight.sol index 7d93054d..5229e4d1 100644 --- a/src/interfaces/IMidnight.sol +++ b/src/interfaces/IMidnight.sol @@ -121,8 +121,8 @@ interface IMidnight { function INITIAL_CHAIN_ID() external view returns (uint256); /// STORAGE GETTERS /// - function position(bytes32 id, address user) external view returns (uint128 credit, uint128 pendingFee, uint128 lastLossFactor, uint128 lastAccrual, uint128 debt, uint128 collateralBitmap); - function marketState(bytes32 id) external view returns (uint128 totalUnits, uint128 lossFactor, uint128 withdrawable, uint128 continuousFeeCredit, uint16 settlementFeeCbp0, uint16 settlementFeeCbp1, uint16 settlementFeeCbp2, uint16 settlementFeeCbp3, uint16 settlementFeeCbp4, uint16 settlementFeeCbp5, uint16 settlementFeeCbp6, uint32 continuousFee, uint8 tickSpacing); + function position(bytes32 id, address user) external view returns (Position memory); + function marketState(bytes32 id) external view returns (MarketState memory); function consumed(address user, bytes32 group) external view returns (uint256); function isAuthorized(address authorizer, address authorized) external view returns (bool); function defaultSettlementFeeCbp(address loanToken, uint256 index) external view returns (uint16); diff --git a/test/OtherFunctionsTest.sol b/test/OtherFunctionsTest.sol index 08827607..b9d86715 100644 --- a/test/OtherFunctionsTest.sol +++ b/test/OtherFunctionsTest.sol @@ -2,7 +2,7 @@ // Copyright (c) 2025 Morpho Association pragma solidity ^0.8.0; -import {IMidnight, Market, CollateralParams} from "../src/interfaces/IMidnight.sol"; +import {IMidnight, Market, CollateralParams, MarketState, Position} from "../src/interfaces/IMidnight.sol"; import { IBuyCallback, ISellCallback, @@ -72,6 +72,30 @@ contract OtherFunctionsTest is BaseTest { id = toId(market); } + function testPositionGetterReturnsPositionStruct() public { + uint256 units = 100e18; + uint256 expectedCollateral = units.mulDivUp(WAD, market.collateralParams[0].lltv) + .mulDivUp(ORACLE_PRICE_SCALE, Oracle(market.collateralParams[0].oracle).price()); + collateralize(market, borrower, units); + + Position memory borrowerPosition = midnight.position(id, borrower); + + assertEq(borrowerPosition.credit, 0, "borrower credit"); + assertEq(borrowerPosition.debt, 0, "borrower debt"); + assertEq(borrowerPosition.collateral[0], expectedCollateral, "borrower collateral"); + assertEq(borrowerPosition.collateralBitmap, 1, "borrower collateral bitmap"); + } + + function testMarketStateGetterReturnsMarketStateStruct() public { + midnight.touchMarket(market); + + MarketState memory state = midnight.marketState(id); + + assertEq(state.totalUnits, 0, "total units"); + assertEq(state.lossFactor, midnight.lossFactor(id), "loss factor"); + assertEq(state.tickSpacing, midnight.tickSpacing(id), "tick spacing"); + } + function testWithdrawCollateralWithBorrowHealthy(uint256 additionalCollateral, uint256 withdraw, uint256 units) public { @@ -700,37 +724,23 @@ contract OtherFunctionsTest is BaseTest { bytes32 _id = midnight.touchMarket(_market); - ( - uint128 totalUnits, - uint128 _lossFactor, - uint128 _withdrawable, - uint128 _continuousFeeCredit, - uint16 settlementFeeCbp0, - uint16 settlementFeeCbp1, - uint16 settlementFeeCbp2, - uint16 settlementFeeCbp3, - uint16 settlementFeeCbp4, - uint16 settlementFeeCbp5, - uint16 settlementFeeCbp6, - uint32 _continuousFee, - uint8 tickSpacing - ) = midnight.marketState(_id); + MarketState memory state = midnight.marketState(_id); uint8 expectedTickSpacing = 4; - assertEq(totalUnits, 0, "totalUnits"); - assertEq(_lossFactor, 0, "lossFactor"); - assertEq(_withdrawable, 0, "withdrawable"); - assertEq(_continuousFeeCredit, 0, "continuousFeeCredit"); - assertEq(_continuousFee, _defaultContinuousFee, "continuousFee"); - assertEq(tickSpacing, expectedTickSpacing, "tickSpacing"); - assertEq(settlementFeeCbp0, midnight.defaultSettlementFeeCbp(_market.loanToken, 0), "settlementFeeCbp0"); - assertEq(settlementFeeCbp1, midnight.defaultSettlementFeeCbp(_market.loanToken, 1), "settlementFeeCbp1"); - assertEq(settlementFeeCbp2, midnight.defaultSettlementFeeCbp(_market.loanToken, 2), "settlementFeeCbp2"); - assertEq(settlementFeeCbp3, midnight.defaultSettlementFeeCbp(_market.loanToken, 3), "settlementFeeCbp3"); - assertEq(settlementFeeCbp4, midnight.defaultSettlementFeeCbp(_market.loanToken, 4), "settlementFeeCbp4"); - assertEq(settlementFeeCbp5, midnight.defaultSettlementFeeCbp(_market.loanToken, 5), "settlementFeeCbp5"); - assertEq(settlementFeeCbp6, midnight.defaultSettlementFeeCbp(_market.loanToken, 6), "settlementFeeCbp6"); + assertEq(state.totalUnits, 0, "totalUnits"); + assertEq(state.lossFactor, 0, "lossFactor"); + assertEq(state.withdrawable, 0, "withdrawable"); + assertEq(state.continuousFeeCredit, 0, "continuousFeeCredit"); + assertEq(state.continuousFee, _defaultContinuousFee, "continuousFee"); + assertEq(state.tickSpacing, expectedTickSpacing, "tickSpacing"); + assertEq(state.settlementFeeCbp0, midnight.defaultSettlementFeeCbp(_market.loanToken, 0), "settlementFeeCbp0"); + assertEq(state.settlementFeeCbp1, midnight.defaultSettlementFeeCbp(_market.loanToken, 1), "settlementFeeCbp1"); + assertEq(state.settlementFeeCbp2, midnight.defaultSettlementFeeCbp(_market.loanToken, 2), "settlementFeeCbp2"); + assertEq(state.settlementFeeCbp3, midnight.defaultSettlementFeeCbp(_market.loanToken, 3), "settlementFeeCbp3"); + assertEq(state.settlementFeeCbp4, midnight.defaultSettlementFeeCbp(_market.loanToken, 4), "settlementFeeCbp4"); + assertEq(state.settlementFeeCbp5, midnight.defaultSettlementFeeCbp(_market.loanToken, 5), "settlementFeeCbp5"); + assertEq(state.settlementFeeCbp6, midnight.defaultSettlementFeeCbp(_market.loanToken, 6), "settlementFeeCbp6"); } function testMarketStateAfterTake() public { @@ -740,11 +750,11 @@ contract OtherFunctionsTest is BaseTest { collateralize(market, borrower, units); setupMarket(market, units); - (uint128 totalUnits,,,,,,,,,,, uint32 _continuousFee, uint8 tickSpacing) = midnight.marketState(id); + MarketState memory state = midnight.marketState(id); - assertEq(totalUnits, units, "totalUnits after take"); - assertEq(_continuousFee, MAX_CONTINUOUS_FEE, "continuousFee after take"); - assertEq(tickSpacing, 4, "tickSpacing after take"); + assertEq(state.totalUnits, units, "totalUnits after take"); + assertEq(state.continuousFee, MAX_CONTINUOUS_FEE, "continuousFee after take"); + assertEq(state.tickSpacing, 4, "tickSpacing after take"); } function testMidnightRevertsOnCallbacks(address msgSender, bytes calldata data) public {