From 2dfbba9afccf13185aa7c1bbff2599bbd78cfe96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 27 Sep 2024 18:56:34 +0200
Subject: [PATCH 01/26] feat: check non-liquidatable reverts

---
 certora/confs/Reverts.conf | 56 ++++++++++++++++++++++----------------
 certora/specs/Reverts.spec | 49 ++++++++++++++++++++++++++++++++-
 2 files changed, 81 insertions(+), 24 deletions(-)

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index f3845b6..cb9a3fc 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -1,25 +1,35 @@
 {
-    "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",
+  "files": [
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/src/Morpho.sol",
+    "src/mocks/OracleMock.sol",
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=Morpho",
+    "PreLiquidation:PRE_LIQUIDATION_ORACLE=OracleMock",
+  ],
+  "parametric_contracts" : ["Morpho", "OracleMock"],
+  "solc_optimize_map" : {
+    "Morpho" : "99999",
+    "PreLiquidation" : "99999",
+    "OracleMock":"99999",
+  },
+  "solc_via_ir" : true,
+  "solc_map": {
+    "Morpho": "solc-0.8.19",
+    "PreLiquidation": "solc-0.8.27",
+    "OracleMock": "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",
 }
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 03ce32c..09c3c0f 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -1,14 +1,36 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
 using Morpho as MORPHO;
+using OracleMock as PRE_LIQUIDATION_ORACLE;
 
 methods {
     function MORPHO.market(PreLiquidation.Id) external
       returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
+    function MORPHO.position(PreLiquidation.Id, address) external
+      returns (uint256, uint128, uint128) envfree;
+    function PRE_LIQUIDATION_ORACLE.price() external
+      returns (uint256) envfree => ALWAYS(1);
 }
 
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
-    (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
+  (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
+
+function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y + (d-1)) / d);
+}
+
+function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y)/d);
+}
+
+definition tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 =
+    summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
+
+
+definition wMD(uint256 x,uint256 y) returns uint256 =
+    summaryMulDivDown(x, y, require_uint256(10^18));
 
 // Check that preliquidate reverts when its inputs are not validated.
 rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
@@ -35,3 +57,28 @@ invariant marketExists()
 
 invariant preLltvLTlltv()
     currentContract.PRE_LLTV < currentContract.LLTV;
+
+
+rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
+
+    uint256 mTotalBorrowAssets;
+    uint256 mTotalBorrowShares;
+    uint256 mLastUpdate;
+
+    uint256 pBorrowShares;
+    uint256 pCollateral;
+
+    (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    require mLastUpdate == e.block.timestamp;
+
+    uint256 collateralPrice = 1;
+
+    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
+
+    mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    mathint borrowThreshold = require_uint256(wMD(summaryMulDivDown(pCollateral,collateralPrice,(10^36)),currentContract.PRE_LLTV));
+
+    preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
+
+    assert (borrowed <= borrowThreshold) => lastReverted;
+}

From c410c158295cbe5fbef595309cb5fa36d496afa0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Sun, 29 Sep 2024 20:28:07 +0200
Subject: [PATCH 02/26] fix: summarize oracle

---
 certora/confs/Reverts.conf |  6 +-----
 certora/specs/Reverts.spec | 22 +++++++++++++++++-----
 2 files changed, 18 insertions(+), 10 deletions(-)

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index cb9a3fc..f56ae40 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -2,23 +2,19 @@
   "files": [
     "src/PreLiquidation.sol",
     "lib/morpho-blue/src/Morpho.sol",
-    "src/mocks/OracleMock.sol",
   ],
   "link": [
     "PreLiquidation:MORPHO=Morpho",
-    "PreLiquidation:PRE_LIQUIDATION_ORACLE=OracleMock",
   ],
-  "parametric_contracts" : ["Morpho", "OracleMock"],
+  "parametric_contracts" : ["Morpho" ],
   "solc_optimize_map" : {
     "Morpho" : "99999",
     "PreLiquidation" : "99999",
-    "OracleMock":"99999",
   },
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
     "PreLiquidation": "solc-0.8.27",
-    "OracleMock": "solc-0.8.27",
   },
   "verify": "PreLiquidation:certora/specs/Reverts.spec",
   "prover_args": [
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 09c3c0f..7ad1394 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -1,15 +1,26 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
 using Morpho as MORPHO;
-using OracleMock as PRE_LIQUIDATION_ORACLE;
 
 methods {
     function MORPHO.market(PreLiquidation.Id) external
       returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
     function MORPHO.position(PreLiquidation.Id, address) external
       returns (uint256, uint128, uint128) envfree;
-    function PRE_LIQUIDATION_ORACLE.price() external
-      returns (uint256) envfree => ALWAYS(1);
+    function _.price() external => mockPrice() expect uint256;
+}
+
+
+persistent ghost uint256 lastPrice;
+persistent ghost bool priceChanged;
+
+function mockPrice() returns uint256 {
+    uint256 updatedPrice;
+    if (updatedPrice != lastPrice) {
+        priceChanged = true;
+        lastPrice = updatedPrice;
+    }
+    return updatedPrice;
 }
 
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
@@ -71,7 +82,8 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
     require mLastUpdate == e.block.timestamp;
 
-    uint256 collateralPrice = 1;
+    priceChanged = false;
+    uint256 collateralPrice = mockPrice();
 
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
 
@@ -80,5 +92,5 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
-    assert (borrowed <= borrowThreshold) => lastReverted;
+    assert !priceChanged  && (borrowed <= borrowThreshold) => lastReverted;
 }

From ec4d9106432b23484260372bbef2dc3829b44d2f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 30 Sep 2024 14:06:23 +0200
Subject: [PATCH 03/26] feat: check pre-liquidate revers

---
 .github/workflows/certora.yml |  1 +
 certora/README.md             |  7 +++++++
 certora/specs/Reverts.spec    | 10 ++++++----
 3 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index d4c5c3f..2acd2e0 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -18,6 +18,7 @@ jobs:
         conf:
           - Immutability
           - Reentrancy
+          - Reverts
 
     steps:
       - uses: actions/checkout@v4
diff --git a/certora/README.md b/certora/README.md
index a5ca080..b37d6ed 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -38,6 +38,10 @@ 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 [`Revers.spec`](specs/Reverts.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
@@ -52,6 +56,9 @@ The [`certora/specs`](specs) folder contains the following files:
   PreLiquidation contract is immutable because it doesn't perform any
   delegate call.
 
+- [`Reverts.spec`](specs/Reverts.spec) checks the conditions for
+  reverts and that inputs are correctly validated.
+
 The [`certora/confs`](confs) folder contains a configuration file for
 each corresponding specification file.
 
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 7ad1394..fb5d40f 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -40,8 +40,8 @@ definition tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns
     summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
 
 
-definition wMD(uint256 x,uint256 y) returns uint256 =
-    summaryMulDivDown(x, y, require_uint256(10^18));
+definition wDU(uint256 x,uint256 y) returns uint256 =
+    summaryMulDivUp(x, require_uint256(10^18), y);
 
 // Check that preliquidate reverts when its inputs are not validated.
 rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
@@ -87,10 +87,12 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
 
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
 
+    mathint collateralQuoted =
+        require_uint256(summaryMulDivDown(pCollateral, collateralPrice, 10^36));
     mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
-    mathint borrowThreshold = require_uint256(wMD(summaryMulDivDown(pCollateral,collateralPrice,(10^36)),currentContract.PRE_LLTV));
+    mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
-    assert !priceChanged  && (borrowed <= borrowThreshold) => lastReverted;
+    assert !priceChanged  && (ltv <= currentContract.PRE_LLTV) => lastReverted;
 }

From a42149de2856b7df4157d9b66d812c200be93b75 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 30 Sep 2024 14:11:25 +0200
Subject: [PATCH 04/26] fix: remove useless summary

---
 certora/specs/Reverts.spec | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index fb5d40f..1ce2e10 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -31,11 +31,6 @@ function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y + (d-1)) / d);
 }
 
-function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    return require_uint256((x * y)/d);
-}
-
 definition tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 =
     summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
 
@@ -92,6 +87,9 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
     mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
 
+
+    wDivUp(borrowed, collateralQuoted);
+
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
     assert !priceChanged  && (ltv <= currentContract.PRE_LLTV) => lastReverted;

From 68bcaf661f30bbf204c6a300a86e436fd0f38f0e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 30 Sep 2024 14:15:02 +0200
Subject: [PATCH 05/26] Revert "fix: remove useless summary"

This reverts commit a42149de2856b7df4157d9b66d812c200be93b75.
---
 certora/specs/Reverts.spec | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 1ce2e10..fb5d40f 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -31,6 +31,11 @@ function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y + (d-1)) / d);
 }
 
+function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y)/d);
+}
+
 definition tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 =
     summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
 
@@ -87,9 +92,6 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
     mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
 
-
-    wDivUp(borrowed, collateralQuoted);
-
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
     assert !priceChanged  && (ltv <= currentContract.PRE_LLTV) => lastReverted;

From 65fc7f43b8bd0a9ba6aa546503aea8640d9e283c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 1 Oct 2024 09:39:50 +0200
Subject: [PATCH 06/26] fix: fix division by zero

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

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index fb5d40f..d6ca671 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -85,10 +85,15 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     priceChanged = false;
     uint256 collateralPrice = mockPrice();
 
+
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
 
     mathint collateralQuoted =
         require_uint256(summaryMulDivDown(pCollateral, collateralPrice, 10^36));
+
+    // Safe require because the implementation would revert.
+    require collateralQuoted>0;
+
     mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
     mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
 

From 4b0a1128f734fb41aa03059bb73096ad58ff0b56 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 1 Oct 2024 13:29:51 +0200
Subject: [PATCH 07/26] feat: check excessive liquidation revert

---
 certora/specs/Reverts.spec | 104 +++++++++++++++++++++++++++++++++++--
 1 file changed, 100 insertions(+), 4 deletions(-)

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index d6ca671..903029c 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -26,6 +26,10 @@ function mockPrice() returns uint256 {
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
   (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
 
+function min(mathint a, mathint b) returns mathint {
+    return a < b ? a : b;
+}
+
 function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
     // Safe require because the reference implementation would revert.
     return require_uint256((x * y + (d-1)) / d);
@@ -36,12 +40,34 @@ function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y)/d);
 }
 
-definition tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 =
-    summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
+function tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
+    return summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
+}
 
 
-definition wDU(uint256 x,uint256 y) returns uint256 =
-    summaryMulDivUp(x, require_uint256(10^18), y);
+function tSU(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
+    return summaryMulDivUp(assets, require_uint256(totalShares + (10^6)), require_uint256(totalAssets + (10^6)));
+}
+
+function wDU(uint256 x,uint256 y) returns uint256 {
+    return summaryMulDivUp(x, require_uint256(10^18), y);
+}
+
+function wDD(uint256 x,uint256 y) returns uint256 {
+    return summaryMulDivDown(x, require_uint256(10^18), y);
+}
+
+function wMD(uint256 x,uint256 y) returns uint256  {
+    return summaryMulDivDown(x, y, require_uint256(10^18));
+}
+
+function chooseFactor(mathint ltv, mathint lLtv, mathint preLLTV, mathint factor1, mathint factor2)
+    returns mathint {
+    return min(wMD(wDD(require_uint256(ltv - preLLTV),
+                       require_uint256(lLtv - preLLTV)),
+                   require_uint256(factor2 - factor1)) + factor1,
+               factor2);
+}
 
 // Check that preliquidate reverts when its inputs are not validated.
 rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
