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 2508dca37..95643c011 100644 --- a/certora/specs/Healthiness.spec +++ b/certora/specs/Healthiness.spec @@ -2,14 +2,13 @@ import "BitmapSummaries.spec"; -using Havoc as callback; - methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; 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 @@ -26,15 +25,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); - 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. + 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 /// @@ -94,9 +93,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; - // global variable to track which obligation and borrower we're testing. persistent ghost address globalObligationLoanToken; @@ -157,37 +153,9 @@ function callIsHealthy(Midnight.Obligation obligation, bytes32 id, address borro } } -// 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. -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); - - 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"; -} - -// Same as the summary above except that it also returns a non-deterministic value. -function genericCallbackBool() returns (bool) { - bool result; - genericCallback(); - return result; -} +definition takeSeller(address taker, Midnight.Offer offer) returns address = offer.buy ? taker : offer.maker; -function genericCallbackBytes32() returns (bytes32) { - bytes32 result; - genericCallback(); - return result; -} +definition takeBuyer(address taker, Midnight.Offer offer) returns address = offer.buy ? offer.maker : taker; //// RULES ////// @@ -203,9 +171,6 @@ function genericCallbackBytes32() returns (bytes32) { rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 seizedAssetsIn, uint256 repaidUnitsIn, bytes data) { useIsHealthyNoBitmap = 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"; require globalObligationCollateralLength <= 2, "too many collateralParams for the spec to handle"; @@ -235,8 +200,6 @@ 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"; } @@ -244,9 +207,6 @@ rule stayHealthyLiquidateSameBorrower(env e, uint256 collateralIndex, uint256 se rule stayHealthyLiquidateOtherBorrower(env e, Midnight.Obligation obligation, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { useIsHealthyNoBitmap = true; - // 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"; Midnight.Obligation globalObligation = getGlobalObligation(); @@ -256,18 +216,49 @@ 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. +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 !liquidationLocked(globalId, globalBorrower), "seller not transiently liquidation-locked"; + + 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 withdraw collateral we choose isHealthy() for all others the isHealthyNoBitmap function. + // 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); - // 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"; require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; @@ -278,6 +269,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"; }