fix: add getter and hashOfMarketParams invariant

certora/confs/ConsistentInstantiation.conf

@@ -1,19 +1,21 @@
 {
   "files": [
-    "src/PreLiquidation.sol",
+    "certora/helpers/PreLiquidationHarness.sol",
+    "certora/helpers/Util.sol",
     "lib/morpho-blue/src/Morpho.sol",
   ],
   "link": [
-    "PreLiquidation:MORPHO=Morpho",
+    "PreLiquidationHarness:MORPHO=Morpho",
   ],
-  "parametric_contracts" : ["PreLiquidation"],
+  "parametric_contracts" : ["PreLiquidationHarness"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
-    "PreLiquidation": "solc-0.8.27",
+    "PreLiquidationHarness": "solc-0.8.27",
+    "Util": "solc-0.8.27",
   },
-  "verify": "PreLiquidation:certora/specs/ConsistentInstantiation.spec",
+  "verify": "PreLiquidationHarness:certora/specs/ConsistentInstantiation.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 5",
@@ -23,5 +25,5 @@
   ],
   "rule_sanity": "basic",
   "server": "production",
-  "msg": "PreLiquidation ConsistentInstantiation",
+  "msg": "PreLiquidationHarness ConsistentInstantiation",
 }

certora/confs/Reverts.conf

@@ -1,19 +1,21 @@
 {
   "files": [
-    "src/PreLiquidation.sol",
+    "certora/helpers/PreLiquidationHarness.sol",
+    "certora/helpers/Util.sol",
     "lib/morpho-blue/src/Morpho.sol",
   ],
   "link": [
-    "PreLiquidation:MORPHO=Morpho",
+    "PreLiquidationHarness:MORPHO=Morpho",
   ],
-  "parametric_contracts" : ["PreLiquidation"],
+  "parametric_contracts" : ["PreLiquidationHarness"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
-    "PreLiquidation": "solc-0.8.27",
+    "PreLiquidationHarness": "solc-0.8.27",
+    "Util": "solc-0.8.27",
   },
-  "verify": "PreLiquidation:certora/specs/Reverts.spec",
+  "verify": "PreLiquidationHarness:certora/specs/Reverts.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 40",

certora/helpers/PreLiquidationHarness.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {PreLiquidation, Market, Position, Id, PreLiquidationParams} from "src/PreLiquidation.sol";
+
+contract PreLiquidationHarness is PreLiquidation {
+    constructor(address morpho, Id id, PreLiquidationParams memory _preLiquidationParams)
+        PreLiquidation(morpho, id, _preLiquidationParams)
+    {}
+
+    function market_(Id id) external view returns (Market memory) {
+        return MORPHO.market(id);
+    }
+
+    function position_(Id id, address borrower) external view returns (Position memory) {
+        return MORPHO.position(id, borrower);
+    }
+}

certora/helpers/Util.sol

@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {Id, MarketParams} from "src/PreLiquidation.sol";
+
+import {MarketParamsLib} from "lib/morpho-blue/src/libraries/MarketParamsLib.sol";
+
+contract Util {
+    using MarketParamsLib for MarketParams;
+
+    function libId(MarketParams memory marketParams) external pure returns (Id) {
+        return marketParams.id();
+    }
+}

certora/specs/ConsistentInstantiation.spec

@@ -2,8 +2,13 @@
 
 import "SummaryLib.spec";
 
+using Util as Util;
+
 methods {
-    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
+    function _.market(PreLiquidationHarness.Id) external => DISPATCHER(true);
+
+    function Util.libId(PreLiquidationHarness.MarketParams) external
+        returns PreLiquidationHarness.Id envfree;
 }
 
 //Ensure constructor requirements.
@@ -52,3 +57,12 @@ invariant preLIFConsistent()
         requireInvariant lltvNotZero();
     }
 }
+
+// Ensure that ID equals idToMarketParams(marketParams()).
+invariant hashOfMarketParamsOf()
+    Util.libId(summaryMarketParams()) == currentContract.ID
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}

certora/specs/Reverts.spec

