feat: ensure market exists

.github/workflows/certora.yml

@@ -17,6 +17,7 @@ jobs:
       matrix:
         conf:
           - Immutability
+          - MarketExists
           - Liveness
           - Reentrancy
           - Reverts

certora/README.md

@@ -28,7 +28,8 @@ This is checked in [`Immutability.spec`](specs/Immutability.spec).
 
 ## Invalid inputs trigger a revert operation
 
-This is checked in [`Revers.spec`](specs/Reverts.spec).
+This is checked in [`Reverts.spec`](specs/Reverts.spec) and [`MarketExists.spec`](specs/MarketExists.spec)
+
 
 ### Liveness properties
 
@@ -46,6 +47,7 @@ The [`certora/specs`](specs) folder contains the following files:
   For instance, pre-liquidations will always trigger a repay operation.
   We also check that pre-liquidation can successfully be performed by passing shares to be repaid instead of the collateral ammount to be seized.
 - [`Reverts.spec`](specs/Reverts.spec) checks the conditions for reverts and that inputs are correctly validated.
+- [`MarketExists.spec`](specs/MarketExists.spec) checks that PreLiquidations can be instanciated only if the target market exists.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
 

certora/confs/MarketExists.conf

@@ -0,0 +1,28 @@
+{
+  "files": [
+    "src/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/MarketExists.spec",
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation MarketExists"
+}

certora/specs/MarketExists.spec

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using Morpho as MORPHO;
+
+methods {
+    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
+    function MORPHO.market(PreLiquidation.Id) external
+      returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
+    function _.price() external => mockPrice() expect uint256;
+}
+
+persistent ghost uint256 lastTimestamp;
+
+hook TIMESTAMP uint newTimestamp {
+    // Safe require because timestamps are guaranteed to be increasing.
+    require newTimestamp >= lastTimestamp;
+    // Safe require as it corresponds to some time very far into the future.
+    require newTimestamp < 2^63;
+    lastTimestamp = newTimestamp;
+}
+
+function mockPrice() returns uint256 {
+    uint256 price;
+    return price;
+}
+
+function lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
+    mathint lastUpdate;
+    (_,_,_,_,lastUpdate,_) = MORPHO.market(id);
+    return lastUpdate != 0;
+}
+
+//Ensure constructor requirement.
+
+invariant marketExists()
+    lastUpdateIsNotNil(currentContract.ID);