[Certora] Liquidate buffer, with executable code

.github/workflows/certora.yml

@@ -23,6 +23,7 @@ jobs:
           - ExchangeRate
           - Health
           - LibSummary
+          - LiquidateBuffer
           - Liveness
           - Reentrancy
           - Reverts

certora/README.md

@@ -95,7 +95,7 @@ where `sumSupplyShares` only exists in the specification, and is defined to be a
 To ensure proper collateralization, a liquidation system is put in place, where unhealthy positions can be liquidated.
 A position is said to be healthy if the ratio of the borrowed value over collateral value is smaller than the liquidation loan-to-value (LLTV) of that market.
 This leaves a safety buffer before the position can be insolvent, where the aforementioned ratio is above 1.
-To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected.
+To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected and that it leaves room for healthy liquidations to happen.
 Notably, it is verified that in the absence of accrued interest, which is the case when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy.
 
 Let's define bad debt of a position as the amount borrowed when it is backed by no collateral.
@@ -249,11 +249,12 @@ The [`certora/specs`](specs) folder contains the following files:
   This includes checking that the accounting of the total amount and shares is correct, that markets are independent from each other, that only enabled IRMs and LLTVs can be used, and that users cannot have their position made worse by an unauthorized account.
 - [`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.
+- [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate between shares and assets evolves predictably over time.
 - [`Health.spec`](specs/Health.spec) checks properties about the health of the positions.
   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.
+- [`LiquidateBuffer.spec`](specs/LiquidateBuffer.spec) checks that there is a buffer for liquidatable positions, before they are insolvent, such that liquidation leads to healthier position and cannot lead to bad debt.
 - [`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.

certora/confs/LiquidateBuffer.conf

@@ -0,0 +1,21 @@
+{
+  "files": [
+    "certora/helpers/MorphoHarness.sol",
+    "certora/helpers/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoHarness:certora/specs/LiquidateBuffer.spec",
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 20",
+    "-timeout 3600",
+    "-adaptiveSolverConfig false",
+    "-smt_nonLinearArithmetic true",
+    "-destructiveOptimizations twostage",
+    "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+  ],
+  "multi_assert_check": true,
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Liquidate Buffer"
+}

certora/helpers/Util.sol

@@ -8,6 +8,7 @@ import "../../src/libraries/UtilsLib.sol";
 
 contract Util {
     using MarketParamsLib for MarketParams;
+    using MathLib for uint256;
 
     function wad() external pure returns (uint256) {
         return WAD;
@@ -17,6 +18,15 @@ contract Util {
         return MAX_FEE;
     }
 
+    function oraclePriceScale() external pure returns (uint256) {
+        return ORACLE_PRICE_SCALE;
+    }
+
+    function lif(uint256 lltv) external pure returns (uint256) {
+        return
+            UtilsLib.min(MAX_LIQUIDATION_INCENTIVE_FACTOR, WAD.wDivDown(WAD - LIQUIDATION_CURSOR.wMulDown(WAD - lltv)));
+    }
+
     function libId(MarketParams memory marketParams) external pure returns (Id) {
         return marketParams.id();
     }

certora/specs/LiquidateBuffer.spec

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using Util as Util;
+
+methods {
+    function extSloads(bytes32[]) external returns (bytes32[]) => NONDET DELETE;
+
+    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;
+    function totalBorrowShares(MorphoHarness.Id) external returns (uint256) envfree;
+    function totalBorrowAssets(MorphoHarness.Id) external returns (uint256) envfree;
+    function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
+    function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
+
+    function Util.libId(MorphoHarness.MarketParams) external returns (MorphoHarness.Id) envfree;
+    function Util.lif(uint256) external returns (uint256) envfree;
+    function Util.oraclePriceScale() external returns (uint256) envfree;
+    function Util.wad() external returns (uint256) envfree;
+
+    function Morpho._isHealthy(MorphoHarness.MarketParams memory, MorphoHarness.Id,address) internal returns (bool) => NONDET;
+    function Morpho._accrueInterest(MorphoHarness.MarketParams memory, MorphoHarness.Id) internal => NONDET;
+
+    function _.price() external => constantPrice expect uint256;
+}
+
+persistent ghost uint256 constantPrice;
+
+// Check that for a position with LTV < 1 / LIF, its health improves after a liquidation.
+rule liquidateImprovePosition(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssetsInput, uint256 repaidSharesInput, bytes data) {
+    // Assume no callback.
+    require data.length == 0;
+
+    MorphoHarness.Id id = Util.libId(marketParams);
+
+    // We place ourselves at the last block for getting the following variables.
+    require lastUpdate(id) == e.block.timestamp;
+
+    uint256 borrowerShares = borrowShares(id, borrower);
+    // Safe require because of the sumBorrowSharesCorrect invariant.
+    require borrowerShares <= totalBorrowShares(id);
+
+    uint256 borrowerCollateral = collateral(id, borrower);
+    uint256 lif = Util.lif(marketParams.lltv);
+    uint256 virtualTotalAssets = virtualTotalBorrowAssets(id);
+    uint256 virtualTotalShares = virtualTotalBorrowShares(id);
+
+    // Let borrowerAssets = borrowerShares * virtualTotalAssets / virtualTotalShares
+    // and borrowerCollateralQuoted = borrowerCollateral * constantPrice / Util.oraclePriceScale()
+    // then the following line is the assumption borrowerAssets / borrowerCollateralQuoted < 1 / LIF.
+    require borrowerCollateral * constantPrice * virtualTotalShares * Util.wad() > borrowerShares * Util.oraclePriceScale() * virtualTotalAssets * lif;
+
+    uint256 seizedAssets;
+    (seizedAssets, _) = liquidate(e, marketParams, borrower, seizedAssetsInput, repaidSharesInput, data);
+
+    uint256 newBorrowerShares = borrowShares(id, borrower);
+    uint256 newBorrowerCollateral = collateral(id, borrower);
+    uint256 repaidShares = assert_uint256(borrowerShares - newBorrowerShares);
+    uint256 newVirtualTotalAssets = virtualTotalBorrowAssets(id);
+    uint256 newVirtualTotalShares = virtualTotalBorrowShares(id);
+
+    // Hint for the prover to show that there is no bad debt realization.
+    assert newBorrowerCollateral != 0;
+    // Hint for the prover about the ratio used to close the position.
+    assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;
+    // Prove that the ratio of shares of debt over collateral is smaller after the liquidation.
+    assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
+    // Prove that the value of borrow shares is smaller after the liquidation.
+    // Note that this is only shown for the case where there are still borrow positions on the markets.
+    assert totalBorrowAssets(id) > 0 => newVirtualTotalShares * virtualTotalAssets >= newVirtualTotalAssets * virtualTotalShares;
+}