@@ -4,6 +4,8 @@ import "ConsistentInstantiation.spec";
 
 methods {
     function _.price() external => mockPrice() expect uint256;
+    function market_(PreLiquidationHarness.Id) external
+        returns (PreLiquidationHarness.Market memory) envfree;
 
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivDown(a,b,c);
@@ -52,12 +54,12 @@ rule nonLiquidatablePositionReverts(env e, address borrower, uint256 seizedAsset
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
+    requireInvariant hashOfMarketParamsOf();
 
-    uint256 mLastUpdate;
-    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
     mathint ltv = getLtv(borrower);
 
@@ -75,11 +77,10 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    uint256 mLastUpdate;
-    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
     mathint ltv = getLtv(borrower);
 
@@ -93,22 +94,17 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
 
 // Check that a pre-liquidation that repays more shares than available or allowed by the preLCF reverts.
 rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
-    // Market values.
-    uint256 mTotalBorrowAssets;
-    uint256 mTotalBorrowShares;
-    uint256 mLastUpdate;
-
     // Position values.
     uint256 pBorrowShares;
 
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    (_, _, mTotalBorrowAssets, mTotalBorrowShares, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
     (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
 
@@ -126,8 +122,8 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
     mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, mockPrice(), ORACLE_PRICE_SCALE()));
 
     mathint repaidShares = summaryToSharesUp(summaryWDivUp(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
-                               mTotalBorrowAssets,
-                               mTotalBorrowShares);
+                                             m.totalBorrowAssets,
+                                             m.totalBorrowShares);
 
     mathint closeFactor = computeLinearCombination(ltv,
                                                    currentContract.LLTV,
@@ -148,17 +144,18 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
 
 // Check that repaying more shares than available or allowed by the preLCF would revert.
 rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 repaidShares, bytes data) {
+    // Position values.
+    uint256 pBorrowShares;
+
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    uint256 mLastUpdate;
-    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
-    uint256 pBorrowShares;
     (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
 
     mathint ltv = getLtv(borrower);

certora/specs/SummaryLib.spec

@@ -3,9 +3,7 @@
 using Morpho as MORPHO;
 
 methods {
-    function MORPHO.market(PreLiquidation.Id) external
-        returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
-    function MORPHO.position(PreLiquidation.Id, address) external
+    function MORPHO.position(PreLiquidationHarness.Id, address) external
         returns (uint256, uint128, uint128) envfree;
 }
 
@@ -40,7 +38,6 @@ function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
 
 }
 
-
 function summaryToAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
     return summaryMulDivDown(shares,
                              require_uint256(totalAssets + VIRTUAL_ASSETS()),
@@ -59,8 +56,8 @@ function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalSha
                            require_uint256(totalShares + VIRTUAL_SHARES()));
 }
 
-function summaryMarketParams() returns PreLiquidation.MarketParams {
-    PreLiquidation.MarketParams x;
+function summaryMarketParams() returns PreLiquidationHarness.MarketParams {
+    PreLiquidationHarness.MarketParams x;
     require
         x.loanToken == currentContract.LOAN_TOKEN
         && x.collateralToken == currentContract.COLLATERAL_TOKEN
@@ -86,23 +83,23 @@ function mockPrice() returns uint256 {
     return updatedPrice;
 }
 
-function positionAsAssets (address borrower) returns (uint256, uint256) {
-    uint256 mTotalBorrowAssets;
-    uint256 mTotalBorrowShares;
 
+// Ensure this function is only used when no interest is accrued,
+// or enforce that the last update matches the current timestamp.
+function positionAsAssets (address borrower) returns (uint256, uint256) {
     uint256 pBorrowShares;
     uint256 pCollateral;
 
-    (_, _, mTotalBorrowAssets, mTotalBorrowShares,_ , _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
+
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
 
-    uint256 collateralPrice = mockPrice();
-    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_PRICE_SCALE()));
+    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, mockPrice(), ORACLE_PRICE_SCALE()));
 
     // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
 
-    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, m.totalBorrowAssets, m.totalBorrowShares));
 
     return (borrowed, collateralQuoted);
 }