From 81a61d131a2e804097e46ba50d576605d74f1007 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 19 Jun 2026 17:53:40 +0200 Subject: [PATCH 01/10] all absolute paths imports --- test/TickLibTest.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/TickLibTest.sol b/test/TickLibTest.sol index 1f839741..8a80d29f 100644 --- a/test/TickLibTest.sol +++ b/test/TickLibTest.sol @@ -2,7 +2,7 @@ pragma solidity ^0.8.0; import {BaseTest} from "./BaseTest.sol"; -import {console} from "forge-std/Test.sol"; +import {console} from "../lib/forge-std/src/Test.sol"; import {TickLib} from "../src/libraries/TickLib.sol"; import {UtilsLib} from "../src/libraries/UtilsLib.sol"; import {MAX_TICK, PRICE_ROUNDING_STEP} from "../src/libraries/TickLib.sol"; From 95db623fd23862455428549a57abd8c6e7dd6786 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 22 Jun 2026 09:56:03 +0200 Subject: [PATCH 02/10] fix pragma & test contract name --- src/ratifiers/interfaces/IEcrecoverRatifier.sol | 2 +- src/ratifiers/interfaces/ISetterRatifier.sol | 2 +- test/{FlashloanTest.sol => FlashLoanTest.sol} | 0 test/SetIsAuthorizedWithSigTest.sol | 2 +- 4 files changed, 3 insertions(+), 3 deletions(-) rename test/{FlashloanTest.sol => FlashLoanTest.sol} (100%) diff --git a/src/ratifiers/interfaces/IEcrecoverRatifier.sol b/src/ratifiers/interfaces/IEcrecoverRatifier.sol index f9a85ad2..1652a16c 100644 --- a/src/ratifiers/interfaces/IEcrecoverRatifier.sol +++ b/src/ratifiers/interfaces/IEcrecoverRatifier.sol @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later // Copyright (c) 2025 Morpho Association -pragma solidity ^0.8.0; +pragma solidity >=0.5.0; import {IRatifier} from "../../interfaces/IRatifier.sol"; diff --git a/src/ratifiers/interfaces/ISetterRatifier.sol b/src/ratifiers/interfaces/ISetterRatifier.sol index ba880871..cdb41377 100644 --- a/src/ratifiers/interfaces/ISetterRatifier.sol +++ b/src/ratifiers/interfaces/ISetterRatifier.sol @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later // Copyright (c) 2025 Morpho Association -pragma solidity ^0.8.0; +pragma solidity >=0.5.0; import {IRatifier} from "../../interfaces/IRatifier.sol"; diff --git a/test/FlashloanTest.sol b/test/FlashLoanTest.sol similarity index 100% rename from test/FlashloanTest.sol rename to test/FlashLoanTest.sol diff --git a/test/SetIsAuthorizedWithSigTest.sol b/test/SetIsAuthorizedWithSigTest.sol index fd68da74..0d5a24b0 100644 --- a/test/SetIsAuthorizedWithSigTest.sol +++ b/test/SetIsAuthorizedWithSigTest.sol @@ -15,7 +15,7 @@ bytes constant AUTHORIZATION_TYPE = "Authorization(address authorizer,address authorized,bool isAuthorized,uint256 nonce,uint256 deadline)"; bytes constant EIP712_DOMAIN_TYPE = "EIP712Domain(uint256 chainId,address verifyingContract)"; -contract EcrecoverAuthorizerTest is BaseTest { +contract SetIsAuthorizedWithSigTest is BaseTest { function testAuthorizationTypeHash() public pure { assertEq(AUTHORIZATION_TYPEHASH, keccak256(AUTHORIZATION_TYPE)); } From 9995cb9859775bbe22a54d2f4a0313d295042290 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 19 Jun 2026 18:37:22 +0200 Subject: [PATCH 03/10] named multiple returned values --- src/interfaces/IMidnight.sol | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/interfaces/IMidnight.sol b/src/interfaces/IMidnight.sol index 5f27fe0b..a58c85b4 100644 --- a/src/interfaces/IMidnight.sol +++ b/src/interfaces/IMidnight.sol @@ -149,20 +149,20 @@ interface IMidnight { function claimContinuousFee(Market memory market, uint256 amount, address receiver) external; /// ENTRY-POINTS /// - function take(Offer memory offer, bytes memory ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes memory takerCallbackData) external returns (uint256, uint256); + function take(Offer memory offer, bytes memory ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes memory takerCallbackData) external returns (uint256 buyerAssets, uint256 sellerAssets); function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external; function repay(Market memory market, uint256 units, address onBehalf, address callback, bytes memory data) external; function supplyCollateral(Market memory market, uint256 collateralIndex, uint256 assets, address onBehalf) external; function withdrawCollateral(Market memory market, uint256 collateralIndex, uint256 assets, address onBehalf, address receiver) external; - function liquidate(Market memory market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes memory data) external returns (uint256, uint256); + function liquidate(Market memory market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bool postMaturityMode, address receiver, address callback, bytes memory data) external returns (uint256 outputSeizedAssets, uint256 outputRepaidUnits); function setConsumed(bytes32 group, uint256 amount, address onBehalf) external; function setIsAuthorized(address authorized, bool newIsAuthorized, address onBehalf) external; function flashLoan(address[] memory tokens, uint256[] memory assets, address callback, bytes memory data) external; function touchMarket(Market memory market) external returns (bytes32); /// SLASHING AND CONTINUOUS FEE ACCRUAL /// - function updatePositionView(Market memory market, bytes32 id, address user) external view returns (uint128, uint128, uint128); - function updatePosition(Market memory market, address user) external returns (uint128, uint128, uint128); + function updatePositionView(Market memory market, bytes32 id, address user) external view returns (uint128 newCredit, uint128 newPendingFee, uint128 accruedFee); + function updatePosition(Market memory market, address user) external returns (uint128 newCredit, uint128 newPendingFee, uint128 accruedFee); /// OTHER VIEW FUNCTIONS /// function lastLossFactor(bytes32 id, address user) external view returns (uint128); From 7dd02cf57b7e5275fed6f70e4769feef94c9bbec Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 19 Jun 2026 18:45:35 +0200 Subject: [PATCH 04/10] reorder getter functions --- src/Midnight.sol | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/Midnight.sol b/src/Midnight.sol index 2d3e2c4f..d92299ce 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -871,10 +871,26 @@ contract Midnight is IMidnight { /// OTHER VIEW FUNCTIONS /// + function creditOf(bytes32 id, address user) external view returns (uint128) { + return position[id][user].credit; + } + + function pendingFee(bytes32 id, address user) external view returns (uint128) { + return position[id][user].pendingFee; + } + function lastLossFactor(bytes32 id, address user) external view returns (uint128) { return position[id][user].lastLossFactor; } + function lastAccrual(bytes32 id, address user) external view returns (uint128) { + return position[id][user].lastAccrual; + } + + function debtOf(bytes32 id, address user) external view returns (uint128) { + return position[id][user].debt; + } + function collateralBitmap(bytes32 id, address user) external view returns (uint128) { return position[id][user].collateralBitmap; } @@ -895,14 +911,6 @@ contract Midnight is IMidnight { return abi.decode(create2Address.code, (Market)); } - function creditOf(bytes32 id, address user) external view returns (uint128) { - return position[id][user].credit; - } - - function debtOf(bytes32 id, address user) external view returns (uint128) { - return position[id][user].debt; - } - function totalUnits(bytes32 id) external view returns (uint128) { return marketState[id].totalUnits; } @@ -911,14 +919,14 @@ contract Midnight is IMidnight { return marketState[id].lossFactor; } - function tickSpacing(bytes32 id) external view returns (uint8) { - return marketState[id].tickSpacing; - } - function withdrawable(bytes32 id) external view returns (uint128) { return marketState[id].withdrawable; } + function continuousFeeCredit(bytes32 id) external view returns (uint128) { + 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 [ @@ -937,16 +945,8 @@ contract Midnight is IMidnight { return marketState[id].continuousFee; } - function continuousFeeCredit(bytes32 id) external view returns (uint128) { - return marketState[id].continuousFeeCredit; - } - - function pendingFee(bytes32 id, address user) external view returns (uint128) { - return position[id][user].pendingFee; - } - - function lastAccrual(bytes32 id, address user) external view returns (uint128) { - return position[id][user].lastAccrual; + function tickSpacing(bytes32 id) external view returns (uint8) { + return marketState[id].tickSpacing; } function liquidationLocked(bytes32 id, address user) public view returns (bool) { From 60f17e346f3efd0161d94172e067e4c41900f59e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 22 Jun 2026 12:10:15 +0200 Subject: [PATCH 05/10] fix typos --- src/Midnight.sol | 9 +++++---- src/libraries/TickLib.sol | 2 +- src/periphery/MidnightBundles.sol | 2 +- 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Midnight.sol b/src/Midnight.sol index d92299ce..7588c233 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -51,7 +51,7 @@ import {IMidnight, Market, Offer, CollateralParams, MarketState, Position} from /// CONTINUOUS FEES /// @dev A default continuous fee (per loan token) is set on new markets. Then, the fee setter can override it. /// @dev The fee is tracked per lender via pendingFee in each position. If the market's continuous fee changes, the -/// pending fee of existing lenders is not updated (=> their fee is fixed). If the market's continuious fee is decreased +/// pending fee of existing lenders is not updated (=> their fee is fixed). If the market's continuous fee is decreased /// lenders might self-take to exit and re-enter to reduce their pending fee (at the cost of the settlement fee). /// @dev In the absence of bad debt realizations, the face value of a lender's position is credit - pendingFee. /// @dev An offer cannot be taken if its continuousFeeCap value is lower than the current market continuous fee. @@ -76,8 +76,9 @@ import {IMidnight, Market, Offer, CollateralParams, MarketState, Position} from /// minNewCollateral * liquidatedCollatPrice / LIF < rcfThreshold /// <=> (collateral - maxRepaid * LIF / liquidatedCollatPrice) * liquidatedCollatPrice / LIF < rcfThreshold /// <=> collateral * liquidatedCollatPrice / LIF - maxRepaid < rcfThreshold -/// @dev Nothing prevents borrowers to open small positions / liquidators to leave small positions that might not be -/// profitable to liquidate because of gas cost. The RCF deactivation at rcfThreshold just prevents the systemic aspect. +/// @dev Nothing prevents borrowers from opening small positions / liquidators from leaving small positions that might +/// not be profitable to liquidate because of gas cost. The RCF deactivation at rcfThreshold just prevents the systemic +/// aspect. /// @dev In the "post-maturity mode", the LIF (liquidation incentive factor) grows linearly from 1 at maturity to maxLif /// at maturity + TIME_TO_MAX_LIF, and the RCF is deactivated. /// @dev In both modes, maxLif is used to determine if the account has some bad debt, to always assume the worst case. @@ -670,7 +671,7 @@ contract Midnight is IMidnight { if (!postMaturityMode) { uint256 lltv = market.collateralParams[collateralIndex].lltv; // Note that debt >= maxDebt in this branch. - // The imprecision in this computation is at most a few hundreds collateral or loan token assets. + // 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) : type(uint256).max; diff --git a/src/libraries/TickLib.sol b/src/libraries/TickLib.sol index 9f72b408..635de316 100644 --- a/src/libraries/TickLib.sol +++ b/src/libraries/TickLib.sol @@ -51,7 +51,7 @@ library TickLib { } } - /// @dev Among the ticks than are multiples of spacing, returns the lowest one with a price higher or equal. + /// @dev Among the ticks that are multiples of spacing, returns the lowest one with a price higher or equal. /// @dev spacing should divide MAX_TICK. function priceToTick(uint256 price, uint256 spacing) internal pure returns (uint256) { require(price <= 1e18, PriceGreaterThanOne()); diff --git a/src/periphery/MidnightBundles.sol b/src/periphery/MidnightBundles.sol index 7c2ca97c..bcc5d019 100644 --- a/src/periphery/MidnightBundles.sol +++ b/src/periphery/MidnightBundles.sol @@ -360,7 +360,7 @@ contract MidnightBundles is IMidnightBundles { } /// @dev Skips the approval entirely to save gas when the current allowance is already 2^95 - 1 (value chosen - /// because some token like COMP and UNI on ethereum have a max allowance of type(uint96).max). + /// because some tokens like COMP and UNI on Ethereum have a max allowance of type(uint96).max). /// @dev Resets to 0 before re-approving to support USDT like tokens. function forceApproveMax(address token, address spender) internal { if (IERC20(token).allowance(address(this), spender) >= type(uint96).max / 2) return; From 12a081dcb9e6ab249261446b3557072e45a6af19 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 22 Jun 2026 13:04:04 +0200 Subject: [PATCH 06/10] renaming creditOf debtOf --- certora/specs/BalanceEffects.spec | 100 +++++------ certora/specs/BundlerRepayInvertibility.spec | 6 +- certora/specs/ContinuousFee.spec | 8 +- certora/specs/Liquidate.spec | 14 +- certora/specs/LossFactor.spec | 16 +- certora/specs/Midnight.spec | 18 +- certora/specs/NotCreatedMarket.spec | 8 +- certora/specs/OnlyAuthorizedCanChange.spec | 12 +- .../OnlyAuthorizedCanChangeUpdatedValues.spec | 4 +- certora/specs/PostMaturityDebt.spec | 6 +- certora/specs/Reverts.spec | 24 +-- certora/specs/SplitPreservesAccounting.spec | 20 +-- certora/specs/UpdateBeforeCredit.spec | 2 +- src/Midnight.sol | 22 +-- src/interfaces/IMidnight.sol | 4 +- test/AuthorizationTest.sol | 6 +- test/BaseTest.sol | 6 +- test/ContinuousFeeTest.sol | 36 ++-- test/GateTest.sol | 18 +- test/LiquidationTest.sol | 69 ++++---- test/MaxAmountsTest.sol | 2 +- test/MidnightBundlesTest.sol | 36 ++-- test/OtherFunctionsTest.sol | 6 +- test/TakeTest.sol | 162 +++++++++--------- test/TickGatingTest.sol | 6 +- 25 files changed, 305 insertions(+), 306 deletions(-) diff --git a/certora/specs/BalanceEffects.spec b/certora/specs/BalanceEffects.spec index c4f83cb1..67fe2380 100644 --- a/certora/specs/BalanceEffects.spec +++ b/certora/specs/BalanceEffects.spec @@ -3,8 +3,8 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; - function debtOf(bytes32 id, address user) external returns (uint128) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; + function debt(bytes32 id, address user) external returns (uint128) envfree; function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; function collateral(bytes32 id, address user, uint256 index) external returns (uint128) envfree; function pendingFee(bytes32 id, address user) external returns (uint128) envfree; @@ -36,24 +36,24 @@ methods { rule updatePositionEffects(env e, Midnight.Market market, address user, bytes32 anyId, address anyUser) { bytes32 id = toId(e, market); - uint256 creditBefore = creditOf(id, user); + uint256 creditBefore = credit(id, user); uint128 updatedUserCredit; uint128 newPendingFee; uint128 userFee; updatedUserCredit, newPendingFee, userFee = updatePositionView(e, market, id, user); - uint256 anyCredit = creditOf(anyId, anyUser); - uint256 anyDebt = debtOf(anyId, anyUser); + uint256 anyCredit = credit(anyId, anyUser); + uint256 anyDebt = debt(anyId, anyUser); uint256 feeAmountBefore = continuousFeeCredit(id); updatePosition(e, market, user); - assert debtOf(anyId, anyUser) == anyDebt; - assert (anyId != id) || (anyUser != user) => creditOf(anyId, anyUser) == anyCredit; - assert creditOf(id, user) == updatedUserCredit; + assert debt(anyId, anyUser) == anyDebt; + assert (anyId != id) || (anyUser != user) => credit(anyId, anyUser) == anyCredit; + assert credit(id, user) == updatedUserCredit; assert pendingFee(id, user) == newPendingFee; assert continuousFeeCredit(id) == feeAmountBefore + userFee; - assert creditOf(id, user) <= creditBefore; + assert credit(id, user) <= creditBefore; } /// WITHDRAW /// @@ -67,15 +67,15 @@ rule withdrawEffects(env e, Midnight.Market market, uint256 units, address onBeh uint128 userFee; updatedUserCredit, _, userFee = updatePositionView(e, market, id, onBehalf); - uint256 anyCredit = creditOf(anyId, anyUser); - uint256 anyDebt = debtOf(anyId, anyUser); + uint256 anyCredit = credit(anyId, anyUser); + uint256 anyDebt = debt(anyId, anyUser); uint256 feeAmountBefore = continuousFeeCredit(id); withdraw(e, market, units, onBehalf, receiver); - assert creditOf(id, onBehalf) == updatedUserCredit - units; - assert debtOf(anyId, anyUser) == anyDebt; - assert (anyId != id) || (anyUser != onBehalf) => creditOf(anyId, anyUser) == anyCredit; + assert credit(id, onBehalf) == updatedUserCredit - units; + assert debt(anyId, anyUser) == anyDebt; + assert (anyId != id) || (anyUser != onBehalf) => credit(anyId, anyUser) == anyCredit; assert continuousFeeCredit(id) == feeAmountBefore + userFee; } @@ -90,22 +90,22 @@ rule takeEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 units, makerCreditBefore, _, _ = updatePositionView(e, offer.market, id, offer.maker); uint128 takerCreditBefore; takerCreditBefore, _, _ = updatePositionView(e, offer.market, id, taker); - mathint makerNetBefore = to_mathint(makerCreditBefore) - to_mathint(debtOf(id, offer.maker)); - mathint takerNetBefore = to_mathint(takerCreditBefore) - to_mathint(debtOf(id, taker)); - uint256 otherCreditBefore = creditOf(anyId, anyUser); - uint256 otherDebtBefore = debtOf(anyId, anyUser); + mathint makerNetBefore = makerCreditBefore - debt(id, offer.maker); + mathint takerNetBefore = takerCreditBefore - debt(id, taker); + uint256 otherCreditBefore = credit(anyId, anyUser); + uint256 otherDebtBefore = debt(anyId, anyUser); take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - mathint makerNetAfter = to_mathint(creditOf(id, offer.maker)) - to_mathint(debtOf(id, offer.maker)); - mathint takerNetAfter = to_mathint(creditOf(id, taker)) - to_mathint(debtOf(id, taker)); + mathint makerNetAfter = credit(id, offer.maker) - debt(id, offer.maker); + mathint takerNetAfter = credit(id, taker) - debt(id, taker); mathint makerDelta = offer.buy ? units : -units; assert makerNetAfter == makerNetBefore + makerDelta; mathint takerDelta = offer.buy ? -units : units; assert takerNetAfter == takerNetBefore + takerDelta; - assert anyId != id || (anyUser != offer.maker && anyUser != taker) => debtOf(anyId, anyUser) == otherDebtBefore; - assert anyId != id || (anyUser != offer.maker && anyUser != taker) => creditOf(anyId, anyUser) == otherCreditBefore; + assert anyId != id || (anyUser != offer.maker && anyUser != taker) => debt(anyId, anyUser) == otherDebtBefore; + assert anyId != id || (anyUser != offer.maker && anyUser != taker) => credit(anyId, anyUser) == otherCreditBefore; } /// The buyer side cannot newly become a borrower: buyer's debt is non-increasing. If buyer's credit increased, then buyer's debt is zero after the take. @@ -115,17 +115,17 @@ rule takeBuyerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 u bytes32 id = toId(e, offer.market); address buyer = offer.buy ? offer.maker : taker; - uint256 buyerDebtBefore = debtOf(id, buyer); + uint256 buyerDebtBefore = debt(id, buyer); uint128 buyerUpdatedCreditBefore; buyerUpdatedCreditBefore, _, _ = updatePositionView(e, offer.market, id, buyer); take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - assert creditOf(id, buyer) > buyerUpdatedCreditBefore => debtOf(id, buyer) == 0; - assert creditOf(id, buyer) >= buyerUpdatedCreditBefore; - assert creditOf(id, buyer) <= buyerUpdatedCreditBefore + units; - assert debtOf(id, buyer) <= buyerDebtBefore; - assert debtOf(id, buyer) >= buyerDebtBefore - units; + assert credit(id, buyer) > buyerUpdatedCreditBefore => debt(id, buyer) == 0; + assert credit(id, buyer) >= buyerUpdatedCreditBefore; + assert credit(id, buyer) <= buyerUpdatedCreditBefore + units; + assert debt(id, buyer) <= buyerDebtBefore; + assert debt(id, buyer) >= buyerDebtBefore - units; } /// The seller side cannot newly become a lender: seller's credit is non-increasing relative to its post-update value. If seller's debt increased, then seller's credit is zero after the take. @@ -135,17 +135,17 @@ rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 bytes32 id = toId(e, offer.market); address seller = offer.buy ? taker : offer.maker; - uint256 sellerDebtBefore = debtOf(id, seller); + uint256 sellerDebtBefore = debt(id, seller); uint128 sellerUpdatedCreditBefore; sellerUpdatedCreditBefore, _, _ = updatePositionView(e, offer.market, id, seller); take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - assert debtOf(id, seller) > sellerDebtBefore => creditOf(id, seller) == 0; - assert debtOf(id, seller) >= sellerDebtBefore; - assert debtOf(id, seller) <= sellerDebtBefore + units; - assert creditOf(id, seller) <= sellerUpdatedCreditBefore; - assert creditOf(id, seller) >= sellerUpdatedCreditBefore - units; + assert debt(id, seller) > sellerDebtBefore => credit(id, seller) == 0; + assert debt(id, seller) >= sellerDebtBefore; + assert debt(id, seller) <= sellerDebtBefore + units; + assert credit(id, seller) <= sellerUpdatedCreditBefore; + assert credit(id, seller) >= sellerUpdatedCreditBefore - units; } /// REPAY /// @@ -154,15 +154,15 @@ rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 rule repayEffects(env e, Midnight.Market market, uint256 units, address onBehalf, address callback, bytes data, bytes32 anyId, address anyUser) { bytes32 id = toId(e, market); - uint256 debtBefore = debtOf(id, onBehalf); - uint256 otherCreditBefore = creditOf(anyId, anyUser); - uint256 otherDebtBefore = debtOf(anyId, anyUser); + uint256 debtBefore = debt(id, onBehalf); + uint256 otherCreditBefore = credit(anyId, anyUser); + uint256 otherDebtBefore = debt(anyId, anyUser); repay(e, market, units, onBehalf, callback, data); - assert debtOf(id, onBehalf) == debtBefore - units; - assert creditOf(anyId, anyUser) == otherCreditBefore; - assert anyUser != onBehalf || anyId != id => debtOf(anyId, anyUser) == otherDebtBefore; + assert debt(id, onBehalf) == debtBefore - units; + assert credit(anyId, anyUser) == otherCreditBefore; + assert anyUser != onBehalf || anyId != id => debt(anyId, anyUser) == otherDebtBefore; } /// LIQUIDATE /// @@ -172,17 +172,17 @@ rule repayEffects(env e, Midnight.Market market, uint256 units, address onBehalf 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); - uint256 debtBefore = debtOf(id, borrower); - uint256 otherCreditBefore = creditOf(anyId, anyUser); - uint256 otherDebtBefore = debtOf(anyId, anyUser); + uint256 debtBefore = debt(id, borrower); + uint256 otherCreditBefore = credit(anyId, anyUser); + uint256 otherDebtBefore = debt(anyId, anyUser); uint256 seizedResult; uint256 repaidResult; seizedResult, repaidResult = liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); - assert debtOf(id, borrower) <= debtBefore - repaidResult; - assert creditOf(anyId, anyUser) == otherCreditBefore; - assert anyUser != borrower || anyId != id => debtOf(anyId, anyUser) == otherDebtBefore; + assert debt(id, borrower) <= debtBefore - repaidResult; + assert credit(anyId, anyUser) == otherCreditBefore; + assert anyUser != borrower || anyId != id => debt(anyId, anyUser) == otherDebtBefore; } /// ALL OTHER FUNCTIONS /// @@ -197,11 +197,11 @@ filtered { && f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector && f.selector != sig:updatePosition(Midnight.Market, address).selector } { - uint256 creditBefore = creditOf(id, user); - uint256 debtBefore = debtOf(id, user); + uint256 creditBefore = credit(id, user); + uint256 debtBefore = debt(id, user); f(e, args); - assert creditOf(id, user) == creditBefore; - assert debtOf(id, user) == debtBefore; + assert credit(id, user) == creditBefore; + assert debt(id, user) == debtBefore; } /// SUPPLY COLLATERAL /// diff --git a/certora/specs/BundlerRepayInvertibility.spec b/certora/specs/BundlerRepayInvertibility.spec index c4212fb2..e1ccd3ce 100644 --- a/certora/specs/BundlerRepayInvertibility.spec +++ b/certora/specs/BundlerRepayInvertibility.spec @@ -5,7 +5,7 @@ using Midnight as midnight; methods { function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; - function midnight.debtOf(bytes32 id, address user) external returns (uint128) envfree; + function midnight.debt(bytes32 id, address user) external returns (uint128) envfree; function midnight.isAuthorized(address authorizer, address authorized) external returns (bool) envfree; function midnight.tickSpacing(bytes32 id) external returns (uint8) envfree; @@ -45,7 +45,7 @@ rule repayAndWithdrawCollateralRepaysTargetUnits(env e, Midnight.Market market, require referralFeePct < WAD(), "PctExceeded"; bytes32 id = summaryToId(market); - uint256 debtBefore = midnight.debtOf(id, onBehalf); + uint256 debtBefore = midnight.debt(id, onBehalf); uint256 wMinusP = assert_uint256(WAD() - referralFeePct); uint256 assets = summaryMulDivDown(U, WAD(), wMinusP); @@ -59,5 +59,5 @@ rule repayAndWithdrawCollateralRepaysTargetUnits(env e, Midnight.Market market, repayAndWithdrawCollateral(e, market, assets, onBehalf, loanTokenPermit, collateralWithdrawals, collateralReceiver, referralFeePct, referralFeeRecipient); - assert midnight.debtOf(id, onBehalf) == debtBefore - U; + assert midnight.debt(id, onBehalf) == debtBefore - U; } diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec index 5d27e6ee..847f314d 100644 --- a/certora/specs/ContinuousFee.spec +++ b/certora/specs/ContinuousFee.spec @@ -5,7 +5,7 @@ methods { function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => CVL_toId(market); - function creditOf(bytes32 id, address user) external returns (uint128) envfree; + 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; @@ -48,7 +48,7 @@ rule continuousFeeNotOverchargedForBuyer(env e, Midnight.Offer offer, bytes rati postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.market, id, buyer); - require pendingFee(id, buyer) <= creditOf(id, buyer), "See pendingContinuousFeeBoundedByCredit in Midnight.spec"; + require pendingFee(id, buyer) <= credit(id, buyer), "See pendingContinuousFeeBoundedByCredit in Midnight.spec"; take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); @@ -57,7 +57,7 @@ rule continuousFeeNotOverchargedForBuyer(env e, Midnight.Offer offer, bytes rati uint256 contFee = continuousFee(id); uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0; - mathint creditDelta = creditOf(id, buyer) - postUpdateCredit; + mathint creditDelta = credit(id, buyer) - postUpdateCredit; assert pendingFee(id, buyer) == postUpdatePendingFee + (creditDelta * contFee * timeToMaturity) / WAD(); } @@ -78,7 +78,7 @@ rule pendingFeeDecreasesProportionallyForSeller(env e, Midnight.Offer offer, byt require id == lastId, "id should be derived from market"; - uint256 creditAfter = creditOf(id, seller); + uint256 creditAfter = credit(id, seller); uint256 pendingFeeAfter = pendingFee(id, seller); require creditAfter > 0 || pendingFeeAfter == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec"; diff --git a/certora/specs/Liquidate.spec b/certora/specs/Liquidate.spec index d2a01e3a..4ca0919c 100644 --- a/certora/specs/Liquidate.spec +++ b/certora/specs/Liquidate.spec @@ -3,8 +3,8 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; - function debtOf(bytes32 id, address user) external returns (uint128) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; + function debt(bytes32 id, address user) external returns (uint128) envfree; function collateral(bytes32 id, address user, uint256 index) external returns (uint128) envfree; function liquidationLocked(bytes32 id, address user) external returns (bool) envfree; function isHealthy(Midnight.Market, bytes32, address) external returns (bool) envfree; @@ -49,16 +49,16 @@ rule liquidateOnlyAffectsBalancesWhenLiquidatable(env e, Midnight.Market market, address user; uint256 collateralIndex; - bool wasLiquidatable = debtOf(id, liqUser) > 0 && !liquidationLocked(id, liqUser) && (e.block.timestamp > market.maturity || !isHealthy(market, id, liqUser)); + bool wasLiquidatable = debt(id, liqUser) > 0 && !liquidationLocked(id, liqUser) && (e.block.timestamp > market.maturity || !isHealthy(market, id, liqUser)); - uint256 creditBefore = creditOf(id, user); - uint256 debtBefore = debtOf(id, user); + uint256 creditBefore = credit(id, user); + uint256 debtBefore = debt(id, user); uint256 collateralBefore = collateral(id, user, collateralIndex); liquidate(e, market, liqIndex, seizedAssets, repaidUnits, liqUser, postMaturityMode, receiver, callback, data); - uint256 creditAfter = creditOf(id, user); - uint256 debtAfter = debtOf(id, user); + uint256 creditAfter = credit(id, user); + uint256 debtAfter = debt(id, user); uint256 collateralAfter = collateral(id, user, collateralIndex); assert id == liqId => wasLiquidatable; diff --git a/certora/specs/LossFactor.spec b/certora/specs/LossFactor.spec index e1b44e8d..05f71ad0 100644 --- a/certora/specs/LossFactor.spec +++ b/certora/specs/LossFactor.spec @@ -5,7 +5,7 @@ using Utils as Utils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; function totalUnits(bytes32 id) external returns (uint128) envfree; function pendingFee(bytes32 id, address user) external returns (uint128) envfree; function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; @@ -75,7 +75,7 @@ rule updatePositionDoesNotRevert(env e, Midnight.Market market, address user) { 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 pendingFee(id, user) <= creditOf(id, user), "pending fee bounded by credit, 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"; @@ -90,13 +90,13 @@ rule updatePositionDoesNotRevert(env e, Midnight.Market market, address user) { rule updatePositionIsIdempotent(env e, Midnight.Market market, address user) { bytes32 id = summaryToId(market); - require pendingFee(id, user) <= creditOf(id, user), "see pendingContinuousFeeBoundedByCredit in Midnight.spec"; + 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"; // Snapshot the relevant position state after a first updatePosition. updatePosition(e, market, user); - mathint creditAfterFirst = creditOf(id, user); + mathint creditAfterFirst = credit(id, user); mathint pendingFeeAfterFirst = pendingFee(id, user); uint128 lastLossFactorAfterFirst = lastLossFactor(id, user); uint128 lastAccrualAfterFirst = currentContract.position[id][user].lastAccrual; @@ -113,7 +113,7 @@ rule updatePositionIsIdempotent(env e, Midnight.Market market, address user) { assert accruedFee == 0; // Stored position state is unchanged by the second call. - assert creditOf(id, user) == creditAfterFirst; + assert credit(id, user) == creditAfterFirst; assert pendingFee(id, user) == pendingFeeAfterFirst; assert lastLossFactor(id, user) == lastLossFactorAfterFirst; assert currentContract.position[id][user].lastAccrual == lastAccrualAfterFirst; @@ -127,10 +127,10 @@ rule updatePositionPreservesCreditWhenLossIndexCurrent(env e, Midnight.Market ma 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) <= creditOf(id, user), "see pendingContinuousFeeBoundedByCredit in Midnight.spec"; + require pendingFee(id, user) <= credit(id, user), "see pendingContinuousFeeBoundedByCredit in Midnight.spec"; require e.block.timestamp < 2 ^ 128, "reasonable timestamp"; - mathint creditBefore = creditOf(id, user); + mathint creditBefore = credit(id, user); mathint pendingFeeBefore = pendingFee(id, user); uint128 newCredit; @@ -141,7 +141,7 @@ rule updatePositionPreservesCreditWhenLossIndexCurrent(env e, Midnight.Market ma // Credit and pendingFee only decrease by the accrued fee (no slashing). assert newCredit + accruedFee == creditBefore; assert newPendingFee + accruedFee == pendingFeeBefore; - assert creditOf(id, user) + accruedFee == creditBefore; + assert credit(id, user) + accruedFee == creditBefore; assert pendingFee(id, user) + accruedFee == pendingFeeBefore; } diff --git a/certora/specs/Midnight.spec b/certora/specs/Midnight.spec index 204a8e6e..a8731d84 100644 --- a/certora/specs/Midnight.spec +++ b/certora/specs/Midnight.spec @@ -8,8 +8,8 @@ methods { function withdrawable(bytes32 id) external returns (uint128) envfree; function totalUnits(bytes32 id) external returns (uint128) envfree; function claimableSettlementFee(address token) external returns (uint256) envfree; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; - function debtOf(bytes32 id, address user) external returns (uint128) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; + function debt(bytes32 id, address user) external returns (uint128) envfree; function pendingFee(bytes32 id, address user) external returns (uint128) envfree; function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; function tickSpacing(bytes32 id) external returns (uint8) envfree; @@ -109,13 +109,13 @@ 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"; - uint256 creditBefore = creditOf(id, user); - uint256 debtBefore = debtOf(id, user); + uint256 creditBefore = credit(id, user); + uint256 debtBefore = debt(id, user); f(e, args); - assert creditOf(id, user) <= creditBefore; - assert debtOf(id, user) <= debtBefore; + assert credit(id, user) <= creditBefore; + assert debt(id, user) <= debtBefore; } /// INVARIANTS /// @@ -135,7 +135,7 @@ strong invariant continuousFeeBounded(bytes32 id) } strong invariant pendingContinuousFeeBoundedByCredit(bytes32 id, address user) - pendingFee(id, user) <= creditOf(id, user) + pendingFee(id, user) <= credit(id, user) { preserved with (env e) { requireInvariant continuousFeeBounded(id); @@ -150,7 +150,7 @@ strong invariant pendingContinuousFeeBoundedByCredit(bytes32 id, address user) rule noRemainingContinuousFeeWithoutCredit(bytes32 id, address user) { requireInvariant pendingContinuousFeeBoundedByCredit(id, user); - assert creditOf(id, user) == 0 => pendingFee(id, user) == 0; + assert credit(id, user) == 0 => pendingFee(id, user) == 0; } strong invariant lastLossFactorLeqMarketLossFactor(bytes32 id, address user) @@ -158,4 +158,4 @@ strong invariant lastLossFactorLeqMarketLossFactor(bytes32 id, address user) /// A user cannot have both credit and debt. strong invariant noCreditAndDebt(bytes32 id, address user) - creditOf(id, user) == 0 || debtOf(id, user) == 0; + credit(id, user) == 0 || debt(id, user) == 0; diff --git a/certora/specs/NotCreatedMarket.spec b/certora/specs/NotCreatedMarket.spec index a8cf715e..9fbf41a5 100644 --- a/certora/specs/NotCreatedMarket.spec +++ b/certora/specs/NotCreatedMarket.spec @@ -7,8 +7,8 @@ methods { function withdrawable(bytes32) external returns (uint128) envfree; function settlementFeeCbps(bytes32) external returns (uint16[7]) envfree; function continuousFee(bytes32) external returns (uint32) envfree; - function creditOf(bytes32, address) external returns (uint128) envfree; - function debtOf(bytes32, address) external returns (uint128) envfree; + function credit(bytes32, address) external returns (uint128) envfree; + function debt(bytes32, address) external returns (uint128) envfree; function pendingFee(bytes32, address) external returns (uint128) envfree; function lastAccrual(bytes32, address) external returns (uint128) envfree; function tickSpacing(bytes32) external returns (uint8) envfree; @@ -63,10 +63,10 @@ strong invariant marketLossFactorIsEmptyIfNotCreated(bytes32 id) !marketIsCreated(id) => currentContract.marketState[id].lossFactor == 0; strong invariant marketCreditIsEmptyIfNotCreated(bytes32 id, address user) - !marketIsCreated(id) => creditOf(id, user) == 0; + !marketIsCreated(id) => credit(id, user) == 0; strong invariant marketDebtIsEmptyIfNotCreated(bytes32 id, address user) - !marketIsCreated(id) => debtOf(id, user) == 0; + !marketIsCreated(id) => debt(id, user) == 0; strong invariant marketCollateralBitmapAreEmptyIfNotCreated(bytes32 id, address user) !marketIsCreated(id) => userHasEmptyCollateralBitmap(id, user); diff --git a/certora/specs/OnlyAuthorizedCanChange.spec b/certora/specs/OnlyAuthorizedCanChange.spec index 04ebc8f1..03b6ef45 100644 --- a/certora/specs/OnlyAuthorizedCanChange.spec +++ b/certora/specs/OnlyAuthorizedCanChange.spec @@ -4,8 +4,8 @@ methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function toId(Midnight.Market market) external returns (bytes32) envfree; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; - function debtOf(bytes32 id, address user) external returns (uint128) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; + function debt(bytes32 id, address user) external returns (uint128) envfree; function collateral(bytes32 id, address user, uint256 index) external returns (uint128) envfree; function consumed(address user, bytes32 group) external returns (uint256) envfree; function isAuthorized(address authorizer, address authorized) external returns (bool) envfree; @@ -51,11 +51,11 @@ function CVL_isRatified(Midnight.Offer offer) returns bytes32 { rule onlyAuthorizedCanChangeCreditAndDebtExceptLiquidateAndUpdatePosition(env e, method f, calldataarg args, bytes32 id, address user) filtered { f -> f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector && f.selector != sig:updatePosition(Midnight.Market, address).selector } { bool userIsAuthorized = user == e.msg.sender || isAuthorized(user, e.msg.sender); - uint256 creditBefore = creditOf(id, user); - uint256 debtBefore = debtOf(id, user); + uint256 creditBefore = credit(id, user); + uint256 debtBefore = debt(id, user); f(e, args); - uint256 creditAfter = creditOf(id, user); - uint256 debtAfter = debtOf(id, user); + uint256 creditAfter = credit(id, user); + uint256 debtAfter = debt(id, user); assert (creditAfter == creditBefore && debtAfter == debtBefore) || userIsAuthorized || makerRatified[user]; } diff --git a/certora/specs/OnlyAuthorizedCanChangeUpdatedValues.spec b/certora/specs/OnlyAuthorizedCanChangeUpdatedValues.spec index dab7042d..22dc0aa4 100644 --- a/certora/specs/OnlyAuthorizedCanChangeUpdatedValues.spec +++ b/certora/specs/OnlyAuthorizedCanChangeUpdatedValues.spec @@ -9,7 +9,7 @@ methods { function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; // Position/marketState getters used to express protocol invariants as preconditions. - function creditOf(bytes32, address) external returns (uint128) envfree; + function credit(bytes32, address) external returns (uint128) envfree; function pendingFee(bytes32, address) external returns (uint128) envfree; function lastLossFactor(bytes32, address) external returns (uint128) envfree; function lastAccrual(bytes32, address) external returns (uint128) envfree; @@ -102,7 +102,7 @@ rule onlyAuthorizedCanChangeUpdatedValuesExceptLiquidate(env e, method f, callda bytes32 id = summaryToId(market); bool userIsAuthorized = user == e.msg.sender || isAuthorized(user, e.msg.sender); - require pendingFee(id, user) <= creditOf(id, user), "see pendingContinuousFeeBoundedByCredit"; + require pendingFee(id, user) <= credit(id, user), "see pendingContinuousFeeBoundedByCredit"; require lastLossFactor(id, user) <= lossFactor(id), "see lastLossFactorLeqMarketLossFactor"; require lastAccrual(id, user) <= require_uint128(e.block.timestamp), "lastAccrual <= block.timestamp by timestamp monotonicity"; diff --git a/certora/specs/PostMaturityDebt.spec b/certora/specs/PostMaturityDebt.spec index 86d77d67..ee689b83 100644 --- a/certora/specs/PostMaturityDebt.spec +++ b/certora/specs/PostMaturityDebt.spec @@ -5,7 +5,7 @@ using Utils as Utils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function debtOf(bytes32 id, address user) external returns (uint128) envfree; + function debt(bytes32 id, address user) external returns (uint128) envfree; function Utils.hashMarket(Midnight.Market) external returns (bytes32) envfree; // Deterministic toId summary. @@ -31,9 +31,9 @@ function summaryToId(Midnight.Market market) returns bytes32 { rule debtCannotIncreasePostMaturity(env e, method f, calldataarg args, Midnight.Market market, address user) filtered { f -> !f.isView } { bytes32 id = summaryToId(market); - mathint debtBefore = debtOf(id, user); + mathint debtBefore = debt(id, user); f(e, args); - assert e.block.timestamp > market.maturity => debtOf(id, user) <= debtBefore; + assert e.block.timestamp > market.maturity => debt(id, user) <= debtBefore; } diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 23890e8f..2dfcccde 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -7,8 +7,8 @@ using Utils as Utils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function debtOf(bytes32 id, address user) external returns (uint128) envfree; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; + function debt(bytes32 id, address user) external returns (uint128) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; function collateral(bytes32 id, address user, uint256) external returns (uint128) envfree; function collateralBitmap(bytes32 id, address user) external returns (uint128) envfree; function liquidationLocked(bytes32 id, address user) external returns (bool) envfree; @@ -205,7 +205,7 @@ rule oracleRevertCausesWithdrawCollateralRevert(env e, Midnight.Market market, u withdrawCollateral@withrevert(e, market, collateralIndex, assets, onBehalf, receiver); bool reverted = lastReverted; - assert debtOf(id, onBehalf) > 0 => reverted; + assert debt(id, onBehalf) > 0 => reverted; } /// If an activated collateral oracle reverts on price, isHealthy reverts when the borrower has debt. @@ -218,7 +218,7 @@ rule oracleRevertCausesIsHealthyRevert(env e, Midnight.Market market, bytes32 id isHealthy@withrevert(e, market, id, borrower); bool reverted = lastReverted; - assert debtOf(id, borrower) > 0 => reverted; + assert debt(id, borrower) > 0 => reverted; } /// If an activated collateral oracle reverts on price and take succeeds, the seller must have no debt. @@ -237,7 +237,7 @@ rule oracleRevertPreventsTakeWhenSellerHasDebt(env e, Midnight.Offer offer, byte take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - assert debtOf(id, seller) == 0; + assert debt(id, seller) == 0; } /// ORACLE RETURNS ZERO /// @@ -261,7 +261,7 @@ rule oracleZeroCausesIsHealthyReturnFalse(env e, Midnight.Market market, address bool healthy = isHealthy(e, market, id, borrower); - assert debtOf(id, borrower) > 0 => !healthy; + assert debt(id, borrower) > 0 => !healthy; } /// If all oracles return 0, withdrawCollateral reverts when the borrower has debt. @@ -273,7 +273,7 @@ rule oracleZeroPreventsWithdrawCollateralWhenBorrowerHasDebt(env e, Midnight.Mar withdrawCollateral(e, market, collateralIndex, assets, onBehalf, receiver); - assert debtOf(id, onBehalf) == 0; + assert debt(id, onBehalf) == 0; } /// If all oracles return 0 and take succeeds, the seller must have no debt. @@ -286,7 +286,7 @@ rule oracleZeroPreventsTakeWhenSellerHasDebt(env e, Midnight.Offer offer, bytes take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - assert debtOf(id, seller) == 0; + assert debt(id, seller) == 0; } /// GATE BLOCKING /// @@ -297,11 +297,11 @@ rule enterGateBlocksCreditIncrease(env e, Midnight.Offer offer, bytes ratifierDa require offer.market.enterGate != 0, "enter gate is set"; bytes32 id = summaryToId(offer.market); - uint256 creditBefore = creditOf(id, user); + uint256 creditBefore = credit(id, user); take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - uint256 creditAfter = creditOf(id, user); + uint256 creditAfter = credit(id, user); assert creditAfter <= creditBefore; } @@ -312,11 +312,11 @@ rule enterGateBlocksDebtIncrease(env e, Midnight.Offer offer, bytes ratifierData require offer.market.enterGate != 0, "enter gate is set"; bytes32 id = summaryToId(offer.market); - uint256 debtBefore = debtOf(id, user); + uint256 debtBefore = debt(id, user); take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); - uint256 debtAfter = debtOf(id, user); + uint256 debtAfter = debt(id, user); assert debtAfter <= debtBefore; } diff --git a/certora/specs/SplitPreservesAccounting.spec b/certora/specs/SplitPreservesAccounting.spec index 9f68588e..829fc188 100644 --- a/certora/specs/SplitPreservesAccounting.spec +++ b/certora/specs/SplitPreservesAccounting.spec @@ -5,8 +5,8 @@ using Utils as Utils; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function creditOf(bytes32 id, address user) external returns (uint128) envfree; - function debtOf(bytes32 id, address user) external returns (uint128) envfree; + function credit(bytes32 id, address user) external returns (uint128) envfree; + function debt(bytes32 id, address user) external returns (uint128) envfree; function totalUnits(bytes32 id) external returns (uint128) envfree; function lastLossFactor(bytes32 id, address user) external returns (uint128) envfree; function lastAccrual(bytes32 id, address user) external returns (uint128) envfree; @@ -71,10 +71,10 @@ 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 creditOfBuyer1 = creditOf(id, buyer); - uint128 debtOfBuyer1 = debtOf(id, buyer); - uint128 creditOfSeller1 = creditOf(id, seller); - uint128 debtOfSeller1 = debtOf(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); @@ -89,10 +89,10 @@ rule splitPreservesAccounting(env e, uint256 unitsA, uint256 unitsB, uint256 uni take(e, offer, ratifierData, unitsC, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); - assert creditOfBuyer1 == creditOf(id, buyer); - assert debtOfBuyer1 == debtOf(id, buyer); - assert creditOfSeller1 == creditOf(id, seller); - assert debtOfSeller1 == debtOf(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); diff --git a/certora/specs/UpdateBeforeCredit.spec b/certora/specs/UpdateBeforeCredit.spec index 43336564..323eeaf6 100644 --- a/certora/specs/UpdateBeforeCredit.spec +++ b/certora/specs/UpdateBeforeCredit.spec @@ -73,7 +73,7 @@ rule creditNotStoredBeforeUpdate(env e, method f, calldataarg args, bytes32 id, /// Check that credit is never loaded before _updatePosition is called. /// The SLOADs of _updatePosition are ignored (see summary above). -rule creditNotLoadedBeforeUpdate(env e, method f, calldataarg args, bytes32 id, address user) filtered { f -> f.selector != sig:creditOf(bytes32, address).selector && f.selector != sig:updatePositionView(Midnight.Market, bytes32, address).selector && f.selector != sig:position(bytes32, address).selector } { +rule creditNotLoadedBeforeUpdate(env e, method f, calldataarg args, bytes32 id, address user) filtered { f -> f.selector != sig:credit(bytes32, address).selector && f.selector != sig:updatePositionView(Midnight.Market, bytes32, address).selector && f.selector != sig:position(bytes32, address).selector } { require !creditLoadedBeforeUpdate[id][user], "initialize the ghost variable"; f(e, args); diff --git a/src/Midnight.sol b/src/Midnight.sol index 7588c233..6e551b30 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -68,8 +68,8 @@ import {IMidnight, Market, Offer, CollateralParams, MarketState, Position} from /// @dev In the "normal mode", the liquidation incentive factor (LIF) is maxLif and the liquidation amount is capped /// by what is needed to put back the position into health ("recovery close factor", or "RCF"). /// @dev The RCF condition is (omitting scaling and roundings): -/// newDebt >= newMaxDebt <=> debtOf - repaidUnits >= maxDebt - repaidUnits*LIF*LLTV -/// <=> repaidUnits <= (debtOf-maxDebt) / (1 - LIF*LLTV). +/// newDebt >= newMaxDebt <=> debt - repaidUnits >= maxDebt - repaidUnits*LIF*LLTV +/// <=> repaidUnits <= (debt-maxDebt) / (1 - LIF*LLTV). /// @dev The RCF is deactivated for small collateral amount, essentially to mitigate issues with liquidations that are /// too small compared to the gas cost. More precisely, it is deactivated if the liquidation could leave a collateral /// with a value that would not be enough to repay rcfThreshold units. Which means (omitting scaling and roundings): @@ -176,7 +176,7 @@ import {IMidnight, Market, Offer, CollateralParams, MarketState, Position} from /// @dev No-ops are allowed. /// @dev Zero checks are not systematically performed. /// @dev NatSpec comments are included only when they bring clarity. -/// @dev creditOf, pendingFee, and lastLossFactor are not up to date. Use updatePositionView to get the up-to-date +/// @dev credit, pendingFee, and lastLossFactor are not up to date. Use updatePositionView to get the up-to-date /// values. /// @dev The max amount of totalUnits, collateral, credit, continuousFeeCredit and debt is type(uint128).max (~1e38). /// @dev INITIAL_CHAIN_ID is captured at construction and used in place of block.chainid when computing market ids, @@ -816,14 +816,14 @@ contract Midnight is IMidnight { returns (uint128, uint128, uint128) { Position storage _position = position[id][user]; - uint128 credit = _position.credit; + uint128 _credit = _position.credit; uint128 _lastLossFactor = _position.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; uint256 postSlashPendingFee = - credit > 0 ? _pendingFee - _pendingFee.mulDivUp(credit - postSlashCredit, credit) : 0; + _credit > 0 ? _pendingFee - _pendingFee.mulDivUp(_credit - postSlashCredit, _credit) : 0; uint256 accrualEnd = UtilsLib.min(block.timestamp, market.maturity); uint128 _lastAccrual = _position.lastAccrual; // forge-lint: disable-next-item(unsafe-typecast) as fee <= pending <= credit which are uint128 position fields @@ -872,7 +872,7 @@ contract Midnight is IMidnight { /// OTHER VIEW FUNCTIONS /// - function creditOf(bytes32 id, address user) external view returns (uint128) { + function credit(bytes32 id, address user) external view returns (uint128) { return position[id][user].credit; } @@ -888,7 +888,7 @@ contract Midnight is IMidnight { return position[id][user].lastAccrual; } - function debtOf(bytes32 id, address user) external view returns (uint128) { + function debt(bytes32 id, address user) external view returns (uint128) { return position[id][user].debt; } @@ -959,9 +959,9 @@ contract Midnight is IMidnight { /// @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; + uint256 _debt = _position.debt; uint256 maxDebt; - if (debt > 0) { + if (_debt > 0) { uint128 _collateralBitmap = _position.collateralBitmap; while (_collateralBitmap != 0) { uint256 i = UtilsLib.msb(_collateralBitmap); @@ -972,7 +972,7 @@ contract Midnight is IMidnight { _collateralBitmap = _collateralBitmap.clearBit(i); } } - return maxDebt >= debt; + return maxDebt >= _debt; } /// @dev Returns the settlement fee using piecewise linear interpolation between breakpoints. diff --git a/src/interfaces/IMidnight.sol b/src/interfaces/IMidnight.sol index a58c85b4..faf0a370 100644 --- a/src/interfaces/IMidnight.sol +++ b/src/interfaces/IMidnight.sol @@ -170,8 +170,8 @@ interface IMidnight { function collateral(bytes32 id, address user, uint256 index) external view returns (uint128); function toId(Market memory market) external view returns (bytes32); function toMarket(bytes32 id) external view returns (Market memory); - function creditOf(bytes32 id, address user) external view returns (uint128); - function debtOf(bytes32 id, address user) external view returns (uint128); + function credit(bytes32 id, address user) external view returns (uint128); + function debt(bytes32 id, address user) external view returns (uint128); function totalUnits(bytes32 id) external view returns (uint128); function lossFactor(bytes32 id) external view returns (uint128); function tickSpacing(bytes32 id) external view returns (uint8); diff --git a/test/AuthorizationTest.sol b/test/AuthorizationTest.sol index 2ff493d9..f901bdab 100644 --- a/test/AuthorizationTest.sol +++ b/test/AuthorizationTest.sol @@ -249,7 +249,7 @@ contract AuthorizationTest is BaseTest { vm.prank(operator); midnight.take(offer, hex"", units, taker, taker, address(0), hex""); - assertEq(midnight.debtOf(id, taker), units); + assertEq(midnight.debt(id, taker), units); } function testRepayAuthorization(address authorized) public { @@ -275,7 +275,7 @@ contract AuthorizationTest is BaseTest { vm.prank(authorized); midnight.repay(market, units, borrower, address(0), hex""); - assertEq(midnight.debtOf(id, borrower), 0); + assertEq(midnight.debt(id, borrower), 0); } function testSetConsumedAuthorization(address user, address authorized) public { @@ -328,6 +328,6 @@ contract AuthorizationTest is BaseTest { // Borrower can take for themselves (no authorization needed) take(units, borrower, offer); - assertEq(midnight.debtOf(id, borrower), units); + assertEq(midnight.debt(id, borrower), units); } } diff --git a/test/BaseTest.sol b/test/BaseTest.sol index ea494bdd..7596771d 100644 --- a/test/BaseTest.sol +++ b/test/BaseTest.sol @@ -233,9 +233,9 @@ abstract contract BaseTest is Test { // then empty the market (borrow side only). vm.prank(badBorrower); midnight.setIsAuthorized(address(this), true, badBorrower); - deal(address(loanToken), address(this), midnight.debtOf(toId(market), badBorrower)); - midnight.repay(market, midnight.debtOf(toId(market), badBorrower), badBorrower, address(0), hex""); - assertEq(midnight.debtOf(toId(market), badBorrower), 0, "debt"); + deal(address(loanToken), address(this), midnight.debt(toId(market), badBorrower)); + midnight.repay(market, midnight.debt(toId(market), badBorrower), badBorrower, address(0), hex""); + assertEq(midnight.debt(toId(market), badBorrower), 0, "debt"); // reset the price. Oracle(market.collateralParams[0].oracle).setPrice(ORACLE_PRICE_SCALE); diff --git a/test/ContinuousFeeTest.sol b/test/ContinuousFeeTest.sol index da6d0724..3507e525 100644 --- a/test/ContinuousFeeTest.sol +++ b/test/ContinuousFeeTest.sol @@ -87,7 +87,7 @@ contract ContinuousFeeTest is BaseTest { emit EventsLib.Withdraw(lender, id, 0, lender, lender, 0); vm.prank(lender); midnight.withdraw(market, 0, lender, lender); - assertEq(midnight.creditOf(id, lender), credit - expectedFee, "credit after withdraw"); + assertEq(midnight.credit(id, lender), credit - expectedFee, "credit after withdraw"); assertEq(midnight.pendingFee(id, lender), remaining - expectedFee, "remaining after withdraw"); vm.revertToState(snap); @@ -95,7 +95,7 @@ contract ContinuousFeeTest is BaseTest { vm.expectEmit(); emit EventsLib.UpdatePosition(id, lender, expectedFee, expectedFee, expectedFee); midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), credit - expectedFee, "credit after direct call"); + assertEq(midnight.credit(id, lender), credit - expectedFee, "credit after direct call"); assertEq(midnight.pendingFee(id, lender), remaining - expectedFee, "remaining after direct call"); assertEq(midnight.lastAccrual(id, lender), vm.getBlockTimestamp(), "lender lastAccrual after update"); @@ -125,7 +125,7 @@ contract ContinuousFeeTest is BaseTest { emit EventsLib.Withdraw(lender, id, 0, lender, lender, 0); vm.prank(lender); midnight.withdraw(market, 0, lender, lender); - assertEq(midnight.creditOf(id, lender), credit - remaining, "all remaining consumed (withdraw)"); + assertEq(midnight.credit(id, lender), credit - remaining, "all remaining consumed (withdraw)"); assertEq(midnight.pendingFee(id, lender), 0, "remaining is zero (withdraw)"); vm.revertToState(snap); @@ -133,7 +133,7 @@ contract ContinuousFeeTest is BaseTest { vm.expectEmit(); emit EventsLib.UpdatePosition(id, lender, remaining, remaining, remaining); midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), credit - remaining, "all remaining consumed (direct)"); + assertEq(midnight.credit(id, lender), credit - remaining, "all remaining consumed (direct)"); assertEq(midnight.pendingFee(id, lender), 0, "remaining is zero (direct)"); } @@ -160,13 +160,13 @@ contract ContinuousFeeTest is BaseTest { midnight.updatePosition(market, lender); vm.warp(vm.getBlockTimestamp() + elapsed2); midnight.updatePosition(market, lender); - uint256 creditTwoAccruals = midnight.creditOf(id, lender); + uint256 creditTwoAccruals = midnight.credit(id, lender); vm.revertToState(snap); // Single accrual for same total elapsed vm.warp(vm.getBlockTimestamp() + elapsed1 + elapsed2); midnight.updatePosition(market, lender); - uint256 creditOneAccrual = midnight.creditOf(id, lender); + uint256 creditOneAccrual = midnight.credit(id, lender); assertApproxEqAbs(creditTwoAccruals, creditOneAccrual, 2, "two accruals ~ one accrual"); } @@ -181,7 +181,7 @@ contract ContinuousFeeTest is BaseTest { uint256 expectedRemaining = (uint256(feeRate) * credit).mulDivDown(ttm, WAD); assertEq(midnight.pendingFee(id, lender), expectedRemaining, "lender remaining after entry"); assertEq(midnight.pendingFee(id, borrower), 0, "borrower has no pending fee"); - assertEq(midnight.debtOf(id, borrower), credit, "debt unchanged at entry"); + assertEq(midnight.debt(id, borrower), credit, "debt unchanged at entry"); } function _makeBorrowOffer(uint256 credit2) internal view returns (Offer memory borrowOffer) { @@ -235,7 +235,7 @@ contract ContinuousFeeTest is BaseTest { midnight.updatePosition(market, lender); uint256 expectedFee = blendedRemaining.mulDivDown(elapsed, ttm); - assertApproxEqAbs(midnight.creditOf(id, lender), credit1 + credit2 - expectedFee, 1, "credit after accrual"); + assertApproxEqAbs(midnight.credit(id, lender), credit1 + credit2 - expectedFee, 1, "credit after accrual"); assertApproxEqAbs(midnight.pendingFee(id, lender), blendedRemaining - expectedFee, 1, "remaining after accrual"); } @@ -298,7 +298,7 @@ contract ContinuousFeeTest is BaseTest { take(exitAmount, lender, _makeBuyOffer(keccak256("lender-exit"))); // lender is taker = seller uint256 expectedRemaining = creditAfterAccrual > 0 ? remainingAfterAccrual - sellerPendingFeeDecrease : 0; - assertEq(midnight.creditOf(id, lender), creditAfterAccrual - exitAmount, "credit after exit"); + assertEq(midnight.credit(id, lender), creditAfterAccrual - exitAmount, "credit after exit"); assertApproxEqAbs(midnight.pendingFee(id, lender), expectedRemaining, 1, "remaining after exit"); if (exitAmount == creditAfterAccrual) { @@ -306,7 +306,7 @@ contract ContinuousFeeTest is BaseTest { } assertEq(midnight.pendingFee(id, otherLender), buyerPendingFeeIncrease, "buyer pendingFee after exit"); - assertEq(midnight.creditOf(id, otherLender), exitAmount, "buyer credit after exit"); + assertEq(midnight.credit(id, otherLender), exitAmount, "buyer credit after exit"); } function testWithdrawReducesPendingFee( @@ -350,7 +350,7 @@ contract ContinuousFeeTest is BaseTest { uint256 expectedRemaining = creditAfterAccrual > 0 ? remainingAfterAccrual - pendingFeeDecrease : 0; - assertEq(midnight.creditOf(id, lender), creditAfterAccrual - withdrawAmount, "credit after withdraw"); + assertEq(midnight.credit(id, lender), creditAfterAccrual - withdrawAmount, "credit after withdraw"); assertApproxEqAbs(midnight.pendingFee(id, lender), expectedRemaining, 1, "remaining after withdraw"); if (withdrawAmount == creditAfterAccrual) { @@ -379,13 +379,13 @@ contract ContinuousFeeTest is BaseTest { vm.warp(vm.getBlockTimestamp() + elapsed1); midnight.updatePosition(market, lender); - uint256 creditBeforeSlash = midnight.creditOf(id, lender); + uint256 creditBeforeSlash = midnight.credit(id, lender); // Slash. createBadDebt(market); midnight.updatePosition(market, lender); - uint256 creditAfterSlash = midnight.creditOf(id, lender); + uint256 creditAfterSlash = midnight.credit(id, lender); vm.assume(creditAfterSlash < creditBeforeSlash); uint256 pendingAfterSlash = midnight.pendingFee(id, lender); @@ -396,7 +396,7 @@ contract ContinuousFeeTest is BaseTest { midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), creditAfterSlash - accruedFee, "credit after slash and accrual"); + assertEq(midnight.credit(id, lender), creditAfterSlash - accruedFee, "credit after slash and accrual"); assertApproxEqAbs( midnight.pendingFee(id, lender), pendingAfterSlash - accruedFee, 1, "remaining after slash and accrual" ); @@ -521,7 +521,7 @@ contract ContinuousFeeTest is BaseTest { midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), newCredit, "view matches credit"); + assertEq(midnight.credit(id, lender), newCredit, "view matches credit"); assertEq(midnight.pendingFee(id, lender), newPendingFee, "view matches pendingFee"); } @@ -553,7 +553,7 @@ contract ContinuousFeeTest is BaseTest { assertEq(returnedCredit, expectedCredit, "returned credit"); assertEq(returnedPendingFee, expectedPendingFee, "returned pendingFee"); assertEq(returnedAccruedFee, expectedAccruedFee, "returned accruedFee"); - assertEq(midnight.creditOf(id, lender), returnedCredit, "stored credit"); + assertEq(midnight.credit(id, lender), returnedCredit, "stored credit"); assertEq(midnight.pendingFee(id, lender), returnedPendingFee, "stored pendingFee"); assertEq(midnight.continuousFeeCredit(id), expectedContinuousFeeCredit, "continuousFeeCredit"); } @@ -614,7 +614,7 @@ contract ContinuousFeeTest is BaseTest { offer.continuousFeeCap = continuousFeeCap; take(units, borrower, offer); - assertEq(midnight.debtOf(id, borrower), units, "borrower took on debt"); + assertEq(midnight.debt(id, borrower), units, "borrower took on debt"); } function testTakeRevertsWhenSellOfferContinuousFeeCapExceeded(uint256 feeRate, uint256 continuousFeeCap) public { @@ -646,6 +646,6 @@ contract ContinuousFeeTest is BaseTest { offer.continuousFeeCap = continuousFeeCap; take(units, lender, offer); // lender is the buyer, otherBorrower (maker) is the seller. - assertEq(midnight.creditOf(id, lender), units, "lender gained credit"); + assertEq(midnight.credit(id, lender), units, "lender gained credit"); } } diff --git a/test/GateTest.sol b/test/GateTest.sol index 8c6597ed..f587e812 100644 --- a/test/GateTest.sol +++ b/test/GateTest.sol @@ -123,8 +123,8 @@ contract GateTest is BaseTest { take(units, lender, borrowerOffer); - assertGt(midnight.creditOf(gatedId, lender), 0, "lender should have credit"); - assertGt(midnight.debtOf(gatedId, borrower), 0, "borrower should have debt"); + assertGt(midnight.credit(gatedId, lender), 0, "lender should have credit"); + assertGt(midnight.debt(gatedId, borrower), 0, "borrower should have debt"); } function testEnterGateAllowsTakeWhenLenderHadCreditBefore(uint256 units) public { @@ -134,7 +134,7 @@ contract GateTest is BaseTest { collateralize(gatedMarket, borrower, units); take(units, lender, borrowerOffer); - assertGt(midnight.creditOf(gatedId, lender), 0, "lender should already have credit"); + assertGt(midnight.credit(gatedId, lender), 0, "lender should already have credit"); gate.setWhitelisted(lender, false); gate.setWhitelisted(borrower, false); @@ -149,7 +149,7 @@ contract GateTest is BaseTest { collateralize(gatedMarket, borrower, units); take(units, lender, borrowerOffer); - assertGt(midnight.debtOf(gatedId, borrower), 0, "borrower should already have debt"); + assertGt(midnight.debt(gatedId, borrower), 0, "borrower should already have debt"); gate.setWhitelisted(lender, false); gate.setWhitelisted(borrower, false); @@ -184,7 +184,7 @@ contract GateTest is BaseTest { take(units, borrower, otherBorrowerOffer); - assertEq(midnight.debtOf(gatedId, borrower), 0, "borrower should have exited debt"); + assertEq(midnight.debt(gatedId, borrower), 0, "borrower should have exited debt"); } function testNoGateCheckWhenBothExit(uint256 units) public { @@ -224,7 +224,7 @@ contract GateTest is BaseTest { deal(address(loanToken), otherBorrower, units); take(units, otherBorrower, exitOffer); - assertEq(midnight.debtOf(gatedId, otherBorrower), 0, "otherBorrower should have exited"); + assertEq(midnight.debt(gatedId, otherBorrower), 0, "otherBorrower should have exited"); } function testNoGateCheckOnRepay(uint256 units) public { @@ -241,7 +241,7 @@ contract GateTest is BaseTest { vm.prank(borrower); midnight.repay(gatedMarket, units, borrower, address(0), hex""); - assertEq(midnight.debtOf(gatedId, borrower), 0, "borrower should have repaid"); + assertEq(midnight.debt(gatedId, borrower), 0, "borrower should have repaid"); } function testNoGateCheckOnWithdraw(uint256 units) public { @@ -261,7 +261,7 @@ contract GateTest is BaseTest { vm.prank(lender); midnight.withdraw(gatedMarket, units, lender, lender); - assertEq(midnight.creditOf(gatedId, lender), 0, "lender should have withdrawn"); + assertEq(midnight.credit(gatedId, lender), 0, "lender should have withdrawn"); } // --- Liquidator gate tests --- @@ -317,7 +317,7 @@ contract GateTest is BaseTest { take(units, borrower, ungatedLenderOffer); bytes32 ungatedId = toId(market); - assertGt(midnight.debtOf(ungatedId, borrower), 0); + assertGt(midnight.debt(ungatedId, borrower), 0); } // --- Market identity tests --- diff --git a/test/LiquidationTest.sol b/test/LiquidationTest.sol index cb95826f..b1c503a7 100644 --- a/test/LiquidationTest.sol +++ b/test/LiquidationTest.sol @@ -99,7 +99,7 @@ contract LiquidationTest is BaseTest { uint256 collatBefore = midnight.collateral(id, borrower, 0); midnight.liquidate(market, 1, 0, 0, borrower, false, address(this), address(0), ""); - assertEq(midnight.debtOf(id, borrower), 0); + assertEq(midnight.debt(id, borrower), 0); assertEq(midnight.collateral(id, borrower, 0), collatBefore); assertEq(midnight.collateral(id, borrower, 1), 0); } @@ -211,7 +211,7 @@ contract LiquidationTest is BaseTest { "seized assets" ); - assertEq(midnight.debtOf(id, borrower), units - repaidUnits); + assertEq(midnight.debt(id, borrower), units - repaidUnits); assertEq(midnight.collateral(id, borrower, 0), initialCollateral - seizedAssets); } @@ -244,7 +244,7 @@ contract LiquidationTest is BaseTest { ); assertEq(seizedAssets, seized, "seized assets"); - assertEq(midnight.debtOf(id, borrower), units - repaidUnits, "debt"); + assertEq(midnight.debt(id, borrower), units - repaidUnits, "debt"); assertEq(midnight.collateral(id, borrower, 0), initialCollateral - seizedAssets, "collateral"); } @@ -354,11 +354,11 @@ contract LiquidationTest is BaseTest { midnight.liquidate(market, 0, 0, 0, borrower, false, address(this), address(0), ""); - assertEq(midnight.debtOf(id, borrower), units - expectedBadDebt, "debt"); + assertEq(midnight.debt(id, borrower), units - expectedBadDebt, "debt"); assertEq(midnight.totalUnits(id), units - expectedBadDebt, "total units"); - assertEq(midnight.creditOf(id, lender), units, "lender units"); + assertEq(midnight.credit(id, lender), units, "lender units"); midnight.updatePosition(market, lender); - assertApproxEqAbs(midnight.creditOf(id, lender), units - expectedBadDebt, 1, "lender units after slashing"); + assertApproxEqAbs(midnight.credit(id, lender), units - expectedBadDebt, 1, "lender units after slashing"); } function testLiquidateEmitsLossFactorAndContinuousFeeCredit(uint256 units) public { @@ -417,7 +417,7 @@ contract LiquidationTest is BaseTest { emit EventsLib.UpdatePosition(id, lender, units - expectedCredit, 0, 0); midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), expectedCredit, "credit"); + assertEq(midnight.credit(id, lender), expectedCredit, "credit"); assertEq(midnight.lastLossFactor(id, lender), lossFactor, "last loss factor"); } @@ -432,11 +432,11 @@ contract LiquidationTest is BaseTest { (, uint256 repaid) = midnight.liquidate(market, 0, seized, 0, borrower, false, address(this), address(0), ""); - assertEq(midnight.debtOf(id, borrower), debtAfterBadDebt - repaid, "debt"); + assertEq(midnight.debt(id, borrower), debtAfterBadDebt - repaid, "debt"); assertEq(midnight.totalUnits(id), debtAfterBadDebt, "total units"); - assertEq(midnight.creditOf(id, lender), units, "lender units"); + assertEq(midnight.credit(id, lender), units, "lender units"); midnight.updatePosition(market, lender); - assertApproxEqAbs(midnight.creditOf(id, lender), debtAfterBadDebt, 1, "lender units after slashing"); + assertApproxEqAbs(midnight.credit(id, lender), debtAfterBadDebt, 1, "lender units after slashing"); } function testLiquidateWithBadDebtRepaidInput(uint256 units, uint256 repaid, uint256 liquidationOraclePrice) public { @@ -454,11 +454,11 @@ contract LiquidationTest is BaseTest { midnight.liquidate(market, 0, 0, repaid, borrower, false, address(this), address(0), ""); - assertEq(midnight.debtOf(id, borrower), debtAfterBadDebt - repaid, "debt"); + assertEq(midnight.debt(id, borrower), debtAfterBadDebt - repaid, "debt"); assertEq(midnight.totalUnits(id), debtAfterBadDebt, "total units"); - assertEq(midnight.creditOf(id, lender), units, "lender units"); + assertEq(midnight.credit(id, lender), units, "lender units"); midnight.updatePosition(market, lender); - assertApproxEqAbs(midnight.creditOf(id, lender), debtAfterBadDebt, 1, "lender units after slashing"); + assertApproxEqAbs(midnight.credit(id, lender), debtAfterBadDebt, 1, "lender units after slashing"); } // Check that if there is bad debt it is possible to seize almost all collateral. @@ -473,7 +473,7 @@ contract LiquidationTest is BaseTest { market, 0, midnight.collateral(id, borrower, 0), 0, borrower, false, address(this), address(0), "" ); - assertApproxEqAbs(midnight.debtOf(id, borrower), 0, 1e3, "almost all remaining debt repaid"); + assertApproxEqAbs(midnight.debt(id, borrower), 0, 1e3, "almost all remaining debt repaid"); assertApproxEqAbs( midnight.collateral(id, borrower, 0).mulDivDown(liquidationOraclePrice, ORACLE_PRICE_SCALE), 0, @@ -504,7 +504,7 @@ contract LiquidationTest is BaseTest { midnight.liquidate(market, 0, 0, repaid, borrower, true, address(this), address(0), ""); - assertEq(midnight.debtOf(id, borrower), units - repaid, "debt"); + assertEq(midnight.debt(id, borrower), units - repaid, "debt"); assertEq( midnight.collateral(id, borrower, 0), initialCollateral @@ -535,7 +535,7 @@ contract LiquidationTest is BaseTest { uint256 lif = WAD + (market.collateralParams[0].maxLif - WAD) * delay / TIME_TO_MAX_LIF; - assertEq(midnight.debtOf(id, borrower), units - repaid, "debt"); + assertEq(midnight.debt(id, borrower), units - repaid, "debt"); assertEq( midnight.collateral(id, borrower, 0), initialCollateral - repaid.mulDivDown(lif, WAD).mulDivDown(ORACLE_PRICE_SCALE, liquidationOraclePrice), @@ -572,7 +572,7 @@ contract LiquidationTest is BaseTest { midnight.liquidate(market, 0, 0, min(maxR, units), borrower, false, address(this), address(0), ""); uint256 remainingCollateral = midnight.collateral(id, borrower, 0); - uint256 remainingDebt = midnight.debtOf(id, borrower); + uint256 remainingDebt = midnight.debt(id, borrower); uint256 newMaxDebt = remainingCollateral.mulDivDown(liquidationOraclePrice, ORACLE_PRICE_SCALE) .mulDivDown(market.collateralParams[0].lltv, WAD); // After max repayment the position should be just healthy or almost healthy (within rounding tolerance). @@ -619,7 +619,7 @@ contract LiquidationTest is BaseTest { // Full liquidation should succeed because remaining debt < rcfThreshold. midnight.liquidate(market, 0, 0, units, borrower, false, address(this), address(0), ""); - assertEq(midnight.debtOf(toId(market), borrower), 0, "debt should be zero"); + assertEq(midnight.debt(toId(market), borrower), 0, "debt should be zero"); } /// @dev When rcfThreshold <= remaining debt after max repayment, recovery close factor is enforced. @@ -705,7 +705,7 @@ contract LiquidationTest is BaseTest { bytes32 borrowerSlot = keccak256(abi.encode(borrower, intermediateSlot)); vm.store(address(midnight), bytes32(uint256(borrowerSlot) + 2), bytes32(units)); - assertEq(midnight.debtOf(id, borrower), units, "debt"); + assertEq(midnight.debt(id, borrower), units, "debt"); // Collateralize with both collateralParams. @@ -730,7 +730,7 @@ contract LiquidationTest is BaseTest { midnight.liquidate(market, 0, collateral1, 0, borrower, false, address(this), address(0), ""); } - uint256 debtAfter = midnight.debtOf(id, borrower); + uint256 debtAfter = midnight.debt(id, borrower); uint256 collateralAfter = midnight.collateral(id, borrower, 0); assertTrue(debtAfter == 0 || collateralAfter == 0, "either debt repaid or collateral seized"); } @@ -836,11 +836,11 @@ contract LiquidationTest is BaseTest { collateralize(market, borrower, units); setupMarket(market, units); - uint256 creditBefore = midnight.creditOf(id, lender); + uint256 creditBefore = midnight.credit(id, lender); midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), creditBefore, "credit unchanged"); + assertEq(midnight.credit(id, lender), creditBefore, "credit unchanged"); } function testSlashNoCredit(uint256 units) public { @@ -851,15 +851,14 @@ contract LiquidationTest is BaseTest { Oracle(market.collateralParams[0].oracle).setPrice(badDebtPriceDown(units)); midnight.liquidate(market, 0, 0, 0, borrower, false, address(this), address(0), ""); - assertEq(midnight.creditOf(id, borrower), 0, "no credit before"); - uint256 debtBefore = midnight.debtOf(id, borrower); + assertEq(midnight.credit(id, borrower), 0, "no credit before"); + uint256 debtBefore = midnight.debt(id, borrower); uint128 oblLossFactor = midnight.lossFactor(id); assertGt(oblLossFactor, midnight.lastLossFactor(id, borrower), "last loss factor stale before"); - midnight.updatePosition(market, borrower); - assertEq(midnight.creditOf(id, borrower), 0, "no credit after"); - assertEq(midnight.debtOf(id, borrower), debtBefore, "debt unchanged"); + assertEq(midnight.credit(id, borrower), 0, "no credit after"); + assertEq(midnight.debt(id, borrower), debtBefore, "debt unchanged"); assertEq(midnight.lastLossFactor(id, borrower), oblLossFactor, "last loss factor synced"); } @@ -871,15 +870,15 @@ contract LiquidationTest is BaseTest { Oracle(market.collateralParams[0].oracle).setPrice(badDebtPriceDown(units)); midnight.liquidate(market, 0, 0, 0, borrower, false, address(this), address(0), ""); - uint256 creditBeforeSlash = midnight.creditOf(id, lender); + uint256 creditBeforeSlash = midnight.credit(id, lender); midnight.updatePosition(market, lender); - uint256 creditAfterFirstSlash = midnight.creditOf(id, lender); + uint256 creditAfterFirstSlash = midnight.credit(id, lender); uint128 lastLossFactorAfterFirstSlash = midnight.lastLossFactor(id, lender); assertLt(creditAfterFirstSlash, creditBeforeSlash, "first slash reduced credit"); midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), creditAfterFirstSlash, "credit unchanged"); + assertEq(midnight.credit(id, lender), creditAfterFirstSlash, "credit unchanged"); assertEq(midnight.lastLossFactor(id, lender), lastLossFactorAfterFirstSlash, "last loss factor unchanged"); } @@ -893,12 +892,12 @@ contract LiquidationTest is BaseTest { Oracle(market.collateralParams[0].oracle).setPrice(0); midnight.liquidate(market, 0, 0, 0, borrower, false, address(this), address(0), ""); - assertEq(midnight.debtOf(id, borrower), 0, "debt"); + assertEq(midnight.debt(id, borrower), 0, "debt"); assertEq(midnight.totalUnits(id), 0, "total units"); uint128 _lossFactor = midnight.lossFactor(id); assertEq(_lossFactor, type(uint128).max, "loss factor"); midnight.updatePosition(market, lender); - assertEq(midnight.creditOf(id, lender), 0, "credit after slashing"); + assertEq(midnight.credit(id, lender), 0, "credit after slashing"); // withdrawCollateral still works uint256 collateral = midnight.collateral(id, borrower, 0); @@ -913,7 +912,7 @@ contract LiquidationTest is BaseTest { /// @dev Bad debt as computed in liquidate function _badDebt() internal view returns (uint256) { - uint256 badDebt = midnight.debtOf(id, borrower); + uint256 badDebt = midnight.debt(id, borrower); uint128 collateralBitmap = midnight.collateralBitmap(id, borrower); while (collateralBitmap != 0) { uint256 i = UtilsLib.msb(collateralBitmap); @@ -988,10 +987,10 @@ contract LiquidationTest is BaseTest { // Drop price so position is unhealthy. Oracle(market.collateralParams[0].oracle).setPrice(ORACLE_PRICE_SCALE / 2); - uint256 debtBefore = midnight.debtOf(id, borrower); + uint256 debtBefore = midnight.debt(id, borrower); // Non-zero seizedAssets exercises the recovery close factor path. midnight.liquidate(market, 0, 1, 0, borrower, false, address(this), address(0), ""); - assertLt(midnight.debtOf(id, borrower), debtBefore, "debt should decrease after liquidation"); + assertLt(midnight.debt(id, borrower), debtBefore, "debt should decrease after liquidation"); } function testLiquidateNoDebtReverts() public { diff --git a/test/MaxAmountsTest.sol b/test/MaxAmountsTest.sol index 50b12afc..fe1cefae 100644 --- a/test/MaxAmountsTest.sol +++ b/test/MaxAmountsTest.sol @@ -74,7 +74,7 @@ contract MaxAmountsTest is BaseTest { take(amount, lender, borrowerOffer); assertEq(midnight.totalUnits(id), amount, "total units at max"); - assertEq(midnight.debtOf(id, borrower), amount, "debt at max"); + assertEq(midnight.debt(id, borrower), amount, "debt at max"); } function testTakeAboveMaxAmountReverts() public { diff --git a/test/MidnightBundlesTest.sol b/test/MidnightBundlesTest.sol index c480c451..47f2a844 100644 --- a/test/MidnightBundlesTest.sol +++ b/test/MidnightBundlesTest.sol @@ -175,8 +175,8 @@ contract MidnightBundlesTest is BaseTest { uint256 consumed0 = midnight.consumed(offers[0].maker, offers[0].group); uint256 consumed1 = midnight.consumed(offers[1].maker, offers[1].group); assertEq(consumed0, fromOffer0, "consumed offer 0"); - assertEq(consumed0 + consumed1, midnight.debtOf(id, borrower), "total consumed"); - assertEq(midnight.debtOf(id, borrower), units, "debt"); + assertEq(consumed0 + consumed1, midnight.debt(id, borrower), "total consumed"); + assertEq(midnight.debt(id, borrower), units, "debt"); } else { vm.prank(borrower); vm.expectRevert(IMidnightBundles.OutOfOffers.selector); @@ -231,7 +231,7 @@ contract MidnightBundlesTest is BaseTest { uint256 consumed0 = midnight.consumed(offers[0].maker, offers[0].group); uint256 consumed1 = midnight.consumed(offers[1].maker, offers[1].group); assertEq(consumed0, fromOffer0, "consumed offer 0"); - assertEq(consumed0 + consumed1, midnight.debtOf(id, borrower), "total consumed"); + assertEq(consumed0 + consumed1, midnight.debt(id, borrower), "total consumed"); assertEq(loanToken.balanceOf(lender), type(uint256).max - targetBuyerAssets, "lender balance"); } else { vm.prank(lender); @@ -284,7 +284,7 @@ contract MidnightBundlesTest is BaseTest { assertEq(loanToken.allowance(lender, address(midnightBundles)), 0); assertEq(loanToken.allowance(lender, PERMIT2), 0); assertEq(loanToken.balanceOf(lender), type(uint256).max - targetBuyerAssets); - assertEq(midnight.creditOf(id, lender), units); + assertEq(midnight.credit(id, lender), units); } function testBuyBuyerAssetsTargetPermit() public { @@ -316,7 +316,7 @@ contract MidnightBundlesTest is BaseTest { assertEq(loanToken.allowance(lender, address(midnightBundles)), 0); assertEq(loanToken.balanceOf(lender), type(uint256).max - targetBuyerAssets); - assertEq(midnight.creditOf(id, lender), units); + assertEq(midnight.credit(id, lender), units); } function testBuyUnitsTargetPermit2() public { @@ -350,7 +350,7 @@ contract MidnightBundlesTest is BaseTest { assertEq(loanToken.allowance(lender, address(midnightBundles)), 0); assertEq(loanToken.allowance(lender, PERMIT2), 0); assertEq(loanToken.balanceOf(lender), type(uint256).max - maxBuyerAssets); - assertEq(midnight.creditOf(id, lender), units); + assertEq(midnight.credit(id, lender), units); } function testBuyUnitsTargetInconsistentMarket() public { @@ -468,7 +468,7 @@ contract MidnightBundlesTest is BaseTest { uint256 consumed0 = midnight.consumed(offers[0].maker, offers[0].group); uint256 consumed1 = midnight.consumed(offers[1].maker, offers[1].group); assertEq(consumed0, fromOffer0, "consumed offer 0"); - assertEq(consumed0 + consumed1, midnight.debtOf(id, borrower), "total consumed"); + assertEq(consumed0 + consumed1, midnight.debt(id, borrower), "total consumed"); assertEq(loanToken.balanceOf(borrower), targetSellerAssets, "borrower balance"); } else { vm.prank(borrower); @@ -543,7 +543,7 @@ contract MidnightBundlesTest is BaseTest { referrer ); - assertEq(midnight.debtOf(id, borrower), units, "units filled"); + assertEq(midnight.debt(id, borrower), units, "units filled"); assertEq(loanToken.balanceOf(borrower), expectedFilledBuyerAssets, "maker receipt"); assertEq(loanToken.balanceOf(referrer), expectedFee, "referrer fee"); assertEq( @@ -577,7 +577,7 @@ contract MidnightBundlesTest is BaseTest { units, 0, borrower, receiver, new CollateralSupply[](0), takes, referralFeePct, referrer ); - assertEq(midnight.debtOf(id, borrower), units, "units sold"); + assertEq(midnight.debt(id, borrower), units, "units sold"); assertEq(loanToken.balanceOf(receiver), expectedFilledSellerAssets - expectedFee, "receiver net"); assertEq(loanToken.balanceOf(referrer), expectedFee, "referrer fee"); assertEq(loanToken.balanceOf(address(midnightBundles)), 0, "bundler residual"); @@ -705,7 +705,7 @@ contract MidnightBundlesTest is BaseTest { market, assets, borrower, _noPermit(), new CollateralWithdrawal[](0), address(0), referralFeePct, referrer ); - assertEq(midnight.debtOf(id, borrower), units - expectedUnits, "debt"); + assertEq(midnight.debt(id, borrower), units - expectedUnits, "debt"); assertEq(loanToken.balanceOf(referrer), expectedFee, "referrer fee"); assertEq(loanToken.balanceOf(borrower), 0, "borrower spent assets"); assertEq(loanToken.balanceOf(address(midnightBundles)), 0, "bundler residual"); @@ -742,7 +742,7 @@ contract MidnightBundlesTest is BaseTest { market, assets, borrower, _noPermit(), new CollateralWithdrawal[](0), address(0), referralFeePct, referrer ); - assertEq(midnight.debtOf(id, borrower), 0, "debt fully repaid"); + assertEq(midnight.debt(id, borrower), 0, "debt fully repaid"); assertEq(loanToken.balanceOf(referrer), expectedFee, "referrer fee"); assertEq(loanToken.balanceOf(borrower), 0, "borrower spent assets"); assertEq(loanToken.balanceOf(address(midnightBundles)), 0, "bundler residual"); @@ -910,7 +910,7 @@ contract MidnightBundlesTest is BaseTest { for (uint256 i; i < numCollaterals; i++) { assertEq(midnight.collateral(id, borrower, i), supplies[i].assets); } - assertEq(midnight.debtOf(id, borrower), units); + assertEq(midnight.debt(id, borrower), units); } function testSellUnitsTargetPermit2() public { @@ -943,7 +943,7 @@ contract MidnightBundlesTest is BaseTest { assertEq(ERC20(collateralToken).allowance(borrower, address(midnightBundles)), 0); assertEq(ERC20(collateralToken).allowance(borrower, PERMIT2), 0); assertEq(midnight.collateral(id, borrower, 0), amount); - assertEq(midnight.debtOf(id, borrower), units); + assertEq(midnight.debt(id, borrower), units); } function testRepay(uint256 units, uint256 repayUnits, uint256 withdrawAssets) public { @@ -985,7 +985,7 @@ contract MidnightBundlesTest is BaseTest { market, repayUnits, borrower, _noPermit(), withdrawals, collateralReceiver, 0, address(0) ); - assertEq(midnight.debtOf(id, borrower), units - repayUnits, "debt"); + assertEq(midnight.debt(id, borrower), units - repayUnits, "debt"); assertEq(midnight.collateral(id, borrower, 0), collateralAmount - withdrawAssets, "remaining collateral"); assertEq( ERC20(market.collateralParams[0].token).balanceOf(collateralReceiver), withdrawAssets, "collateral receiver" @@ -1204,7 +1204,7 @@ contract MidnightBundlesTest is BaseTest { assertEq(midnight.consumed(offers[0].maker, offers[0].group), 100, "consumed offer 0"); assertEq(midnight.consumed(offers[1].maker, offers[1].group), 30, "consumed offer 1"); - assertEq(midnight.debtOf(id, borrower), 100, "debt"); + assertEq(midnight.debt(id, borrower), 100, "debt"); } function testSellSellerAssetsTargetPartiallyConsumed() public { @@ -1238,7 +1238,7 @@ contract MidnightBundlesTest is BaseTest { // Offer 0 should hit its cap (consumed 30 + filled up to 70). assertEq(consumed0, 100, "consumed offer 0"); // Total newly filled units equal the borrower's debt. - assertEq(consumed0 - 30 + consumed1, midnight.debtOf(id, borrower), "total consumed"); + assertEq(consumed0 - 30 + consumed1, midnight.debt(id, borrower), "total consumed"); assertEq(loanToken.balanceOf(borrower), targetSellerAssets, "borrower balance"); } @@ -1277,7 +1277,7 @@ contract MidnightBundlesTest is BaseTest { assertEq(midnight.consumed(offers[0].maker, offers[0].group), 100, "consumed offer 0"); assertEq(midnight.consumed(offers[1].maker, offers[1].group), 30, "consumed offer 1"); - assertEq(midnight.debtOf(id, borrower), 100, "debt"); + assertEq(midnight.debt(id, borrower), 100, "debt"); } function testBuyBuyerAssetsTargetPartiallyConsumed() public { @@ -1316,6 +1316,6 @@ contract MidnightBundlesTest is BaseTest { uint256 consumed0 = midnight.consumed(offers[0].maker, offers[0].group); uint256 consumed1 = midnight.consumed(offers[1].maker, offers[1].group); assertEq(consumed0, 100, "consumed offer 0"); - assertEq(consumed0 - 30 + consumed1, midnight.debtOf(id, borrower), "total consumed"); + assertEq(consumed0 - 30 + consumed1, midnight.debt(id, borrower), "total consumed"); } } diff --git a/test/OtherFunctionsTest.sol b/test/OtherFunctionsTest.sol index 03660e36..08827607 100644 --- a/test/OtherFunctionsTest.sol +++ b/test/OtherFunctionsTest.sol @@ -135,7 +135,7 @@ contract OtherFunctionsTest is BaseTest { vm.prank(borrower); midnight.repay(market, repaid, borrower, address(0), hex""); - assertEq(midnight.debtOf(id, borrower), units - repaid); + assertEq(midnight.debt(id, borrower), units - repaid); assertEq(midnight.withdrawable(id), repaid); assertEq(loanToken.balanceOf(address(midnight)), repaid); assertEq(loanToken.balanceOf(borrower), 0); @@ -158,7 +158,7 @@ contract OtherFunctionsTest is BaseTest { vm.prank(caller); midnight.repay(market, repaid, borrower, address(callback), data); - assertEq(midnight.debtOf(id, borrower), units - repaid); + assertEq(midnight.debt(id, borrower), units - repaid); assertEq(callback.recordedId(), id, "id"); assertEq(toId(callback.recordedMarket()), id, "market"); assertEq(callback.recordedOnBehalf(), borrower, "onBehalf"); @@ -174,7 +174,7 @@ contract OtherFunctionsTest is BaseTest { vm.prank(lender); midnight.withdraw(market, withdraw, lender, lender); - assertEq(midnight.creditOf(id, lender), units - withdraw, "creditOf"); + assertEq(midnight.credit(id, lender), units - withdraw, "credit"); assertEq(midnight.withdrawable(id), 0, "withdrawable"); assertEq(midnight.totalUnits(id), units - withdraw, "totalUnits"); assertEq(loanToken.balanceOf(address(midnight)), 0, "balance of midnight"); diff --git a/test/TakeTest.sol b/test/TakeTest.sol index e8c820b0..3d9abbc4 100644 --- a/test/TakeTest.sol +++ b/test/TakeTest.sol @@ -224,8 +224,8 @@ contract TakeTest is BaseTest { take(units, lender, borrowerOffer); - assertEq(midnight.creditOf(id, lender), units, "lender units"); - assertEq(midnight.debtOf(id, borrower), units, "borrower debt"); + assertEq(midnight.credit(id, lender), units, "lender units"); + assertEq(midnight.debt(id, borrower), units, "borrower debt"); assertEq(midnight.totalUnits(id), units, "total units"); assertEq(loanToken.balanceOf(borrower), expectedAssets, "borrower balance"); assertEq(loanToken.balanceOf(lender), 0, "lender balance"); @@ -244,8 +244,8 @@ contract TakeTest is BaseTest { take(units, borrower, lenderOffer); - assertEq(midnight.creditOf(id, lender), units, "lender units"); - assertEq(midnight.debtOf(id, borrower), units, "borrower debt"); + assertEq(midnight.credit(id, lender), units, "lender units"); + assertEq(midnight.debt(id, borrower), units, "borrower debt"); assertEq(midnight.totalUnits(id), units, "total units"); assertEq(loanToken.balanceOf(borrower), expectedAssets, "borrower balance"); assertEq(loanToken.balanceOf(lender), 0, "lender balance"); @@ -262,7 +262,7 @@ contract TakeTest is BaseTest { uint256 buyerAssets = units.mulDivDown(price, WAD); otherLenderUnits = bound(otherLenderUnits, units, max(units, maxAssets)); setupOtherUsers(market, otherLenderUnits); - uint256 actualOtherLenderCredit = midnight.creditOf(id, otherLender); + uint256 actualOtherLenderCredit = midnight.credit(id, otherLender); deal(address(loanToken), lender, buyerAssets + 1); otherLenderOffer.buy = false; otherLenderOffer.maxUnits = type(uint256).max; @@ -271,10 +271,10 @@ contract TakeTest is BaseTest { take(units, lender, otherLenderOffer); - assertEq(midnight.creditOf(id, lender), units, "lender units"); - assertEq(midnight.debtOf(id, lender), 0, "lender debt"); - assertEq(midnight.creditOf(id, otherLender), actualOtherLenderCredit - units, "other lender units"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, lender), units, "lender units"); + assertEq(midnight.debt(id, lender), 0, "lender debt"); + assertEq(midnight.credit(id, otherLender), actualOtherLenderCredit - units, "other lender units"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } @@ -286,7 +286,7 @@ contract TakeTest is BaseTest { uint256 buyerAssets = units.mulDivDown(price, WAD); otherLenderUnits = bound(otherLenderUnits, units, max(units, maxAssets)); setupOtherUsers(market, otherLenderUnits); - uint256 actualOtherLenderCredit = midnight.creditOf(id, otherLender); + uint256 actualOtherLenderCredit = midnight.credit(id, otherLender); deal(address(loanToken), lender, buyerAssets + 1); lenderOffer.maxUnits = type(uint256).max; lenderOffer.tick = tick; @@ -294,10 +294,10 @@ contract TakeTest is BaseTest { take(units, otherLender, lenderOffer); - assertEq(midnight.creditOf(id, lender), units, "lender units"); - assertEq(midnight.debtOf(id, lender), 0, "lender debt"); - assertEq(midnight.creditOf(id, otherLender), actualOtherLenderCredit - units, "other lender units"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, lender), units, "lender units"); + assertEq(midnight.debt(id, lender), 0, "lender debt"); + assertEq(midnight.credit(id, otherLender), actualOtherLenderCredit - units, "other lender units"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } @@ -306,7 +306,7 @@ contract TakeTest is BaseTest { otherLenderUnits = bound(otherLenderUnits, 1, maxAssets - 1); units = bound(units, otherLenderUnits + 1, maxAssets); setupOtherUsers(market, otherLenderUnits); - uint256 otherLenderCredit = midnight.creditOf(id, otherLender); + uint256 otherLenderCredit = midnight.credit(id, otherLender); uint256 price = TickLib.tickToPrice(MAX_TICK); deal(address(loanToken), lender, units.mulDivUp(price, WAD)); collateralize(market, otherLender, units); @@ -316,9 +316,9 @@ contract TakeTest is BaseTest { take(units, lender, otherLenderOffer); // otherLender crossed from lender to borrower. - assertEq(midnight.creditOf(id, otherLender), 0, "otherLender credit"); - assertEq(midnight.debtOf(id, otherLender), units - otherLenderCredit, "otherLender debt"); - assertEq(midnight.creditOf(id, lender), units, "lender credit"); + assertEq(midnight.credit(id, otherLender), 0, "otherLender credit"); + assertEq(midnight.debt(id, otherLender), units - otherLenderCredit, "otherLender debt"); + assertEq(midnight.credit(id, lender), units, "lender credit"); assertEq(midnight.totalUnits(id), totalUnitsBefore + units - otherLenderCredit, "total units"); } @@ -329,7 +329,7 @@ contract TakeTest is BaseTest { tick = bound(tick, 0, MAX_TICK); existingUnits = bound(existingUnits, units, max(units, maxAssets)); setupOtherUsers(market, existingUnits); - uint256 otherBorrowerDebt = midnight.debtOf(id, otherBorrower); + uint256 otherBorrowerDebt = midnight.debt(id, otherBorrower); collateralize(market, borrower, units); borrowerOffer.maxUnits = type(uint256).max; borrowerOffer.tick = tick; @@ -339,8 +339,8 @@ contract TakeTest is BaseTest { take(units, otherBorrower, borrowerOffer); - assertEq(midnight.debtOf(id, borrower), units, "borrower debt"); - assertEq(midnight.debtOf(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); + assertEq(midnight.debt(id, borrower), units, "borrower debt"); + assertEq(midnight.debt(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } @@ -349,7 +349,7 @@ contract TakeTest is BaseTest { tick = bound(tick, 0, MAX_TICK); existingUnits = bound(existingUnits, units, max(units, maxAssets)); setupOtherUsers(market, existingUnits); - uint256 otherBorrowerDebt = midnight.debtOf(id, otherBorrower); + uint256 otherBorrowerDebt = midnight.debt(id, otherBorrower); collateralize(market, borrower, units); otherBorrowerOffer.maxUnits = type(uint256).max; otherBorrowerOffer.tick = tick; @@ -357,8 +357,8 @@ contract TakeTest is BaseTest { take(units, borrower, otherBorrowerOffer); - assertEq(midnight.debtOf(id, borrower), units, "borrower debt"); - assertEq(midnight.debtOf(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); + assertEq(midnight.debt(id, borrower), units, "borrower debt"); + assertEq(midnight.debt(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } @@ -367,7 +367,7 @@ contract TakeTest is BaseTest { otherUnits = bound(otherUnits, 1, maxAssets - 1); units = bound(units, otherUnits + 1, maxAssets); setupOtherUsers(market, otherUnits); - uint256 otherBorrowerDebt = midnight.debtOf(id, otherBorrower); + uint256 otherBorrowerDebt = midnight.debt(id, otherBorrower); uint256 price = TickLib.tickToPrice(MAX_TICK); deal(address(loanToken), otherBorrower, units.mulDivUp(price, WAD)); collateralize(market, borrower, units); @@ -377,9 +377,9 @@ contract TakeTest is BaseTest { take(units, otherBorrower, borrowerOffer); // otherBorrower crossed from borrower to lender. - assertEq(midnight.debtOf(id, otherBorrower), 0, "otherBorrower debt"); - assertEq(midnight.creditOf(id, otherBorrower), units - otherBorrowerDebt, "otherBorrower credit"); - assertEq(midnight.debtOf(id, borrower), units, "borrower debt"); + assertEq(midnight.debt(id, otherBorrower), 0, "otherBorrower debt"); + assertEq(midnight.credit(id, otherBorrower), units - otherBorrowerDebt, "otherBorrower credit"); + assertEq(midnight.debt(id, borrower), units, "borrower debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore + units - otherBorrowerDebt, "total units"); } @@ -393,8 +393,8 @@ contract TakeTest is BaseTest { uint256 buyerAssets = units.mulDivUp(price, WAD); existingUnits = bound(existingUnits, units, max(units, maxAssets)); setupOtherUsers(market, existingUnits); - uint256 otherLenderCredit = midnight.creditOf(id, otherLender); - uint256 otherBorrowerDebt = midnight.debtOf(id, otherBorrower); + uint256 otherLenderCredit = midnight.credit(id, otherLender); + uint256 otherBorrowerDebt = midnight.debt(id, otherBorrower); otherLenderOffer.maxUnits = type(uint256).max; otherLenderOffer.tick = tick; @@ -402,8 +402,8 @@ contract TakeTest is BaseTest { take(units, otherBorrower, otherLenderOffer); - assertEq(midnight.creditOf(id, otherLender), otherLenderCredit - units, "otherLender units"); - assertEq(midnight.debtOf(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); + assertEq(midnight.credit(id, otherLender), otherLenderCredit - units, "otherLender units"); + assertEq(midnight.debt(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); assertEq(midnight.totalUnits(id), otherBorrowerDebt - units, "total units"); assertEq(loanToken.balanceOf(otherLender), buyerAssets, "otherLender balance"); } @@ -416,16 +416,16 @@ contract TakeTest is BaseTest { uint256 buyerAssets = units.mulDivDown(price, WAD); existingUnits = bound(existingUnits, units, max(units, maxAssets)); setupOtherUsers(market, existingUnits); - uint256 otherLenderCredit = midnight.creditOf(id, otherLender); - uint256 otherBorrowerDebt = midnight.debtOf(id, otherBorrower); + uint256 otherLenderCredit = midnight.credit(id, otherLender); + uint256 otherBorrowerDebt = midnight.debt(id, otherBorrower); otherBorrowerOffer.maxUnits = type(uint256).max; otherBorrowerOffer.tick = tick; take(units, otherLender, otherBorrowerOffer); - assertEq(midnight.creditOf(id, otherLender), otherLenderCredit - units, "otherLender units"); - assertEq(midnight.debtOf(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); + assertEq(midnight.credit(id, otherLender), otherLenderCredit - units, "otherLender units"); + assertEq(midnight.debt(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); assertEq(midnight.totalUnits(id), otherBorrowerDebt - units, "total units"); assertEq(loanToken.balanceOf(otherLender), buyerAssets, "otherLender balance"); } @@ -459,8 +459,8 @@ contract TakeTest is BaseTest { function testBuy2PostMaturity() public { uint256 units = 100; setupOtherUsers(market, units); - assertEq(midnight.creditOf(id, otherLender), units, "other lender credit"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, otherLender), units, "other lender credit"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertTrue(midnight.isHealthy(market, id, otherLender), "other lender healthy"); uint256 totalUnitsBefore = midnight.totalUnits(id); @@ -472,18 +472,18 @@ contract TakeTest is BaseTest { take(units, lender, otherLenderOffer); - assertEq(midnight.creditOf(id, lender), units, "lender units"); - assertEq(midnight.debtOf(id, lender), 0, "lender debt"); - assertEq(midnight.creditOf(id, otherLender), 0, "other lender units"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, lender), units, "lender units"); + assertEq(midnight.debt(id, lender), 0, "lender debt"); + assertEq(midnight.credit(id, otherLender), 0, "other lender units"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } function testSell2PostMaturity() public { uint256 units = 100; setupOtherUsers(market, units); - assertEq(midnight.creditOf(id, otherLender), units, "other lender credit"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, otherLender), units, "other lender credit"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertTrue(midnight.isHealthy(market, id, otherLender), "other lender healthy"); uint256 totalUnitsBefore = midnight.totalUnits(id); @@ -495,10 +495,10 @@ contract TakeTest is BaseTest { take(units, otherLender, lenderOffer); - assertEq(midnight.creditOf(id, lender), units, "lender units"); - assertEq(midnight.debtOf(id, lender), 0, "lender debt"); - assertEq(midnight.creditOf(id, otherLender), 0, "other lender units"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, lender), units, "lender units"); + assertEq(midnight.debt(id, lender), 0, "lender debt"); + assertEq(midnight.credit(id, otherLender), 0, "other lender units"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } @@ -535,10 +535,10 @@ contract TakeTest is BaseTest { function testBuy4PostMaturity() public { uint256 units = 100; setupOtherUsers(market, units); - assertEq(midnight.creditOf(id, otherLender), units, "other lender credit"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, otherLender), units, "other lender credit"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertTrue(midnight.isHealthy(market, id, otherLender), "other lender healthy"); - uint256 otherBorrowerDebt = midnight.debtOf(id, otherBorrower); + uint256 otherBorrowerDebt = midnight.debt(id, otherBorrower); uint256 timestamp = market.maturity + 1; vm.warp(timestamp); @@ -548,18 +548,18 @@ contract TakeTest is BaseTest { take(units, otherBorrower, otherLenderOffer); - assertEq(midnight.creditOf(id, otherLender), 0, "otherLender units"); - assertEq(midnight.debtOf(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); + assertEq(midnight.credit(id, otherLender), 0, "otherLender units"); + assertEq(midnight.debt(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); assertEq(midnight.totalUnits(id), otherBorrowerDebt - units, "total units"); } function testSell4PostMaturity() public { uint256 units = 100; setupOtherUsers(market, units); - assertEq(midnight.creditOf(id, otherLender), units, "other lender credit"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, otherLender), units, "other lender credit"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertTrue(midnight.isHealthy(market, id, otherLender), "other lender healthy"); - uint256 otherBorrowerDebt = midnight.debtOf(id, otherBorrower); + uint256 otherBorrowerDebt = midnight.debt(id, otherBorrower); uint256 timestamp = market.maturity + 1; vm.warp(timestamp); @@ -569,8 +569,8 @@ contract TakeTest is BaseTest { take(units, otherLender, otherBorrowerOffer); - assertEq(midnight.creditOf(id, otherLender), 0, "otherLender units"); - assertEq(midnight.debtOf(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); + assertEq(midnight.credit(id, otherLender), 0, "otherLender units"); + assertEq(midnight.debt(id, otherBorrower), otherBorrowerDebt - units, "otherBorrower debt"); assertEq(midnight.totalUnits(id), otherBorrowerDebt - units, "total units"); } @@ -588,14 +588,14 @@ contract TakeTest is BaseTest { deal(address(loanToken), otherBorrower, exitUnits.mulDivUp(price, WAD)); collateralize(market, borrower, exitUnits); - uint256 debtBefore = midnight.debtOf(id, otherBorrower); + uint256 debtBefore = midnight.debt(id, otherBorrower); uint256 totalUnitsBefore = midnight.totalUnits(id); take(exitUnits, borrower, otherBorrowerOffer); - assertEq(midnight.debtOf(id, borrower), exitUnits, "borrower debt"); - assertEq(midnight.creditOf(id, otherBorrower), 0, "otherBorrower units"); - assertEq(midnight.debtOf(id, otherBorrower), debtBefore - exitUnits, "otherBorrower debt"); + assertEq(midnight.debt(id, borrower), exitUnits, "borrower debt"); + assertEq(midnight.credit(id, otherBorrower), 0, "otherBorrower units"); + assertEq(midnight.debt(id, otherBorrower), debtBefore - exitUnits, "otherBorrower debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } @@ -622,15 +622,15 @@ contract TakeTest is BaseTest { uint256 price = TickLib.tickToPrice(MAX_TICK); deal(address(loanToken), lender, exitUnits.mulDivUp(price, WAD)); - uint256 creditBefore = midnight.creditOf(id, otherLender); + uint256 creditBefore = midnight.credit(id, otherLender); uint256 totalUnitsBefore = midnight.totalUnits(id); take(exitUnits, lender, otherLenderOffer); - assertEq(midnight.creditOf(id, lender), exitUnits, "lender units"); - assertEq(midnight.debtOf(id, lender), 0, "lender debt"); - assertEq(midnight.creditOf(id, otherLender), creditBefore - exitUnits, "other lender units"); - assertEq(midnight.debtOf(id, otherLender), 0, "other lender debt"); + assertEq(midnight.credit(id, lender), exitUnits, "lender units"); + assertEq(midnight.debt(id, lender), 0, "lender debt"); + assertEq(midnight.credit(id, otherLender), creditBefore - exitUnits, "other lender units"); + assertEq(midnight.debt(id, otherLender), 0, "other lender debt"); assertEq(midnight.totalUnits(id), totalUnitsBefore, "total units"); } @@ -752,8 +752,8 @@ contract TakeTest is BaseTest { take(units, address(this), borrowerOffer); take(units, address(this), lenderOffer); - assertEq(midnight.creditOf(id, address(this)), 0, "credit"); - assertEq(midnight.debtOf(id, address(this)), 0, "debt"); + assertEq(midnight.credit(id, address(this)), 0, "credit"); + assertEq(midnight.debt(id, address(this)), 0, "debt"); } // address(this) makes an arbitrage for 2 crossed offers. @@ -779,8 +779,8 @@ contract TakeTest is BaseTest { take(units, address(this), lenderOffer); take(units, address(this), borrowerOffer); - assertEq(midnight.creditOf(id, address(this)), 0, "credit"); - assertEq(midnight.debtOf(id, address(this)), 0, "debt"); + assertEq(midnight.credit(id, address(this)), 0, "credit"); + assertEq(midnight.debt(id, address(this)), 0, "debt"); } function testBuyPastMaturity(uint256 timestamp) public { @@ -1036,8 +1036,8 @@ contract TakeTest is BaseTest { vm.prank(lender); midnight.setConsumed(lenderOffer.group, lenderOffer.maxAssets, lender); - uint256 lenderCreditBefore = midnight.creditOf(id, lender); - uint256 borrowerDebtBefore = midnight.debtOf(id, borrower); + uint256 lenderCreditBefore = midnight.credit(id, lender); + uint256 borrowerDebtBefore = midnight.debt(id, borrower); uint256 totalUnitsBefore = midnight.totalUnits(id); uint256 lenderBalBefore = loanToken.balanceOf(lender); uint256 borrowerBalBefore = loanToken.balanceOf(borrower); @@ -1052,8 +1052,8 @@ contract TakeTest is BaseTest { assertEq(loanToken.balanceOf(lender), lenderBalBefore); assertEq(loanToken.balanceOf(borrower), borrowerBalBefore); // But position state strictly changed: - assertGt(midnight.creditOf(id, lender), lenderCreditBefore); - assertGt(midnight.debtOf(id, borrower), borrowerDebtBefore); + assertGt(midnight.credit(id, lender), lenderCreditBefore); + assertGt(midnight.debt(id, borrower), borrowerDebtBefore); assertGt(midnight.totalUnits(id), totalUnitsBefore); } @@ -1286,7 +1286,7 @@ contract TakeTest is BaseTest { assertFalse(callback.liquidateSucceeded()); assertEq(callback.liquidateErrorSelector(), IMidnight.NotLiquidatable.selector); - assertEq(midnight.debtOf(id, borrower), units); + assertEq(midnight.debt(id, borrower), units); assertEq(midnight.collateral(id, borrower, 0), collateral); } @@ -1319,7 +1319,7 @@ contract TakeTest is BaseTest { assertFalse(callback.liquidateSucceeded()); assertEq(callback.liquidateErrorSelector(), IMidnight.NotLiquidatable.selector); assertTrue(midnight.liquidationLocked(id, borrower) == false); - assertEq(midnight.debtOf(id, borrower), 2 * units); + assertEq(midnight.debt(id, borrower), 2 * units); assertEq(midnight.collateral(id, borrower, 0), 2 * collateral); } @@ -1411,8 +1411,8 @@ contract TakeTest is BaseTest { (uint256 buyerAssets, uint256 sellerAssets) = take(units, lender, borrowerOffer); assertEq(buyerAssets, 0, "buyerAssets"); assertEq(sellerAssets, 0, "sellerAssets"); - assertEq(midnight.creditOf(id, lender), units, "creditOf"); - assertEq(midnight.debtOf(id, borrower), units, "debtOf"); + assertEq(midnight.credit(id, lender), units, "credit"); + assertEq(midnight.debt(id, borrower), units, "debt"); } // fee>0, buy, units @@ -1441,8 +1441,8 @@ contract TakeTest is BaseTest { (uint256 buyerAssets, uint256 sellerAssets) = take(units, lender, borrowerOffer); assertEq(buyerAssets, expectedBuyerAssets, "buyerAssets"); assertEq(sellerAssets, 0, "sellerAssets"); - assertEq(midnight.creditOf(id, lender), units, "creditOf"); - assertEq(midnight.debtOf(id, borrower), units, "debtOf"); + assertEq(midnight.credit(id, lender), units, "credit"); + assertEq(midnight.debt(id, borrower), units, "debt"); } function testTakeWithAddressZero(uint256 units) public { diff --git a/test/TickGatingTest.sol b/test/TickGatingTest.sol index b013c724..015d1405 100644 --- a/test/TickGatingTest.sol +++ b/test/TickGatingTest.sol @@ -71,7 +71,7 @@ contract TickGatingTest is BaseTest { deal(address(loanToken), lender, units.mulDivUp(price, WAD)); collateralize(market, borrower, units); take(units, borrower, offer); - assertEq(midnight.creditOf(id, lender), units); + assertEq(midnight.credit(id, lender), units); } function testTakeRevertsAtInaccessibleTick() public { @@ -122,7 +122,7 @@ contract TickGatingTest is BaseTest { // Now should succeed. take(units, borrower, offer); - assertEq(midnight.creditOf(id, lender), units); + assertEq(midnight.credit(id, lender), units); } // --- setMarketTickSpacing governance --- @@ -183,6 +183,6 @@ contract TickGatingTest is BaseTest { collateralize(market, borrower, units); take(units, borrower, offer2); - assertEq(midnight.creditOf(id, lender), 2 * units); + assertEq(midnight.credit(id, lender), 2 * units); } } From 0336d529f12a5d15f990f7d0af4ecd672d864e58 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 22 Jun 2026 13:29:35 +0200 Subject: [PATCH 07/10] rename test file --- ...tIsAuthorizedWithSigTest.sol => EcrecoverAuthorizerTest.sol} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename test/{SetIsAuthorizedWithSigTest.sol => EcrecoverAuthorizerTest.sol} (99%) diff --git a/test/SetIsAuthorizedWithSigTest.sol b/test/EcrecoverAuthorizerTest.sol similarity index 99% rename from test/SetIsAuthorizedWithSigTest.sol rename to test/EcrecoverAuthorizerTest.sol index 0d5a24b0..fd68da74 100644 --- a/test/SetIsAuthorizedWithSigTest.sol +++ b/test/EcrecoverAuthorizerTest.sol @@ -15,7 +15,7 @@ bytes constant AUTHORIZATION_TYPE = "Authorization(address authorizer,address authorized,bool isAuthorized,uint256 nonce,uint256 deadline)"; bytes constant EIP712_DOMAIN_TYPE = "EIP712Domain(uint256 chainId,address verifyingContract)"; -contract SetIsAuthorizedWithSigTest is BaseTest { +contract EcrecoverAuthorizerTest is BaseTest { function testAuthorizationTypeHash() public pure { assertEq(AUTHORIZATION_TYPEHASH, keccak256(AUTHORIZATION_TYPE)); } From ac3480da92764069514a0dd762582deb8b3c6427 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 22 Jun 2026 11:59:22 +0000 Subject: [PATCH 08/10] refactor: return storage structs from getters Rename the backing storage mappings to _position and _marketState, then add explicit getters returning Position and MarketState structs. --- certora/helpers/MidnightWrapper.sol | 6 +- certora/specs/BalanceEffects.spec | 10 +- certora/specs/CollateralBitmap.spec | 4 +- certora/specs/LiquidationBoundedByLIF.spec | 2 +- certora/specs/LossFactor.spec | 40 +-- certora/specs/Midnight.spec | 12 +- certora/specs/NoDebtWithoutCollateral.spec | 4 +- certora/specs/NoDivisionByZero.spec | 6 +- certora/specs/NotCreatedMarket.spec | 10 +- certora/specs/Role.spec | 6 +- certora/specs/SettlementFeeBoundaries.spec | 2 +- certora/specs/Solvency.spec | 8 +- certora/specs/SplitPreservesAccounting.spec | 4 +- certora/specs/UpdateBeforeCredit.spec | 6 +- src/Midnight.sol | 280 ++++++++++---------- src/interfaces/IMidnight.sol | 4 +- test/OtherFunctionsTest.sol | 76 +++--- 17 files changed, 249 insertions(+), 231 deletions(-) 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 05f71ad0..37743e79 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, "setup the call"; updatePosition@withrevert(e, market, user); @@ -92,15 +92,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; @@ -116,8 +116,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), @@ -125,7 +125,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"; @@ -150,11 +150,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; } @@ -168,9 +168,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 43b09175..e332ab9d 100644 --- a/certora/specs/Role.spec +++ b/certora/specs/Role.spec @@ -30,7 +30,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()); @@ -254,7 +254,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]; @@ -264,7 +264,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 829fc188..037c4f1c 100644 --- a/certora/specs/SplitPreservesAccounting.spec +++ b/certora/specs/SplitPreservesAccounting.spec @@ -78,7 +78,7 @@ rule splitPreservesAccounting(env e, uint256 unitsA, uint256 unitsB, uint256 uni 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); @@ -98,5 +98,5 @@ rule splitPreservesAccounting(env e, uint256 unitsA, uint256 unitsB, uint256 uni 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/src/Midnight.sol b/src/Midnight.sol index 6e551b30..11114f11 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; @@ -258,29 +258,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); } @@ -295,12 +295,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); } @@ -321,13 +321,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); @@ -355,11 +355,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()); @@ -388,8 +388,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); @@ -398,7 +398,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; @@ -427,8 +427,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; @@ -497,18 +496,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); @@ -521,8 +520,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); @@ -544,13 +543,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() ); @@ -573,12 +572,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()); @@ -606,10 +605,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() @@ -617,15 +616,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) @@ -640,18 +639,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; } @@ -673,23 +672,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; @@ -705,8 +705,8 @@ contract Midnight is IMidnight { receiver, payer, badDebt, - _marketState.lossFactor, - _marketState.continuousFeeCredit + state.lossFactor, + state.continuousFeeCredit ); SafeTransferLib.safeTransfer(market.collateralParams[collateralIndex].token, receiver, seizedAssets); @@ -770,7 +770,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()); @@ -788,17 +788,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); @@ -815,17 +815,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)) @@ -838,7 +838,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); } @@ -849,17 +849,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); @@ -867,37 +867,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) { @@ -907,47 +915,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) { @@ -958,16 +966,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); } @@ -977,19 +985,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 faf0a370..a70b2eb0 100644 --- a/src/interfaces/IMidnight.sol +++ b/src/interfaces/IMidnight.sol @@ -120,8 +120,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 { From da33e3653ac386d021abfede01963f4da4870b64 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 22 Jun 2026 14:22:22 +0000 Subject: [PATCH 09/10] chore: lower optimizer runs for contract size Lower optimizer_runs from 800 to the round value 700 so Midnight stays below the EIP-170 runtime size limit. --- foundry.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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" }] From a4353f3afddcdc7f15b929f2ff9652edd189c038 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Tue, 23 Jun 2026 13:51:48 +0200 Subject: [PATCH 10/10] fix timeout & optim certora --- certora/confs/BundlerRepayInvertibility.conf | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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" }