feat: verify health position can't worsen

.github/workflows/certora.yml

@@ -17,6 +17,7 @@ jobs:
       matrix:
         conf:
           - ConsistentInstantiation
+          - Health
           - Immutability
           - MarketExists
           - Liveness
@@ -48,6 +49,9 @@ jobs:
           chmod +x solc-static-linux
           sudo mv solc-static-linux /usr/local/bin/solc-0.8.27
 
+      - name: Apply munging
+        run: make -C certora munged
+
       - name: Verify ${{ matrix.conf }} specification
         run: certoraRun certora/confs/${{ matrix.conf }}.conf
         env:

certora/Makefile

@@ -0,0 +1,12 @@
+munged: $(wildcard ../src/*.sol) applyMunging.patch
+	@rm -rf munged
+	@cp -r ../src munged
+	@patch -p0 -d munged < applyMunging.patch
+
+record:
+	diff -ruN ../src munged | sed 's+\.\./src/++g' | sed 's+munged/++g' > applyMunging.patch
+
+clean:
+	rm -rf munged
+
+.PHONY: help clean # do not add munged here, as it is useful to protect munged edits

certora/README.md

@@ -38,6 +38,10 @@ This is checked in [`ConsistentInstantiation.spec`](specs/ConsistentInstantiatio
 
 This is checked in [`Liveness.spec`](specs/Liveness.spec).
 
+### Position health properties
+
+This is checked in [`Health.spec`](specs/Health.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
@@ -52,9 +56,12 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`Reverts.spec`](specs/Reverts.spec) checks the conditions for reverts and that inputs are correctly validated.
 - [`ConsistentInstantiation.spec`](specs/ConsistentInstantiation.spec) checks the conditions for reverts are met in PreLiquidation constructor.
 - [`MarketExists.spec`](specs/MarketExists.spec) checks that PreLiquidations can be instanciated only if the target market exists.
+- [`Health.spec`](specs/Health.spec) checks that after a pre-liquidations can't worsen.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
 
+The_[`certora/Makefile`](Makefile)_file is used to perform munging on the original sources.
+
 ## TODO
 
 - [ ] Provide an overview of the specification.

certora/applyMunging.patch

@@ -0,0 +1,140 @@
+diff -ruN PreLiquidation.sol PreLiquidation.sol
+--- PreLiquidation.sol	2024-10-07 11:26:46.000000000 +0200
++++ PreLiquidation.sol	2024-10-21 20:49:12.000000000 +0200
+@@ -1,20 +1,21 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity 0.8.27;
+
+-import {Id, MarketParams, IMorpho, Position, Market} from "../lib/morpho-blue/src/interfaces/IMorpho.sol";
+-import {IMorphoRepayCallback} from "../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
++import {Id, MarketParams, IMorpho, Position, Market} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {IMorphoRepayCallback} from "../../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
+ import {IPreLiquidation, PreLiquidationParams} from "./interfaces/IPreLiquidation.sol";
+ import {IPreLiquidationCallback} from "./interfaces/IPreLiquidationCallback.sol";
+-import {IOracle} from "../lib/morpho-blue/src/interfaces/IOracle.sol";
++import {IOracle} from "../../lib/morpho-blue/src/interfaces/IOracle.sol";
+
+-import {ORACLE_PRICE_SCALE} from "../lib/morpho-blue/src/libraries/ConstantsLib.sol";
+-import {SharesMathLib} from "../lib/morpho-blue/src/libraries/SharesMathLib.sol";
+-import {SafeTransferLib} from "../lib/solmate/src/utils/SafeTransferLib.sol";
+-import {WAD, MathLib} from "../lib/morpho-blue/src/libraries/MathLib.sol";
+-import {UtilsLib} from "../lib/morpho-blue/src/libraries/UtilsLib.sol";
+-import {ERC20} from "../lib/solmate/src/tokens/ERC20.sol";
++import {ORACLE_PRICE_SCALE} from "../../lib/morpho-blue/src/libraries/ConstantsLib.sol";
++import {SharesMathLib} from "../../lib/morpho-blue/src/libraries/SharesMathLib.sol";
++import {SafeTransferLib} from "../../lib/solmate/src/utils/SafeTransferLib.sol";
++import {WAD, MathLib} from "../../lib/morpho-blue/src/libraries/MathLib.sol";
++import {UtilsLib} from "../../lib/morpho-blue/src/libraries/UtilsLib.sol";
++import {ERC20} from "../../lib/solmate/src/tokens/ERC20.sol";
+ import {EventsLib} from "./libraries/EventsLib.sol";
+ import {ErrorsLib} from "./libraries/ErrorsLib.sol";
++import "../../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
+
+ /// @title PreLiquidation
+ /// @author Morpho Labs
+@@ -25,6 +26,12 @@
+     using MathLib for uint256;
+     using SafeTransferLib for ERC20;
+
++    using MarketParamsLib for MarketParams;
++
++    function libId(MarketParams memory marketParams) external pure returns (Id) {
++        return marketParams.id();
++    }
++
+     /* IMMUTABLE */
+
+     /// @notice The address of the Morpho contract.
+@@ -47,6 +54,9 @@
+     uint256 internal immutable PRE_LIF_2;
+     address internal immutable PRE_LIQUIDATION_ORACLE;
+
++    uint256 public lastLtv;
++    uint256 public lastLtvAfter;
++
+     /// @notice The Morpho market parameters specific to the PreLiquidation contract.
+     function marketParams() public view returns (MarketParams memory) {
+         return MarketParams({
+@@ -142,6 +152,7 @@
+
+         uint256 collateralPrice = IOracle(PRE_LIQUIDATION_ORACLE).price();
+         uint256 collateralQuoted = uint256(position.collateral).mulDivDown(collateralPrice, ORACLE_PRICE_SCALE);
++
+         uint256 borrowed = uint256(position.borrowShares).toAssetsUp(market.totalBorrowAssets, market.totalBorrowShares);
+
+         // The two following require-statements ensure that collateralQuoted is different from zero.
+@@ -150,11 +161,11 @@
+         require(borrowed > collateralQuoted.wMulDown(PRE_LLTV), ErrorsLib.NotPreLiquidatablePosition());
+
+         uint256 ltv = borrowed.wDivUp(collateralQuoted);
++        lastLtv = ltv;
+         uint256 preLIF = (ltv - PRE_LLTV).wDivDown(LLTV - PRE_LLTV).wMulDown(PRE_LIF_2 - PRE_LIF_1) + PRE_LIF_1;
+
+         if (seizedAssets > 0) {
+             uint256 seizedAssetsQuoted = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE);
+-
+             repaidShares =
+                 seizedAssetsQuoted.wDivUp(preLIF).toSharesUp(market.totalBorrowAssets, market.totalBorrowShares);
+         } else {
+@@ -173,8 +184,13 @@
+         bytes memory callbackData = abi.encode(seizedAssets, borrower, msg.sender, data);
+         (uint256 repaidAssets,) = MORPHO.repay(marketParams(), 0, repaidShares, borrower, callbackData);
+
+-        emit EventsLib.PreLiquidate(ID, msg.sender, borrower, repaidAssets, repaidShares, seizedAssets);
++        uint256 collateralQuotedAfter =
++            MathLib.mulDivDown(position.collateral - seizedAssets, collateralPrice, ORACLE_PRICE_SCALE);
++        require(collateralQuotedAfter > 0, "division by zero");
++        uint256 borrowedAfter = borrowed - repaidAssets;
++        lastLtvAfter = borrowedAfter.wDivDown(collateralQuotedAfter);
+
++        emit EventsLib.PreLiquidate(ID, msg.sender, borrower, repaidAssets, repaidShares, seizedAssets);
+         return (seizedAssets, repaidAssets);
+     }
+
+diff -ruN interfaces/IPreLiquidation.sol interfaces/IPreLiquidation.sol
+--- interfaces/IPreLiquidation.sol	2024-10-07 11:26:46.000000000 +0200
++++ interfaces/IPreLiquidation.sol	2024-10-14 21:45:26.000000000 +0200
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity >= 0.5.0;
+
+-import {Id, IMorpho, MarketParams} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {Id, IMorpho, MarketParams} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
+
+ /// @notice The pre-liquidation parameters are:
+ ///  - preLltv, the maximum LTV of a position before allowing pre-liquidation.
+@@ -20,8 +20,9 @@
+ }
+
+ interface IPreLiquidation {
+-    function MORPHO() external view returns (IMorpho);
++    function libId(MarketParams memory) external returns (Id);
+
++    function MORPHO() external view returns (IMorpho);
+     function ID() external view returns (Id);
+
+     function marketParams() external returns (MarketParams memory);
+diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
+--- libraries/EventsLib.sol	2024-10-07 11:26:46.000000000 +0200
++++ libraries/EventsLib.sol	2024-10-11 14:02:26.000000000 +0200
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity ^0.8.0;
+
+-import {Id} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {Id} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
+ import {PreLiquidationParams} from "../interfaces/IPreLiquidation.sol";
+
+ /// @title EventsLib
+diff -ruN libraries/periphery/PreLiquidationAddressLib.sol libraries/periphery/PreLiquidationAddressLib.sol
+--- libraries/periphery/PreLiquidationAddressLib.sol	2024-10-07 11:26:46.000000000 +0200
++++ libraries/periphery/PreLiquidationAddressLib.sol	2024-10-11 13:55:21.000000000 +0200
+@@ -3,7 +3,7 @@
+
+ import {PreLiquidation} from "../../PreLiquidation.sol";
+ import {PreLiquidationParams} from "../../interfaces/IPreLiquidation.sol";
+-import {Id} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {Id} from "../../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
+
+ library PreLiquidationAddressLib {
+     /// @notice Computes the CREATE2 address of the pre-liquidation contract generated by the `factory`

certora/confs/Health.conf

@@ -0,0 +1,32 @@
+{
+  "files": [
+    "certora/munged/PreLiquidation.sol",
+    "lib/morpho-blue/src/Morpho.sol",
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=Morpho"
+  ],
+  "parametric_contracts": ["Morpho"],
+  "solc_optimize_map" : {
+    "Morpho" : "99999",
+    "PreLiquidation" : "99999",
+  },
+  "solc_via_ir" : true,
+  "solc_map": {
+    "Morpho": "solc-0.8.19",
+    "PreLiquidation": "solc-0.8.27",
+  },
+  "verify": "PreLiquidation:certora/specs/Health.spec",
+  "rule": ["positionDoesntDegrade"],
+  "prover_args": [
+    "-depth 8",
+    "-mediumTimeout 40",
+    "-timeout 3600",
+    "-smt_nonLinearArithmetic true",
+    "-smt_easy_LIA true",
+    "-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:lia2]",
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Health"
+}

certora/specs/Health.spec

@@ -0,0 +1,118 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+import "ConsistentInstantiation.spec";
+import "SummaryLib.spec";
+
+using Morpho as MORPHO;
+
+methods {
+    function _.onMorphoRepay(uint256,bytes) external => DISPATCHER(true);
+    function _.price() external => mockPrice() expect uint256;
+
+    function marketParams() internal returns (PreLiquidation.MarketParams memory)
+        => summaryMarketParams();
+    function lastLtv() external returns uint256 envfree;
+    function lastLtvAfter() external returns uint256 envfree;
+
+    function MORPHO.market(PreLiquidation.Id) external
+      returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
+    function MORPHO.position(PreLiquidation.Id, address) external
+      returns (uint256, uint128, uint128) envfree;
+    function MORPHO.repay(PreLiquidation.MarketParams marketParams,
+                           uint256 assets,
+                           uint256 shares,
+                           address onBehalf,
+                           bytes data
+                          ) external returns (uint256, uint256)
+        => summaryMorphoRepay(marketParams, assets, shares, onBehalf,data);
+    function MORPHO.extSloads(bytes32[]) external
+        returns bytes32[] => NONDET DELETE;
+    function MORPHO.accrueInterest(PreLiquidation.MarketParams) external =>
+        CONSTANT;
+
+    function UtilsLib.exactlyOneZero(uint256 a, uint256 b) internal
+        returns bool => summaryExactlyOneZero(a,b);
+
+    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => summaryMulDivDown(a,b,c) ALL;
+    function MathLib.wMulDown(uint256 a, uint256 b) internal
+        returns uint256 => summaryWMulDown(a,b) ALL;
+    function MathLib.wDivUp(uint256 a, uint256 b) internal
+        returns uint256 => summaryWDivUp(a,b) ALL;
+    function MathLib.wDivDown(uint256 a, uint256 b) internal
+        returns uint256 => summaryWDivDown(a,b) ALL;
+    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => summaryMulDivUp(a,b,c) ALL;
+
+    function SharesMathLib.toSharesUp(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => summaryToSharesUp(a,b,c);
+    function SharesMathLib.toAssetsUp(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => summaryToAssetsUp(a,b,c);
+    function SharesMathLib.toAssetsDown(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => summaryToAssetsDown(a,b,c);
+
+    function libId(PreLiquidation.MarketParams) external returns PreLiquidation.Id envfree;
+}
+
+function summaryMorphoRepay(
+                            PreLiquidation.MarketParams marketParams,
+                            uint256 assets,
+                            uint256 shares,
+                            address onBehalf,
+                            bytes data
+) returns (uint256, uint256)
+{
+    uint256 mTotalBorrowAssets;
+    uint256 mTotalBorrowShares;
+    uint256 mLastUpdate;
+
+    uint256 repaidAssets;
+
+    assert libId(marketParams) == currentContract.ID;
+    assert assets == 0;
+    assert shares != 0;
+    assert data.length != 0;
+    require onBehalf != 0;
+
+    (_, _, mTotalBorrowAssets, mTotalBorrowShares, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    // assert mLastUpdate > 0;
+
+    repaidAssets = summaryToAssetsUp(shares, mTotalBorrowAssets, mTotalBorrowShares);
+
+    return (repaidAssets, shares);
+}
+
+// Check correctness of applying idToMarketParams() to an identifier.
+invariant hashOfMarketParamsOf()
+    libId(summaryMarketParams()) == currentContract.ID
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+rule positionDoesntDegrade(env e,address borrower, uint256 seizedAssets, bytes data) {
+    // Market value.
+    uint256 mLastUpdate;
+
+    // Avoid division by zero.
+    requireInvariant preLltvConsistent();
+    requireInvariant preLCFConsistent();
+    requireInvariant preLIFConsistent();
+
+    // Ensure consisitent positions.
+    requireInvariant hashOfMarketParamsOf();
+
+    // Ensure no callback is performed.
+    require data.lenght == 0;
+
+    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+
+    // Ensure that no interest is accumulated.
+    require mLastUpdate == e.block.timestamp;
+
+    preLiquidate(e, borrower, seizedAssets, 0, data);
+
+    require !priceChanged;
+    assert lastLtvAfter() <= lastLtv();
+}