Verif pre-liquidations repay

.github/workflows/certora.yml

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

certora/README.md

@@ -1,34 +1,22 @@
 # Pre-liquidation Contract Formal Verification
 
-This folder contains the
-[CVL](https://docs.certora.com/en/latest/docs/cvl/index.html)
-specification and verification setup for the
-[pre-liquidation](../src/PreLiquidation.sol) contract using the
-[Certora Prover](https://www.certora.com/).
+This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the [PreLiquidation](../src/PreLiquidation.sol) contract.
 
 ## Getting Started
 
-This project depends on two different versions of
-[Solidity](https://soliditylang.org/) which are required for running
-the verification. The compiler binaries should be available under the
-following path names:
+This project depends on two different versions of [Solidity](https://soliditylang.org/) which are required for running the verification.
+The compiler binaries should be available under the following path names:
 
-  - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is
-    used for `Morpho`;
-  - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
-    used for `PreLiquidation`.
+- `solc-0.8.19` for the solidity compiler version `0.8.19`, which is used for `Morpho`;
+- `solc-0.8.27` for the solidity compiler version `0.8.27`, which is used for `PreLiquidation`.
 
-To verifying a specification, run the command `certoraRun Spec.conf`
-where `Spec.conf` is the configuration file of the matching CVL
-specification. Configuration files are available in
-[`certora/conf`](./confs). Please ensure that `CERTORAKEY` is set up
-in your environment.
+To verify a specification, run the command `certoraRun Spec.conf`where `Spec.conf` is the configuration file of the matching CVL specification.
+Configuration files are available in [`certora/confs`](confs).
+Please ensure that `CERTORAKEY` is set up in your environment.
 
 ## Overview
 
-The PreLiquidation contract enables Morpho Blue borrowers to set up a
-safer liquidation plan on a given position, thus preventing undesired
-liquidations.
+The PreLiquidation contract enables Morpho borrowers to set up a safer liquidation plan on a given position, thus preventing undesired liquidations.
 
 ### Reentrancy
 
@@ -38,28 +26,22 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 
 This is checked in [`Immutability.spec`](specs/Immutability.spec).
 
+### Liveness properties
+
+This is checked in [`Liveness.spec`](specs/Liveness.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
 
 The [`certora/specs`](specs) folder contains the following files:
 
-- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that
-  PreLiquidation is reentrancy safe by checking that the storage is never
-  used.
-
-- [`Immutability.spec`](specs/Immutability.spec) checks that
-  PreLiquidation contract is immutable because it doesn't perform any
-  delegate call.
-
-The [`certora/confs`](confs) folder contains a configuration file for
-each corresponding specification file.
+- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that PreLiquidation is reentrancy safe by checking that the storage is never used;
+- [`Immutability.spec`](specs/Immutability.spec) checks that PreLiquidation contract is immutable because it doesn't perform any delegate call;
+- [`Liveness.spec`](specs/Liveness.spec) ensure that expected computations will always be performed.
+  For instance, pre-liquidations will always trigger a repay operation.
 
-The [`certora/helpers`](helpers) folder contains helper contracts that
-enable the verification of PreLiquidation. Notably, this allows
-handling the fact that library functions should be called from a
-contract to be verified independently, and it allows defining needed
-getters.
+The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
 
 ## TODO
 

certora/confs/Immutability.conf

@@ -1,16 +1,16 @@
 {
-    "files": [
-        "src/PreLiquidation.sol",
-    ],
-    "solc": "solc-0.8.27",
-    "solc_via_ir" : true,
-    "verify": "PreLiquidation:certora/specs/Immutability.spec",
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "PreLiquidation Immutability",
+  "files": [
+    "src/PreLiquidation.sol"
+  ],
+  "solc": "solc-0.8.27",
+  "solc_via_ir": true,
+  "verify": "PreLiquidation:certora/specs/Immutability.spec",
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Immutability"
 }

certora/confs/Liveness.conf

@@ -0,0 +1,31 @@
+{
+  "files": [
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/src/Morpho.sol"
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=Morpho"
+  ],
+  "parametric_contracts": [
+    "PreLiquidation"
+  ],
+  "solc_via_ir": true,
+  "verify": "PreLiquidation:certora/specs/Liveness.spec",
+  "solc_optimize_map": {
+    "Morpho": "99999",
+    "PreLiquidation": "99999"
+  },
+  "solc_map": {
+    "Morpho": "solc-0.8.19",
+    "PreLiquidation": "solc-0.8.27"
+  },
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120",
+    "-smt_nonLinearArithmetic true"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Liveness"
+}

certora/confs/Reentrancy.conf

@@ -1,17 +1,17 @@
 {
-    "files": [
-        "src/PreLiquidation.sol",
-    ],
-    "solc": "solc-0.8.27",
-    "solc_via_ir" : true,
-    "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
-    "prover_args": [
-        "-enableStorageSplitting false",
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "PreLiquidation Reentrancy",
+  "files": [
+    "src/PreLiquidation.sol"
+  ],
+  "solc": "solc-0.8.27",
+  "solc_via_ir": true,
+  "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
+  "prover_args": [
+    "-enableStorageSplitting false",
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Reentrancy"
 }

certora/specs/Liveness.spec

@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using PreLiquidation as preLiq;
+
+methods {
+    function preLiq.MORPHO() external returns address envfree;
+}
+
+// True when `preLiquidate` has been called.
+persistent ghost bool preLiquidateCalled;
+
+// True when `onMorphoRepay` has been called.
+persistent ghost bool onMorphoRepayCalled;
+
+hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
+    if (selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
+       preLiquidateCalled = true;
+    } else if (selector == sig:onMorphoRepay(uint256, bytes).selector) {
+       onMorphoRepayCalled = true;
+    }
+}
+
+// Check that pre-liquidations happen if and only if `onMorphoRepay` is called.
+rule preLiquidateRepays(method f, env e, calldataarg data) {
+
+    // Set up the initial state.
+    require !preLiquidateCalled;
+    require !onMorphoRepayCalled;
+
+    // Safe require because Morpho cannot send transactions.
+    require e.msg.sender != preLiq.MORPHO();
+
+    // Capture the first method call which is not performed with a CALL opcode.
+    if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
+       preLiquidateCalled = true;
+    } else if (f.selector == sig:onMorphoRepay(uint256, bytes).selector) {
+       onMorphoRepayCalled = true;
+    }
+
+    f@withrevert(e,data);
+
+    // Avoid failing vacuity checks, either the proposition is true or the execution reverts.
+    assert !lastReverted => (preLiquidateCalled <=> onMorphoRepayCalled);
+}

certora/specs/Reentrancy.spec

@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-
-
 // True when storage has been accessed with either a SSTORE or a SLOAD.
 persistent ghost bool hasAccessedStorage;