From f96a3de7aa3e9d296c6e10e16bc55174661d2a51 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 24 Sep 2024 12:31:21 +0200
Subject: [PATCH 01/26] feat: draft should revert spec

---
 certora/confs/Reverts.conf | 24 ++++++++++++++++++++++++
 certora/specs/Reverts.spec | 17 +++++++++++++++++
 2 files changed, 41 insertions(+)
 create mode 100644 certora/confs/Reverts.conf
 create mode 100644 certora/specs/Reverts.spec

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
new file mode 100644
index 0000000..9a3c97e
--- /dev/null
+++ b/certora/confs/Reverts.conf
@@ -0,0 +1,24 @@
+{
+    "files": [
+        "certora/helpers/PreLiquidationHarness.sol",
+        "lib/morpho-blue/src/Morpho.sol",
+    ],
+    "link": [
+     "PreLiquidationHarness:MORPHO=Morpho",
+     ],
+    "solc_via_ir" : true,
+    "solc_experimental_via_ir" : true,
+    "solc_map": {
+        "Morpho": "solc-0.8.19",
+        "PreLiquidationHarness": "solc-0.8.27",
+    },
+    "verify": "PreLiquidationHarness:certora/specs/Reverts.spec",
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "PreLiquidation Reverts",
+}
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
new file mode 100644
index 0000000..c699551
--- /dev/null
+++ b/certora/specs/Reverts.spec
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+methods {
+    function _.market(Id) external returns (Market memory);
+}
+
+definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
+    (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
+
+invariant marketExists()
+    MORPHO.market(currentContract.ID()).lastUpdate != 0;
+
+
+// Check that preliquidate reverts when its inputs are not validated.
+rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
+    preLiquidate@withrevert(e, borrower, seizedAssets, repaidShares, data);
+    assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted;
+}

From 2ccb6656c17719a0feaeff7ba4bf85087c06d185 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 24 Sep 2024 15:05:26 +0200
Subject: [PATCH 02/26] fix: reverts conf

---
 certora/confs/Reverts.conf | 2 +-
 certora/specs/Reverts.spec | 7 -------
 2 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index 9a3c97e..5ea22a3 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -6,8 +6,8 @@
     "link": [
      "PreLiquidationHarness:MORPHO=Morpho",
      ],
+    "solc_optimize_map" : { "Morpho" : "99999", "PreLiquidationHarness" : "99999"},
     "solc_via_ir" : true,
