Merge pull request #37 from morpho-org/colin@verif/expected-reverts

[Certora] Verif expected reverts

.github/workflows/certora.yml

@@ -16,9 +16,12 @@ jobs:
 
       matrix:
         conf:
+          - ConsistentInstantiation
           - Immutability
+          - MarketExists
           - Liveness
           - Reentrancy
+          - Reverts
 
     steps:
       - uses: actions/checkout@v4

certora/README.md

@@ -26,6 +26,14 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 
 This is checked in [`Immutability.spec`](specs/Immutability.spec).
 
+## Reverts
+
+This is checked in [`Reverts.spec`](specs/Reverts.spec) and [`MarketExists.spec`](specs/MarketExists.spec)
+
+# Consitent Instantiation
+
+This is checked in [`ConsistentInstantiation.spec`](specs/ConsistentInstantiation.spec).
+
 ### Liveness properties
 
 This is checked in [`Liveness.spec`](specs/Liveness.spec).
@@ -41,6 +49,9 @@ 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.
+- [`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.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
 

certora/confs/ConsistentInstantiation.conf

@@ -0,0 +1,29 @@
+{
+  "files": [
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=MorphoHarness",
+  ],
+  "parametric_contracts" : ["PreLiquidation"],
+  "solc_optimize" : "99999",
+  "solc_via_ir" : true,
+  "solc_map": {
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+    "PreLiquidation": "solc-0.8.27",
+  },
+  "verify": "PreLiquidation:certora/specs/ConsistentInstantiation.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 ConsistentInstantiation",
+}

certora/confs/MarketExists.conf

@@ -0,0 +1,25 @@
+{
+  "files": [
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/src/Morpho.sol",
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=Morpho"
+  ],
+  "parametric_contracts" : ["Morpho"],
+  "solc_optimize" : "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,30 @@
+{
+  "files": [
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=MorphoHarness",
+  ],
+  "parametric_contracts" : ["PreLiquidation"],
+  "solc_optimize" : "99999",
+  "solc_via_ir" : true,
+  "solc_map": {
+    "PreLiquidation": "solc-0.8.27",
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+  },
+  "verify": "PreLiquidation:certora/specs/Reverts.spec",
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 40",
+    "-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/ConsistentInstantiation.spec

@@ -0,0 +1,66 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+import "SummaryLib.spec";
+
+methods {
+    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
+
+    function Util.libId(PreLiquidation.MarketParams) external
+        returns PreLiquidation.Id envfree;
+}
+
+//Ensure constructor requirements.
+
+// Base case for mutually dependent invariants.
+// Ensure that in a successfully deployed contract the preLLTV value is not zero.
+invariant lltvNotZero()
+    0 < currentContract.LLTV
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+// Ensure that a successfully deployed contract has a consistent preLLTV value.
+invariant preLltvConsistent()
+    currentContract.PRE_LLTV < currentContract.LLTV
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+// Ensure that a successfully deployed contract has a consistent preLCF values.
+invariant preLCFConsistent()
+    currentContract.PRE_LCF_1 <= currentContract.PRE_LCF_2
+    && currentContract.PRE_LCF_1 <= WAD()
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+// Base case for mutually dependent invariants.
+// Ensure that in a successfully deployed contract the preLIF value is not zero.
+invariant preLIFNotZero()
+    0 < currentContract.PRE_LIF_1;
+
+// Ensure that a successfully deployed contract has a consistent preLIF values.
+invariant preLIFConsistent()
+    WAD() < currentContract.PRE_LIF_1
+    && currentContract.PRE_LIF_1 <= currentContract.PRE_LIF_2
+    && currentContract.PRE_LIF_2 <= summaryWDivDown(WAD(),currentContract.LLTV)
+{
+    preserved {
+        requireInvariant lltvNotZero();
+    }
+}
+
+// Ensure that ID equals idToMarketParams(marketParams()).
+invariant hashOfMarketParamsOf()
+    Util.libId(summaryMarketParams()) == currentContract.ID
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}

certora/specs/MarketExists.spec

@@ -0,0 +1,31 @@
+// 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 => NONDET;
+}
+
+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 lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
+    mathint lastUpdate;
+    (_,_,_,_,lastUpdate,_) = MORPHO.market(id);
+    return lastUpdate != 0;
+}
+
+// Ensure that the pre-liquidation contract interacts with a created market.
+
+invariant marketExists()
+    lastUpdateIsNotNil(currentContract.ID);