From a929033ea9f43232522d42d9b662e92ce5f2723c Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 3 Jun 2026 16:04:03 +0200 Subject: [PATCH 1/3] more return values --- certora/specs/BalanceEffects.spec | 20 ++++++++++--- certora/specs/Midnight.spec | 8 ++++-- certora/specs/SettlementFeeSpread.spec | 4 +-- certora/specs/WithdrawableMonotonicity.spec | 2 +- src/Midnight.sol | 21 +++++++++++--- src/interfaces/IMidnight.sol | 4 +-- src/periphery/MidnightBundles.sol | 8 +++--- test/BaseTest.sol | 4 ++- test/ContinuousFeeTest.sol | 24 ++++++++++++++-- test/LiquidationTest.sol | 31 +++++++++++++++++++++ 10 files changed, 104 insertions(+), 22 deletions(-) diff --git a/certora/specs/BalanceEffects.spec b/certora/specs/BalanceEffects.spec index 4fc950791..2b050d0e6 100644 --- a/certora/specs/BalanceEffects.spec +++ b/certora/specs/BalanceEffects.spec @@ -115,15 +115,21 @@ rule takeBuyerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 u address buyer = offer.buy ? offer.maker : taker; uint256 buyerDebtBefore = debtOf(id, buyer); uint128 buyerUpdatedCreditBefore; - buyerUpdatedCreditBefore, _, _ = updatePositionView(e, offer.market, id, buyer); + uint128 buyerUpdatedPendingFeeBefore; + buyerUpdatedCreditBefore, buyerUpdatedPendingFeeBefore, _ = updatePositionView(e, offer.market, id, buyer); - take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + uint256 buyerCreditIncrease; + uint256 buyerPendingFeeIncrease; + _, _, buyerCreditIncrease, buyerPendingFeeIncrease, _, _ = 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 creditOf(id, buyer) == buyerUpdatedCreditBefore + buyerCreditIncrease; + assert pendingFee(id, buyer) == buyerUpdatedPendingFeeBefore + buyerPendingFeeIncrease; + assert debtOf(id, buyer) + units == buyerDebtBefore + buyerCreditIncrease; } /// 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,15 +141,21 @@ rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 address seller = offer.buy ? taker : offer.maker; uint256 sellerDebtBefore = debtOf(id, seller); uint128 sellerUpdatedCreditBefore; - sellerUpdatedCreditBefore, _, _ = updatePositionView(e, offer.market, id, seller); + uint128 sellerUpdatedPendingFeeBefore; + sellerUpdatedCreditBefore, sellerUpdatedPendingFeeBefore, _ = updatePositionView(e, offer.market, id, seller); - take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + uint256 sellerCreditDecrease; + uint256 sellerPendingFeeDecrease; + _, _, _, _, sellerCreditDecrease, sellerPendingFeeDecrease = 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 creditOf(id, seller) + sellerCreditDecrease == sellerUpdatedCreditBefore; + assert pendingFee(id, seller) + sellerPendingFeeDecrease == sellerUpdatedPendingFeeBefore; + assert debtOf(id, seller) == sellerDebtBefore + units - sellerCreditDecrease; } /// REPAY /// diff --git a/certora/specs/Midnight.spec b/certora/specs/Midnight.spec index b908ee0da..c53a17b1d 100644 --- a/certora/specs/Midnight.spec +++ b/certora/specs/Midnight.spec @@ -63,13 +63,17 @@ function summaryMulDiv(uint256 x, uint256 y, uint256 d) returns uint256 { rule takeInputOutputConsistency(env e, Midnight.Offer offer, bytes ratifierData, uint256 unitsInput, address taker, address receiver, address takerCallbackAddress, bytes takerCallbackData) { uint256 buyerAssetsOutput; uint256 sellerAssetsOutput; + uint256 buyerCreditIncreaseOutput; + uint256 buyerPendingFeeIncreaseOutput; + uint256 sellerCreditDecreaseOutput; + uint256 sellerPendingFeeDecreaseOutput; uint256 claimableBefore = claimableSettlementFee(offer.market.loanToken); - buyerAssetsOutput, sellerAssetsOutput = take(e, offer, ratifierData, unitsInput, taker, receiver, takerCallbackAddress, takerCallbackData); + buyerAssetsOutput, sellerAssetsOutput, buyerCreditIncreaseOutput, buyerPendingFeeIncreaseOutput, sellerCreditDecreaseOutput, sellerPendingFeeDecreaseOutput = take(e, offer, ratifierData, unitsInput, taker, receiver, takerCallbackAddress, takerCallbackData); // If the input is zero, all the output arguments are zero. - assert unitsInput == 0 => buyerAssetsOutput == 0 && sellerAssetsOutput == 0; + assert unitsInput == 0 => buyerAssetsOutput == 0 && sellerAssetsOutput == 0 && buyerCreditIncreaseOutput == 0 && buyerPendingFeeIncreaseOutput == 0 && sellerCreditDecreaseOutput == 0 && sellerPendingFeeDecreaseOutput == 0; // The claimable settlement fee increases by exactly the spread. assert claimableSettlementFee(offer.market.loanToken) == claimableBefore + buyerAssetsOutput - sellerAssetsOutput; diff --git a/certora/specs/SettlementFeeSpread.spec b/certora/specs/SettlementFeeSpread.spec index dba07ea3a..443d77024 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -40,7 +40,7 @@ rule makerFavorableRounding(env e, Midnight.Offer offer, bytes ratifierData, uin uint256 buyerAssets; uint256 sellerAssets; - buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); assert offer.buy => buyerAssets * WAD() <= units * offerPrice; assert !offer.buy => sellerAssets * WAD() >= units * offerPrice; @@ -55,7 +55,7 @@ rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 buyerAssets; uint256 sellerAssets; - buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); assert buyerAssets - sellerAssets >= (units * fee) / WAD(); assert buyerAssets - sellerAssets <= (units * fee + WAD() - 1) / WAD(); diff --git a/certora/specs/WithdrawableMonotonicity.spec b/certora/specs/WithdrawableMonotonicity.spec index 046572958..2d5b11df6 100644 --- a/certora/specs/WithdrawableMonotonicity.spec +++ b/certora/specs/WithdrawableMonotonicity.spec @@ -69,7 +69,7 @@ rule takeIncreasesClaimableSettlementFee(env e, Midnight.Offer offer, bytes rati uint256 buyerAssets; uint256 sellerAssets; - buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); + buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); // We know that buyerAssets - sellerAssets >= 0, see rule settlementFeeSpreadBounds. assert anyToken == offer.market.loanToken => claimableSettlementFee(anyToken) == before + buyerAssets - sellerAssets; diff --git a/src/Midnight.sol b/src/Midnight.sol index a95c455c1..cea6e8d42 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -334,7 +334,8 @@ contract Midnight is IMidnight { /// @dev All sellerAssets are reachable with the units input, and all buyerAssets are reachable only if buyerPrice /// <= WAD. /// @dev The seller cannot be liquidated during the callbacks of a take. - /// @dev Returns buyerAssets and sellerAssets. + /// @dev Returns buyerAssets, sellerAssets, buyerCreditIncrease, buyerPendingFeeIncrease, sellerCreditDecrease, and + /// sellerPendingFeeDecrease. function take( Offer memory offer, bytes memory ratifierData, @@ -343,7 +344,7 @@ contract Midnight is IMidnight { address receiverIfTakerIsSeller, address takerCallback, bytes memory takerCallbackData - ) external returns (uint256, uint256) { + ) external returns (uint256, uint256, uint256, uint256, uint256, uint256) { require(taker == msg.sender || isAuthorized[taker][msg.sender], TakerUnauthorized()); bytes32 id = touchMarket(offer.market); MarketState storage _marketState = marketState[id]; @@ -480,10 +481,21 @@ contract Midnight is IMidnight { if (!wasLocked) UtilsLib.tExchange(LIQUIDATION_LOCK_SLOT, id, seller, false); require(liquidationLocked(id, seller) || isHealthy(offer.market, id, seller), SellerIsLiquidatable()); - return (buyerAssets, sellerAssets); + return ( + buyerAssets, + sellerAssets, + buyerCreditIncrease, + buyerPendingFeeIncrease, + sellerCreditDecrease, + sellerPendingFeeDecrease + ); } - function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external { + /// @dev Returns the pending fee decrease. + function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) + external + returns (uint128) + { require(onBehalf == msg.sender || isAuthorized[onBehalf][msg.sender], Unauthorized()); bytes32 id = touchMarket(market); MarketState storage _marketState = marketState[id]; @@ -502,6 +514,7 @@ contract Midnight is IMidnight { emit EventsLib.Withdraw(msg.sender, id, units, onBehalf, receiver, pendingFeeDecrease); SafeTransferLib.safeTransfer(market.loanToken, receiver, units); + return pendingFeeDecrease; } function repay(Market memory market, uint256 units, address onBehalf, address callback, bytes calldata data) diff --git a/src/interfaces/IMidnight.sol b/src/interfaces/IMidnight.sol index eb5af676c..767d7df3c 100644 --- a/src/interfaces/IMidnight.sol +++ b/src/interfaces/IMidnight.sol @@ -147,8 +147,8 @@ 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 withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external; + function take(Offer memory offer, bytes memory ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes memory takerCallbackData) external returns (uint256, uint256, uint256, uint256, uint256, uint256); + function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external returns (uint128); 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; diff --git a/src/periphery/MidnightBundles.sol b/src/periphery/MidnightBundles.sol index fa673f9f6..b95866ad6 100644 --- a/src/periphery/MidnightBundles.sol +++ b/src/periphery/MidnightBundles.sol @@ -78,7 +78,7 @@ contract MidnightBundles is IMidnightBundles { ); try IMidnight(MIDNIGHT) .take(takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(0), address(0), "") returns ( - uint256 resBuyerAssets, uint256 + uint256 resBuyerAssets, uint256, uint256, uint256, uint256, uint256 ) { filledUnits += unitsToTake; filledBuyerAssets += resBuyerAssets; @@ -153,7 +153,7 @@ contract MidnightBundles is IMidnightBundles { .take( takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(this), address(0), "" ) returns ( - uint256, uint256 resSellerAssets + uint256, uint256 resSellerAssets, uint256, uint256, uint256, uint256 ) { filledUnits += unitsToTake; filledSellerAssets += resSellerAssets; @@ -214,7 +214,7 @@ contract MidnightBundles is IMidnightBundles { ); try IMidnight(MIDNIGHT) .take(takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(0), address(0), "") returns ( - uint256 resBuyerAssets, uint256 + uint256 resBuyerAssets, uint256, uint256, uint256, uint256, uint256 ) { filledUnits += unitsToTake; filledBuyerAssets += resBuyerAssets; @@ -293,7 +293,7 @@ contract MidnightBundles is IMidnightBundles { .take( takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(this), address(0), "" ) returns ( - uint256, uint256 resSellerAssets + uint256, uint256 resSellerAssets, uint256, uint256, uint256, uint256 ) { filledUnits += unitsToTake; filledSellerAssets += resSellerAssets; diff --git a/test/BaseTest.sol b/test/BaseTest.sol index e54072f91..6a1fd5542 100644 --- a/test/BaseTest.sol +++ b/test/BaseTest.sol @@ -170,7 +170,9 @@ abstract contract BaseTest is Test { // receiverIfTakerIsSeller param is for taker (when offer.buy == true), and must be zero otherwise. // offer.receiverIfMakerIsSeller is for maker (when offer.buy == false). vm.prank(taker); - return midnight.take(offer, hex"", units, taker, offer.buy ? taker : address(0), address(0), hex""); + (uint256 buyerAssets, uint256 sellerAssets,,,,) = + midnight.take(offer, hex"", units, taker, offer.buy ? taker : address(0), address(0), hex""); + return (buyerAssets, sellerAssets); } function setupOtherUsers(Market memory market, uint256 units) internal { diff --git a/test/ContinuousFeeTest.sol b/test/ContinuousFeeTest.sol index 9b80ea47f..bad9affd8 100644 --- a/test/ContinuousFeeTest.sol +++ b/test/ContinuousFeeTest.sol @@ -293,7 +293,25 @@ contract ContinuousFeeTest is BaseTest { lender, otherLender ); - take(exitAmount, lender, _makeBuyOffer(keccak256("lender-exit"))); // lender is taker = seller + Offer memory exitOffer = _makeBuyOffer(keccak256("lender-exit")); + + // lender is taker = seller + vm.prank(lender); + ( + uint256 returnedBuyerAssets, + uint256 returnedSellerAssets, + uint256 returnedBuyerCreditIncrease, + uint256 returnedBuyerPendingFeeIncrease, + uint256 returnedSellerCreditDecrease, + uint256 returnedSellerPendingFeeDecrease + ) = midnight.take(exitOffer, hex"", exitAmount, lender, lender, address(0), hex""); + + assertEq(returnedBuyerAssets, takeAssets, "returned buyerAssets"); + assertEq(returnedSellerAssets, takeAssets, "returned sellerAssets"); + assertEq(returnedBuyerCreditIncrease, exitAmount, "returned buyerCreditIncrease"); + assertEq(returnedBuyerPendingFeeIncrease, buyerPendingFeeIncrease, "returned buyerPendingFeeIncrease"); + assertEq(returnedSellerCreditDecrease, exitAmount, "returned sellerCreditDecrease"); + assertEq(returnedSellerPendingFeeDecrease, sellerPendingFeeDecrease, "returned sellerPendingFeeDecrease"); uint256 expectedRemaining = creditAfterAccrual > 0 ? remainingAfterAccrual - sellerPendingFeeDecrease : 0; assertEq(midnight.creditOf(id, lender), creditAfterAccrual - exitAmount, "credit after exit"); @@ -344,7 +362,9 @@ contract ContinuousFeeTest is BaseTest { vm.expectEmit(); emit EventsLib.Withdraw(lender, id, withdrawAmount, lender, lender, pendingFeeDecrease); vm.prank(lender); - midnight.withdraw(market, withdrawAmount, lender, lender); + uint256 returnedPendingFeeDecrease = midnight.withdraw(market, withdrawAmount, lender, lender); + + assertEq(returnedPendingFeeDecrease, pendingFeeDecrease, "returned pendingFeeDecrease"); uint256 expectedRemaining = creditAfterAccrual > 0 ? remainingAfterAccrual - pendingFeeDecrease : 0; diff --git a/test/LiquidationTest.sol b/test/LiquidationTest.sol index e2800d706..d0dec954f 100644 --- a/test/LiquidationTest.sol +++ b/test/LiquidationTest.sol @@ -579,6 +579,37 @@ contract LiquidationTest is BaseTest { assertLe(remainingDebt, newMaxDebt + 3, "position should be approximately just healthy after max repayment"); } + function testSeizedAssetsInputRcfRejectsNextAmountButMaxAllowedStaysUnhealthy() public { + delete market.collateralParams; + market.collateralParams + .push( + CollateralParams({ + token: address(collateralToken1), + lltv: 0.385e18, + maxLif: maxLif(0.385e18, LIQUIDATION_CURSOR_LOW), + oracle: address(oracle1) + }) + ); + id = toId(market); + + Oracle(market.collateralParams[0].oracle).setPrice(3 * ORACLE_PRICE_SCALE); + deal(address(collateralToken1), borrower, 100); + vm.startPrank(borrower); + collateralToken1.approve(address(midnight), 100); + midnight.supplyCollateral(market, 0, 100, borrower); + vm.stopPrank(); + setupMarket(market, 81); + Oracle(market.collateralParams[0].oracle).setPrice(2 * ORACLE_PRICE_SCALE); + + uint256 seizedAssets = 4; + vm.expectRevert(IMidnight.RecoveryCloseFactorConditionsViolated.selector); + midnight.liquidate(market, 0, seizedAssets + 1, 0, borrower, false, address(this), address(0), ""); + + midnight.liquidate(market, 0, seizedAssets, 0, borrower, false, address(this), address(0), ""); + + assertFalse(midnight.isHealthy(market, id, borrower), "borrower should remain unhealthy"); + } + /// @dev When rcfThreshold > remaining debt after max repayment, full liquidation is allowed pre-maturity. function testRcfThresholdAllowsFullLiquidation(uint256 units, uint256 liquidationOraclePrice, uint256 rcfThreshold) public From 24094c6f15e7390addf59d095101d3efafd3c904 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 3 Jun 2026 17:06:29 +0200 Subject: [PATCH 2/3] Revert "more return values" This reverts commit eb8d8cdb3b346da678a6756a243e6c81e07f2b1c. --- certora/specs/BalanceEffects.spec | 20 +++---------- certora/specs/Midnight.spec | 8 ++---- certora/specs/SettlementFeeSpread.spec | 4 +-- certora/specs/WithdrawableMonotonicity.spec | 2 +- src/Midnight.sol | 21 +++----------- src/interfaces/IMidnight.sol | 4 +-- src/periphery/MidnightBundles.sol | 8 +++--- test/BaseTest.sol | 4 +-- test/ContinuousFeeTest.sol | 24 ++-------------- test/LiquidationTest.sol | 31 --------------------- 10 files changed, 22 insertions(+), 104 deletions(-) diff --git a/certora/specs/BalanceEffects.spec b/certora/specs/BalanceEffects.spec index 2b050d0e6..4fc950791 100644 --- a/certora/specs/BalanceEffects.spec +++ b/certora/specs/BalanceEffects.spec @@ -115,21 +115,15 @@ rule takeBuyerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 u address buyer = offer.buy ? offer.maker : taker; uint256 buyerDebtBefore = debtOf(id, buyer); uint128 buyerUpdatedCreditBefore; - uint128 buyerUpdatedPendingFeeBefore; - buyerUpdatedCreditBefore, buyerUpdatedPendingFeeBefore, _ = updatePositionView(e, offer.market, id, buyer); + buyerUpdatedCreditBefore, _, _ = updatePositionView(e, offer.market, id, buyer); - uint256 buyerCreditIncrease; - uint256 buyerPendingFeeIncrease; - _, _, buyerCreditIncrease, buyerPendingFeeIncrease, _, _ = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + 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 creditOf(id, buyer) == buyerUpdatedCreditBefore + buyerCreditIncrease; - assert pendingFee(id, buyer) == buyerUpdatedPendingFeeBefore + buyerPendingFeeIncrease; - assert debtOf(id, buyer) + units == buyerDebtBefore + buyerCreditIncrease; } /// 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. @@ -141,21 +135,15 @@ rule takeSellerEffects(env e, Midnight.Offer offer, bytes ratifierData, uint256 address seller = offer.buy ? taker : offer.maker; uint256 sellerDebtBefore = debtOf(id, seller); uint128 sellerUpdatedCreditBefore; - uint128 sellerUpdatedPendingFeeBefore; - sellerUpdatedCreditBefore, sellerUpdatedPendingFeeBefore, _ = updatePositionView(e, offer.market, id, seller); + sellerUpdatedCreditBefore, _, _ = updatePositionView(e, offer.market, id, seller); - uint256 sellerCreditDecrease; - uint256 sellerPendingFeeDecrease; - _, _, _, _, sellerCreditDecrease, sellerPendingFeeDecrease = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + 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 creditOf(id, seller) + sellerCreditDecrease == sellerUpdatedCreditBefore; - assert pendingFee(id, seller) + sellerPendingFeeDecrease == sellerUpdatedPendingFeeBefore; - assert debtOf(id, seller) == sellerDebtBefore + units - sellerCreditDecrease; } /// REPAY /// diff --git a/certora/specs/Midnight.spec b/certora/specs/Midnight.spec index c53a17b1d..b908ee0da 100644 --- a/certora/specs/Midnight.spec +++ b/certora/specs/Midnight.spec @@ -63,17 +63,13 @@ function summaryMulDiv(uint256 x, uint256 y, uint256 d) returns uint256 { rule takeInputOutputConsistency(env e, Midnight.Offer offer, bytes ratifierData, uint256 unitsInput, address taker, address receiver, address takerCallbackAddress, bytes takerCallbackData) { uint256 buyerAssetsOutput; uint256 sellerAssetsOutput; - uint256 buyerCreditIncreaseOutput; - uint256 buyerPendingFeeIncreaseOutput; - uint256 sellerCreditDecreaseOutput; - uint256 sellerPendingFeeDecreaseOutput; uint256 claimableBefore = claimableSettlementFee(offer.market.loanToken); - buyerAssetsOutput, sellerAssetsOutput, buyerCreditIncreaseOutput, buyerPendingFeeIncreaseOutput, sellerCreditDecreaseOutput, sellerPendingFeeDecreaseOutput = take(e, offer, ratifierData, unitsInput, taker, receiver, takerCallbackAddress, takerCallbackData); + buyerAssetsOutput, sellerAssetsOutput = take(e, offer, ratifierData, unitsInput, taker, receiver, takerCallbackAddress, takerCallbackData); // If the input is zero, all the output arguments are zero. - assert unitsInput == 0 => buyerAssetsOutput == 0 && sellerAssetsOutput == 0 && buyerCreditIncreaseOutput == 0 && buyerPendingFeeIncreaseOutput == 0 && sellerCreditDecreaseOutput == 0 && sellerPendingFeeDecreaseOutput == 0; + assert unitsInput == 0 => buyerAssetsOutput == 0 && sellerAssetsOutput == 0; // The claimable settlement fee increases by exactly the spread. assert claimableSettlementFee(offer.market.loanToken) == claimableBefore + buyerAssetsOutput - sellerAssetsOutput; diff --git a/certora/specs/SettlementFeeSpread.spec b/certora/specs/SettlementFeeSpread.spec index 443d77024..dba07ea3a 100644 --- a/certora/specs/SettlementFeeSpread.spec +++ b/certora/specs/SettlementFeeSpread.spec @@ -40,7 +40,7 @@ rule makerFavorableRounding(env e, Midnight.Offer offer, bytes ratifierData, uin uint256 buyerAssets; uint256 sellerAssets; - buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); assert offer.buy => buyerAssets * WAD() <= units * offerPrice; assert !offer.buy => sellerAssets * WAD() >= units * offerPrice; @@ -55,7 +55,7 @@ rule settlementFeeSpreadBounds(env e, Midnight.Offer offer, bytes ratifierData, uint256 buyerAssets; uint256 sellerAssets; - buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); + buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); assert buyerAssets - sellerAssets >= (units * fee) / WAD(); assert buyerAssets - sellerAssets <= (units * fee + WAD() - 1) / WAD(); diff --git a/certora/specs/WithdrawableMonotonicity.spec b/certora/specs/WithdrawableMonotonicity.spec index 2d5b11df6..046572958 100644 --- a/certora/specs/WithdrawableMonotonicity.spec +++ b/certora/specs/WithdrawableMonotonicity.spec @@ -69,7 +69,7 @@ rule takeIncreasesClaimableSettlementFee(env e, Midnight.Offer offer, bytes rati uint256 buyerAssets; uint256 sellerAssets; - buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); + buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); // We know that buyerAssets - sellerAssets >= 0, see rule settlementFeeSpreadBounds. assert anyToken == offer.market.loanToken => claimableSettlementFee(anyToken) == before + buyerAssets - sellerAssets; diff --git a/src/Midnight.sol b/src/Midnight.sol index cea6e8d42..a95c455c1 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -334,8 +334,7 @@ contract Midnight is IMidnight { /// @dev All sellerAssets are reachable with the units input, and all buyerAssets are reachable only if buyerPrice /// <= WAD. /// @dev The seller cannot be liquidated during the callbacks of a take. - /// @dev Returns buyerAssets, sellerAssets, buyerCreditIncrease, buyerPendingFeeIncrease, sellerCreditDecrease, and - /// sellerPendingFeeDecrease. + /// @dev Returns buyerAssets and sellerAssets. function take( Offer memory offer, bytes memory ratifierData, @@ -344,7 +343,7 @@ contract Midnight is IMidnight { address receiverIfTakerIsSeller, address takerCallback, bytes memory takerCallbackData - ) external returns (uint256, uint256, uint256, uint256, uint256, uint256) { + ) external returns (uint256, uint256) { require(taker == msg.sender || isAuthorized[taker][msg.sender], TakerUnauthorized()); bytes32 id = touchMarket(offer.market); MarketState storage _marketState = marketState[id]; @@ -481,21 +480,10 @@ contract Midnight is IMidnight { if (!wasLocked) UtilsLib.tExchange(LIQUIDATION_LOCK_SLOT, id, seller, false); require(liquidationLocked(id, seller) || isHealthy(offer.market, id, seller), SellerIsLiquidatable()); - return ( - buyerAssets, - sellerAssets, - buyerCreditIncrease, - buyerPendingFeeIncrease, - sellerCreditDecrease, - sellerPendingFeeDecrease - ); + return (buyerAssets, sellerAssets); } - /// @dev Returns the pending fee decrease. - function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) - external - returns (uint128) - { + 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]; @@ -514,7 +502,6 @@ contract Midnight is IMidnight { emit EventsLib.Withdraw(msg.sender, id, units, onBehalf, receiver, pendingFeeDecrease); SafeTransferLib.safeTransfer(market.loanToken, receiver, units); - return pendingFeeDecrease; } function repay(Market memory market, uint256 units, address onBehalf, address callback, bytes calldata data) diff --git a/src/interfaces/IMidnight.sol b/src/interfaces/IMidnight.sol index 767d7df3c..eb5af676c 100644 --- a/src/interfaces/IMidnight.sol +++ b/src/interfaces/IMidnight.sol @@ -147,8 +147,8 @@ 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, uint256, uint256, uint256, uint256); - function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external returns (uint128); + function take(Offer memory offer, bytes memory ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes memory takerCallbackData) external returns (uint256, uint256); + 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; diff --git a/src/periphery/MidnightBundles.sol b/src/periphery/MidnightBundles.sol index b95866ad6..fa673f9f6 100644 --- a/src/periphery/MidnightBundles.sol +++ b/src/periphery/MidnightBundles.sol @@ -78,7 +78,7 @@ contract MidnightBundles is IMidnightBundles { ); try IMidnight(MIDNIGHT) .take(takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(0), address(0), "") returns ( - uint256 resBuyerAssets, uint256, uint256, uint256, uint256, uint256 + uint256 resBuyerAssets, uint256 ) { filledUnits += unitsToTake; filledBuyerAssets += resBuyerAssets; @@ -153,7 +153,7 @@ contract MidnightBundles is IMidnightBundles { .take( takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(this), address(0), "" ) returns ( - uint256, uint256 resSellerAssets, uint256, uint256, uint256, uint256 + uint256, uint256 resSellerAssets ) { filledUnits += unitsToTake; filledSellerAssets += resSellerAssets; @@ -214,7 +214,7 @@ contract MidnightBundles is IMidnightBundles { ); try IMidnight(MIDNIGHT) .take(takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(0), address(0), "") returns ( - uint256 resBuyerAssets, uint256, uint256, uint256, uint256, uint256 + uint256 resBuyerAssets, uint256 ) { filledUnits += unitsToTake; filledBuyerAssets += resBuyerAssets; @@ -293,7 +293,7 @@ contract MidnightBundles is IMidnightBundles { .take( takes[i].offer, takes[i].ratifierData, unitsToTake, taker, address(this), address(0), "" ) returns ( - uint256, uint256 resSellerAssets, uint256, uint256, uint256, uint256 + uint256, uint256 resSellerAssets ) { filledUnits += unitsToTake; filledSellerAssets += resSellerAssets; diff --git a/test/BaseTest.sol b/test/BaseTest.sol index 6a1fd5542..e54072f91 100644 --- a/test/BaseTest.sol +++ b/test/BaseTest.sol @@ -170,9 +170,7 @@ abstract contract BaseTest is Test { // receiverIfTakerIsSeller param is for taker (when offer.buy == true), and must be zero otherwise. // offer.receiverIfMakerIsSeller is for maker (when offer.buy == false). vm.prank(taker); - (uint256 buyerAssets, uint256 sellerAssets,,,,) = - midnight.take(offer, hex"", units, taker, offer.buy ? taker : address(0), address(0), hex""); - return (buyerAssets, sellerAssets); + return midnight.take(offer, hex"", units, taker, offer.buy ? taker : address(0), address(0), hex""); } function setupOtherUsers(Market memory market, uint256 units) internal { diff --git a/test/ContinuousFeeTest.sol b/test/ContinuousFeeTest.sol index bad9affd8..9b80ea47f 100644 --- a/test/ContinuousFeeTest.sol +++ b/test/ContinuousFeeTest.sol @@ -293,25 +293,7 @@ contract ContinuousFeeTest is BaseTest { lender, otherLender ); - Offer memory exitOffer = _makeBuyOffer(keccak256("lender-exit")); - - // lender is taker = seller - vm.prank(lender); - ( - uint256 returnedBuyerAssets, - uint256 returnedSellerAssets, - uint256 returnedBuyerCreditIncrease, - uint256 returnedBuyerPendingFeeIncrease, - uint256 returnedSellerCreditDecrease, - uint256 returnedSellerPendingFeeDecrease - ) = midnight.take(exitOffer, hex"", exitAmount, lender, lender, address(0), hex""); - - assertEq(returnedBuyerAssets, takeAssets, "returned buyerAssets"); - assertEq(returnedSellerAssets, takeAssets, "returned sellerAssets"); - assertEq(returnedBuyerCreditIncrease, exitAmount, "returned buyerCreditIncrease"); - assertEq(returnedBuyerPendingFeeIncrease, buyerPendingFeeIncrease, "returned buyerPendingFeeIncrease"); - assertEq(returnedSellerCreditDecrease, exitAmount, "returned sellerCreditDecrease"); - assertEq(returnedSellerPendingFeeDecrease, sellerPendingFeeDecrease, "returned sellerPendingFeeDecrease"); + 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"); @@ -362,9 +344,7 @@ contract ContinuousFeeTest is BaseTest { vm.expectEmit(); emit EventsLib.Withdraw(lender, id, withdrawAmount, lender, lender, pendingFeeDecrease); vm.prank(lender); - uint256 returnedPendingFeeDecrease = midnight.withdraw(market, withdrawAmount, lender, lender); - - assertEq(returnedPendingFeeDecrease, pendingFeeDecrease, "returned pendingFeeDecrease"); + midnight.withdraw(market, withdrawAmount, lender, lender); uint256 expectedRemaining = creditAfterAccrual > 0 ? remainingAfterAccrual - pendingFeeDecrease : 0; diff --git a/test/LiquidationTest.sol b/test/LiquidationTest.sol index d0dec954f..e2800d706 100644 --- a/test/LiquidationTest.sol +++ b/test/LiquidationTest.sol @@ -579,37 +579,6 @@ contract LiquidationTest is BaseTest { assertLe(remainingDebt, newMaxDebt + 3, "position should be approximately just healthy after max repayment"); } - function testSeizedAssetsInputRcfRejectsNextAmountButMaxAllowedStaysUnhealthy() public { - delete market.collateralParams; - market.collateralParams - .push( - CollateralParams({ - token: address(collateralToken1), - lltv: 0.385e18, - maxLif: maxLif(0.385e18, LIQUIDATION_CURSOR_LOW), - oracle: address(oracle1) - }) - ); - id = toId(market); - - Oracle(market.collateralParams[0].oracle).setPrice(3 * ORACLE_PRICE_SCALE); - deal(address(collateralToken1), borrower, 100); - vm.startPrank(borrower); - collateralToken1.approve(address(midnight), 100); - midnight.supplyCollateral(market, 0, 100, borrower); - vm.stopPrank(); - setupMarket(market, 81); - Oracle(market.collateralParams[0].oracle).setPrice(2 * ORACLE_PRICE_SCALE); - - uint256 seizedAssets = 4; - vm.expectRevert(IMidnight.RecoveryCloseFactorConditionsViolated.selector); - midnight.liquidate(market, 0, seizedAssets + 1, 0, borrower, false, address(this), address(0), ""); - - midnight.liquidate(market, 0, seizedAssets, 0, borrower, false, address(this), address(0), ""); - - assertFalse(midnight.isHealthy(market, id, borrower), "borrower should remain unhealthy"); - } - /// @dev When rcfThreshold > remaining debt after max repayment, full liquidation is allowed pre-maturity. function testRcfThresholdAllowsFullLiquidation(uint256 units, uint256 liquidationOraclePrice, uint256 rcfThreshold) public From 82f767453de80d9ec6c8f7a9b863cd057b18af3b Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 3 Jun 2026 17:07:55 +0200 Subject: [PATCH 3/3] Return pending fee decrease from withdraw --- certora/specs/ContinuousFee.spec | 5 ++++- src/Midnight.sol | 7 ++++++- src/interfaces/IMidnight.sol | 2 +- 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec index 5d27e6eed..f2bcaac59 100644 --- a/certora/specs/ContinuousFee.spec +++ b/certora/specs/ContinuousFee.spec @@ -98,10 +98,13 @@ rule pendingFeeDecreasesProportionallyOnWithdraw(env e, Midnight.Market market, postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, market, id, onBehalf); - withdraw(e, market, units, onBehalf, receiver); + uint128 returnedPendingFeeDecrease; + returnedPendingFeeDecrease = withdraw(e, market, units, onBehalf, receiver); require id == lastId, "id should be derived from market"; + assert postUpdatePendingFee == pendingFee(id, onBehalf) + returnedPendingFeeDecrease; + // When postUpdateCredit == 0, pendingFee(id, onBehalf) is unchanged on withdraw. assert postUpdateCredit == 0 ? pendingFee(id, onBehalf) == postUpdatePendingFee : pendingFee(id, onBehalf) == postUpdatePendingFee - (postUpdatePendingFee * units + postUpdateCredit - 1) / postUpdateCredit; } diff --git a/src/Midnight.sol b/src/Midnight.sol index a95c455c1..7db63c228 100644 --- a/src/Midnight.sol +++ b/src/Midnight.sol @@ -483,7 +483,11 @@ contract Midnight is IMidnight { return (buyerAssets, sellerAssets); } - function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external { + /// @dev Returns the pending fee decrease. + function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) + external + returns (uint128) + { require(onBehalf == msg.sender || isAuthorized[onBehalf][msg.sender], Unauthorized()); bytes32 id = touchMarket(market); MarketState storage _marketState = marketState[id]; @@ -502,6 +506,7 @@ contract Midnight is IMidnight { emit EventsLib.Withdraw(msg.sender, id, units, onBehalf, receiver, pendingFeeDecrease); SafeTransferLib.safeTransfer(market.loanToken, receiver, units); + return pendingFeeDecrease; } function repay(Market memory market, uint256 units, address onBehalf, address callback, bytes calldata data) diff --git a/src/interfaces/IMidnight.sol b/src/interfaces/IMidnight.sol index eb5af676c..d089f4df5 100644 --- a/src/interfaces/IMidnight.sol +++ b/src/interfaces/IMidnight.sol @@ -148,7 +148,7 @@ interface IMidnight { /// 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 withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external; + function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external returns (uint128); 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;