[Certora] Verif expected reverts

.github/workflows/certora.yml

@@ -17,8 +17,10 @@ jobs:
       matrix:
         conf:
           - Immutability
+          - MarketExists
           - Liveness
           - Reentrancy
+          - Reverts
 
     steps:
       - uses: actions/checkout@v4

certora/README.md

@@ -26,6 +26,11 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 
 This is checked in [`Immutability.spec`](specs/Immutability.spec).
 
+## Invalid inputs trigger a revert operation
+
+This is checked in [`Reverts.spec`](specs/Reverts.spec) and [`MarketExists.spec`](specs/MarketExists.spec)
+
+
 ### Liveness properties
 
 This is checked in [`Liveness.spec`](specs/Liveness.spec).
@@ -41,6 +46,8 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`Liveness.spec`](specs/Liveness.spec) ensure that expected computations will always be performed.
   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/confs/Reverts.conf

@@ -0,0 +1,31 @@
+{
+  "files": [
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/src/Morpho.sol",
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=Morpho",
+  ],
+  "parametric_contracts" : ["PreLiquidation"],
+  "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/Reverts.spec",
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 5",
+    "-timeout 3600",
+    "-smt_nonLinearArithmetic 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 Reverts",
+}

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);