@@ -69,6 +95,13 @@ invariant marketExists()
 invariant preLltvLTlltv()
     currentContract.PRE_LLTV < currentContract.LLTV;
 
+invariant preCFIncreasing()
+    currentContract.PRE_CF_2 >= currentContract.PRE_CF_1;
+
+invariant preLIFIncreasing()
+    currentContract.PRE_LIF_1 >= 10^18 && currentContract.PRE_LIF_2 >= currentContract.PRE_LIF_1;
+
+
 
 rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
 
@@ -100,4 +133,67 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
     assert !priceChanged  && (ltv <= currentContract.PRE_LLTV) => lastReverted;
+
+}
+
+rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
+
+    uint256 mTotalBorrowAssets;
+    uint256 mTotalBorrowShares;
+    uint256 mLastUpdate;
+
+    uint256 pBorrowShares;
+    uint256 pCollateral;
+
+    (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
+
+    require mLastUpdate == e.block.timestamp;
+
+    priceChanged = false;
+    uint256 collateralPrice = mockPrice();
+
+    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
+
+    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, 10^36));
+
+    // Safe require because the implementation would revert.
+    require collateralQuoted > 0;
+    require seizedAssets > 0;
+    require currentContract.PRE_LIF_1 == currentContract.PRE_LIF_2;
+    require currentContract.PRE_CF_1 == currentContract.PRE_CF_2;
+
+    requireInvariant preLltvLTlltv();
+    requireInvariant preCFIncreasing();
+    requireInvariant preLIFIncreasing();
+
+
+    mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
+
+    mathint preLIF = chooseFactor(ltv,
+                                  currentContract.LLTV,
+                                  currentContract.PRE_LLTV,
+                                  currentContract.PRE_LIF_1,
+                                  currentContract.PRE_LIF_2);
+
+    mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, collateralPrice, 10^36));
+
+    mathint repaidShares = tSU(wDU(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
+                               mTotalBorrowAssets,
+                               mTotalBorrowShares);
+
+    mathint closeFactor = chooseFactor(ltv,
+                                       currentContract.LLTV,
+                                       currentContract.PRE_LLTV,
+                                       currentContract.PRE_CF_1,
+                                       currentContract.PRE_CF_2);
+
+    mathint repayableShares = wMD(pBorrowShares, require_uint256(closeFactor));
+
+    preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
+
+    require !priceChanged;
+    require (repaidShares > repayableShares );
+    assert lastReverted;
+
 }

From 983863ceb4d34ff8ab0f9d7ffe748b80dedd7057 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 1 Oct 2024 16:38:33 +0200
Subject: [PATCH 08/26] fix: change spec

---
 certora/specs/Reverts.spec | 2 --
 1 file changed, 2 deletions(-)

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 903029c..7c6c808 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -159,8 +159,6 @@ rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets
     // Safe require because the implementation would revert.
     require collateralQuoted > 0;
     require seizedAssets > 0;
-    require currentContract.PRE_LIF_1 == currentContract.PRE_LIF_2;
-    require currentContract.PRE_CF_1 == currentContract.PRE_CF_2;
 
     requireInvariant preLltvLTlltv();
     requireInvariant preCFIncreasing();

From 67b036c54c925588ea136689436de5b0f5ce8f77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 7 Oct 2024 18:09:02 +0200
Subject: [PATCH 09/26] feat: check revert conditions

---
 certora/confs/Reverts.conf |   4 +-
 certora/specs/Reverts.spec | 195 ++++++++++++++++++++++++-------------
 2 files changed, 129 insertions(+), 70 deletions(-)

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index f56ae40..2a86154 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -6,7 +6,7 @@
   "link": [
     "PreLiquidation:MORPHO=Morpho",
   ],
-  "parametric_contracts" : ["Morpho" ],
+  "parametric_contracts" : ["PreLiquidation"],
   "solc_optimize_map" : {
     "Morpho" : "99999",
     "PreLiquidation" : "99999",
@@ -20,7 +20,7 @@
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 5",
-    "-timeout 3600",
+    "-timeout 7000",
     "-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]",
 
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 7c6c808..d257930 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -3,16 +3,19 @@
 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 MORPHO.position(PreLiquidation.Id, address) external
       returns (uint256, uint128, uint128) envfree;
+    function MORPHO.idToMarketParams(PreLiquidation.Id) external
+      returns (address, address, address, address, uint256) envfree;
     function _.price() external => mockPrice() expect uint256;
 }
 
-
 persistent ghost uint256 lastPrice;
 persistent ghost bool priceChanged;
+persistent  ghost bool preLiquidateReverted;
 
 function mockPrice() returns uint256 {
     uint256 updatedPrice;
@@ -23,13 +26,6 @@ function mockPrice() returns uint256 {
     return updatedPrice;
 }
 
-definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
-  (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
-
-function min(mathint a, mathint b) returns mathint {
-    return a < b ? a : b;
-}
-
 function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
     // Safe require because the reference implementation would revert.
     return require_uint256((x * y + (d-1)) / d);
@@ -40,41 +36,30 @@ function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y)/d);
 }
 
-function tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
-    return summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
-}
+definition WAD() returns uint256 = 10^18;
 
+definition ORACLE_SCALE() returns uint256  = 10^36;
 
-function tSU(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
-    return summaryMulDivUp(assets, require_uint256(totalShares + (10^6)), require_uint256(totalAssets + (10^6)));
-}
+definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
+  (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
 
-function wDU(uint256 x,uint256 y) returns uint256 {
-    return summaryMulDivUp(x, require_uint256(10^18), y);
-}
+definition tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 =
+    summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
 
-function wDD(uint256 x,uint256 y) returns uint256 {
-    return summaryMulDivDown(x, require_uint256(10^18), y);
-}
+definition tSU(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 =
+    summaryMulDivUp(assets, require_uint256(totalShares + (10^6)), require_uint256(totalAssets + (10^6)));
 
-function wMD(uint256 x,uint256 y) returns uint256  {
-    return summaryMulDivDown(x, y, require_uint256(10^18));
-}
+definition wDU(uint256 x,uint256 y) returns uint256 = summaryMulDivUp(x, WAD(), y);
 
-function chooseFactor(mathint ltv, mathint lLtv, mathint preLLTV, mathint factor1, mathint factor2)
-    returns mathint {
-    return min(wMD(wDD(require_uint256(ltv - preLLTV),
-                       require_uint256(lLtv - preLLTV)),
-                   require_uint256(factor2 - factor1)) + factor1,
-               factor2);
-}
+definition wDD(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, WAD(), y);
 
-// 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;
-}
+definition wMD(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, y, WAD());
 
+definition computeFactor(mathint ltv, mathint lLtv, mathint preLLTV, mathint factor1, mathint factor2)
+    returns mathint =
+    wMD(wDD(require_uint256(ltv - preLLTV),
+            require_uint256(lLtv - preLLTV)),
+        require_uint256(factor2 - factor1)) + factor1;
 
 // Checks that onMorphoRepay is only triggered by Morpho
 rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
@@ -88,56 +73,128 @@ function lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
     return lastUpdate != 0;
 }
 
+//Ensure constructor requirements.
+
 invariant marketExists()
     lastUpdateIsNotNil(currentContract.ID);
 
-
 invariant preLltvLTlltv()
     currentContract.PRE_LLTV < currentContract.LLTV;
 
-invariant preCFIncreasing()
-    currentContract.PRE_CF_2 >= currentContract.PRE_CF_1;
+invariant preLCFIncreasing()
+    currentContract.PRE_LCF_1 <= currentContract.PRE_LCF_2
+    && currentContract.PRE_LCF_1 <= WAD();
 
 invariant preLIFIncreasing()
-    currentContract.PRE_LIF_1 >= 10^18 && currentContract.PRE_LIF_2 >= currentContract.PRE_LIF_1;
+    WAD() <= currentContract.PRE_LIF_1
+    && currentContract.PRE_LIF_1 <= currentContract.PRE_LIF_2
+    && currentContract.PRE_LIF_2 <= wDD(WAD(),currentContract.LLTV)
+{
+    preserved
+        {
+            requireInvariant preLltvLTlltv ();
+        }
+}
+
+// Check that preLiquidate reverts when its inputs are not validated.
+rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
+    requireInvariant preLltvLTlltv();
+    requireInvariant preLCFIncreasing();
+    requireInvariant preLIFIncreasing();
+    preLiquidate@withrevert(e, borrower, seizedAssets, repaidShares, data);
+    assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted;
+}
 
+// Check that collateralQuoted == 0 would revert by failing require-statements.
+rule zeroCollateralQuotedReverts() {
+    // Market values.
+    uint256 mTotalBorrowAssets;
+    uint256 mTotalBorrowShares;
 
+    // Position values.
+    uint256 pBorrowShares;
+    uint256 pCollateral;
 
-rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
+    uint256 collateralPrice;
+
+    requireInvariant preLltvLTlltv();
+
+    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
+    uint256 borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
 
+    uint256 higherBound = wMD(collateralQuoted, currentContract.LLTV);
+    uint256 lowerBound = wMD(collateralQuoted, currentContract.PRE_LLTV);
+
+    assert  collateralQuoted == 0 => (lowerBound >= borrowed || borrowed > higherBound);
+}
+
+// Check that a liquidatable position implies that ltv > PRE_LLTV holds.
+rule preLiquidatableImplLtvLTPreLltv() {
+    // Market values.
+    uint256 mTotalBorrowAssets;
+    uint256 mTotalBorrowShares;
+
+    // Position values.
+    uint256 pBorrowShares;
+    uint256 pCollateral;
+
+    uint256 collateralPrice;
+
+    requireInvariant preLltvLTlltv();
+
+    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
+
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
+    require collateralQuoted > 0;
+
+    uint256 borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    uint256 ltv = require_uint256(wDU(borrowed,collateralQuoted));
+    uint256 lowerBound = wMD(collateralQuoted, currentContract.PRE_LLTV);
+
+    assert (lowerBound < borrowed) => ltv > currentContract.PRE_LLTV;
+}
+
+// Check that pre-liqudidating a position such that ltv <= PRE_LLTV would revert.
+rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
+    // Market values.
     uint256 mTotalBorrowAssets;
     uint256 mTotalBorrowShares;
     uint256 mLastUpdate;
 
+    // Position values.
     uint256 pBorrowShares;
     uint256 pCollateral;
 
+    requireInvariant preLltvLTlltv();
+    requireInvariant preLCFIncreasing();
+    requireInvariant preLIFIncreasing();
+
     (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
+
+    // Ensure that no interest is accumulated.
     require mLastUpdate == e.block.timestamp;
 
+    // Consider that the collateral price hasn't changed.
     priceChanged = false;
-    uint256 collateralPrice = mockPrice();
 
+    uint256 collateralPrice = mockPrice();
 
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
 
-    mathint collateralQuoted =
-        require_uint256(summaryMulDivDown(pCollateral, collateralPrice, 10^36));
+    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
 
-    // Safe require because the implementation would revert.
-    require collateralQuoted>0;
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
+    require collateralQuoted > 0;
 
     mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
     mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
-    assert !priceChanged  && (ltv <= currentContract.PRE_LLTV) => lastReverted;
-
+    assert !priceChanged && (ltv <= currentContract.PRE_LLTV) => lastReverted;
 }
 
 rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
-
     uint256 mTotalBorrowAssets;
     uint256 mTotalBorrowShares;
     uint256 mLastUpdate;
@@ -147,51 +204,53 @@ rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets
 
     (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
 
+    // Ensure that no interest is accumulated.
     require mLastUpdate == e.block.timestamp;
 
+    // Consider that the collateral price hasn't changed.
     priceChanged = false;
+
     uint256 collateralPrice = mockPrice();
 
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
 
-    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, 10^36));
+    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
 