-    "solc_experimental_via_ir" : true,
     "solc_map": {
         "Morpho": "solc-0.8.19",
         "PreLiquidationHarness": "solc-0.8.27",
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index c699551..1d0abb0 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -1,15 +1,8 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-methods {
-    function _.market(Id) external returns (Market memory);
-}
 
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
     (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
 
-invariant marketExists()
-    MORPHO.market(currentContract.ID()).lastUpdate != 0;
-
-
 // Check that preliquidate reverts when its inputs are not validated.
 rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
     preLiquidate@withrevert(e, borrower, seizedAssets, repaidShares, data);

From b99d080500a056c27624f6075b33782df336fb2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 24 Sep 2024 17:42:12 +0200
Subject: [PATCH 03/26] draft: add specs

---
 certora/confs/Reverts.conf                |  1 +
 certora/helpers/PreLiquidationHarness.sol |  9 ++++++++-
 certora/specs/Reverts.spec                | 22 ++++++++++++++++++++++
 3 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index 5ea22a3..d630573 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -6,6 +6,7 @@
     "link": [
      "PreLiquidationHarness:MORPHO=Morpho",
      ],
+    "parametric_contracts" : ["Morpho"],
     "solc_optimize_map" : { "Morpho" : "99999", "PreLiquidationHarness" : "99999"},
     "solc_via_ir" : true,
     "solc_map": {
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
index 9cb462e..ea7eb10 100644
--- a/certora/helpers/PreLiquidationHarness.sol
+++ b/certora/helpers/PreLiquidationHarness.sol
@@ -1,7 +1,14 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.27;
 
-import {PreLiquidation, Id, Market, Position, PreLiquidationParams} from "../../src/PreLiquidation.sol";
+import {
+    PreLiquidation,
+    Id,
+    Market,
+    Position,
+    PreLiquidationParams,
+    IMorphoRepayCallback
+} from "../../src/PreLiquidation.sol";
 
 contract PreLiquidationHarness is PreLiquidation {
     constructor(Id id, PreLiquidationParams memory _preLiquidationParams, address morpho)
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 1d0abb0..1343276 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -1,5 +1,11 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+using Morpho as MORPHO;
+
+methods {
+    function MORPHO.market(PreLiquidationHarness.Id) external returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
+}
+
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
     (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
 
@@ -8,3 +14,19 @@ rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets,
     preLiquidate@withrevert(e, borrower, seizedAssets, repaidShares, data);
     assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted;
 }
+
+
+// Checks that onMorphoRepay is only triggered by Morpho
+rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
+    onMorphoRepay@withrevert(e, repaidAssets, data);
+    assert e.msg.sender != currentContract.MORPHO => lastReverted;
+}
+
+function lastUpdateIsNotNil(PreLiquidationHarness.Id id) returns bool {
+    mathint lastUpdate;
+    (_,_,_,_,lastUpdate,_) = MORPHO.market(id);
+    return lastUpdate > 0;
+}
+
+invariant marketExists()
+    lastUpdateIsNotNil(currentContract.ID);

From 7636e910d56938e9ebaba5e82b7c317dcb77de51 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 27 Sep 2024 10:28:24 +0200
Subject: [PATCH 04/26] chore:remove pre-liquidation harness

---
 certora/confs/Immutability.conf           |  6 +++---
 certora/confs/Reentrancy.conf             |  4 ++--
 certora/confs/Reverts.conf                | 10 ++++-----
 certora/helpers/PreLiquidationHarness.sol | 25 -----------------------
 certora/specs/Reverts.spec                | 11 +++++++---
 5 files changed, 18 insertions(+), 38 deletions(-)
 delete mode 100644 certora/helpers/PreLiquidationHarness.sol

diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
index dd47345..6fae19c 100644
--- a/certora/confs/Immutability.conf
+++ b/certora/confs/Immutability.conf
@@ -1,10 +1,10 @@
 {
     "files": [
-        "certora/helpers/PreLiquidationHarness.sol",
+        "src/PreLiquidation.sol",
     ],
     "solc": "solc-0.8.27",
-    "solc_via_ir" : true,	
-    "verify": "PreLiquidationHarness:certora/specs/Immutability.spec",
+    "solc_via_ir" : true,
+    "verify": "PreLiquidation:certora/specs/Immutability.spec",
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index 41cf094..f217f93 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -1,10 +1,10 @@
 {
     "files": [
-        "certora/helpers/PreLiquidationHarness.sol",
+        "src/PreLiquidation.sol",
     ],
     "solc": "solc-0.8.27",
     "solc_via_ir" : true,
-    "verify": "PreLiquidationHarness:certora/specs/Reentrancy.spec",
+    "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
     "prover_args": [
         "-enableStorageSplitting false",
         "-depth 3",
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index d630573..f3845b6 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -1,19 +1,19 @@
 {
     "files": [
-        "certora/helpers/PreLiquidationHarness.sol",
+        "src/PreLiquidation.sol",
         "lib/morpho-blue/src/Morpho.sol",
     ],
     "link": [
-     "PreLiquidationHarness:MORPHO=Morpho",
+     "PreLiquidation:MORPHO=Morpho",
      ],
     "parametric_contracts" : ["Morpho"],
-    "solc_optimize_map" : { "Morpho" : "99999", "PreLiquidationHarness" : "99999"},
+    "solc_optimize_map" : { "Morpho" : "99999", "PreLiquidation" : "99999"},
     "solc_via_ir" : true,
     "solc_map": {
         "Morpho": "solc-0.8.19",
-        "PreLiquidationHarness": "solc-0.8.27",
+        "PreLiquidation": "solc-0.8.27",
     },
-    "verify": "PreLiquidationHarness:certora/specs/Reverts.spec",
+    "verify": "PreLiquidation:certora/specs/Reverts.spec",
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
deleted file mode 100644
index ea7eb10..0000000
--- a/certora/helpers/PreLiquidationHarness.sol
+++ /dev/null
@@ -1,25 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.27;
-
-import {
-    PreLiquidation,
-    Id,
-    Market,
-    Position,
-    PreLiquidationParams,
-    IMorphoRepayCallback
-} from "../../src/PreLiquidation.sol";
-
-contract PreLiquidationHarness is PreLiquidation {
-    constructor(Id id, PreLiquidationParams memory _preLiquidationParams, address morpho)
-        PreLiquidation(id, _preLiquidationParams, morpho)
-    {}
-
-    function _isPreLiquidatable_(uint256 collateralPrice, Position memory position, Market memory market)
-        external
-        view
-        returns (bool)
-    {
-        return _isPreLiquidatable(collateralPrice, position, market);
-    }
-}
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 1343276..03ce32c 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -3,7 +3,8 @@
 using Morpho as MORPHO;
 
 methods {
-    function MORPHO.market(PreLiquidationHarness.Id) external returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
+    function MORPHO.market(PreLiquidation.Id) external
+      returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
 }
 
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
@@ -22,11 +23,15 @@ rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
     assert e.msg.sender != currentContract.MORPHO => lastReverted;
 }
 
-function lastUpdateIsNotNil(PreLiquidationHarness.Id id) returns bool {
+function lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
     mathint lastUpdate;
     (_,_,_,_,lastUpdate,_) = MORPHO.market(id);
-    return lastUpdate > 0;
+    return lastUpdate != 0;
 }
 
 invariant marketExists()
     lastUpdateIsNotNil(currentContract.ID);
+
+
+invariant preLltvLTlltv()
+    currentContract.PRE_LLTV < currentContract.LLTV;

From b6fe2eaad114959f61084f41e0b4a10bb7356acb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 27 Sep 2024 10:40:04 +0200
Subject: [PATCH 05/26] feat: verify pre-liquidation repay

---
 certora/confs/Liveness.conf | 26 ++++++++++++++++++++++++++
 certora/specs/Liveness.spec | 19 +++++++++++++++++++
 2 files changed, 45 insertions(+)
 create mode 100644 certora/confs/Liveness.conf
 create mode 100644 certora/specs/Liveness.spec

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
new file mode 100644
index 0000000..90726c1
--- /dev/null
+++ b/certora/confs/Liveness.conf
@@ -0,0 +1,26 @@
+{
+    "files": [
+        "src/PreLiquidation.sol",
+        "lib/morpho-blue/src/Morpho.sol",
+    ],
+    "link": [
+     "PreLiquidation:MORPHO=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/Liveness.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "PreLiquidation Liveness",
+}
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
new file mode 100644
index 0000000..6cd9fb9
--- /dev/null
+++ b/certora/specs/Liveness.spec
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+persistent ghost bool preLiquidateCalled;
+persistent ghost bool repayed;
+
+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 && preLiquidateCalled) {
+        repayed = true;
+    }
+}
+
+rule preLiquidateRepays(method f, env e, calldataarg data) {
+    require !preLiquidateCalled;
+    require !repayed;
+    f(e,data);
+    assert preLiquidateCalled <=> repayed;
+}

From 7eee316b90f11cae934bb2f9e7344a4219d3e76b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 27 Sep 2024 10:45:45 +0200
Subject: [PATCH 06/26] doc: describe liveness in readme

---
 certora/README.md | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index f01cfa2..c493db4 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -45,6 +45,12 @@ 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
@@ -59,15 +65,13 @@ The [`certora/specs`](specs) folder contains the following files:
   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/confs`](confs) folder contains a configuration file for
 each corresponding specification file.
 
-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.
-
 ## TODO
 
 - [ ] Provide an overview of the specification.

From 27bed0452dd4831276785f92006ed2f5366c6f71 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 27 Sep 2024 11:03:27 +0200
Subject: [PATCH 07/26] fix: simplify conf; ignore `extSload`

---
 certora/confs/Liveness.conf | 2 --
 certora/specs/Liveness.spec | 4 ++++
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index 90726c1..a983208 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -13,8 +13,6 @@
         "PreLiquidation": "solc-0.8.27",
     },
     "verify": "PreLiquidation:certora/specs/Liveness.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 6cd9fb9..66bc12a 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -1,5 +1,9 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+methods {
+    function _.extSloads(bytes32[]) external => NONDET DELETE;
+}
+
 persistent ghost bool preLiquidateCalled;
 persistent ghost bool repayed;
 

From f6f4b6ce625ea372675b94f1409a6ca5f1db4dc4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 27 Sep 2024 16:48:24 +0200
Subject: [PATCH 08/26] doc: add doc in spec

---
 certora/specs/Liveness.spec | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 66bc12a..1bd71b1 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -4,7 +4,11 @@ methods {
     function _.extSloads(bytes32[]) external => NONDET DELETE;
 }
 
+
+// True when preLiquidate has been called
 persistent ghost bool preLiquidateCalled;
+
+// True when preLiquidate and onMorphoRepay has been called
 persistent ghost bool repayed;
 
 hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
@@ -15,6 +19,7 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, ui
     }
 }
 
+// Checkt that liquidation will always trigger the repay callback
 rule preLiquidateRepays(method f, env e, calldataarg data) {
     require !preLiquidateCalled;
     require !repayed;

From a4b66796b2f811a784619fb9a96e7a311557106d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Sun, 29 Sep 2024 21:20:32 +0200
Subject: [PATCH 09/26] feat: setup CI for liveness specs

---
 .github/workflows/certora.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index d4c5c3f..01f909f 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -17,6 +17,7 @@ jobs:
       matrix:
         conf:
           - Immutability
+          - Liveness
           - Reentrancy
 
     steps:

From ad9fdd06e387a30a89b89fbe5ad9744514d26f5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 30 Sep 2024 14:44:53 +0200
Subject: [PATCH 10/26] fix: patch spec

---
 certora/specs/Liveness.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 1bd71b1..1bbf350 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -14,7 +14,7 @@ persistent ghost bool repayed;
 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 && preLiquidateCalled) {
+    } else if(selector == sig:onMorphoRepay(uint256, bytes).selector) {
         repayed = true;
     }
 }

From 253eefb747dd20f96e57fbcef40b4ae1b1d0763b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 1 Oct 2024 14:40:35 +0200
Subject: [PATCH 11/26] fix: add a helper

---
 certora/confs/Liveness.conf | 11 +++--------
 certora/helpers/Wallet.sol  | 24 ++++++++++++++++++++++++
 certora/specs/Liveness.spec |  5 -----
 3 files changed, 27 insertions(+), 13 deletions(-)
 create mode 100644 certora/helpers/Wallet.sol

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index a983208..332e276 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -1,17 +1,12 @@
 {
     "files": [
-        "src/PreLiquidation.sol",
-        "lib/morpho-blue/src/Morpho.sol",
+        "certora/helpers/Wallet.sol",
+        "src/PreLiquidation.sol"
     ],
     "link": [
-     "PreLiquidation:MORPHO=Morpho",
+     "Wallet:preLiq=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/Liveness.spec",
     "prover_args": [
         "-depth 3",
diff --git a/certora/helpers/Wallet.sol b/certora/helpers/Wallet.sol
new file mode 100644
index 0000000..f98ff27
--- /dev/null
+++ b/certora/helpers/Wallet.sol
@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {PreLiquidation, Id, Market, Position, PreLiquidationParams} from "../../src/PreLiquidation.sol";
+// import {IMorphoRepayCallback} from "../../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
+
+contract Wallet {
+    PreLiquidation immutable preLiq;
+
+    constructor(PreLiquidation p) {
+        preLiq = p;
+    }
+
+    function preLiquidateCall(bytes calldata args) external {
+        (address borrower, uint256 seizedAssets, uint256 repaidShares, bytes memory data) =
+            abi.decode(args, (address, uint256, uint256, bytes));
+        preLiq.preLiquidate(borrower, seizedAssets, repaidShares, data);
+    }
+
+    function onMorphoRepayCall(bytes calldata args) external {
+        (uint256 repaidAssets, bytes memory data) = abi.decode(args, (uint256, bytes));
+        preLiq.onMorphoRepay(repaidAssets, data);
+    }
+}
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 1bbf350..3e5f8ef 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -1,10 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-methods {
-    function _.extSloads(bytes32[]) external => NONDET DELETE;
-}
-
-
 // True when preLiquidate has been called
 persistent ghost bool preLiquidateCalled;
 

From 982420f4e6840f47a245411ccd95779791393725 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 1 Oct 2024 16:45:03 +0200
Subject: [PATCH 12/26] fix: improve spec

---
 certora/confs/Liveness.conf | 16 +++++++++++++++-
 certora/helpers/Wallet.sol  | 18 +++++++++++++++++-
 certora/specs/Liveness.spec |  7 +++++++
 3 files changed, 39 insertions(+), 2 deletions(-)

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index 332e276..27d824f 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -1,17 +1,31 @@
 {
     "files": [
         "certora/helpers/Wallet.sol",
-        "src/PreLiquidation.sol"
+        "src/PreLiquidation.sol",
+        "lib/morpho-blue/src/Morpho.sol",
     ],
     "link": [
      "Wallet:preLiq=PreLiquidation",
+     "PreLiquidation:MORPHO=Morpho",
      ],
+     "parametric_contracts" : ["Wallet"],
     "solc_via_ir" : true,
     "verify": "PreLiquidation:certora/specs/Liveness.spec",
+    "solc_optimize_map" : {
+        "Morpho" : "99999",
+        "PreLiquidation" : "99999",
+        "Wallet" : "99999"
+    },
+    "solc_map": {
+        "Morpho": "solc-0.8.19",
+        "PreLiquidation": "solc-0.8.27",
+        "Wallet": "solc-0.8.27",
+    },
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
         "-timeout 120",
+        "-smt_nonLinearArithmetic true",
     ],
     "rule_sanity": "basic",
     "server": "production",
diff --git a/certora/helpers/Wallet.sol b/certora/helpers/Wallet.sol
index f98ff27..ca5e2a8 100644
--- a/certora/helpers/Wallet.sol
+++ b/certora/helpers/Wallet.sol
@@ -2,7 +2,7 @@
 pragma solidity 0.8.27;
 
 import {PreLiquidation, Id, Market, Position, PreLiquidationParams} from "../../src/PreLiquidation.sol";
-// import {IMorphoRepayCallback} from "../../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
+import {IMorphoStaticTyping} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
 
 contract Wallet {
     PreLiquidation immutable preLiq;
@@ -21,4 +21,20 @@ contract Wallet {
         (uint256 repaidAssets, bytes memory data) = abi.decode(args, (uint256, bytes));
         preLiq.onMorphoRepay(repaidAssets, data);
     }
+
+    function marketParamsCall() external view {
+        preLiq.marketParams();
+    }
+
+    function preLiquidationParamsCall() external view {
+        preLiq.preLiquidationParams();
+    }
+
+    function morphoCall() external view {
+        preLiq.MORPHO();
+    }
+
+    function idCall() external view {
+        preLiq.ID();
+    }
 }
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 3e5f8ef..2fb89ff 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -1,5 +1,11 @@
 // 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;
 
@@ -18,6 +24,7 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, ui
 rule preLiquidateRepays(method f, env e, calldataarg data) {
     require !preLiquidateCalled;
     require !repayed;
+    require e.msg.sender != preLiq.MORPHO();
     f(e,data);
     assert preLiquidateCalled <=> repayed;
 }

From 1a43913de2fee6927ebfd49883aeae51b3dcd644 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 1 Oct 2024 18:02:25 +0200
Subject: [PATCH 13/26] fix: patch helper

---
 certora/README.md          |  4 ++++
 certora/confs/Reverts.conf | 25 -------------------------
 certora/helpers/Wallet.sol |  9 ++++-----
 certora/specs/Reverts.spec | 37 -------------------------------------
 4 files changed, 8 insertions(+), 67 deletions(-)
 delete mode 100644 certora/confs/Reverts.conf
 delete mode 100644 certora/specs/Reverts.spec

diff --git a/certora/README.md b/certora/README.md
index feaf3cb..af90fb1 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -65,6 +65,10 @@ will always trigger a repay operation.
 The [`certora/confs`](confs) folder contains a configuration file for
 each corresponding specification file.
 
+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.
+
+
 ## TODO
 
 - [ ] Provide an overview of the specification.
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
deleted file mode 100644
index f3845b6..0000000
--- a/certora/confs/Reverts.conf
+++ /dev/null
@@ -1,25 +0,0 @@
-{
-    "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/Reverts.spec",
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "PreLiquidation Reverts",
-}
diff --git a/certora/helpers/Wallet.sol b/certora/helpers/Wallet.sol
index ca5e2a8..e1a27cb 100644
--- a/certora/helpers/Wallet.sol
+++ b/certora/helpers/Wallet.sol
@@ -11,14 +11,13 @@ contract Wallet {
         preLiq = p;
     }
 
-    function preLiquidateCall(bytes calldata args) external {
-        (address borrower, uint256 seizedAssets, uint256 repaidShares, bytes memory data) =
-            abi.decode(args, (address, uint256, uint256, bytes));
+    function preLiquidateCall(address borrower, uint256 seizedAssets, uint256 repaidShares, bytes memory data)
+        external
+    {
         preLiq.preLiquidate(borrower, seizedAssets, repaidShares, data);
     }
 
-    function onMorphoRepayCall(bytes calldata args) external {
-        (uint256 repaidAssets, bytes memory data) = abi.decode(args, (uint256, bytes));
+    function onMorphoRepayCall(uint256 repaidAssets, bytes memory data) external {
         preLiq.onMorphoRepay(repaidAssets, data);
     }
 
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
deleted file mode 100644
index 03ce32c..0000000
--- a/certora/specs/Reverts.spec
+++ /dev/null
@@ -1,37 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-
-using Morpho as MORPHO;
-
-methods {
-    function MORPHO.market(PreLiquidation.Id) external
-      returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
-}
-
-definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
-    (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
-
-// Check that preliquidate reverts when its inputs are not validated.
-rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
-    preLiquidate@withrevert(e, borrower, seizedAssets, repaidShares, data);
-    assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted;
-}
-
-
-// Checks that onMorphoRepay is only triggered by Morpho
-rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
-    onMorphoRepay@withrevert(e, repaidAssets, data);
-    assert e.msg.sender != currentContract.MORPHO => lastReverted;
-}
-
-function lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
-    mathint lastUpdate;
-    (_,_,_,_,lastUpdate,_) = MORPHO.market(id);
-    return lastUpdate != 0;
-}
-
-invariant marketExists()
-    lastUpdateIsNotNil(currentContract.ID);
-
-
-invariant preLltvLTlltv()
-    currentContract.PRE_LLTV < currentContract.LLTV;

From 99d27d024c2cc953ed3a8c06de68564b70d1e74f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 2 Oct 2024 17:07:15 +0200
Subject: [PATCH 14/26] fix: simplify verif by removing harness

---
 certora/confs/Liveness.conf | 6 +-----
 certora/specs/Liveness.spec | 5 +++++
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index 27d824f..dbf11f2 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -1,25 +1,21 @@
 {
     "files": [
-        "certora/helpers/Wallet.sol",
         "src/PreLiquidation.sol",
         "lib/morpho-blue/src/Morpho.sol",
     ],
     "link": [
-     "Wallet:preLiq=PreLiquidation",
      "PreLiquidation:MORPHO=Morpho",
      ],
-     "parametric_contracts" : ["Wallet"],
+     "parametric_contracts" : ["PreLiquidation"],
     "solc_via_ir" : true,
     "verify": "PreLiquidation:certora/specs/Liveness.spec",
     "solc_optimize_map" : {
         "Morpho" : "99999",
         "PreLiquidation" : "99999",
-        "Wallet" : "99999"
     },
     "solc_map": {
         "Morpho": "solc-0.8.19",
         "PreLiquidation": "solc-0.8.27",
-        "Wallet": "solc-0.8.27",
     },
     "prover_args": [
         "-depth 3",
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 2fb89ff..fd45a3f 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -25,6 +25,11 @@ rule preLiquidateRepays(method f, env e, calldataarg data) {
     require !preLiquidateCalled;
     require !repayed;
     require e.msg.sender != preLiq.MORPHO();
+    if(f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
+       preLiquidateCalled = true;
+    } else if(f.selector == sig:onMorphoRepay(uint256, bytes).selector) {
+        repayed = true;
+    }
     f(e,data);
     assert preLiquidateCalled <=> repayed;
 }

From 6e98c1cead3b1d52a9143c9c97c099bdf414ad48 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 2 Oct 2024 18:29:31 +0200
Subject: [PATCH 15/26] fix: pass non vacuity test

---
 certora/helpers/Wallet.sol  | 39 -------------------------------------
 certora/specs/Liveness.spec |  4 ++--
 2 files changed, 2 insertions(+), 41 deletions(-)
 delete mode 100644 certora/helpers/Wallet.sol

diff --git a/certora/helpers/Wallet.sol b/certora/helpers/Wallet.sol
deleted file mode 100644
index e1a27cb..0000000
--- a/certora/helpers/Wallet.sol
+++ /dev/null
@@ -1,39 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.27;
-
-import {PreLiquidation, Id, Market, Position, PreLiquidationParams} from "../../src/PreLiquidation.sol";
-import {IMorphoStaticTyping} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-
-contract Wallet {
-    PreLiquidation immutable preLiq;
-
-    constructor(PreLiquidation p) {
-        preLiq = p;
-    }
-
-    function preLiquidateCall(address borrower, uint256 seizedAssets, uint256 repaidShares, bytes memory data)
-        external
-    {
-        preLiq.preLiquidate(borrower, seizedAssets, repaidShares, data);
-    }
-
-    function onMorphoRepayCall(uint256 repaidAssets, bytes memory data) external {
-        preLiq.onMorphoRepay(repaidAssets, data);
-    }
-
-    function marketParamsCall() external view {
-        preLiq.marketParams();
-    }
-
-    function preLiquidationParamsCall() external view {
-        preLiq.preLiquidationParams();
-    }
-
-    function morphoCall() external view {
-        preLiq.MORPHO();
-    }
-
-    function idCall() external view {
-        preLiq.ID();
-    }
-}
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index fd45a3f..6fb755b 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -30,6 +30,6 @@ rule preLiquidateRepays(method f, env e, calldataarg data) {
     } else if(f.selector == sig:onMorphoRepay(uint256, bytes).selector) {
         repayed = true;
     }
-    f(e,data);
-    assert preLiquidateCalled <=> repayed;
+    f@withrevert(e,data);
+    assert !lastReverted => (preLiquidateCalled <=> repayed);
 }

From ac1b180d807aa08b2ad441d7d3856821e60afe63 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 2 Oct 2024 18:34:53 +0200
Subject: [PATCH 16/26] chore: format liveness conf

---
 certora/confs/Liveness.conf | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index dbf11f2..4abffba 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -1,29 +1,24 @@
 {
-    "files": [
-        "src/PreLiquidation.sol",
-        "lib/morpho-blue/src/Morpho.sol",
-    ],
-    "link": [
-     "PreLiquidation:MORPHO=Morpho",
-     ],
-     "parametric_contracts" : ["PreLiquidation"],
-    "solc_via_ir" : true,
+    "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_optimize_map": {
+        "Morpho": "99999",
+        "PreLiquidation": "99999"
     },
     "solc_map": {
         "Morpho": "solc-0.8.19",
-        "PreLiquidation": "solc-0.8.27",
+        "PreLiquidation": "solc-0.8.27"
     },
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
         "-timeout 120",
-        "-smt_nonLinearArithmetic true",
+        "-smt_nonLinearArithmetic true"
     ],
     "rule_sanity": "basic",
     "server": "production",
-    "msg": "PreLiquidation Liveness",
+    "msg": "PreLiquidation Liveness"
 }

From ea9212f9d4a22b30492ea6da8fc35d773a4f1e9a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 2 Oct 2024 21:02:30 +0200
Subject: [PATCH 17/26] fix: add docs and fix formatting

---
 certora/confs/Immutability.conf | 14 ++++----------
 certora/confs/Reentrancy.conf   | 10 ++++------
 certora/specs/Liveness.spec     | 25 +++++++++++++------------
 3 files changed, 21 insertions(+), 28 deletions(-)

diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
index 6fae19c..1224505 100644
--- a/certora/confs/Immutability.conf
+++ b/certora/confs/Immutability.conf
@@ -1,16 +1,10 @@
 {
-    "files": [
-        "src/PreLiquidation.sol",
-    ],
+    "files": ["src/PreLiquidation.sol"],
     "solc": "solc-0.8.27",
-    "solc_via_ir" : true,
+    "solc_via_ir": true,
     "verify": "PreLiquidation:certora/specs/Immutability.spec",
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-    ],
+    "prover_args": ["-depth 3", "-mediumTimeout 20", "-timeout 120"],
     "rule_sanity": "basic",
     "server": "production",
-    "msg": "PreLiquidation Immutability",
+    "msg": "PreLiquidation Immutability"
 }
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index f217f93..6b0ca75 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -1,17 +1,15 @@
 {
-    "files": [
-        "src/PreLiquidation.sol",
-    ],
+    "files": ["src/PreLiquidation.sol"],
     "solc": "solc-0.8.27",
-    "solc_via_ir" : true,
+    "solc_via_ir": true,
     "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
     "prover_args": [
         "-enableStorageSplitting false",
         "-depth 3",
         "-mediumTimeout 20",
-        "-timeout 120",
+        "-timeout 120"
     ],
     "rule_sanity": "basic",
     "server": "production",
-    "msg": "PreLiquidation Reentrancy",
+    "msg": "PreLiquidation Reentrancy"
 }
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 6fb755b..c5abcb7 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -2,34 +2,35 @@
 
 using PreLiquidation as preLiq;
 
-methods {
-    function preLiq.MORPHO() external returns address envfree;
-}
-
 // True when preLiquidate has been called
 persistent ghost bool preLiquidateCalled;
 
-// True when preLiquidate and onMorphoRepay has been called
+// True when onMorphoRepay has been called
 persistent ghost bool repayed;
 
 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) {
+    if (selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
        preLiquidateCalled = true;
-    } else if(selector == sig:onMorphoRepay(uint256, bytes).selector) {
-        repayed = true;
+    } else if (selector == sig:onMorphoRepay(uint256, bytes).selector) {
+       repayed = true;
     }
 }
 
-// Checkt that liquidation will always trigger the repay callback
+
+// Check that pre-liquidations happen if and only if `onMorphoRepay` is called.
 rule preLiquidateRepays(method f, env e, calldataarg data) {
     require !preLiquidateCalled;
     require !repayed;
     require e.msg.sender != preLiq.MORPHO();
-    if(f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
+
+    if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
        preLiquidateCalled = true;
-    } else if(f.selector == sig:onMorphoRepay(uint256, bytes).selector) {
-        repayed = true;
+    } else if (f.selector == sig:onMorphoRepay(uint256, bytes).selector) {
+       repayed = true;
     }
+
     f@withrevert(e,data);
+
+    // Avoid failing vacuity checks, either the proposition is true or the execution reverts
     assert !lastReverted => (preLiquidateCalled <=> repayed);
 }

From cffe9f29d00e722585159d016ab566752358f976 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 2 Oct 2024 21:21:54 +0200
Subject: [PATCH 18/26] fix: rollback mistake

---
 certora/specs/Liveness.spec | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index c5abcb7..591b6df 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -2,6 +2,10 @@
 
 using PreLiquidation as preLiq;
 
+methods {
+    function preLiq.MORPHO() external returns address envfree;
+}
+
 // True when preLiquidate has been called
 persistent ghost bool preLiquidateCalled;
 

From 0a194fb6ed6cd12eea3b7716b78069743dee42a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 2 Oct 2024 22:25:55 +0200
Subject: [PATCH 19/26] fix: fmt README

---
 certora/README.md | 61 +++++++++++++++++++----------------------------
 1 file changed, 24 insertions(+), 37 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index af90fb1..8590231 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -1,34 +1,29 @@
 # 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
+[pre-liquidation](../src/PreLiquidation.sol) contract using the [Certora Prover](https://www.certora.com/).
 
 ## 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:
+[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 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.
 
 ## 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 Blue borrowers to set up a safer
+liquidation plan on a given position, thus preventing undesired liquidations.
 
 ### Reentrancy
 
@@ -38,36 +33,28 @@ 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.
-
-- [`Liveness.spec`](specs/Liveness.spec) ensure that expected
-computations will always be performed. For instance, pre-liquidations
-will always trigger a repay operation.
+- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that PreLiquidation is
+  reentrancy safe by checking that the storage is never used.
 
-The [`certora/confs`](confs) folder contains a configuration file for
-each corresponding specification file.
+- [`Immutability.spec`](specs/Immutability.spec) checks that PreLiquidation
+  contract is immutable because it doesn't perform any delegate call.
 
-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.
+- [`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/confs`](confs) folder contains a configuration file for each
+corresponding specification file.
 
 ## TODO
 

From 557b0d7096433e14c5f294403590a75abf3a1a03 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 3 Oct 2024 10:22:49 +0200
Subject: [PATCH 20/26] refactor: format files

---
 certora/confs/Immutability.conf | 22 ++++++++------
 certora/confs/Liveness.conf     | 51 +++++++++++++++++++--------------
 certora/confs/Reentrancy.conf   | 28 +++++++++---------
 certora/specs/Liveness.spec     |  7 ++---
 certora/specs/Reentrancy.spec   |  2 --
 5 files changed, 61 insertions(+), 49 deletions(-)

diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
index 1224505..be04841 100644
--- a/certora/confs/Immutability.conf
+++ b/certora/confs/Immutability.conf
@@ -1,10 +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"
 }
diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index 4abffba..5485f14 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -1,24 +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"
+  "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"
 }
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index 6b0ca75..494929d 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -1,15 +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"
 }
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 591b6df..578e571 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -6,10 +6,10 @@ methods {
     function preLiq.MORPHO() external returns address envfree;
 }
 
-// True when preLiquidate has been called
+// True when `preLiquidate` has been called.
 persistent ghost bool preLiquidateCalled;
 
-// True when onMorphoRepay has been called
+// True when `onMorphoRepay` has been called.
 persistent ghost bool repayed;
 
 hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
@@ -20,7 +20,6 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, ui
     }
 }
 
-
 // Check that pre-liquidations happen if and only if `onMorphoRepay` is called.
 rule preLiquidateRepays(method f, env e, calldataarg data) {
     require !preLiquidateCalled;
@@ -35,6 +34,6 @@ rule preLiquidateRepays(method f, env e, calldataarg data) {
 
     f@withrevert(e,data);
 
-    // Avoid failing vacuity checks, either the proposition is true or the execution reverts
+    // Avoid failing vacuity checks, either the proposition is true or the execution reverts.
     assert !lastReverted => (preLiquidateCalled <=> repayed);
 }
diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
index 12c808d..b6a7432 100644
--- a/certora/specs/Reentrancy.spec
+++ b/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;
 

From 0640540ead1edce156c7a605ec722aee48ad1a02 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 3 Oct 2024 10:27:57 +0200
Subject: [PATCH 21/26] refactor: one sentence per line in README

---
 certora/README.md | 34 ++++++++++++----------------------
 1 file changed, 12 insertions(+), 22 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index 8590231..e411b74 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -1,29 +1,24 @@
 # 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 [pre-liquidation](../src/PreLiquidation.sol) contract using the [Certora Prover](https://www.certora.com/).
 
 ## 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
+[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).
+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.
 
 ## 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 Blue borrowers to set up a safer liquidation plan on a given position, thus preventing undesired liquidations.
 
 ### Reentrancy
 
@@ -43,15 +38,10 @@ This is checked in [`Liveness.spec`](specs/Liveness.spec).
 
 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.
-
-- [`Liveness.spec`](specs/Liveness.spec) ensure that expected computations will
-  always be performed. For instance, pre-liquidations will always trigger a
-  repay operation.
+- [`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/confs`](confs) folder contains a configuration file for each
 corresponding specification file.

From 2e54f89001a6c9ae609a81141edbfb0cd47fb17e Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 3 Oct 2024 10:30:27 +0200
Subject: [PATCH 22/26] refactor: small changes in README

---
 certora/README.md | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index e411b74..8f7f1bf 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -1,6 +1,6 @@
 # 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
 
@@ -12,13 +12,13 @@ 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`.
 
-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).
+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
 
@@ -43,8 +43,7 @@ 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.
 
-The [`certora/confs`](confs) folder contains a configuration file for each
-corresponding specification file.
+The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
 
 ## TODO
 

From 046509d487a230c7fba80cb2b634b039e2d56734 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 3 Oct 2024 10:33:18 +0200
Subject: [PATCH 23/26] refactor: more sentence in newlines

---
 certora/README.md | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index 8f7f1bf..e3d3b47 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -4,10 +4,8 @@ This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index
 
 ## 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`.

From 84da5fbcf7ba716d98af17df010a4c6a6b53c6bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 3 Oct 2024 16:00:54 +0200
Subject: [PATCH 24/26] fix: typo

---
 certora/specs/Liveness.spec | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 578e571..e3a6a58 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -10,30 +10,30 @@ methods {
 persistent ghost bool preLiquidateCalled;
 
 // True when `onMorphoRepay` has been called.
-persistent ghost bool repayed;
+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) {
-       repayed = true;
+       onMorphoRepayCalled = true;
     }
 }
 
 // Check that pre-liquidations happen if and only if `onMorphoRepay` is called.
 rule preLiquidateRepays(method f, env e, calldataarg data) {
     require !preLiquidateCalled;
-    require !repayed;
+    require !onMorphoRepayCalled;
     require e.msg.sender != preLiq.MORPHO();
 
     if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
        preLiquidateCalled = true;
     } else if (f.selector == sig:onMorphoRepay(uint256, bytes).selector) {
-       repayed = true;
+       onMorphoRepayCalled = true;
     }
 
     f@withrevert(e,data);
 
     // Avoid failing vacuity checks, either the proposition is true or the execution reverts.
-    assert !lastReverted => (preLiquidateCalled <=> repayed);
+    assert !lastReverted => (preLiquidateCalled <=> onMorphoRepayCalled);
 }

From 89ff510e3744d5323393c2051ea722ae2c5e6e49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 3 Oct 2024 16:06:47 +0200
Subject: [PATCH 25/26] fix: add doc on spec

---
 certora/specs/Liveness.spec | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index e3a6a58..a741273 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -22,8 +22,12 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, ui
 
 // 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();
 
     if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {

From 0c27b5c71ddce94bb723b1cabace5cbca07d458c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 3 Oct 2024 16:42:52 +0200
Subject: [PATCH 26/26] fix: add more doc

---
 certora/specs/Liveness.spec | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index a741273..28f686b 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -26,10 +26,11 @@ 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) {