[Certora] Stay healthy liquidate

.github/workflows/certora.yml

@@ -26,6 +26,7 @@ jobs:
           - Liveness
           - Reentrancy
           - Reverts
+          - StayHealthy
           - Transfer
 
     steps:

certora/README.md

@@ -250,12 +250,13 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division.
   Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start.
 - [`Health.spec`](specs/Health.spec) checks properties about the health of the positions.
-  Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism).
+  Notably, debt positions always have some collateral thanks to the bad debt realization mechanism.
 - [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files.
 - [`Liveness.spec`](specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position.
 - [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate between shares and assets evolves predictably over time.
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues.
 - [`Reverts.spec`](specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated.
+- [`StayHealthy.spec`](specs/Health.spec) checks that functions cannot render an account unhealthy.
 - [`Transfer.spec`](specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.

certora/confs/AccrueInterest.conf

@@ -6,8 +6,8 @@
     "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
     "prover_args": [
         "-depth 3",
-        "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30",
+        "-smt_hashingScheme plaininjectivity",
     ],
     "rule_sanity": "basic",
     "server": "production",

certora/confs/StayHealthy.conf

@@ -0,0 +1,18 @@
+{
+	"files": [
+		"certora/harness/MorphoHarness.sol",
+		"src/mocks/OracleMock.sol",
+	],
+	"msg": "Morpho Blue Stay Healthy",
+	"process": "emv",
+	"prover_args": [
+		"-depth 5",
+		"-mediumTimeout 5",
+		"-timeout 3600",
+		"-smt_hashingScheme plaininjectivity"
+	],
+	"rule_sanity": "basic",
+	"server": "production",
+	"solc": "solc-0.8.19",
+	"verify": "MorphoHarness:certora/specs/StayHealthy.spec"
+}

certora/specs/Health.spec

@@ -2,7 +2,10 @@
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
 
+    function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
     function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
+    function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
+    function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
     function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
@@ -46,35 +49,6 @@ function summaryMin(uint256 a, uint256 b) returns uint256 {
     return a < b ? a : b;
 }
 
-// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one.
-// The liquidate function times out in this rule, but has been checked separately.
-rule stayHealthy(env e, method f, calldataarg data)
-filtered {
-    f -> !f.isView &&
-    f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector
-}
-{
-    MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = libId(marketParams);
-    address user;
-
-    // Assume that the position is healthy before the interaction.
-    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;
-
-    priceChanged = false;
-    f(e, data);
-
-    // Safe require because of the invariant sumBorrowSharesCorrect.
-    require borrowShares(id, user) <= totalBorrowShares(id);
-
-    bool stillHealthy = isHealthy(marketParams, user);
-    assert !priceChanged => 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 }

certora/specs/StayHealthy.spec

@@ -0,0 +1,118 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+import "Health.spec";
+
+// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one.
+// The liquidate function times out in this rule, but has been checked separately.
+rule stayHealthy(env e, method f, calldataarg data)
+filtered {
+    f -> !f.isView &&
+    f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector
+}
+{
+    MorphoHarness.MarketParams marketParams;
+    MorphoHarness.Id id = libId(marketParams);
+    address user;
+
+    // Assume that the position is healthy before the interaction.
+    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;
+
+    f(e, data);
+
+    // Safe require because of the invariant sumBorrowSharesCorrect.
+    require borrowShares(id, user) <= totalBorrowShares(id);
+
+    bool stillHealthy = isHealthy(marketParams, user);
+    assert !priceChanged => stillHealthy;
+}
+
+// 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, see the *DifferentMarkets rule,
+//   - there is still some borrow on the market after liquidation, see the *LastBorrow rule.
+rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+    address user;
+
+    // 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.
+    require marketParams.lltv < 10^18;
+    // Assumption to ensure that no interest is accumulated.
+    require lastUpdate(id) == e.block.timestamp;
+
+    liquidate(e, marketParams, borrower, seizedAssets, 0, data);
+    require !priceChanged;
+
+    // Safe require because of the invariant sumBorrowSharesCorrect.
+    require borrowShares(id, user) <= totalBorrowShares(id);
+    // Assume that there is still some borrow on the market after liquidation.
+    require totalBorrowAssets(id) > 0;
+    // Assume no bad debt realization.
+    require collateral(id, borrower) > 0;
+
+    assert user != borrower;
+    assert debtSharesBefore == borrowShares(id, user);
+    assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
+
+    bool stillHealthy = isHealthy(marketParams, user);
+    require !priceChanged;
+    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;
+}
+
+rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+    address user;
+
+    // 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;
+
+    liquidate(e, marketParams, borrower, seizedAssets, 0, data);
+    require !priceChanged;
+
+    // Safe require because of the invariant sumBorrowSharesCorrect.
+    require borrowShares(id, user) <= totalBorrowShares(id);
+    // Assume that there is no remaining borrow on the market after liquidation.
+    require totalBorrowAssets(id) == 0;
+
+    bool stillHealthy = isHealthy(marketParams, user);
+    require !priceChanged;
+    assert stillHealthy;
+}