From beea950ecbbc23d300214bd8ad502381a1db880e Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 26 Sep 2024 18:06:34 +0200
Subject: [PATCH] feat: stay healthy liquidate with different markets

---
 certora/specs/Health.spec | 35 +++++++++++++++++++++++++++++++----
 1 file changed, 31 insertions(+), 4 deletions(-)

diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
index 58b4e4ce..3ff23803 100644
--- a/certora/specs/Health.spec
+++ b/certora/specs/Health.spec
@@ -80,14 +80,15 @@ filtered {
 
 // The liquidate case for the stayHealthy rule, assuming no bad debt realization, otherwise it times out.
 // This particular rule makes the following assumptions:
-//   - the market of the liquidation is the market of the user,
+//   - the market of the liquidation is the market of the user, see the *DifferentMarkets rule
 //   - there is still some borrow on the market after liquidation.
 rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
     MorphoHarness.Id id = libId(marketParams);
     address user;
 
-    // Assume that the position is healthy before the interaction.
+    // Assume the invariant initially.
     require isHealthy(marketParams, user);
+
     uint256 debtSharesBefore = borrowShares(id, user);
     uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
     // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec.
@@ -100,9 +101,9 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres
 
     // Safe require because of the invariant sumBorrowSharesCorrect.
     require borrowShares(id, user) <= totalBorrowShares(id);
-    // Handle the case where not everything was repaid.
+    // Assume that there is still some borrow on the market after liquidation.
     require totalBorrowAssets(id) > 0;
-    // Handle the case where the user has some collateral left.
+    // Assume no bad debt realization.
     require collateral(id, borrower) > 0;
 
     assert user != borrower;
@@ -114,6 +115,32 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres
     assert stillHealthy;
 }
 
+rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+    address user;
+    MorphoHarness.MarketParams liquidationMarketParams;
+
+    // Assume the invariant initially.
+    require isHealthy(marketParams, user);
+
+    // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec.
+    require marketParams.lltv < 10^18;
+    // Assumption to ensure that no interest is accumulated.
+    require lastUpdate(id) == e.block.timestamp;
+    // Assume that the liquidation is on a different market.
+    require liquidationMarketParams != marketParams;
+
+    liquidate(e, liquidationMarketParams, borrower, seizedAssets, 0, data);
+    require !priceChanged;
+
+    // Safe require because of the invariant sumBorrowSharesCorrect.
+    require borrowShares(id, user) <= totalBorrowShares(id);
+
+    bool stillHealthy = isHealthy(marketParams, user);
+    require !priceChanged;
+    assert stillHealthy;
+}
+
 // Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position.
 rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data)
 filtered { f -> !f.isView }