From 59eb0fed1edb45a849acb1e73e878f57413f83a9 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 08:31:24 +0000 Subject: [PATCH 01/10] certora: weaken stayHealthy for take Stacked on #645. --- certora/specs/Healthiness.spec | 72 ++++++++++++++++++++++++++++++++-- 1 file changed, 68 insertions(+), 4 deletions(-) diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index 2508dca37..fa6969a9d 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -97,6 +97,10 @@ persistent ghost bool useIsHealthyNoBitmap; // global variable to track whether the user was healthy before the callbacks. ghost bool healthyBeforeCallback; +// In take's same-seller case, the seller may become unhealthy during callbacks and only recover by the +// end of the call. We model that case with a weak callback condition. +persistent ghost bool weakHealthyDuringCallbacks; + // global variable to track which obligation and borrower we're testing. persistent ghost address globalObligationLoanToken; @@ -157,23 +161,34 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } +definition takeSeller(address taker, Midnight.Offer offer) returns address = offer.buy ? taker : offer.maker; + +definition takeBuyer(address taker, Midnight.Offer offer) returns address = offer.buy ? offer.maker : taker; + // Summary for every callback (token transfer, onLiquidate, onFlashloan, onBuy, onSell) // we check that the user is healthy before the callback, do some external call (to simulate changes by the callback), -// and then require that the user is still healthy after the callback. +// and then require that the user is still healthy after the callback. For take's same-seller case we weaken the +// callback condition, since the seller is only required to be healthy again by the end of take. function genericCallback() { address dummy; env e; Midnight.Obligation globalObligation = getGlobalObligation(); - // check that isHealthy holds before the callback. We remember any violation and check that none occurred at the end of each rule. - bool savedHealthyBefore = healthyBeforeCallback && callIsHealthy(globalObligation, globalId, globalBorrower); + // check that isHealthy holds before the callback, unless the current rule is using the weak take-seller case. + // We remember any violation and check that none occurred at the end of each strong rule. + bool savedHealthyBefore = healthyBeforeCallback; + if (!weakHealthyDuringCallbacks) { + savedHealthyBefore = healthyBeforeCallback && callIsHealthy(globalObligation, globalId, globalBorrower); + } callback.callHavoc(e, dummy); // the callback havocs the global variable healthyBeforeCallback, so we restore the variable using the saved value in the local variable. healthyBeforeCallback = savedHealthyBefore; - require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after callback"; + if (!weakHealthyDuringCallbacks) { + require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after callback"; + } } // Same as the summary above except that it also returns a non-deterministic value. @@ -202,6 +217,7 @@ function genericCallbackBytes32() returns (bytes32) { // Show that the user stays healthy on liquidate, if the user gets liquidated (can occur if blocktime exceeds maturity) rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 seizedAssetsIn, uint256 repaidUnitsIn, bytes data) { useIsHealthyNoBitmap = false; + weakHealthyDuringCallbacks = false; // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. healthyBeforeCallback = true; @@ -243,6 +259,7 @@ rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 se // Show that the user stays healthy on liquidate, if another user gets liquidated or obligation differs. rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { useIsHealthyNoBitmap = true; + weakHealthyDuringCallbacks = false; // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. healthyBeforeCallback = true; @@ -260,10 +277,57 @@ rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, ui assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } +// Show that the user stays healthy on take, if the user under consideration is the seller on the obligation under consideration. +// This is a weak property: the seller may only become healthy again by the end of take. +rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { + useIsHealthyNoBitmap = false; + weakHealthyDuringCallbacks = true; + + // This variable is only asserted in the strong rules. We still initialize it for consistency. + healthyBeforeCallback = true; + + require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; + + Midnight.Obligation globalObligation = getGlobalObligation(); + require equalsGlobalObligation(offer.obligation), "obligation matches"; + require takeSeller(taker, offer) == globalBorrower, "seller matches"; + + require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); + + assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; +} + +// Show that the user stays healthy on take, if the user is neither buyer nor seller on the obligation under consideration, +// or the obligation differs. +rule stayHealthyTakeOtherBorrower(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { + useIsHealthyNoBitmap = true; + weakHealthyDuringCallbacks = false; + + // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. + healthyBeforeCallback = true; + + require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; + + Midnight.Obligation globalObligation = getGlobalObligation(); + require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) + || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; + + require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); + + assert healthyBeforeCallback, "user is healthy before callbacks"; + assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; +} + // Show that the user stays healthy on any other function than liquidate or take. +// Take is handled by the two dedicated rules above. rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, Midnight.Signature, bytes32, bytes32[]).selector } { // for withdraw collateral we choose isHealthy() for all others the isHealthyNoBitmap function. useIsHealthyNoBitmap = (f.selector != sig:withdrawCollateral(Midnight.Obligation, uint256, uint256, address, address).selector); + weakHealthyDuringCallbacks = false; // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. healthyBeforeCallback = true; From 12aafb7c77c416db1bad6e7fcafee92cf1701512 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 08:39:04 +0000 Subject: [PATCH 02/10] certora: remove callback healthiness assertions Adjust scope per feedback: callback-time healthiness no longer matters. --- certora/specs/Healthiness.spec | 57 ++-------------------------------- 1 file changed, 3 insertions(+), 54 deletions(-) diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index fa6969a9d..b47466364 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -94,13 +94,6 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { // see callIsHealthy() below. persistent ghost bool useIsHealthyNoBitmap; -// global variable to track whether the user was healthy before the callbacks. -ghost bool healthyBeforeCallback; - -// In take's same-seller case, the seller may become unhealthy during callbacks and only recover by the -// end of the call. We model that case with a weak callback condition. -persistent ghost bool weakHealthyDuringCallbacks; - // global variable to track which obligation and borrower we're testing. persistent ghost address globalObligationLoanToken; @@ -165,30 +158,13 @@ definition takeSeller(address taker, Midnight.Offer offer) returns address = off definition takeBuyer(address taker, Midnight.Offer offer) returns address = offer.buy ? offer.maker : taker; -// Summary for every callback (token transfer, onLiquidate, onFlashloan, onBuy, onSell) -// we check that the user is healthy before the callback, do some external call (to simulate changes by the callback), -// and then require that the user is still healthy after the callback. For take's same-seller case we weaken the -// callback condition, since the seller is only required to be healthy again by the end of take. +// Summary for every callback (token transfer, onLiquidate, onFlashloan, onBuy, onSell). +// We do not prove healthiness during callbacks; we only prove healthiness again at the end of the outer call. function genericCallback() { address dummy; env e; - Midnight.Obligation globalObligation = getGlobalObligation(); - - // check that isHealthy holds before the callback, unless the current rule is using the weak take-seller case. - // We remember any violation and check that none occurred at the end of each strong rule. - bool savedHealthyBefore = healthyBeforeCallback; - if (!weakHealthyDuringCallbacks) { - savedHealthyBefore = healthyBeforeCallback && callIsHealthy(globalObligation, globalId, globalBorrower); - } callback.callHavoc(e, dummy); - - // the callback havocs the global variable healthyBeforeCallback, so we restore the variable using the saved value in the local variable. - healthyBeforeCallback = savedHealthyBefore; - - if (!weakHealthyDuringCallbacks) { - require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after callback"; - } } // Same as the summary above except that it also returns a non-deterministic value. @@ -217,10 +193,6 @@ function genericCallbackBytes32() returns (bytes32) { // Show that the user stays healthy on liquidate, if the user gets liquidated (can occur if blocktime exceeds maturity) rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 seizedAssetsIn, uint256 repaidUnitsIn, bytes data) { useIsHealthyNoBitmap = false; - weakHealthyDuringCallbacks = false; - - // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. - healthyBeforeCallback = true; require globalObligationCollateralLLTV[collateralIndex] * globalObligationCollateralMaxLif[collateralIndex] <= WAD() * WAD(), "Proved in lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec: maxLif is at most 1/lltv"; @@ -251,18 +223,12 @@ rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 se require axiomAddDownUp(collateralAfter, seizedAssetsOut, price, ORACLE_PRICE_SCALE()), "axiom"; require axiomAddDownUp(summaryMulDivDownM(collateralAfter, price, ORACLE_PRICE_SCALE()), summaryMulDivUpM(seizedAssetsOut, price, ORACLE_PRICE_SCALE()), globalObligationCollateralLLTV[collateralIndex], WAD()), "axiom"; - // check that the user was healthy before all callbacks. We can only assert this after we included all the needed axioms. - assert healthyBeforeCallback, "user is healthy before callbacks"; assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } // Show that the user stays healthy on liquidate, if another user gets liquidated or obligation differs. rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { useIsHealthyNoBitmap = true; - weakHealthyDuringCallbacks = false; - - // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. - healthyBeforeCallback = true; require globalObligationCollateralLength <= 2, "too many collateralParams for the spec to handle"; @@ -273,18 +239,12 @@ rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, ui liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); - assert healthyBeforeCallback, "user is healthy before callbacks"; assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } // Show that the user stays healthy on take, if the user under consideration is the seller on the obligation under consideration. -// This is a weak property: the seller may only become healthy again by the end of take. rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { useIsHealthyNoBitmap = false; - weakHealthyDuringCallbacks = true; - - // This variable is only asserted in the strong rules. We still initialize it for consistency. - healthyBeforeCallback = true; require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; @@ -303,22 +263,16 @@ rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address take // or the obligation differs. rule stayHealthyTakeOtherBorrower(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { useIsHealthyNoBitmap = true; - weakHealthyDuringCallbacks = false; - - // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. - healthyBeforeCallback = true; require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; Midnight.Obligation globalObligation = getGlobalObligation(); - require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) - || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; + require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); - assert healthyBeforeCallback, "user is healthy before callbacks"; assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } @@ -327,10 +281,6 @@ rule stayHealthyTakeOtherBorrower(env e, uint256 units, address taker, address t rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, Midnight.Signature, bytes32, bytes32[]).selector } { // for withdraw collateral we choose isHealthy() for all others the isHealthyNoBitmap function. useIsHealthyNoBitmap = (f.selector != sig:withdrawCollateral(Midnight.Obligation, uint256, uint256, address, address).selector); - weakHealthyDuringCallbacks = false; - - // This variable is set to false whenever isHealthy() is violated before a callback. Initially we set it to true to indicate no violations detected. - healthyBeforeCallback = true; require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomDownMonotoneA(a1, a2, b, d), "axiom"; @@ -342,6 +292,5 @@ rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector ! f(e, args); - assert healthyBeforeCallback, "user is healthy before callbacks"; assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } From 840dd2409ef57b3bf6bf5056b5a3aff5c7a2e84c Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 08:57:22 +0000 Subject: [PATCH 03/10] certora: simplify Healthiness proof Per feedback, stop caring about healthiness during callbacks and simplify the proof accordingly. --- certora/confs/Healthiness.conf | 3 +- certora/specs/Healthiness.spec | 88 +++++----------------------------- 2 files changed, 14 insertions(+), 77 deletions(-) diff --git a/certora/confs/Healthiness.conf b/certora/confs/Healthiness.conf index 7afc42f72..8208c368b 100644 --- a/certora/confs/Healthiness.conf +++ b/certora/confs/Healthiness.conf @@ -1,7 +1,6 @@ { "files": [ - "certora/helpers/MidnightWrapper.sol", - "certora/helpers/Havoc.sol" + "certora/helpers/MidnightWrapper.sol" ], "parametric_contracts": [ "MidnightWrapper" diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index b47466364..8290e5769 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -2,8 +2,6 @@ import "BitmapSummaries.spec"; -using Havoc as callback; - methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -26,15 +24,16 @@ methods { */ function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); - function _.havocAll() external => HAVOC_ALL; - - function _.transferFrom(address from, address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); - function _.transfer(address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); - function _.onBuy(bytes32 id, Midnight.Obligation obligation, address buyer, uint256 buyerAssets, uint256 units, bytes data) external => genericCallbackBytes32() expect(bytes32); - function _.onSell(bytes32 id, Midnight.Obligation obligation, address seller, uint256 sellerAssets, uint256 units, bytes data) external => genericCallbackBytes32() expect(bytes32); - function _.onRepay(bytes32 id, Midnight.Obligation obligation, uint256 units, address onBehalf, bytes data) external => genericCallback() expect void; - function _.onLiquidate(bytes32 id, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) external => genericCallback() expect void; - function _.onFlashLoan(address token, uint256 amount, bytes data) external => genericCallback() expect void; + + // Assume no reentrancy: callbacks and token transfers do not re-enter Midnight for this property. + // This proof only cares that a borrower is healthy before the outer call and healthy again after a successful return. + function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Obligation, uint256, address, bytes) external => NONDET; + function _.onLiquidate(bytes32, Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onFlashLoan(address, uint256, bytes) external => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; } /// SUMMARY /// @@ -154,32 +153,6 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } -definition takeSeller(address taker, Midnight.Offer offer) returns address = offer.buy ? taker : offer.maker; - -definition takeBuyer(address taker, Midnight.Offer offer) returns address = offer.buy ? offer.maker : taker; - -// Summary for every callback (token transfer, onLiquidate, onFlashloan, onBuy, onSell). -// We do not prove healthiness during callbacks; we only prove healthiness again at the end of the outer call. -function genericCallback() { - address dummy; - env e; - - callback.callHavoc(e, dummy); -} - -// Same as the summary above except that it also returns a non-deterministic value. -function genericCallbackBool() returns (bool) { - bool result; - genericCallback(); - return result; -} - -function genericCallbackBytes32() returns (bytes32) { - bytes32 result; - genericCallback(); - return result; -} - //// RULES ////// // The remaining rules show that a healthy borrower cannot get unhealthy by calling any function of the contract. @@ -242,44 +215,9 @@ rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, ui assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } -// Show that the user stays healthy on take, if the user under consideration is the seller on the obligation under consideration. -rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { - useIsHealthyNoBitmap = false; - - require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; - - Midnight.Obligation globalObligation = getGlobalObligation(); - require equalsGlobalObligation(offer.obligation), "obligation matches"; - require takeSeller(taker, offer) == globalBorrower, "seller matches"; - - require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; - - take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); - - assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; -} - -// Show that the user stays healthy on take, if the user is neither buyer nor seller on the obligation under consideration, -// or the obligation differs. -rule stayHealthyTakeOtherBorrower(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { - useIsHealthyNoBitmap = true; - - require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; - - Midnight.Obligation globalObligation = getGlobalObligation(); - require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; - - require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; - - take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); - - assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; -} - -// Show that the user stays healthy on any other function than liquidate or take. -// Take is handled by the two dedicated rules above. -rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, Midnight.Signature, bytes32, bytes32[]).selector } { - // for withdraw collateral we choose isHealthy() for all others the isHealthyNoBitmap function. +// Show that the user stays healthy on any other function than liquidate. +rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector } { + // for withdrawCollateral we choose isHealthy(); for all others we choose the bitmap-less implementation. useIsHealthyNoBitmap = (f.selector != sig:withdrawCollateral(Midnight.Obligation, uint256, uint256, address, address).selector); require forall mathint a1. forall mathint a2. forall mathint b. forall mathint d. axiomDownMonotoneA(a1, a2, b, d), "axiom"; From c931cac7ada2f6be245eba1c29693bbdb4f728fd Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 09:10:41 +0000 Subject: [PATCH 04/10] certora: keep callback/token effects reachable Restore callback/token havoc modeling while keeping take inside the generic stayHealthy rule. --- certora/confs/Healthiness.conf | 3 ++- certora/specs/Healthiness.spec | 45 ++++++++++++++++++++++++++-------- 2 files changed, 37 insertions(+), 11 deletions(-) diff --git a/certora/confs/Healthiness.conf b/certora/confs/Healthiness.conf index 8208c368b..7afc42f72 100644 --- a/certora/confs/Healthiness.conf +++ b/certora/confs/Healthiness.conf @@ -1,6 +1,7 @@ { "files": [ - "certora/helpers/MidnightWrapper.sol" + "certora/helpers/MidnightWrapper.sol", + "certora/helpers/Havoc.sol" ], "parametric_contracts": [ "MidnightWrapper" diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index 8290e5769..69549b4b1 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -2,6 +2,8 @@ import "BitmapSummaries.spec"; +using Havoc as callback; + methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -24,16 +26,17 @@ methods { */ function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); - - // Assume no reentrancy: callbacks and token transfers do not re-enter Midnight for this property. - // This proof only cares that a borrower is healthy before the outer call and healthy again after a successful return. - function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; - function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; - function _.onRepay(bytes32, Midnight.Obligation, uint256, address, bytes) external => NONDET; - function _.onLiquidate(bytes32, Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; - function _.onFlashLoan(address, uint256, bytes) external => NONDET; - function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; - function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function _.havocAll() external => HAVOC_ALL; + + // Model callbacks and token transfers as arbitrary external code so reentrant effects remain reachable, + // but do not assert healthiness during the callback window. + function _.transferFrom(address from, address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); + function _.transfer(address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); + function _.onBuy(bytes32 id, Midnight.Obligation obligation, address buyer, uint256 buyerAssets, uint256 units, bytes data) external => genericCallbackBytes32() expect(bytes32); + function _.onSell(bytes32 id, Midnight.Obligation obligation, address seller, uint256 sellerAssets, uint256 units, bytes data) external => genericCallbackBytes32() expect(bytes32); + function _.onRepay(bytes32 id, Midnight.Obligation obligation, uint256 units, address onBehalf, bytes data) external => genericCallback() expect void; + function _.onLiquidate(bytes32 id, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) external => genericCallback() expect void; + function _.onFlashLoan(address token, uint256 amount, bytes data) external => genericCallback() expect void; } /// SUMMARY /// @@ -153,6 +156,28 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } +// Summary for every callback (token transfer, onLiquidate, onFlashLoan, onBuy, onSell). +// We keep arbitrary callback/token side effects reachable via HAVOC, but only prove healthiness before the +// outer call and after the successful outer call returns. +function genericCallback() { + address dummy; + env e; + + callback.callHavoc(e, dummy); +} + +function genericCallbackBool() returns (bool) { + bool result; + genericCallback(); + return result; +} + +function genericCallbackBytes32() returns (bytes32) { + bytes32 result; + genericCallback(); + return result; +} + //// RULES ////// // The remaining rules show that a healthy borrower cannot get unhealthy by calling any function of the contract. From 035ad4133d6bf6877f0d06f11956fda48036d22f Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 09:27:49 +0000 Subject: [PATCH 05/10] certora: drop callback/token summaries Per feedback, remove callback/token summaries entirely from Healthiness. --- certora/confs/Healthiness.conf | 3 +-- certora/specs/Healthiness.spec | 35 ---------------------------------- 2 files changed, 1 insertion(+), 37 deletions(-) diff --git a/certora/confs/Healthiness.conf b/certora/confs/Healthiness.conf index 7afc42f72..8208c368b 100644 --- a/certora/confs/Healthiness.conf +++ b/certora/confs/Healthiness.conf @@ -1,7 +1,6 @@ { "files": [ - "certora/helpers/MidnightWrapper.sol", - "certora/helpers/Havoc.sol" + "certora/helpers/MidnightWrapper.sol" ], "parametric_contracts": [ "MidnightWrapper" diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index 69549b4b1..b07385403 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -2,8 +2,6 @@ import "BitmapSummaries.spec"; -using Havoc as callback; - methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -26,17 +24,6 @@ methods { */ function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); - function _.havocAll() external => HAVOC_ALL; - - // Model callbacks and token transfers as arbitrary external code so reentrant effects remain reachable, - // but do not assert healthiness during the callback window. - function _.transferFrom(address from, address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); - function _.transfer(address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); - function _.onBuy(bytes32 id, Midnight.Obligation obligation, address buyer, uint256 buyerAssets, uint256 units, bytes data) external => genericCallbackBytes32() expect(bytes32); - function _.onSell(bytes32 id, Midnight.Obligation obligation, address seller, uint256 sellerAssets, uint256 units, bytes data) external => genericCallbackBytes32() expect(bytes32); - function _.onRepay(bytes32 id, Midnight.Obligation obligation, uint256 units, address onBehalf, bytes data) external => genericCallback() expect void; - function _.onLiquidate(bytes32 id, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) external => genericCallback() expect void; - function _.onFlashLoan(address token, uint256 amount, bytes data) external => genericCallback() expect void; } /// SUMMARY /// @@ -156,28 +143,6 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } -// Summary for every callback (token transfer, onLiquidate, onFlashLoan, onBuy, onSell). -// We keep arbitrary callback/token side effects reachable via HAVOC, but only prove healthiness before the -// outer call and after the successful outer call returns. -function genericCallback() { - address dummy; - env e; - - callback.callHavoc(e, dummy); -} - -function genericCallbackBool() returns (bool) { - bool result; - genericCallback(); - return result; -} - -function genericCallbackBytes32() returns (bytes32) { - bytes32 result; - genericCallback(); - return result; -} - //// RULES ////// // The remaining rules show that a healthy borrower cannot get unhealthy by calling any function of the contract. From 2c6cbede80852d98f3bd648c94f93bd8e6359aaa Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 10:17:07 +0000 Subject: [PATCH 06/10] certora: re-split take in Healthiness Fix failing Healthiness proof by excluding tracked take buyers from the generic stayHealthy rule. --- certora/specs/Healthiness.spec | 42 ++++++++++++++++++++++++++++++++-- 1 file changed, 40 insertions(+), 2 deletions(-) diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index b07385403..e541f78a2 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -143,6 +143,10 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } +definition takeSeller(address taker, Midnight.Offer offer) returns address = offer.buy ? taker : offer.maker; + +definition takeBuyer(address taker, Midnight.Offer offer) returns address = offer.buy ? offer.maker : taker; + //// RULES ////// // The remaining rules show that a healthy borrower cannot get unhealthy by calling any function of the contract. @@ -205,8 +209,42 @@ rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, ui assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } -// Show that the user stays healthy on any other function than liquidate. -rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector } { +// Show that the user stays healthy on take, if the user under consideration is the seller on the obligation under consideration. +rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { + useIsHealthyNoBitmap = false; + + require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; + + Midnight.Obligation globalObligation = getGlobalObligation(); + require equalsGlobalObligation(offer.obligation), "obligation matches"; + require takeSeller(taker, offer) == globalBorrower, "seller matches"; + + require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); + + assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; +} + +// Show that the user stays healthy on take, if the user is neither buyer nor seller on the obligation under consideration, +// or the obligation differs. +rule stayHealthyTakeOtherBorrower(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { + useIsHealthyNoBitmap = true; + + require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; + + Midnight.Obligation globalObligation = getGlobalObligation(); + require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; + + require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); + + assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; +} + +// Show that the user stays healthy on any other function than liquidate or take. +rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, Midnight.Signature, bytes32, bytes32[]).selector } { // for withdrawCollateral we choose isHealthy(); for all others we choose the bitmap-less implementation. useIsHealthyNoBitmap = (f.selector != sig:withdrawCollateral(Midnight.Obligation, uint256, uint256, address, address).selector); From abb338b0a4e2b89d28f62d2ccee8885bcbc0ed63 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 14:46:11 +0000 Subject: [PATCH 07/10] certora: fold take back into generic Healthiness rule Fix PR #665 by reverting the take-specific Healthiness split so take stays under the generic outer-call healthiness proof. Stacked on #645. --- certora/specs/Healthiness.spec | 42 ++-------------------------------- 1 file changed, 2 insertions(+), 40 deletions(-) diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index e541f78a2..b07385403 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -143,10 +143,6 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } -definition takeSeller(address taker, Midnight.Offer offer) returns address = offer.buy ? taker : offer.maker; - -definition takeBuyer(address taker, Midnight.Offer offer) returns address = offer.buy ? offer.maker : taker; - //// RULES ////// // The remaining rules show that a healthy borrower cannot get unhealthy by calling any function of the contract. @@ -209,42 +205,8 @@ rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, ui assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } -// Show that the user stays healthy on take, if the user under consideration is the seller on the obligation under consideration. -rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { - useIsHealthyNoBitmap = false; - - require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; - - Midnight.Obligation globalObligation = getGlobalObligation(); - require equalsGlobalObligation(offer.obligation), "obligation matches"; - require takeSeller(taker, offer) == globalBorrower, "seller matches"; - - require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; - - take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); - - assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; -} - -// Show that the user stays healthy on take, if the user is neither buyer nor seller on the obligation under consideration, -// or the obligation differs. -rule stayHealthyTakeOtherBorrower(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { - useIsHealthyNoBitmap = true; - - require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; - - Midnight.Obligation globalObligation = getGlobalObligation(); - require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; - - require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; - - take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); - - assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; -} - -// Show that the user stays healthy on any other function than liquidate or take. -rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, Midnight.Signature, bytes32, bytes32[]).selector } { +// Show that the user stays healthy on any other function than liquidate. +rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector } { // for withdrawCollateral we choose isHealthy(); for all others we choose the bitmap-less implementation. useIsHealthyNoBitmap = (f.selector != sig:withdrawCollateral(Midnight.Obligation, uint256, uint256, address, address).selector); From f2cf1925b057010acfed5a5ec54714170c68923f Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 15:22:27 +0000 Subject: [PATCH 08/10] certora: summarize take callbacks in Healthiness Assume no callback/token reentrancy in Healthiness so the outer-call property does not fail on take callback side effects. Stacked on #645. --- certora/specs/Healthiness.spec | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index b07385403..bb2e5f51a 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -24,6 +24,15 @@ methods { */ function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); + + // Assume no reentrancy: callbacks and token transfers do not re-enter Midnight. + function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET; + function _.onRepay(bytes32, Midnight.Obligation, uint256, address, bytes) external => NONDET; + function _.onLiquidate(bytes32, Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.onFlashLoan(address, uint256, bytes) external => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; } /// SUMMARY /// From 95033d95bf37099af798cc6e0efa4373220ba6c5 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 15:49:08 +0000 Subject: [PATCH 09/10] certora: exclude take buyers from Healthiness Keep the no-reentrancy summaries, but split take back out so Healthiness only tracks seller and unrelated borrowers. Stacked on #645. --- certora/specs/Healthiness.spec | 42 ++++++++++++++++++++++++++++++++-- 1 file changed, 40 insertions(+), 2 deletions(-) diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index bb2e5f51a..dd2dd90b8 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -152,6 +152,10 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } +definition takeSeller(address taker, Midnight.Offer offer) returns address = offer.buy ? taker : offer.maker; + +definition takeBuyer(address taker, Midnight.Offer offer) returns address = offer.buy ? offer.maker : taker; + //// RULES ////// // The remaining rules show that a healthy borrower cannot get unhealthy by calling any function of the contract. @@ -214,8 +218,42 @@ rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, ui assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; } -// Show that the user stays healthy on any other function than liquidate. -rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector } { +// Show that the user stays healthy on take, if the user under consideration is the seller on the obligation under consideration. +rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { + useIsHealthyNoBitmap = false; + + require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; + + Midnight.Obligation globalObligation = getGlobalObligation(); + require equalsGlobalObligation(offer.obligation), "obligation matches"; + require takeSeller(taker, offer) == globalBorrower, "seller matches"; + + require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); + + assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; +} + +// Show that the user stays healthy on take, if the user is neither buyer nor seller on the obligation under consideration, +// or the obligation differs. +rule stayHealthyTakeOtherBorrower(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiverIfTakerIsSeller, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) { + useIsHealthyNoBitmap = true; + + require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; + + Midnight.Obligation globalObligation = getGlobalObligation(); + require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; + + require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call"; + + take(e, units, taker, takerCallback, takerCallbackData, receiverIfTakerIsSeller, offer, signature, root, proof); + + assert callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy after call"; +} + +// Show that the user stays healthy on any other function than liquidate or take. +rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, Midnight.Signature, bytes32, bytes32[]).selector } { // for withdrawCollateral we choose isHealthy(); for all others we choose the bitmap-less implementation. useIsHealthyNoBitmap = (f.selector != sig:withdrawCollateral(Midnight.Obligation, uint256, uint256, address, address).selector); From 568e0b2f84dede99bc494dafa83528f1fc413b3f Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Mon, 6 Apr 2026 16:31:54 +0000 Subject: [PATCH 10/10] certora: exclude prelocked sellers from Healthiness Restrict the same-seller Healthiness rule to fresh take entries where the tracked seller is not already transiently liquidation-locked. Stacked on #645. --- certora/specs/Healthiness.spec | 2 ++ 1 file changed, 2 insertions(+) diff --git a/certora/specs/Healthiness.spec b/certora/specs/Healthiness.spec index dd2dd90b8..95643c011 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -8,6 +8,7 @@ methods { function collateral(bytes32 id, address user, uint256) external returns (uint128) envfree; function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; function isHealthyNoBitmap(Midnight.Obligation, bytes32, address) external returns (bool) envfree; + function liquidationLocked(bytes32, address) external returns (bool) envfree; /* Assumption: price does not change during rules. * Under this assumption we can prove that a healthy borrower cannot get unhealthy by @@ -227,6 +228,7 @@ rule stayHealthyTakeSameSeller(env e, uint256 units, address taker, address take Midnight.Obligation globalObligation = getGlobalObligation(); require equalsGlobalObligation(offer.obligation), "obligation matches"; require takeSeller(taker, offer) == globalBorrower, "seller matches"; + require !liquidationLocked(globalId, globalBorrower), "seller not transiently liquidation-locked"; require callIsHealthy(globalObligation, globalId, globalBorrower), "user is healthy before call";