[Certora] drop callback/token summaries

certora/confs/Healthiness.conf

@@ -1,7 +1,6 @@
 {
   "files": [
-    "certora/helpers/MidnightWrapper.sol",
-    "certora/helpers/Havoc.sol"
+    "certora/helpers/MidnightWrapper.sol"
   ],
   "parametric_contracts": [
     "MidnightWrapper"

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,18 +200,13 @@ 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;
 
-    // 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";
 }