-    // Safe require because the implementation would revert.
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
-    require seizedAssets > 0;
 
     requireInvariant preLltvLTlltv();
-    requireInvariant preCFIncreasing();
+    requireInvariant preLCFIncreasing();
     requireInvariant preLIFIncreasing();
 
-
     mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
     mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
 
-    mathint preLIF = chooseFactor(ltv,
-                                  currentContract.LLTV,
-                                  currentContract.PRE_LLTV,
-                                  currentContract.PRE_LIF_1,
-                                  currentContract.PRE_LIF_2);
 
-    mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, collateralPrice, 10^36));
+    mathint preLIF = computeFactor(ltv,
+                                   currentContract.LLTV,
+                                   currentContract.PRE_LLTV,
+                                   currentContract.PRE_LIF_1,
+                                   currentContract.PRE_LIF_2) ;
+
+    // Safe require as implementation would revert.
+    require seizedAssets > 0;
+
+    mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, collateralPrice, ORACLE_SCALE()));
 
     mathint repaidShares = tSU(wDU(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
                                mTotalBorrowAssets,
                                mTotalBorrowShares);
 
-    mathint closeFactor = chooseFactor(ltv,
-                                       currentContract.LLTV,
-                                       currentContract.PRE_LLTV,
-                                       currentContract.PRE_CF_1,
-                                       currentContract.PRE_CF_2);
+    mathint closeFactor = computeFactor(ltv,
+                                        currentContract.LLTV,
+                                        currentContract.PRE_LLTV,
+                                        currentContract.PRE_LCF_1,
+                                        currentContract.PRE_LCF_2) ;
 
     mathint repayableShares = wMD(pBorrowShares, require_uint256(closeFactor));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
-
-    require !priceChanged;
-    require (repaidShares > repayableShares );
-    assert lastReverted;
+    assert (!priceChanged && repaidShares > repayableShares ) => lastReverted;
 
 }

From b06ebdb5e841646bc42da2a85b1b733674a8c111 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 7 Oct 2024 18:23:45 +0200
Subject: [PATCH 10/26] fix: improve spec

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

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index d257930..db1af1f 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -129,7 +129,7 @@ rule zeroCollateralQuotedReverts() {
 }
 
 // Check that a liquidatable position implies that ltv > PRE_LLTV holds.
-rule preLiquidatableImplLtvLTPreLltv() {
+rule preLiquidatableEquivlLtvLTPreLltv() {
     // Market values.
     uint256 mTotalBorrowAssets;
     uint256 mTotalBorrowShares;
@@ -151,7 +151,7 @@ rule preLiquidatableImplLtvLTPreLltv() {
     uint256 ltv = require_uint256(wDU(borrowed,collateralQuoted));
     uint256 lowerBound = wMD(collateralQuoted, currentContract.PRE_LLTV);
 
-    assert (lowerBound < borrowed) => ltv > currentContract.PRE_LLTV;
+    assert (lowerBound < borrowed) <=> ltv <= currentContract.PRE_LLTV;
 }
 
 // Check that pre-liqudidating a position such that ltv <= PRE_LLTV would revert.

From 98c5060b28860853c543a555b21ea8bb788b99fc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 7 Oct 2024 18:29:56 +0200
Subject: [PATCH 11/26] fix: revert fix spec

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

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index db1af1f..38b4ec6 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -151,7 +151,7 @@ rule preLiquidatableEquivlLtvLTPreLltv() {
     uint256 ltv = require_uint256(wDU(borrowed,collateralQuoted));
     uint256 lowerBound = wMD(collateralQuoted, currentContract.PRE_LLTV);
 
-    assert (lowerBound < borrowed) <=> ltv <= currentContract.PRE_LLTV;
+    assert (lowerBound < borrowed) <=> ltv > currentContract.PRE_LLTV;
 }
 
 // Check that pre-liqudidating a position such that ltv <= PRE_LLTV would revert.

From 3ce933112ea73253f59d0f68ac6be1aff16e6438 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 7 Oct 2024 19:19:09 +0200
Subject: [PATCH 12/26] fix: summarize maths

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

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 38b4ec6..cab232a 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -11,6 +11,11 @@ methods {
     function MORPHO.idToMarketParams(PreLiquidation.Id) external
       returns (address, address, address, address, uint256) envfree;
     function _.price() external => mockPrice() expect uint256;
+    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
+        returns uint256
+        => summaryMulDivDown(a,b,c);
+    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => summaryMulDivUp(a,b,c);
 }
 
 persistent ghost uint256 lastPrice;

From 07d22699eb0ac2e7a09b52764c92e424c5b1035d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 7 Oct 2024 21:51:51 +0200
Subject: [PATCH 13/26] feat: remove marketExists

---
 certora/confs/Reverts.conf |  2 +-
 certora/specs/Reverts.spec | 67 +++++++++++++++++++++++++-------------
 2 files changed, 45 insertions(+), 24 deletions(-)

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index 2a86154..08c0e23 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -20,7 +20,7 @@
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 5",
-    "-timeout 7000",
+    "-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]",
 
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index cab232a..6b332f4 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -3,7 +3,6 @@
 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 MORPHO.position(PreLiquidation.Id, address) external
@@ -16,11 +15,15 @@ methods {
         => summaryMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivUp(a,b,c);
+    function SharesMathLib.toSharesUp(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => tSU(a,b,c);
+    function SharesMathLib.toAssetsUp(uint256 a, uint256 b, uint256 c) internal
+        returns uint256 => tAU(a,b,c);
+
 }
 
 persistent ghost uint256 lastPrice;
 persistent ghost bool priceChanged;
-persistent  ghost bool preLiquidateReverted;
 
 function mockPrice() returns uint256 {
     uint256 updatedPrice;
@@ -41,6 +44,18 @@ function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y)/d);
 }
 
+function tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
+    return summaryMulDivUp(shares,
+                           require_uint256(totalAssets + (10^6)),
+                           require_uint256(totalShares + (10^6)));
+}
+
+function tSU(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
+    return summaryMulDivUp(assets,
+                           require_uint256(totalShares + (10^6)),
+                           require_uint256(totalAssets + (10^6)));
+}
+
 definition WAD() returns uint256 = 10^18;
 
 definition ORACLE_SCALE() returns uint256  = 10^36;
@@ -48,12 +63,6 @@ definition ORACLE_SCALE() returns uint256  = 10^36;
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
   (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
 
-definition tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 =
-    summaryMulDivUp(shares, require_uint256(totalAssets + (10^6)), require_uint256(totalShares + (10^6)));
-
-definition tSU(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 =
-    summaryMulDivUp(assets, require_uint256(totalShares + (10^6)), require_uint256(totalAssets + (10^6)));
-
 definition wDU(uint256 x,uint256 y) returns uint256 = summaryMulDivUp(x, WAD(), y);
 
 definition wDD(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, WAD(), y);
@@ -72,35 +81,47 @@ rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
     assert e.msg.sender != currentContract.MORPHO => lastReverted;
 }
 
-function lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
-    mathint lastUpdate;
-    (_,_,_,_,lastUpdate,_) = MORPHO.market(id);
-    return lastUpdate != 0;
-}
-
 //Ensure constructor requirements.
 
-invariant marketExists()
-    lastUpdateIsNotNil(currentContract.ID);
+invariant lltvNotZero()
+    0 < currentContract.LLTV
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
 
 invariant preLltvLTlltv()
-    currentContract.PRE_LLTV < currentContract.LLTV;
+    currentContract.PRE_LLTV < currentContract.LLTV
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
 
 invariant preLCFIncreasing()
     currentContract.PRE_LCF_1 <= currentContract.PRE_LCF_2
-    && currentContract.PRE_LCF_1 <= WAD();
+    && currentContract.PRE_LCF_1 <= WAD()
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+invariant preLIFNotZero()
+    0 < currentContract.PRE_LIF_1;
 
 invariant preLIFIncreasing()
-    WAD() <= currentContract.PRE_LIF_1
+    WAD() < currentContract.PRE_LIF_1
     && currentContract.PRE_LIF_1 <= currentContract.PRE_LIF_2
     && currentContract.PRE_LIF_2 <= wDD(WAD(),currentContract.LLTV)
 {
-    preserved
-        {
-            requireInvariant preLltvLTlltv ();
-        }
+    preserved {
+        requireInvariant lltvNotZero();
+    }
 }
 
+
 // Check that preLiquidate reverts when its inputs are not validated.
 rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
     requireInvariant preLltvLTlltv();

From 7f5e1c63ac9f9044233d37b363b3e88ce56a38aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 7 Oct 2024 22:06:54 +0200
Subject: [PATCH 14/26] fix: avoid unexpected havocs

---
 certora/specs/Reverts.spec | 1 +
 1 file changed, 1 insertion(+)

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 6b332f4..bc3fd76 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -3,6 +3,7 @@
 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 MORPHO.position(PreLiquidation.Id, address) external

From 5ab47a5eed5d3346d337c79bc23433337d2df983 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 9 Oct 2024 12:43:22 +0200
Subject: [PATCH 15/26] feat: ensure market exists

---
 .github/workflows/certora.yml   |  1 +
 certora/README.md               |  4 +++-
 certora/confs/MarketExists.conf | 28 +++++++++++++++++++++++++
 certora/specs/MarketExists.spec | 36 +++++++++++++++++++++++++++++++++
 4 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 certora/confs/MarketExists.conf
 create mode 100644 certora/specs/MarketExists.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 28a2d89..333c7d2 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -17,6 +17,7 @@ jobs:
       matrix:
         conf:
           - Immutability
+          - MarketExists
           - Liveness
           - Reentrancy
           - Reverts
diff --git a/certora/README.md b/certora/README.md
index 8b0a56d..dd1f12c 100644
--- a/certora/README.md
+++ b/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.
 
diff --git a/certora/confs/MarketExists.conf b/certora/confs/MarketExists.conf
new file mode 100644
index 0000000..d1c4037
--- /dev/null
+++ b/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"
+}
diff --git a/certora/specs/MarketExists.spec b/certora/specs/MarketExists.spec
new file mode 100644
index 0000000..162ea5b
--- /dev/null
+++ b/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);

From 4b1dc0a6ac503942c35ac02ba1cccc52990fea4d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 10 Oct 2024 12:53:48 +0200
Subject: [PATCH 16/26] fix: externalize invariants, revert on liquidatable,
 severa minor fixes

---
 certora/README.md                          |   6 +-
 certora/confs/ConsistentInstantiation.conf |  29 ++++
 certora/specs/ConsistentInstantiation.spec |  52 ++++++
 certora/specs/MarketExists.spec            |   9 +-
 certora/specs/Reverts.spec                 | 192 +++++++++------------
 5 files changed, 169 insertions(+), 119 deletions(-)
 create mode 100644 certora/confs/ConsistentInstantiation.conf
 create mode 100644 certora/specs/ConsistentInstantiation.spec

diff --git a/certora/README.md b/certora/README.md
index dd1f12c..183c976 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -26,10 +26,13 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 
 This is checked in [`Immutability.spec`](specs/Immutability.spec).
 
-## Invalid inputs trigger a revert operation
+## 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
 
@@ -47,6 +50,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.
+- [`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.
diff --git a/certora/confs/ConsistentInstantiation.conf b/certora/confs/ConsistentInstantiation.conf
new file mode 100644
index 0000000..cc1b1d6
--- /dev/null
+++ b/certora/confs/ConsistentInstantiation.conf
@@ -0,0 +1,29 @@
+{
+  "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/ConsistentInstantiation.spec",
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 3",
+    "-timeout 3600",
+    "-smt_nonLinearArithmetic true"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation ConsistentInstantiation",
+}
diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec
new file mode 100644
index 0000000..399410f
--- /dev/null
+++ b/certora/specs/ConsistentInstantiation.spec
@@ -0,0 +1,52 @@
+//Ensure constructor requirements.
+
+methods {
+    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
+}
+
+function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y)/d);
+}
+
+definition WAD() returns uint256 = 10^18;
+
+definition wDivDown(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, WAD(), y);
+
+invariant lltvNotZero()
+    0 < currentContract.LLTV
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+invariant preLltvConsistent()
+    currentContract.PRE_LLTV < currentContract.LLTV
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+invariant preLCFConsistent()
+    currentContract.PRE_LCF_1 <= currentContract.PRE_LCF_2
+    && currentContract.PRE_LCF_1 <= WAD()
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
+
+invariant preLIFNotZero()
+    0 < currentContract.PRE_LIF_1;
+
+invariant preLIFConsistent()
+    WAD() < currentContract.PRE_LIF_1
+    && currentContract.PRE_LIF_1 <= currentContract.PRE_LIF_2
+    && currentContract.PRE_LIF_2 <= wDivDown(WAD(),currentContract.LLTV)
+{
+    preserved {
+        requireInvariant lltvNotZero();
+    }
+}
diff --git a/certora/specs/MarketExists.spec b/certora/specs/MarketExists.spec
index 162ea5b..5633394 100644
--- a/certora/specs/MarketExists.spec
+++ b/certora/specs/MarketExists.spec
@@ -6,7 +6,7 @@ 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;
+    function _.price() external => NONDET;
 }
 
 persistent ghost uint256 lastTimestamp;
@@ -19,18 +19,13 @@ hook TIMESTAMP uint newTimestamp {
     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.
+// Ensure that the pre-liquidation contract interacts with a created market.
 
 invariant marketExists()
     lastUpdateIsNotNil(currentContract.ID);
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index bc3fd76..b8ad211 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -1,9 +1,13 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+import "ConsistentInstantiation.spec";
+
 using Morpho as MORPHO;
 
 methods {
-    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
+    function _.position(PreLiquidation.Id, address) external => DISPATCHER(true);
+    function _.accrueInterest(PreLiquidation.MarketParams) external => DISPATCHER(true);
+    function _.borrowRate(PreLiquidation.MarketParams, PreLiquidation.Id) external => HAVOC_ECF;
     function MORPHO.market(PreLiquidation.Id) external
       returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
     function MORPHO.position(PreLiquidation.Id, address) external
@@ -17,9 +21,9 @@ methods {
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivUp(a,b,c);
     function SharesMathLib.toSharesUp(uint256 a, uint256 b, uint256 c) internal
-        returns uint256 => tSU(a,b,c);
+        returns uint256 => summaryToSharesUp(a,b,c);
     function SharesMathLib.toAssetsUp(uint256 a, uint256 b, uint256 c) internal
-        returns uint256 => tAU(a,b,c);
+        returns uint256 => summaryToAssetsUp(a,b,c);
 
 }
 
@@ -40,41 +44,32 @@ function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y + (d-1)) / d);
 }
 
-function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    return require_uint256((x * y)/d);
-}
-
-function tAU(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
+function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
     return summaryMulDivUp(shares,
                            require_uint256(totalAssets + (10^6)),
                            require_uint256(totalShares + (10^6)));
 }
 
-function tSU(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
+function summaryToSharesUp(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
     return summaryMulDivUp(assets,
                            require_uint256(totalShares + (10^6)),
                            require_uint256(totalAssets + (10^6)));
 }
 
-definition WAD() returns uint256 = 10^18;
-
 definition ORACLE_SCALE() returns uint256  = 10^36;
 
 definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
   (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
 
-definition wDU(uint256 x,uint256 y) returns uint256 = summaryMulDivUp(x, WAD(), y);
-
-definition wDD(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, WAD(), y);
+definition wDivUp(uint256 x,uint256 y) returns uint256 = summaryMulDivUp(x, WAD(), y);
 
-definition wMD(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, y, WAD());
+definition wMulDown(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, y, WAD());
 
-definition computeFactor(mathint ltv, mathint lLtv, mathint preLLTV, mathint factor1, mathint factor2)
+definition computeLinearCombination(mathint ltv, mathint lltv, mathint preLltv, mathint yAtPreLltv, mathint yAtLltv)
     returns mathint =
-    wMD(wDD(require_uint256(ltv - preLLTV),
-            require_uint256(lLtv - preLLTV)),
-        require_uint256(factor2 - factor1)) + factor1;
+    wMulDown(wDivDown(require_uint256(ltv - preLltv),
+            require_uint256(lltv - preLltv)),
+        require_uint256(yAtLltv - yAtPreLltv)) + yAtPreLltv;
 
 // Checks that onMorphoRepay is only triggered by Morpho
 rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
@@ -82,58 +77,17 @@ rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
     assert e.msg.sender != currentContract.MORPHO => lastReverted;
 }
 
-//Ensure constructor requirements.
-
-invariant lltvNotZero()
-    0 < currentContract.LLTV
-{
-    preserved {
-        requireInvariant preLIFNotZero();
-    }
-}
-
-invariant preLltvLTlltv()
-    currentContract.PRE_LLTV < currentContract.LLTV
-{
-    preserved {
-        requireInvariant preLIFNotZero();
-    }
-}
-
-invariant preLCFIncreasing()
-    currentContract.PRE_LCF_1 <= currentContract.PRE_LCF_2
-    && currentContract.PRE_LCF_1 <= WAD()
-{
-    preserved {
-        requireInvariant preLIFNotZero();
-    }
-}
-
-invariant preLIFNotZero()
-    0 < currentContract.PRE_LIF_1;
-
-invariant preLIFIncreasing()
-    WAD() < currentContract.PRE_LIF_1
-    && currentContract.PRE_LIF_1 <= currentContract.PRE_LIF_2
-    && currentContract.PRE_LIF_2 <= wDD(WAD(),currentContract.LLTV)
-{
-    preserved {
-        requireInvariant lltvNotZero();
-    }
-}
-
-
 // Check that preLiquidate reverts when its inputs are not validated.
 rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
-    requireInvariant preLltvLTlltv();
-    requireInvariant preLCFIncreasing();
-    requireInvariant preLIFIncreasing();
+    requireInvariant preLltvConsistent();
+    requireInvariant preLCFConsistent();
+    requireInvariant preLIFConsistent();
     preLiquidate@withrevert(e, borrower, seizedAssets, repaidShares, data);
     assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted;
 }
 
 // Check that collateralQuoted == 0 would revert by failing require-statements.
-rule zeroCollateralQuotedReverts() {
+rule zeroCollateralQuotedReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
     // Market values.
     uint256 mTotalBorrowAssets;
     uint256 mTotalBorrowShares;
@@ -144,45 +98,60 @@ rule zeroCollateralQuotedReverts() {
 
     uint256 collateralPrice;
 
-    requireInvariant preLltvLTlltv();
+    requireInvariant preLltvConsistent();
 
     uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
-    uint256 borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
 
-    uint256 higherBound = wMD(collateralQuoted, currentContract.LLTV);
-    uint256 lowerBound = wMD(collateralQuoted, currentContract.PRE_LLTV);
+    uint256 higherBound = wMulDown(collateralQuoted, currentContract.LLTV);
+    uint256 lowerBound = wMulDown(collateralQuoted, currentContract.PRE_LLTV);
 
     assert  collateralQuoted == 0 => (lowerBound >= borrowed || borrowed > higherBound);
 }
 
-// Check that a liquidatable position implies that ltv > PRE_LLTV holds.
-rule preLiquidatableEquivlLtvLTPreLltv() {
+// Check that pre-liqudidating a position such that ltv <= PRE_LLTV would revert.
+// This also implies that ltv <= PRE_LLTV is equivalent to borrowed > collateralQuoted.wMulDown(PRE_LLTV).
+rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
     // Market values.
     uint256 mTotalBorrowAssets;
     uint256 mTotalBorrowShares;
+    uint256 mLastUpdate;
 
     // Position values.
     uint256 pBorrowShares;
     uint256 pCollateral;
 
-    uint256 collateralPrice;
+    requireInvariant preLltvConsistent();
+    requireInvariant preLCFConsistent();
+    requireInvariant preLIFConsistent();
 
-    requireInvariant preLltvLTlltv();
+    (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
 
-    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
+    // Ensure that no interest is accumulated.
+    require mLastUpdate == e.block.timestamp;
+
+    uint256 collateralPrice = mockPrice();
+
+    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
+
+    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
 
     // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
 
-    uint256 borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
-    uint256 ltv = require_uint256(wDU(borrowed,collateralQuoted));
-    uint256 lowerBound = wMD(collateralQuoted, currentContract.PRE_LLTV);
+    mathint borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    mathint ltv = require_uint256(wDivUp(require_uint256(borrowed), require_uint256(collateralQuoted)));
+
+    preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
+
+    // Ensure the price is unchanged in the preLiquidate call.
+    require !priceChanged;
 
-    assert (lowerBound < borrowed) <=> ltv > currentContract.PRE_LLTV;
+    assert ltv <= currentContract.PRE_LLTV => lastReverted;
 }
 
-// Check that pre-liqudidating a position such that ltv <= PRE_LLTV would revert.
-rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
+// Check that pre-liqudidating a position such that ltv > LLTV would revert.
+rule liquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
     // Market values.
     uint256 mTotalBorrowAssets;
     uint256 mTotalBorrowShares;
@@ -192,18 +161,15 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     uint256 pBorrowShares;
     uint256 pCollateral;
 
-    requireInvariant preLltvLTlltv();
-    requireInvariant preLCFIncreasing();
-    requireInvariant preLIFIncreasing();
+    requireInvariant preLltvConsistent();
+    requireInvariant preLCFConsistent();
+    requireInvariant preLIFConsistent();
 
     (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require mLastUpdate == e.block.timestamp;
 
-    // Consider that the collateral price hasn't changed.
-    priceChanged = false;
-
     uint256 collateralPrice = mockPrice();
 
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
@@ -213,12 +179,15 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
 
-    mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
-    mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
+    mathint borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    mathint ltv = require_uint256(wDivUp(require_uint256(borrowed), require_uint256(collateralQuoted)));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
-    assert !priceChanged && (ltv <= currentContract.PRE_LLTV) => lastReverted;
+    // Ensure the price is unchanged in the preLiquidate call.
+    require !priceChanged;
+
+    assert  ltv > currentContract.LLTV => lastReverted;
 }
 
 rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
@@ -234,9 +203,6 @@ rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets
     // Ensure that no interest is accumulated.
     require mLastUpdate == e.block.timestamp;
 
-    // Consider that the collateral price hasn't changed.
-    priceChanged = false;
-
     uint256 collateralPrice = mockPrice();
 
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
@@ -246,38 +212,42 @@ rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets
     // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
 
-    requireInvariant preLltvLTlltv();
-    requireInvariant preLCFIncreasing();
-    requireInvariant preLIFIncreasing();
+    requireInvariant preLltvConsistent();
+    requireInvariant preLCFConsistent();
+    requireInvariant preLIFConsistent();
 
-    mathint borrowed = require_uint256(tAU(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
-    mathint ltv = require_uint256(wDU(require_uint256(borrowed), require_uint256(collateralQuoted)));
+    mathint borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    mathint ltv = require_uint256(wDivUp(require_uint256(borrowed), require_uint256(collateralQuoted)));
 
 
-    mathint preLIF = computeFactor(ltv,
-                                   currentContract.LLTV,
-                                   currentContract.PRE_LLTV,
-                                   currentContract.PRE_LIF_1,
-                                   currentContract.PRE_LIF_2) ;
+    mathint preLIF = computeLinearCombination(ltv,
+                                              currentContract.LLTV,
+                                              currentContract.PRE_LLTV,
+                                              currentContract.PRE_LIF_1,
+                                              currentContract.PRE_LIF_2) ;
 
-    // Safe require as implementation would revert.
+    // Safe require as implementation would revert with InconsistentInput.
     require seizedAssets > 0;
 
     mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, collateralPrice, ORACLE_SCALE()));
 
-    mathint repaidShares = tSU(wDU(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
+    mathint repaidShares = summaryToSharesUp(wDivUp(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
                                mTotalBorrowAssets,
                                mTotalBorrowShares);
 
-    mathint closeFactor = computeFactor(ltv,
-                                        currentContract.LLTV,
-                                        currentContract.PRE_LLTV,
-                                        currentContract.PRE_LCF_1,
-                                        currentContract.PRE_LCF_2) ;
+    mathint closeFactor = computeLinearCombination(ltv,
+                                                   currentContract.LLTV,
+                                                   currentContract.PRE_LLTV,
+                                                   currentContract.PRE_LCF_1,
+                                                   currentContract.PRE_LCF_2) ;
 
-    mathint repayableShares = wMD(pBorrowShares, require_uint256(closeFactor));
+    mathint repayableShares = wMulDown(pBorrowShares, require_uint256(closeFactor));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
-    assert (!priceChanged && repaidShares > repayableShares ) => lastReverted;
+
+    // Ensure the price is unchanged in the preLiquidate call.
+    require !priceChanged;
+
+    assert repaidShares > repayableShares => lastReverted;
 
 }

From 44492ddc769a652ea63c6f39c139129ed37a652d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 10 Oct 2024 13:12:44 +0200
Subject: [PATCH 17/26] feat: add invariant checks to the CI

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

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 333c7d2..7b3a5e5 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -16,6 +16,7 @@ jobs:
 
       matrix:
         conf:
+          - ConsistentInstantiation
           - Immutability
           - MarketExists
           - Liveness

From c6055d71c6e780cbf23086ce653f858bb4bb0485 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 10 Oct 2024 14:32:38 +0200
Subject: [PATCH 18/26] fix: invariant timeout

---
 certora/confs/ConsistentInstantiation.conf | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/certora/confs/ConsistentInstantiation.conf b/certora/confs/ConsistentInstantiation.conf
index cc1b1d6..7523699 100644
--- a/certora/confs/ConsistentInstantiation.conf
+++ b/certora/confs/ConsistentInstantiation.conf
@@ -18,10 +18,11 @@
   },
   "verify": "PreLiquidation:certora/specs/ConsistentInstantiation.spec",
   "prover_args": [
-    "-depth 3",
-    "-mediumTimeout 3",
+    "-depth 5",
+    "-mediumTimeout 5",
     "-timeout 3600",
-    "-smt_nonLinearArithmetic true"
+    "-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",

From ebdaff6e0cdf9a9030237d530d03bf9708364178 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 25 Oct 2024 15:37:43 +0200
Subject: [PATCH 19/26] refactor: externalize summaries, minor fixes

---
 certora/confs/MarketExists.conf            |   5 +-
 certora/confs/Reverts.conf                 |   7 +-
 certora/specs/ConsistentInstantiation.spec |  16 +-
 certora/specs/Reverts.spec                 | 215 ++++++++-------------
 certora/specs/SummaryLib.spec              | 110 +++++++++++
 5 files changed, 198 insertions(+), 155 deletions(-)
 create mode 100644 certora/specs/SummaryLib.spec

diff --git a/certora/confs/MarketExists.conf b/certora/confs/MarketExists.conf
index d1c4037..831e0ba 100644
--- a/certora/confs/MarketExists.conf
+++ b/certora/confs/MarketExists.conf
@@ -7,10 +7,7 @@
     "PreLiquidation:MORPHO=Morpho"
   ],
   "parametric_contracts" : ["Morpho"],
-  "solc_optimize_map" : {
-    "Morpho" : "99999",
-    "PreLiquidation" : "99999",
-  },
+  "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index 08c0e23..10fc582 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -7,10 +7,7 @@
     "PreLiquidation:MORPHO=Morpho",
   ],
   "parametric_contracts" : ["PreLiquidation"],
-  "solc_optimize_map" : {
-    "Morpho" : "99999",
-    "PreLiquidation" : "99999",
-  },
+  "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
@@ -19,7 +16,7 @@
   "verify": "PreLiquidation:certora/specs/Reverts.spec",
   "prover_args": [
     "-depth 5",
-    "-mediumTimeout 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]",
diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec
index 399410f..c25af3c 100644
--- a/certora/specs/ConsistentInstantiation.spec
+++ b/certora/specs/ConsistentInstantiation.spec
@@ -1,18 +1,15 @@
 //Ensure constructor requirements.
 
+import "SummaryLib.spec";
+
 methods {
     function _.market(PreLiquidation.Id) external => DISPATCHER(true);
 }
 
-function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    return require_uint256((x * y)/d);
-}
-
-definition WAD() returns uint256 = 10^18;
-
 definition wDivDown(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, WAD(), y);
 
+// Base case for mutually dependent invariants.
+// Ensure that in a successfully deployed contract the preLLTV value is not zero.
 invariant lltvNotZero()
     0 < currentContract.LLTV
 {
@@ -21,6 +18,7 @@ invariant lltvNotZero()
     }
 }
 
+// Ensure that a successfully deployed contract has a consistent preLLTV value.
 invariant preLltvConsistent()
     currentContract.PRE_LLTV < currentContract.LLTV
 {
@@ -29,6 +27,7 @@ invariant preLltvConsistent()
     }
 }
 
+// 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()
@@ -38,9 +37,12 @@ invariant preLCFConsistent()
     }
 }
 
+// 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
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index b8ad211..dae3d41 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -5,73 +5,25 @@ import "ConsistentInstantiation.spec";
 using Morpho as MORPHO;
 
 methods {
-    function _.position(PreLiquidation.Id, address) external => DISPATCHER(true);
-    function _.accrueInterest(PreLiquidation.MarketParams) external => DISPATCHER(true);
-    function _.borrowRate(PreLiquidation.MarketParams, PreLiquidation.Id) external => HAVOC_ECF;
+    function _.price() external => mockPrice() expect uint256;
+
     function MORPHO.market(PreLiquidation.Id) external
-      returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
+        returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
     function MORPHO.position(PreLiquidation.Id, address) external
-      returns (uint256, uint128, uint128) envfree;
-    function MORPHO.idToMarketParams(PreLiquidation.Id) external
-      returns (address, address, address, address, uint256) envfree;
-    function _.price() external => mockPrice() expect uint256;
+        returns (uint256, uint128, uint128) envfree;
+
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
-        returns uint256
-        => summaryMulDivDown(a,b,c);
+        returns uint256 => summaryMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivUp(a,b,c);
+
     function SharesMathLib.toSharesUp(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryToSharesUp(a,b,c);
     function SharesMathLib.toAssetsUp(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryToAssetsUp(a,b,c);
-
-}
-
-persistent ghost uint256 lastPrice;
-persistent ghost bool priceChanged;
-
-function mockPrice() returns uint256 {
-    uint256 updatedPrice;
-    if (updatedPrice != lastPrice) {
-        priceChanged = true;
-        lastPrice = updatedPrice;
-    }
-    return updatedPrice;
-}
-
-function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    return require_uint256((x * y + (d-1)) / d);
-}
-
-function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
-    return summaryMulDivUp(shares,
-                           require_uint256(totalAssets + (10^6)),
-                           require_uint256(totalShares + (10^6)));
 }
 
-function summaryToSharesUp(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
-    return summaryMulDivUp(assets,
-                           require_uint256(totalShares + (10^6)),
-                           require_uint256(totalAssets + (10^6)));
-}
-
-definition ORACLE_SCALE() returns uint256  = 10^36;
-
-definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
-  (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
-
-definition wDivUp(uint256 x,uint256 y) returns uint256 = summaryMulDivUp(x, WAD(), y);
-
-definition wMulDown(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, y, WAD());
-
-definition computeLinearCombination(mathint ltv, mathint lltv, mathint preLltv, mathint yAtPreLltv, mathint yAtLltv)
-    returns mathint =
-    wMulDown(wDivDown(require_uint256(ltv - preLltv),
-            require_uint256(lltv - preLltv)),
-        require_uint256(yAtLltv - yAtPreLltv)) + yAtPreLltv;
-
-// Checks that onMorphoRepay is only triggered by Morpho
+// 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;
@@ -79,68 +31,42 @@ rule onMorphoRepaySenderValidation(env e, uint256 repaidAssets, bytes data) {
 
 // Check that preLiquidate reverts when its inputs are not validated.
 rule preLiquidateInputValidation(env e, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
+    // Avoid absurd divisions by zero.
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
+
     preLiquidate@withrevert(e, borrower, seizedAssets, repaidShares, data);
-    assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted;
+    assert !summaryExactlyOneZero(seizedAssets, repaidShares) => lastReverted;
 }
 
 // Check that collateralQuoted == 0 would revert by failing require-statements.
 rule zeroCollateralQuotedReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
-    // Market values.
-    uint256 mTotalBorrowAssets;
-    uint256 mTotalBorrowShares;
-
-    // Position values.
-    uint256 pBorrowShares;
-    uint256 pCollateral;
-
-    uint256 collateralPrice;
-
     requireInvariant preLltvConsistent();
 
-    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
-    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    uint256 collateralQuoted;
+    uint256 borrowed;
 
-    uint256 higherBound = wMulDown(collateralQuoted, currentContract.LLTV);
-    uint256 lowerBound = wMulDown(collateralQuoted, currentContract.PRE_LLTV);
+    uint256 higherBound = summaryWMulDown(collateralQuoted, currentContract.LLTV);
+    uint256 lowerBound = summaryWMulDown(collateralQuoted, currentContract.PRE_LLTV);
 
     assert  collateralQuoted == 0 => (lowerBound >= borrowed || borrowed > higherBound);
 }
 
-// Check that pre-liqudidating a position such that ltv <= PRE_LLTV would revert.
-// This also implies that ltv <= PRE_LLTV is equivalent to borrowed > collateralQuoted.wMulDown(PRE_LLTV).
+// Check that pre-liquidating a position such that LTV <= PRE_LLTV reverts.
+// This also implies that LTV > PRE_LLTV when borrowed > collateralQuoted.summaryWMulDown(PRE_LLTV).
 rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
-    // Market values.
-    uint256 mTotalBorrowAssets;
-    uint256 mTotalBorrowShares;
-    uint256 mLastUpdate;
-
-    // Position values.
-    uint256 pBorrowShares;
-    uint256 pCollateral;
-
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    uint256 mLastUpdate;
+    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require mLastUpdate == e.block.timestamp;
 
-    uint256 collateralPrice = mockPrice();
-
-    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
-
-    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
-
-    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
-    require collateralQuoted > 0;
-
-    mathint borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
-    mathint ltv = require_uint256(wDivUp(require_uint256(borrowed), require_uint256(collateralQuoted)));
+    mathint ltv = getLtv(borrower);
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
@@ -150,75 +76,50 @@ rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets
     assert ltv <= currentContract.PRE_LLTV => lastReverted;
 }
 
-// Check that pre-liqudidating a position such that ltv > LLTV would revert.
-rule liquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
-    // Market values.
-    uint256 mTotalBorrowAssets;
-    uint256 mTotalBorrowShares;
-    uint256 mLastUpdate;
-
-    // Position values.
-    uint256 pBorrowShares;
-    uint256 pCollateral;
-
+// Check that pre-liquidating a position such that LTV > LLTV would revert.
+rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    uint256 mLastUpdate;
+    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require mLastUpdate == e.block.timestamp;
 
-    uint256 collateralPrice = mockPrice();
-
-    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
-
-    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
-
-    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
-    require collateralQuoted > 0;
-
-    mathint borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
-    mathint ltv = require_uint256(wDivUp(require_uint256(borrowed), require_uint256(collateralQuoted)));
+    mathint ltv = getLtv(borrower);
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
     // Ensure the price is unchanged in the preLiquidate call.
     require !priceChanged;
 
-    assert  ltv > currentContract.LLTV => lastReverted;
+    assert ltv > currentContract.LLTV => lastReverted;
 }
 
-rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
+// Check that a pre-liquidation that repays more shares than available or allowed by the preLCF reverts.
+rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
+    // Market values.
     uint256 mTotalBorrowAssets;
     uint256 mTotalBorrowShares;
     uint256 mLastUpdate;
 
+    // Position values.
     uint256 pBorrowShares;
-    uint256 pCollateral;
-
-    (_, _, mTotalBorrowAssets,mTotalBorrowShares,mLastUpdate, _) = MORPHO.market(currentContract.ID);
-
-    // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
-
-    uint256 collateralPrice = mockPrice();
-
-    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
-
-    mathint collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_SCALE()));
-
-    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
-    require collateralQuoted > 0;
 
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    mathint borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
-    mathint ltv = require_uint256(wDivUp(require_uint256(borrowed), require_uint256(collateralQuoted)));
+    (_, _, mTotalBorrowAssets, mTotalBorrowShares, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+
+    // Ensure that no interest is accumulated.
+    require mLastUpdate == e.block.timestamp;
+
+    (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
 
+    mathint ltv = getLtv(borrower);
 
     mathint preLIF = computeLinearCombination(ltv,
                                               currentContract.LLTV,
@@ -229,9 +130,9 @@ rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets
     // Safe require as implementation would revert with InconsistentInput.
     require seizedAssets > 0;
 
-    mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, collateralPrice, ORACLE_SCALE()));
+    mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, mockPrice(), ORACLE_PRICE_SCALE()));
 
-    mathint repaidShares = summaryToSharesUp(wDivUp(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
+    mathint repaidShares = summaryToSharesUp(summaryWDivUp(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
                                mTotalBorrowAssets,
                                mTotalBorrowShares);
 
@@ -241,7 +142,7 @@ rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets
                                                    currentContract.PRE_LCF_1,
                                                    currentContract.PRE_LCF_2) ;
 
-    mathint repayableShares = wMulDown(pBorrowShares, require_uint256(closeFactor));
+    mathint repayableShares = summaryWMulDown(pBorrowShares, require_uint256(closeFactor));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
@@ -251,3 +152,39 @@ rule excessivePreliquidationReverts(env e,address borrower, uint256 seizedAssets
     assert repaidShares > repayableShares => lastReverted;
 
 }
+
+// Check that repaying more shares than available or allowed by the preLCF would revert.
+rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 repaidShares, bytes data) {
+    requireInvariant preLltvConsistent();
+    requireInvariant preLCFConsistent();
+    requireInvariant preLIFConsistent();
+
+    uint256 mLastUpdate;
+    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+
+    // Ensure that no interest is accumulated.
+    require mLastUpdate == e.block.timestamp;
+
+    uint256 pBorrowShares;
+    (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
+
+    mathint ltv = getLtv(borrower);
+
+    // Safe require as implementation would revert with InconsistentInput.
+    require repaidShares > 0;
+
+    mathint closeFactor = computeLinearCombination(ltv,
+                                                   currentContract.LLTV,
+                                                   currentContract.PRE_LLTV,
+                                                   currentContract.PRE_LCF_1,
+                                                   currentContract.PRE_LCF_2) ;
+
+    mathint repayableShares = summaryWMulDown(pBorrowShares, require_uint256(closeFactor));
+
+    preLiquidate@withrevert(e, borrower, 0, repaidShares, data);
+
+    // Ensure the price is unchanged in the preLiquidate call.
+    require !priceChanged;
+
+    assert repaidShares > repayableShares => lastReverted;
+}
diff --git a/certora/specs/SummaryLib.spec b/certora/specs/SummaryLib.spec
new file mode 100644
index 0000000..5e43632
--- /dev/null
+++ b/certora/specs/SummaryLib.spec
@@ -0,0 +1,110 @@
+definition WAD() returns uint256 = 10^18;
+
+definition ORACLE_PRICE_SCALE() returns uint256 = 10^36;
+
+definition VIRTUAL_SHARES() returns uint256 = 10^6;
+
+definition VIRTUAL_ASSETS() returns uint256 = 1;
+
+function summaryWMulDown(uint256 x,uint256 y) returns uint256 {
+    return summaryMulDivDown(x, y, WAD());
+}
+
+function summaryWDivDown(uint256 x,uint256 y) returns uint256 {
+    return summaryMulDivDown(x, WAD(), y);
+}
+
+function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y)/d);
+}
+
+function summaryWDivUp(uint256 x,uint256 y) returns uint256 {
+    return summaryMulDivUp(x, WAD(), y);
+}
+
+function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y + (d-1)) / d);
+}
+
+
+function summaryToAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
+    return summaryMulDivDown(shares,
+                             require_uint256(totalAssets + VIRTUAL_ASSETS()),
+                             require_uint256(totalShares + VIRTUAL_SHARES()));
+}
+
+function summaryToSharesUp(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
+    return summaryMulDivUp(assets,
+                           require_uint256(totalShares + VIRTUAL_SHARES()),
+                           require_uint256(totalAssets + VIRTUAL_ASSETS()));
+}
+
+function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
+    return summaryMulDivUp(shares,
+                           require_uint256(totalAssets + VIRTUAL_ASSETS()),
+                           require_uint256(totalShares + VIRTUAL_SHARES()));
+}
+
+function summaryMarketParams() returns PreLiquidation.MarketParams {
+    PreLiquidation.MarketParams x;
+    require
+        x.loanToken == currentContract.LOAN_TOKEN
+        && x.collateralToken == currentContract.COLLATERAL_TOKEN
+        && x.oracle == currentContract.ORACLE
+        && x.irm == currentContract.IRM
+        && x.lltv == currentContract.LLTV;
+    return x;
+}
+
+function summaryExactlyOneZero(uint256 assets, uint256 shares) returns bool {
+    return (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
+}
+
+persistent ghost uint256 lastPrice;
+persistent ghost bool priceChanged;
+
+function mockPrice() returns uint256 {
+    uint256 updatedPrice;
+    if (updatedPrice != lastPrice) {
+        priceChanged = true;
+        lastPrice = updatedPrice;
+    }
+    return updatedPrice;
+}
+
+function positionAsAssets (address borrower) returns (uint256, uint256) {
+    uint256 mTotalBorrowAssets;
+    uint256 mTotalBorrowShares;
+
+    uint256 pBorrowShares;
+    uint256 pCollateral;
+
+    (_, _, mTotalBorrowAssets, mTotalBorrowShares,_ , _) = MORPHO.market(currentContract.ID);
+    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
+
+    uint256 collateralPrice = mockPrice();
+    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_PRICE_SCALE()));
+
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
+    require collateralQuoted > 0;
+
+    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+
+    return (borrowed, collateralQuoted);
+}
+
+function getLtv(address borrower) returns uint256 {
+    uint256 borrowed;
+    uint256 collateralQuoted;
+
+    (borrowed, collateralQuoted) = positionAsAssets(borrower);
+
+    return summaryWDivUp(borrowed, collateralQuoted);
+}
+
+definition computeLinearCombination(mathint ltv, mathint lltv, mathint preLltv, mathint yAtPreLltv, mathint yAtLltv)
+    returns mathint = summaryWMulDown(summaryWDivDown(require_uint256(ltv - preLltv),
+                                                      require_uint256(lltv - preLltv)),
+                                      require_uint256(yAtLltv - yAtPreLltv)) + yAtPreLltv;

From cabfbf61f2451104b3c7ec306455792b5172613b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 25 Oct 2024 15:50:46 +0200
Subject: [PATCH 20/26] fix: avoid breaking other specs

---
 certora/confs/ConsistentInstantiation.conf |  5 +----
 certora/specs/ConsistentInstantiation.spec |  6 +++---
 certora/specs/Reverts.spec                 |  7 -------
 certora/specs/SummaryLib.spec              | 12 ++++++++++++
 4 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/certora/confs/ConsistentInstantiation.conf b/certora/confs/ConsistentInstantiation.conf
index 7523699..2886e4d 100644
--- a/certora/confs/ConsistentInstantiation.conf
+++ b/certora/confs/ConsistentInstantiation.conf
@@ -7,10 +7,7 @@
     "PreLiquidation:MORPHO=Morpho",
   ],
   "parametric_contracts" : ["PreLiquidation"],
-  "solc_optimize_map" : {
-    "Morpho" : "99999",
-    "PreLiquidation" : "99999",
-  },
+  "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec
index c25af3c..d458dd1 100644
--- a/certora/specs/ConsistentInstantiation.spec
+++ b/certora/specs/ConsistentInstantiation.spec
@@ -1,4 +1,4 @@
-//Ensure constructor requirements.
+// SPDX-License-Identifier: GPL-2.0-or-later
 
 import "SummaryLib.spec";
 
@@ -6,7 +6,7 @@ methods {
     function _.market(PreLiquidation.Id) external => DISPATCHER(true);
 }
 
-definition wDivDown(uint256 x,uint256 y) returns uint256 = summaryMulDivDown(x, WAD(), y);
+//Ensure constructor requirements.
 
 // Base case for mutually dependent invariants.
 // Ensure that in a successfully deployed contract the preLLTV value is not zero.
@@ -46,7 +46,7 @@ invariant preLIFNotZero()
 invariant preLIFConsistent()
     WAD() < currentContract.PRE_LIF_1
     && currentContract.PRE_LIF_1 <= currentContract.PRE_LIF_2
-    && currentContract.PRE_LIF_2 <= wDivDown(WAD(),currentContract.LLTV)
+    && currentContract.PRE_LIF_2 <= summaryWDivDown(WAD(),currentContract.LLTV)
 {
     preserved {
         requireInvariant lltvNotZero();
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index dae3d41..74e6da9 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -2,16 +2,9 @@
 
 import "ConsistentInstantiation.spec";
 
-using Morpho as MORPHO;
-
 methods {
     function _.price() external => mockPrice() expect uint256;
 
-    function MORPHO.market(PreLiquidation.Id) external
-        returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
-    function MORPHO.position(PreLiquidation.Id, address) external
-        returns (uint256, uint128, uint128) envfree;
-
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal
diff --git a/certora/specs/SummaryLib.spec b/certora/specs/SummaryLib.spec
index 5e43632..f9bc153 100644
--- a/certora/specs/SummaryLib.spec
+++ b/certora/specs/SummaryLib.spec
@@ -1,3 +1,14 @@
+// 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;
+    function MORPHO.position(PreLiquidation.Id, address) external
+        returns (uint256, uint128, uint128) envfree;
+}
+
 definition WAD() returns uint256 = 10^18;
 
 definition ORACLE_PRICE_SCALE() returns uint256 = 10^36;
@@ -26,6 +37,7 @@ function summaryWDivUp(uint256 x,uint256 y) returns uint256 {
 function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
     // Safe require because the reference implementation would revert.
     return require_uint256((x * y + (d-1)) / d);
+
 }
 
 

From 51112e94a1c04c2f5126db8cbdc6cfa8ac77e8e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 25 Oct 2024 15:58:10 +0200
Subject: [PATCH 21/26] fix: formatting

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

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 74e6da9..058f2cf 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -48,7 +48,7 @@ rule zeroCollateralQuotedReverts(env e, address borrower, uint256 seizedAssets,
 
 // Check that pre-liquidating a position such that LTV <= PRE_LLTV reverts.
 // This also implies that LTV > PRE_LLTV when borrowed > collateralQuoted.summaryWMulDown(PRE_LLTV).
-rule nonLiquidatablePositionReverts(env e,address borrower, uint256 seizedAssets, bytes data) {
+rule nonLiquidatablePositionReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();

From 350020475fe843e54d61676820b7ce55ecd6eff2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 28 Oct 2024 00:51:19 +0100
Subject: [PATCH 22/26] fix: add getter and hashOfMarketParams invariant

---
 certora/confs/ConsistentInstantiation.conf | 14 +++++----
 certora/confs/Reverts.conf                 | 12 ++++----
 certora/helpers/PreLiquidationHarness.sol  | 18 +++++++++++
 certora/helpers/Util.sol                   | 14 +++++++++
 certora/specs/ConsistentInstantiation.spec | 16 +++++++++-
 certora/specs/Reverts.spec                 | 35 ++++++++++------------
 certora/specs/SummaryLib.spec              | 23 +++++++-------
 7 files changed, 88 insertions(+), 44 deletions(-)
 create mode 100644 certora/helpers/PreLiquidationHarness.sol
 create mode 100644 certora/helpers/Util.sol

diff --git a/certora/confs/ConsistentInstantiation.conf b/certora/confs/ConsistentInstantiation.conf
index 2886e4d..2fef3e8 100644
--- a/certora/confs/ConsistentInstantiation.conf
+++ b/certora/confs/ConsistentInstantiation.conf
@@ -1,19 +1,21 @@
 {
   "files": [
-    "src/PreLiquidation.sol",
+    "certora/helpers/PreLiquidationHarness.sol",
+    "certora/helpers/Util.sol",
     "lib/morpho-blue/src/Morpho.sol",
   ],
   "link": [
-    "PreLiquidation:MORPHO=Morpho",
+    "PreLiquidationHarness:MORPHO=Morpho",
   ],
-  "parametric_contracts" : ["PreLiquidation"],
+  "parametric_contracts" : ["PreLiquidationHarness"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
-    "PreLiquidation": "solc-0.8.27",
+    "PreLiquidationHarness": "solc-0.8.27",
+    "Util": "solc-0.8.27",
   },
-  "verify": "PreLiquidation:certora/specs/ConsistentInstantiation.spec",
+  "verify": "PreLiquidationHarness:certora/specs/ConsistentInstantiation.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 5",
@@ -23,5 +25,5 @@
   ],
   "rule_sanity": "basic",
   "server": "production",
-  "msg": "PreLiquidation ConsistentInstantiation",
+  "msg": "PreLiquidationHarness ConsistentInstantiation",
 }
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index 10fc582..095d16f 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -1,19 +1,21 @@
 {
   "files": [
-    "src/PreLiquidation.sol",
+    "certora/helpers/PreLiquidationHarness.sol",
+    "certora/helpers/Util.sol",
     "lib/morpho-blue/src/Morpho.sol",
   ],
   "link": [
-    "PreLiquidation:MORPHO=Morpho",
+    "PreLiquidationHarness:MORPHO=Morpho",
   ],
-  "parametric_contracts" : ["PreLiquidation"],
+  "parametric_contracts" : ["PreLiquidationHarness"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
-    "PreLiquidation": "solc-0.8.27",
+    "PreLiquidationHarness": "solc-0.8.27",
+    "Util": "solc-0.8.27",
   },
-  "verify": "PreLiquidation:certora/specs/Reverts.spec",
+  "verify": "PreLiquidationHarness:certora/specs/Reverts.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 40",
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
new file mode 100644
index 0000000..59891df
--- /dev/null
+++ b/certora/helpers/PreLiquidationHarness.sol
@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {PreLiquidation, Market, Position, Id, PreLiquidationParams} from "src/PreLiquidation.sol";
+
+contract PreLiquidationHarness is PreLiquidation {
+    constructor(address morpho, Id id, PreLiquidationParams memory _preLiquidationParams)
+        PreLiquidation(morpho, id, _preLiquidationParams)
+    {}
+
+    function market_(Id id) external view returns (Market memory) {
+        return MORPHO.market(id);
+    }
+
+    function position_(Id id, address borrower) external view returns (Position memory) {
+        return MORPHO.position(id, borrower);
+    }
+}
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
new file mode 100644
index 0000000..7dc5bef
--- /dev/null
+++ b/certora/helpers/Util.sol
@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {Id, MarketParams} from "src/PreLiquidation.sol";
+
+import {MarketParamsLib} from "lib/morpho-blue/src/libraries/MarketParamsLib.sol";
+
+contract Util {
+    using MarketParamsLib for MarketParams;
+
+    function libId(MarketParams memory marketParams) external pure returns (Id) {
+        return marketParams.id();
+    }
+}
diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec
index d458dd1..62d223f 100644
--- a/certora/specs/ConsistentInstantiation.spec
+++ b/certora/specs/ConsistentInstantiation.spec
@@ -2,8 +2,13 @@
 
 import "SummaryLib.spec";
 
+using Util as Util;
+
 methods {
-    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
+    function _.market(PreLiquidationHarness.Id) external => DISPATCHER(true);
+
+    function Util.libId(PreLiquidationHarness.MarketParams) external
+        returns PreLiquidationHarness.Id envfree;
 }
 
 //Ensure constructor requirements.
@@ -52,3 +57,12 @@ invariant preLIFConsistent()
         requireInvariant lltvNotZero();
     }
 }
+
+// Ensure that ID equals idToMarketParams(marketParams()).
+invariant hashOfMarketParamsOf()
+    Util.libId(summaryMarketParams()) == currentContract.ID
+{
+    preserved {
+        requireInvariant preLIFNotZero();
+    }
+}
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 058f2cf..56d4b88 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -4,6 +4,8 @@ import "ConsistentInstantiation.spec";
 
 methods {
     function _.price() external => mockPrice() expect uint256;
+    function market_(PreLiquidationHarness.Id) external
+        returns (PreLiquidationHarness.Market memory) envfree;
 
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivDown(a,b,c);
@@ -52,12 +54,12 @@ rule nonLiquidatablePositionReverts(env e, address borrower, uint256 seizedAsset
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
+    requireInvariant hashOfMarketParamsOf();
 
-    uint256 mLastUpdate;
-    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
     mathint ltv = getLtv(borrower);
 
@@ -75,11 +77,10 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    uint256 mLastUpdate;
-    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
     mathint ltv = getLtv(borrower);
 
@@ -93,11 +94,6 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
 
 // Check that a pre-liquidation that repays more shares than available or allowed by the preLCF reverts.
 rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
-    // Market values.
-    uint256 mTotalBorrowAssets;
-    uint256 mTotalBorrowShares;
-    uint256 mLastUpdate;
-
     // Position values.
     uint256 pBorrowShares;
 
@@ -105,10 +101,10 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    (_, _, mTotalBorrowAssets, mTotalBorrowShares, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
     (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
 
@@ -126,8 +122,8 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
     mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, mockPrice(), ORACLE_PRICE_SCALE()));
 
     mathint repaidShares = summaryToSharesUp(summaryWDivUp(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
-                               mTotalBorrowAssets,
-                               mTotalBorrowShares);
+                                             m.totalBorrowAssets,
+                                             m.totalBorrowShares);
 
     mathint closeFactor = computeLinearCombination(ltv,
                                                    currentContract.LLTV,
@@ -148,17 +144,18 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
 
 // Check that repaying more shares than available or allowed by the preLCF would revert.
 rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 repaidShares, bytes data) {
+    // Position values.
+    uint256 pBorrowShares;
+
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    uint256 mLastUpdate;
-    (_, _, _, _, mLastUpdate, _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
-    require mLastUpdate == e.block.timestamp;
+    require m.lastUpdate == e.block.timestamp;
 
-    uint256 pBorrowShares;
     (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
 
     mathint ltv = getLtv(borrower);
diff --git a/certora/specs/SummaryLib.spec b/certora/specs/SummaryLib.spec
index f9bc153..8858791 100644
--- a/certora/specs/SummaryLib.spec
+++ b/certora/specs/SummaryLib.spec
@@ -3,9 +3,7 @@
 using Morpho as MORPHO;
 
 methods {
-    function MORPHO.market(PreLiquidation.Id) external
-        returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
-    function MORPHO.position(PreLiquidation.Id, address) external
+    function MORPHO.position(PreLiquidationHarness.Id, address) external
         returns (uint256, uint128, uint128) envfree;
 }
 
@@ -40,7 +38,6 @@ function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
 
 }
 
-
 function summaryToAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
     return summaryMulDivDown(shares,
                              require_uint256(totalAssets + VIRTUAL_ASSETS()),
@@ -59,8 +56,8 @@ function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalSha
                            require_uint256(totalShares + VIRTUAL_SHARES()));
 }
 
-function summaryMarketParams() returns PreLiquidation.MarketParams {
-    PreLiquidation.MarketParams x;
+function summaryMarketParams() returns PreLiquidationHarness.MarketParams {
+    PreLiquidationHarness.MarketParams x;
     require
         x.loanToken == currentContract.LOAN_TOKEN
         && x.collateralToken == currentContract.COLLATERAL_TOKEN
@@ -86,23 +83,23 @@ function mockPrice() returns uint256 {
     return updatedPrice;
 }
 
-function positionAsAssets (address borrower) returns (uint256, uint256) {
-    uint256 mTotalBorrowAssets;
-    uint256 mTotalBorrowShares;
 
+// Ensure this function is only used when no interest is accrued,
+// or enforce that the last update matches the current timestamp.
+function positionAsAssets (address borrower) returns (uint256, uint256) {
     uint256 pBorrowShares;
     uint256 pCollateral;
 
-    (_, _, mTotalBorrowAssets, mTotalBorrowShares,_ , _) = MORPHO.market(currentContract.ID);
+    PreLiquidationHarness.Market m = market_(currentContract.ID);
+
     (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
 
-    uint256 collateralPrice = mockPrice();
-    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, collateralPrice, ORACLE_PRICE_SCALE()));
+    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, mockPrice(), ORACLE_PRICE_SCALE()));
 
     // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
 
-    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, mTotalBorrowAssets, mTotalBorrowShares));
+    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, m.totalBorrowAssets, m.totalBorrowShares));
 
     return (borrowed, collateralQuoted);
 }

From 66e34b853f8dad988ed019760515fefe2a68d88d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 28 Oct 2024 08:07:46 +0100
Subject: [PATCH 23/26] fix: fix failing ci

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

diff --git a/certora/specs/SummaryLib.spec b/certora/specs/SummaryLib.spec
index 8858791..6b7804c 100644
--- a/certora/specs/SummaryLib.spec
+++ b/certora/specs/SummaryLib.spec
@@ -5,6 +5,9 @@ using Morpho as MORPHO;
 methods {
     function MORPHO.position(PreLiquidationHarness.Id, address) external
         returns (uint256, uint128, uint128) envfree;
+
+    function market_(PreLiquidationHarness.Id) external
+        returns (PreLiquidationHarness.Market memory) envfree;
 }
 
 definition WAD() returns uint256 = 10^18;

From 8c4110a8134c977d27abc287859c44e362cde28e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 28 Oct 2024 13:57:09 +0100
Subject: [PATCH 24/26] fix: use getters for the morpho-blue project

---
 certora/confs/ConsistentInstantiation.conf | 20 +++++++-------
 certora/confs/Reverts.conf                 | 18 ++++++-------
 certora/helpers/PreLiquidationHarness.sol  | 18 -------------
 certora/helpers/Util.sol                   | 14 ----------
 certora/specs/ConsistentInstantiation.spec |  8 +++---
 certora/specs/Reverts.spec                 | 30 +++++++++------------
 certora/specs/SummaryLib.spec              | 31 +++++++++-------------
 7 files changed, 48 insertions(+), 91 deletions(-)
 delete mode 100644 certora/helpers/PreLiquidationHarness.sol
 delete mode 100644 certora/helpers/Util.sol

diff --git a/certora/confs/ConsistentInstantiation.conf b/certora/confs/ConsistentInstantiation.conf
index 2fef3e8..42e80c9 100644
--- a/certora/confs/ConsistentInstantiation.conf
+++ b/certora/confs/ConsistentInstantiation.conf
@@ -1,21 +1,21 @@
 {
   "files": [
-    "certora/helpers/PreLiquidationHarness.sol",
-    "certora/helpers/Util.sol",
-    "lib/morpho-blue/src/Morpho.sol",
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
   ],
   "link": [
-    "PreLiquidationHarness:MORPHO=Morpho",
+    "PreLiquidation:MORPHO=MorphoHarness",
   ],
-  "parametric_contracts" : ["PreLiquidationHarness"],
+  "parametric_contracts" : ["PreLiquidation"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
-    "Morpho": "solc-0.8.19",
-    "PreLiquidationHarness": "solc-0.8.27",
-    "Util": "solc-0.8.27",
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+    "PreLiquidation": "solc-0.8.27",
   },
-  "verify": "PreLiquidationHarness:certora/specs/ConsistentInstantiation.spec",
+  "verify": "PreLiquidation:certora/specs/ConsistentInstantiation.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 5",
@@ -25,5 +25,5 @@
   ],
   "rule_sanity": "basic",
   "server": "production",
-  "msg": "PreLiquidationHarness ConsistentInstantiation",
+  "msg": "PreLiquidation ConsistentInstantiation",
 }
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index 095d16f..c5efb9c 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -1,21 +1,21 @@
 {
   "files": [
-    "certora/helpers/PreLiquidationHarness.sol",
-    "certora/helpers/Util.sol",
-    "lib/morpho-blue/src/Morpho.sol",
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
   ],
   "link": [
-    "PreLiquidationHarness:MORPHO=Morpho",
+    "PreLiquidation:MORPHO=MorphoHarness",
   ],
-  "parametric_contracts" : ["PreLiquidationHarness"],
+  "parametric_contracts" : ["PreLiquidation"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
-    "Morpho": "solc-0.8.19",
-    "PreLiquidationHarness": "solc-0.8.27",
-    "Util": "solc-0.8.27",
+    "PreLiquidation": "solc-0.8.27",
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
   },
-  "verify": "PreLiquidationHarness:certora/specs/Reverts.spec",
+  "verify": "PreLiquidation:certora/specs/Reverts.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 40",
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
deleted file mode 100644
index 59891df..0000000
--- a/certora/helpers/PreLiquidationHarness.sol
+++ /dev/null
@@ -1,18 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.27;
-
-import {PreLiquidation, Market, Position, Id, PreLiquidationParams} from "src/PreLiquidation.sol";
-
-contract PreLiquidationHarness is PreLiquidation {
-    constructor(address morpho, Id id, PreLiquidationParams memory _preLiquidationParams)
-        PreLiquidation(morpho, id, _preLiquidationParams)
-    {}
-
-    function market_(Id id) external view returns (Market memory) {
-        return MORPHO.market(id);
-    }
-
-    function position_(Id id, address borrower) external view returns (Position memory) {
-        return MORPHO.position(id, borrower);
-    }
-}
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
deleted file mode 100644
index 7dc5bef..0000000
--- a/certora/helpers/Util.sol
+++ /dev/null
@@ -1,14 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.27;
-
-import {Id, MarketParams} from "src/PreLiquidation.sol";
-
-import {MarketParamsLib} from "lib/morpho-blue/src/libraries/MarketParamsLib.sol";
-
-contract Util {
-    using MarketParamsLib for MarketParams;
-
-    function libId(MarketParams memory marketParams) external pure returns (Id) {
-        return marketParams.id();
-    }
-}
diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec
index 62d223f..ec8ec1a 100644
--- a/certora/specs/ConsistentInstantiation.spec
+++ b/certora/specs/ConsistentInstantiation.spec
@@ -2,13 +2,11 @@
 
 import "SummaryLib.spec";
 
-using Util as Util;
-
 methods {
-    function _.market(PreLiquidationHarness.Id) external => DISPATCHER(true);
+    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
 
-    function Util.libId(PreLiquidationHarness.MarketParams) external
-        returns PreLiquidationHarness.Id envfree;
+    function Util.libId(PreLiquidation.MarketParams) external
+        returns PreLiquidation.Id envfree;
 }
 
 //Ensure constructor requirements.
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 56d4b88..3760287 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -4,8 +4,11 @@ import "ConsistentInstantiation.spec";
 
 methods {
     function _.price() external => mockPrice() expect uint256;
-    function market_(PreLiquidationHarness.Id) external
-        returns (PreLiquidationHarness.Market memory) envfree;
+
+    function MORPHO.market_(PreLiquidation.Id) external
+        returns (PreLiquidation.Market memory) envfree;
+    function MORPHO.position_(PreLiquidation.Id, address) external
+        returns (PreLiquidation.Position memory) envfree;
 
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivDown(a,b,c);
@@ -54,9 +57,8 @@ rule nonLiquidatablePositionReverts(env e, address borrower, uint256 seizedAsset
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
-    requireInvariant hashOfMarketParamsOf();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
@@ -77,7 +79,7 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
@@ -94,19 +96,16 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
 
 // Check that a pre-liquidation that repays more shares than available or allowed by the preLCF reverts.
 rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
-    // Position values.
-    uint256 pBorrowShares;
-
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
 
-    (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
+    PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
 
     mathint ltv = getLtv(borrower);
 
@@ -131,7 +130,7 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
                                                    currentContract.PRE_LCF_1,
                                                    currentContract.PRE_LCF_2) ;
 
-    mathint repayableShares = summaryWMulDown(pBorrowShares, require_uint256(closeFactor));
+    mathint repayableShares = summaryWMulDown(p.borrowShares, require_uint256(closeFactor));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
@@ -144,19 +143,16 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
 
 // Check that repaying more shares than available or allowed by the preLCF would revert.
 rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 repaidShares, bytes data) {
-    // Position values.
-    uint256 pBorrowShares;
-
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
 
-    (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
+    PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
 
     mathint ltv = getLtv(borrower);
 
@@ -169,7 +165,7 @@ rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 r
                                                    currentContract.PRE_LCF_1,
                                                    currentContract.PRE_LCF_2) ;
 
-    mathint repayableShares = summaryWMulDown(pBorrowShares, require_uint256(closeFactor));
+    mathint repayableShares = summaryWMulDown(p.borrowShares, require_uint256(closeFactor));
 
     preLiquidate@withrevert(e, borrower, 0, repaidShares, data);
 
diff --git a/certora/specs/SummaryLib.spec b/certora/specs/SummaryLib.spec
index 6b7804c..f2e898a 100644
--- a/certora/specs/SummaryLib.spec
+++ b/certora/specs/SummaryLib.spec
@@ -1,13 +1,13 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-using Morpho as MORPHO;
+using MorphoHarness as MORPHO;
+using Util as Util;
 
 methods {
-    function MORPHO.position(PreLiquidationHarness.Id, address) external
-        returns (uint256, uint128, uint128) envfree;
-
-    function market_(PreLiquidationHarness.Id) external
-        returns (PreLiquidationHarness.Market memory) envfree;
+    function MORPHO.market_(PreLiquidation.Id) external
+        returns (PreLiquidation.Market memory) envfree;
+    function MORPHO.position_(PreLiquidation.Id, address) external
+        returns (PreLiquidation.Position memory) envfree;
 }
 
 definition WAD() returns uint256 = 10^18;
@@ -59,8 +59,8 @@ function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalSha
                            require_uint256(totalShares + VIRTUAL_SHARES()));
 }
 
-function summaryMarketParams() returns PreLiquidationHarness.MarketParams {
-    PreLiquidationHarness.MarketParams x;
+function summaryMarketParams() returns PreLiquidation.MarketParams {
+    PreLiquidation.MarketParams x;
     require
         x.loanToken == currentContract.LOAN_TOKEN
         && x.collateralToken == currentContract.COLLATERAL_TOKEN
@@ -87,22 +87,17 @@ function mockPrice() returns uint256 {
 }
 
 
-// Ensure this function is only used when no interest is accrued,
-// or enforce that the last update matches the current timestamp.
+// Ensure this function is only used when no interest is accrued, or enforce that the last update matches the current timestamp.
 function positionAsAssets (address borrower) returns (uint256, uint256) {
-    uint256 pBorrowShares;
-    uint256 pCollateral;
-
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
-
-    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
+    PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
 
-    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, mockPrice(), ORACLE_PRICE_SCALE()));
+    uint256 collateralQuoted = require_uint256(summaryMulDivDown(p.collateral, mockPrice(), ORACLE_PRICE_SCALE()));
 
     // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
 
-    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, m.totalBorrowAssets, m.totalBorrowShares));
+    uint256 borrowed = require_uint256(summaryToAssetsUp(p.borrowShares, m.totalBorrowAssets, m.totalBorrowShares));
 
     return (borrowed, collateralQuoted);
 }

From 59320f861debc357fac842f0ee452bb924231d2d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 28 Oct 2024 16:27:40 +0100
Subject: [PATCH 25/26] fix: update morpho-blue

---
 lib/morpho-blue | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/morpho-blue b/lib/morpho-blue
index 0448402..3de2df4 160000
--- a/lib/morpho-blue
+++ b/lib/morpho-blue
@@ -1 +1 @@
-Subproject commit 0448402af51b8293ed36653de43cbee8d4d2bfda
+Subproject commit 3de2df4eb94c3f6118963039d4f177839a228e2a

From 3d95811c0211c24a4a72e72f622be2aa3104e021 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 28 Oct 2024 16:42:20 +0100
Subject: [PATCH 26/26] fix: improve comments

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

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 3760287..78c3f08 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -61,6 +61,7 @@ rule nonLiquidatablePositionReverts(env e, address borrower, uint256 seizedAsset
     PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
+    // Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
     require m.lastUpdate == e.block.timestamp;
 
     mathint ltv = getLtv(borrower);
@@ -82,6 +83,7 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
     PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
+    // Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
     require m.lastUpdate == e.block.timestamp;
 
     mathint ltv = getLtv(borrower);
@@ -103,6 +105,7 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
     PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
+    // Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
     require m.lastUpdate == e.block.timestamp;
 
     PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
@@ -150,6 +153,7 @@ rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 r
     PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
+    // Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
     require m.lastUpdate == e.block.timestamp;
 
     PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);