From 9bb8b163d80478bb73bf6f4d84a59e66dfed7884 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 09:12:36 +0200
Subject: [PATCH 01/28] chore: ignore emacs

---
 .gitignore | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.gitignore b/.gitignore
index 021292d..ac72cab 100644
--- a/.gitignore
+++ b/.gitignore
@@ -14,3 +14,9 @@ docs/
 .env
 
 .prettierignore
+
+# Emacs
+*~
+
+# Certora
+.certora_internal
\ No newline at end of file

From 9c5083acc7688d248138745fd9d61420c77bcf57 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 09:14:59 +0200
Subject: [PATCH 02/28] feat: trivial setup for certora prover

---
 certora/Makefile           | 12 ++++++++++++
 certora/applyMunging.patch |  0
 certora/confs/Dummy.conf   | 18 ++++++++++++++++++
 certora/helpers/Dummy.sol  |  1 +
 certora/specs/Dummy.spec   |  2 ++
 5 files changed, 33 insertions(+)
 create mode 100644 certora/Makefile
 create mode 100644 certora/applyMunging.patch
 create mode 100644 certora/confs/Dummy.conf
 create mode 100644 certora/helpers/Dummy.sol
 create mode 100644 certora/specs/Dummy.spec

diff --git a/certora/Makefile b/certora/Makefile
new file mode 100644
index 0000000..62c3396
--- /dev/null
+++ b/certora/Makefile
@@ -0,0 +1,12 @@
+munged: $(wildcard ../src/*.sol) applyMunging.patch
+	@rm -rf munged
+	@cp -r ../src munged
+	@patch -p0 -d munged < applyMunging.patch
+
+record:
+	diff -ruN ../src munged | sed 's+\.\./src/++g' | sed 's+munged/++g' > applyMunging.patch
+
+clean:
+	rm -rf munged
+
+.PHONY: help clean # do not add munged here, as it is useful to protect munged edits
diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
new file mode 100644
index 0000000..e69de29
diff --git a/certora/confs/Dummy.conf b/certora/confs/Dummy.conf
new file mode 100644
index 0000000..487f0f1
--- /dev/null
+++ b/certora/confs/Dummy.conf
@@ -0,0 +1,18 @@
+{
+    "files": [
+        "certora/helpers/Dummy.sol",
+    ],
+    "solc": "solc-0.8.27",
+    "verify": "Dummy:certora/specs/Dummy.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+        "-superOptimisticReturnsize true",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "PreLiquidation Dummy",
+}
diff --git a/certora/helpers/Dummy.sol b/certora/helpers/Dummy.sol
new file mode 100644
index 0000000..8879fc5
--- /dev/null
+++ b/certora/helpers/Dummy.sol
@@ -0,0 +1 @@
+contract Dummy {}
diff --git a/certora/specs/Dummy.spec b/certora/specs/Dummy.spec
new file mode 100644
index 0000000..57f1eb0
--- /dev/null
+++ b/certora/specs/Dummy.spec
@@ -0,0 +1,2 @@
+invariant tt()
+    true;

From 57bdba74878240f4ccfbf18866dd23470f290bf1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 09:15:24 +0200
Subject: [PATCH 03/28] feat: setup certora in ci

---
 .github/workflows/certora.yml | 52 +++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 .github/workflows/certora.yml

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 0000000..cbfbf93
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,52 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - Dummy
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ">=3.11"
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - name: Install solc (0.8.19)
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
+
+      - name: Install solc (0.8.27)
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.27/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.27
+
+      - name: Apply munging
+        run: make -C certora munged
+
+      - name: Verify ${{ matrix.conf }} specification
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

From a29c6b1215afb85a7cfb448464ea7a30dad7de01 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 10:37:00 +0200
Subject: [PATCH 04/28] chore: add verification README

---
 certora/README.md | 50 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 certora/README.md

diff --git a/certora/README.md b/certora/README.md
new file mode 100644
index 0000000..4187854
--- /dev/null
+++ b/certora/README.md
@@ -0,0 +1,50 @@
+# Pre-liquidation Contract Formal Verification
+
+This folder contains the
+[CVL](https://docs.certora.com/en/latest/docs/cvl/index.html)
+specification and verification setup for the
+[pre-liquidation](../src/PreLiquidation.sol) contract on [Morpho
+Blue](https://app.morpho.org/?network=mainnet) using the [Certora
+Prover](https://www.certora.com/).
+
+## Getting Started
+
+This project depends on two different versions of
+[Solidity](https://soliditylang.org/) which are required for running
+the verification. The compiler binaries should be available under the
+following path names:
+
+  - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is
+    used for `MorphoBlue`;
+  - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
+    used for `PreLiquidation`.
+
+The verification is performed on modified source files, which can be
+generated by running the following command.
+
+``` shell
+make -C certora munged
+```
+
+### Installing the Certora Prover
+
+The Certora CLI can be installed by running `python3 -m pip3 install
+certora-cli`. Detailed installation instructions can be found on
+Certora's official
+[documentation](https://docs.certora.com/en/latest/docs/user-guide/install.html).
+
+To verifying a specification, run the command `certoraRun Spec.conf`
+where `Spec.conf` is the configuration file of the matching CVL
+specification. Configuration files are available in
+[`certora/conf`](./confs). Please ensure that `CERTORA_KEY` is set up
+in your environment.
+
+## Overview
+
+The PreLiquidation contract enables Morpho Blue borrowers to set up a
+safer liquidation plan on a given position, thus preventing undesired
+liquidations.
+
+## TODO
+
+- [ ] Provide an overview of the specification.

From 7363a86c95596104f42e8dfb8ac25006e9207042 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 15:52:53 +0200
Subject: [PATCH 05/28] feat: rentrancy-safety spec

---
 .github/workflows/certora.yml                 |   2 +-
 certora/applyMunging.patch                    | 148 ++++++++++++++++++
 certora/confs/{Dummy.conf => Reentrancy.conf} |   8 +-
 certora/helpers/Dummy.sol                     |   1 -
 certora/helpers/IMorphoHarness.sol            |  48 ++++++
 certora/helpers/PreLiquidationHarness.sol     |  18 +++
 certora/specs/Dummy.spec                      |   2 -
 certora/specs/Reentrancy.spec                 |  55 +++++++
 8 files changed, 274 insertions(+), 8 deletions(-)
 rename certora/confs/{Dummy.conf => Reentrancy.conf} (56%)
 delete mode 100644 certora/helpers/Dummy.sol
 create mode 100644 certora/helpers/IMorphoHarness.sol
 create mode 100644 certora/helpers/PreLiquidationHarness.sol
 delete mode 100644 certora/specs/Dummy.spec
 create mode 100644 certora/specs/Reentrancy.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index cbfbf93..f19b9c6 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -16,7 +16,7 @@ jobs:
 
       matrix:
         conf:
-          - Dummy
+          - Reentrancy
 
     steps:
       - uses: actions/checkout@v4
diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
index e69de29..e953262 100644
--- a/certora/applyMunging.patch
+++ b/certora/applyMunging.patch
@@ -0,0 +1,148 @@
+diff -ruN PreLiquidation.sol PreLiquidation.sol
+--- PreLiquidation.sol	2024-09-19 08:12:23.000000000 +0200
++++ PreLiquidation.sol	2024-09-19 13:53:43.000000000 +0200
+@@ -1,20 +1,20 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity 0.8.27;
+ 
+-import {Id, MarketParams, IMorpho, Position, Market} from "../lib/morpho-blue/src/interfaces/IMorpho.sol";
+-import {IOracle} from "../lib/morpho-blue/src/interfaces/IOracle.sol";
+-import {UtilsLib} from "../lib/morpho-blue/src/libraries/UtilsLib.sol";
+-import {MarketParamsLib} from "../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
+-import "../lib/morpho-blue/src/libraries/ConstantsLib.sol";
+-import {MathLib} from "../lib/morpho-blue/src/libraries/MathLib.sol";
+-import {SharesMathLib} from "../lib/morpho-blue/src/libraries/SharesMathLib.sol";
+-import {SafeTransferLib} from "../lib/solmate/src/utils/SafeTransferLib.sol";
+-import {ERC20} from "../lib/solmate/src/tokens/ERC20.sol";
++import {Id, MarketParams, IMorphoHarness, Position, Market} from "../helpers/IMorphoHarness.sol";
++import {IOracle} from "../../lib/morpho-blue/src/interfaces/IOracle.sol";
++import {UtilsLib} from "../../lib/morpho-blue/src/libraries/UtilsLib.sol";
++import {MarketParamsLib} from "../../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
++import "../../lib/morpho-blue/src/libraries/ConstantsLib.sol";
++import {MathLib} from "../../lib/morpho-blue/src/libraries/MathLib.sol";
++import {SharesMathLib} from "../../lib/morpho-blue/src/libraries/SharesMathLib.sol";
++import {SafeTransferLib} from "../../lib/solmate/src/utils/SafeTransferLib.sol";
++import {ERC20} from "../../lib/solmate/src/tokens/ERC20.sol";
+ import {EventsLib} from "./libraries/EventsLib.sol";
+ import {ErrorsLib} from "./libraries/ErrorsLib.sol";
+ import {IPreLiquidationCallback} from "./interfaces/IPreLiquidationCallback.sol";
+ import {IPreLiquidation, PreLiquidationParams} from "./interfaces/IPreLiquidation.sol";
+-import {IMorphoRepayCallback} from "../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
++import {IMorphoRepayCallback} from "../../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
+ 
+ /// @title Morpho
+ /// @author Morpho Labs
+@@ -29,7 +29,7 @@
+     using SafeTransferLib for ERC20;
+ 
+     /* IMMUTABLE */
+-    IMorpho public immutable MORPHO;
++    IMorphoHarness public immutable MORPHO;
+     Id public immutable marketId;
+ 
+     // Market parameters
+@@ -45,7 +45,7 @@
+     uint256 public immutable preLiquidationIncentive;
+ 
+     constructor(MarketParams memory _marketParams, PreLiquidationParams memory _preLiquidationParams, address morpho) {
+-        MORPHO = IMorpho(morpho);
++        MORPHO = IMorphoHarness(morpho);
+         marketId = _marketParams.id();
+ 
+         require(MORPHO.market(marketId).lastUpdate != 0, ErrorsLib.NonexistentMarket(marketId));
+diff -ruN PreLiquidationFactory.sol PreLiquidationFactory.sol
+--- PreLiquidationFactory.sol	2024-09-19 08:12:23.000000000 +0200
++++ PreLiquidationFactory.sol	2024-09-19 11:30:51.000000000 +0200
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity 0.8.27;
+ 
+-import {IMorpho, MarketParams} from "../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {IMorphoHarness, MarketParams} from "../helpers/IMorphoHarness.sol";
+ import {PreLiquidation} from "./PreLiquidation.sol";
+ import {IPreLiquidation, PreLiquidationParams} from "./interfaces/IPreLiquidation.sol";
+ import {ErrorsLib} from "./libraries/ErrorsLib.sol";
+@@ -16,7 +16,7 @@
+     /* IMMUTABLE */
+ 
+     /// @inheritdoc IPreLiquidationFactory
+-    IMorpho public immutable MORPHO;
++    IMorphoHarness public immutable MORPHO;
+ 
+     /* STORAGE */
+ 
+@@ -29,7 +29,7 @@
+     constructor(address morpho) {
+         require(morpho != address(0), ErrorsLib.ZeroAddress());
+ 
+-        MORPHO = IMorpho(morpho);
++        MORPHO = IMorphoHarness(morpho);
+     }
+ 
+     /* EXTERNAL */
+diff -ruN interfaces/IPreLiquidation.sol interfaces/IPreLiquidation.sol
+--- interfaces/IPreLiquidation.sol	2024-09-19 08:12:23.000000000 +0200
++++ interfaces/IPreLiquidation.sol	2024-09-19 13:56:01.000000000 +0200
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity >= 0.5.0;
+ 
+-import {Id, MarketParams, IMorpho} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {Id, MarketParams, IMorphoHarness} from "../../helpers/IMorphoHarness.sol";
+ 
+ struct PreLiquidationParams {
+     uint256 preLltv;
+@@ -10,7 +10,7 @@
+ }
+ 
+ interface IPreLiquidation {
+-    function MORPHO() external view returns (IMorpho);
++    function MORPHO() external view returns (IMorphoHarness);
+ 
+     function marketId() external view returns (Id);
+ 
+diff -ruN interfaces/IPreLiquidationFactory.sol interfaces/IPreLiquidationFactory.sol
+--- interfaces/IPreLiquidationFactory.sol	2024-09-19 08:12:23.000000000 +0200
++++ interfaces/IPreLiquidationFactory.sol	2024-09-19 13:55:49.000000000 +0200
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity >= 0.5.0;
+ 
+-import {MarketParams, IMorpho} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {MarketParams, IMorpho} from "../../helpers/IMorphoHarness.sol";
+ import {IPreLiquidation, PreLiquidationParams} from "./IPreLiquidation.sol";
+ 
+ /// @title IPreLiquidationFactory
+@@ -10,7 +10,7 @@
+ /// @notice Interface of PreLiquidation's factory.
+ interface IPreLiquidationFactory {
+     /// @notice The address of the Morpho contract.
+-    function MORPHO() external view returns (IMorpho);
++    function MORPHO() external view returns (IMorphoHarness);
+ 
+     /// @notice The contract address created for a specific preLiquidationId.
+     function preLiquidations(bytes32) external view returns (IPreLiquidation);
+diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol
+--- libraries/ErrorsLib.sol	2024-09-19 08:12:23.000000000 +0200
++++ libraries/ErrorsLib.sol	2024-09-19 13:51:28.000000000 +0200
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity 0.8.27;
+ 
+-import {Id} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {Id} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
+ 
+ /// @title ErrorsLib
+ /// @author Morpho Labs
+diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
+--- libraries/EventsLib.sol	2024-09-19 08:12:23.000000000 +0200
++++ libraries/EventsLib.sol	2024-09-19 13:51:50.000000000 +0200
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity 0.8.27;
+ 
+-import {Id, MarketParams} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
++import {Id, MarketParams} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
+ import {PreLiquidationParams} from "../interfaces/IPreLiquidation.sol";
+ 
+ /// @title EventsLib
diff --git a/certora/confs/Dummy.conf b/certora/confs/Reentrancy.conf
similarity index 56%
rename from certora/confs/Dummy.conf
rename to certora/confs/Reentrancy.conf
index 487f0f1..b61839d 100644
--- a/certora/confs/Dummy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -1,18 +1,18 @@
 {
     "files": [
-        "certora/helpers/Dummy.sol",
+        "certora/helpers/PreLiquidationHarness.sol",
     ],
     "solc": "solc-0.8.27",
-    "verify": "Dummy:certora/specs/Dummy.spec",
+    "verify": "PreLiquidationHarness:certora/specs/Reentrancy.spec",
     "loop_iter": "2",
     "optimistic_loop": true,
     "prover_args": [
+        "-enableStorageSplitting false",
         "-depth 3",
         "-mediumTimeout 20",
         "-timeout 120",
-        "-superOptimisticReturnsize true",
     ],
     "rule_sanity": "basic",
     "server": "production",
-    "msg": "PreLiquidation Dummy",
+    "msg": "PreLiquidation Reentrancy",
 }
diff --git a/certora/helpers/Dummy.sol b/certora/helpers/Dummy.sol
deleted file mode 100644
index 8879fc5..0000000
--- a/certora/helpers/Dummy.sol
+++ /dev/null
@@ -1 +0,0 @@
-contract Dummy {}
diff --git a/certora/helpers/IMorphoHarness.sol b/certora/helpers/IMorphoHarness.sol
new file mode 100644
index 0000000..69ce618
--- /dev/null
+++ b/certora/helpers/IMorphoHarness.sol
@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {Id, MarketParams, Position, Market, IMorpho} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
+
+interface IMorphoHarness is IMorpho {
+    function supplyShares(Id id, address user) external view returns (uint256);
+
+    function borrowShares(Id id, address user) external view returns (uint256);
+
+    function collateral(Id id, address user) external view returns (uint256);
+
+    function totalSupplyAssets(Id id) external view returns (uint256);
+
+    function totalSupplyShares(Id id) external view returns (uint256);
+
+    function totalBorrowAssets(Id id) external view returns (uint256);
+
+    function totalBorrowShares(Id id) external view returns (uint256);
+
+    function lastUpdate(Id id) external view returns (uint256);
+
+    function fee(Id id) external view returns (uint256);
+
+    function expectedMarketBalances(MarketParams memory marketParams)
+        external
+        view
+        returns (uint256, uint256, uint256, uint256);
+
+    function expectedTotalSupplyAssets(MarketParams memory marketParams)
+        external
+        view
+        returns (uint256 totalSupplyAssets);
+
+    function expectedTotalBorrowAssets(MarketParams memory marketParams)
+        external
+        view
+        returns (uint256 totalBorrowAssets);
+
+    function expectedTotalSupplyShares(MarketParams memory marketParams)
+        external
+        view
+        returns (uint256 totalSupplyShares);
+
+    function expectedSupplyAssets(MarketParams memory marketParams, address user) external view returns (uint256);
+
+    function expectedBorrowAssets(MarketParams memory marketParams, address user) external view returns (uint256);
+}
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
new file mode 100644
index 0000000..f71de39
--- /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, Id, MarketParams, PreLiquidationParams} from "../munged/PreLiquidation.sol";
+
+/// @title PreLiquidationHarness
+/// @author Morpho Labs
+/// @custom:contact security@morpho.org
+/// @notice The Pre Liquidation Harness Contract to be used with the Certora prover
+contract PreLiquidationHarness is PreLiquidation {
+    constructor(MarketParams memory _marketParams, PreLiquidationParams memory _preLiquidationParams, address morpho)
+        PreLiquidation(_marketParams, _preLiquidationParams, morpho)
+    {}
+
+    function _isPreLiquidatable_(address borrower, uint256 collateralPrice) external view returns (bool) {
+        return _isPreLiquidatable(borrower, collateralPrice);
+    }
+}
diff --git a/certora/specs/Dummy.spec b/certora/specs/Dummy.spec
deleted file mode 100644
index 57f1eb0..0000000
--- a/certora/specs/Dummy.spec
+++ /dev/null
@@ -1,2 +0,0 @@
-invariant tt()
-    true;
diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
new file mode 100644
index 0000000..34b6c4f
--- /dev/null
+++ b/certora/specs/Reentrancy.spec
@@ -0,0 +1,55 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+methods {
+    function _.accrueInterest(PreLiquidationHarness.MarketParams) external => voidSummary() expect void;
+    function _.repay(PreLiquidationHarness.MarketParams, uint256, uint256, address, bytes) external =>
+      uintPairSummary() expect (uint256, uint256);
+    function _.withdrawCollateral(PreLiquidationHarness.MarketParams, uint256, address, address) external
+      => voidSummary() expect void;
+}
+
+// True when storage has been accessed with either a SSTORE or a SLOAD.
+persistent ghost bool hasAccessedStorage;
+// True when a CALL has been done after storage has been accessed.
+persistent ghost bool hasCallAfterAccessingStorage;
+// True when storage has been accessed, after which an external call is made, followed by accessing storage again.
+persistent ghost bool hasReentrancyUnsafeCall;
+// True for reentrant-safe functions of Morpho Blue are being called.
+persistent ghost bool ignoredCall;
+
+function voidSummary() {
+    ignoredCall = true;
+}
+
+function uintPairSummary() returns (uint256, uint256) {
+    ignoredCall = true;
+    uint256 firstValue;
+    uint256 secondValue;
+    return (firstValue, secondValue);
+}
+
+hook ALL_SSTORE(uint loc, uint v) {
+    hasAccessedStorage = true;
+    hasReentrancyUnsafeCall = hasCallAfterAccessingStorage;
+}
+
+hook ALL_SLOAD(uint loc) uint v {
+    hasAccessedStorage = true;
+    hasReentrancyUnsafeCall = hasCallAfterAccessingStorage;
+}
+
+hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
+    if (ignoredCall) {
+        // Ignore calls to tokens and Morpho markets as they are trusted (they have gone through a timelock).
+        ignoredCall = false;
+    } else {
+        hasCallAfterAccessingStorage = hasAccessedStorage;
+    }
+}
+
+// Check that no function is accessing storage, then making an external CALL other than to the IRM, and accessing storage again.
+rule reentrancySafe(method f, env e, calldataarg data) {
+    // Set up the initial state.
+    require !ignoredCall && !hasAccessedStorage && !hasCallAfterAccessingStorage && !hasReentrancyUnsafeCall;
+    f(e,data);
+    assert !hasReentrancyUnsafeCall;
+}

From 390891c6e2481c9aa84d1c98ebb4456caf36a524 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 15:53:39 +0200
Subject: [PATCH 06/28] chore: ignore verification related munged files

---
 .gitignore | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index ac72cab..42ed0b1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,4 +19,5 @@ docs/
 *~
 
 # Certora
-.certora_internal
\ No newline at end of file
+.certora_internal
+certora/munged
\ No newline at end of file

From eb30d6ab4d313adb85199988baa3de81f4ceb83b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 16:03:09 +0200
Subject: [PATCH 07/28] chore: provide reentrancy safety documentation

---
 certora/README.md | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/certora/README.md b/certora/README.md
index 4187854..2ae9866 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -45,6 +45,34 @@ The PreLiquidation contract enables Morpho Blue borrowers to set up a
 safer liquidation plan on a given position, thus preventing undesired
 liquidations.
 
+### Reentrancy
+
+PreLiquidation only interacts with Morpho Blue and with the loan token
+of the vault.  This is checked in
+[`Reentrancy.spec`](specs/Reentrancy.spec).  Informally, the loan
+token and the markets of Morpho Blue are trusted.
+
+
+## Verification architecture
+
+### Folders and file structure
+
+The [`certora/specs`](specs) folder contains the following files:
+
+- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that
+  PreLiquidation is reentrancy safe by making sure that there are no
+  untrusted external calls.
+
+The [`certora/confs`](confs) folder contains a configuration file for
+each corresponding specification file.
+
+The [`certora/helpers`](helpers) folder contains helper contracts that
+enable the verification of PreLiquidation. Notably, this allows
+handling the fact that library functions should be called from a
+contract to be verified independently, and it allows defining needed
+getters.
+
 ## TODO
 
 - [ ] Provide an overview of the specification.
+- [ ] Update the verification architecture.

From 1603b4ccd7c87e009fa9410a15709c530f493c99 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 19 Sep 2024 16:59:52 +0200
Subject: [PATCH 08/28] feat: strenghten reentrancy specification

---
 certora/specs/Reentrancy.spec | 46 +++--------------------------------
 1 file changed, 3 insertions(+), 43 deletions(-)

diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
index 34b6c4f..eba1a06 100644
--- a/certora/specs/Reentrancy.spec
+++ b/certora/specs/Reentrancy.spec
@@ -1,55 +1,15 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-methods {
-    function _.accrueInterest(PreLiquidationHarness.MarketParams) external => voidSummary() expect void;
-    function _.repay(PreLiquidationHarness.MarketParams, uint256, uint256, address, bytes) external =>
-      uintPairSummary() expect (uint256, uint256);
-    function _.withdrawCollateral(PreLiquidationHarness.MarketParams, uint256, address, address) external
-      => voidSummary() expect void;
-}
-
 // True when storage has been accessed with either a SSTORE or a SLOAD.
 persistent ghost bool hasAccessedStorage;
-// True when a CALL has been done after storage has been accessed.
-persistent ghost bool hasCallAfterAccessingStorage;
-// True when storage has been accessed, after which an external call is made, followed by accessing storage again.
-persistent ghost bool hasReentrancyUnsafeCall;
-// True for reentrant-safe functions of Morpho Blue are being called.
-persistent ghost bool ignoredCall;
-
-function voidSummary() {
-    ignoredCall = true;
-}
-
-function uintPairSummary() returns (uint256, uint256) {
-    ignoredCall = true;
-    uint256 firstValue;
-    uint256 secondValue;
-    return (firstValue, secondValue);
-}
 
 hook ALL_SSTORE(uint loc, uint v) {
     hasAccessedStorage = true;
-    hasReentrancyUnsafeCall = hasCallAfterAccessingStorage;
-}
-
-hook ALL_SLOAD(uint loc) uint v {
-    hasAccessedStorage = true;
-    hasReentrancyUnsafeCall = hasCallAfterAccessingStorage;
-}
-
-hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
-    if (ignoredCall) {
-        // Ignore calls to tokens and Morpho markets as they are trusted (they have gone through a timelock).
-        ignoredCall = false;
-    } else {
-        hasCallAfterAccessingStorage = hasAccessedStorage;
-    }
 }
 
-// Check that no function is accessing storage, then making an external CALL other than to the IRM, and accessing storage again.
+// Check that no function is accessing storage.
 rule reentrancySafe(method f, env e, calldataarg data) {
     // Set up the initial state.
-    require !ignoredCall && !hasAccessedStorage && !hasCallAfterAccessingStorage && !hasReentrancyUnsafeCall;
+    require !hasAccessedStorage;
     f(e,data);
-    assert !hasReentrancyUnsafeCall;
+    assert !hasAccessedStorage;
 }

From e666d77ce72c30f2d146f04190151906706b7c0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:10:02 +0200
Subject: [PATCH 09/28] feat:verif immutability

---
 .github/workflows/certora.yml   |  1 +
 certora/confs/Immutability.conf | 17 +++++++++++++++++
 certora/specs/Immutability.spec | 15 +++++++++++++++
 3 files changed, 33 insertions(+)
 create mode 100644 certora/confs/Immutability.conf
 create mode 100644 certora/specs/Immutability.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index f19b9c6..4c5167a 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -17,6 +17,7 @@ jobs:
       matrix:
         conf:
           - Reentrancy
+          - Immutability
 
     steps:
       - uses: actions/checkout@v4
diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
new file mode 100644
index 0000000..e4e43a1
--- /dev/null
+++ b/certora/confs/Immutability.conf
@@ -0,0 +1,17 @@
+{
+    "files": [
+        "certora/helpers/PreLiquidationHarness.sol",
+    ],
+    "solc": "solc-0.8.27",
+    "verify": "PreLiquidationHarness:certora/specs/Immutability.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "PreLiquidation Immutability",
+}
diff --git a/certora/specs/Immutability.spec b/certora/specs/Immutability.spec
new file mode 100644
index 0000000..6c357af
--- /dev/null
+++ b/certora/specs/Immutability.spec
@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+persistent ghost bool delegateCall;
+
+hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
+    delegateCall = true;
+}
+
+// Check that the contract is truly immutable.
+rule noDelegateCalls(method f, env e, calldataarg data) {
+    // Set up the initial state.
+    require !delegateCall;
+    f(e,data);
+    assert !delegateCall;
+}

From 5c60ef2ac785add483e36d0df5747448cbe18d90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:12:19 +0200
Subject: [PATCH 10/28] fix: remove MB link

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

diff --git a/certora/README.md b/certora/README.md
index 4187854..86581e1 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -3,9 +3,8 @@
 This folder contains the
 [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html)
 specification and verification setup for the
-[pre-liquidation](../src/PreLiquidation.sol) contract on [Morpho
-Blue](https://app.morpho.org/?network=mainnet) using the [Certora
-Prover](https://www.certora.com/).
+[pre-liquidation](../src/PreLiquidation.sol) contract using the
+[Certora Prover](https://www.certora.com/).
 
 ## Getting Started
 

From 0ea070a61210de90503305a7412d0489c23917a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:13:03 +0200
Subject: [PATCH 11/28] fix: MorphoBlue -> Morpho

---
 certora/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/README.md b/certora/README.md
index 86581e1..42cfa5d 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -14,7 +14,7 @@ the verification. The compiler binaries should be available under the
 following path names:
 
   - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is
-    used for `MorphoBlue`;
+    used for `Morpho`;
   - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
     used for `PreLiquidation`.
 

From 7813f880e0d7f637315ef283a221c844ea69951a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:33:42 +0200
Subject: [PATCH 12/28] fix: remove munging

---
 .github/workflows/certora.yml             |   3 -
 certora/Makefile                          |  12 --
 certora/applyMunging.patch                | 148 ----------------------
 certora/helpers/IMorphoHarness.sol        |  48 -------
 certora/helpers/PreLiquidationHarness.sol |   2 +-
 5 files changed, 1 insertion(+), 212 deletions(-)
 delete mode 100644 certora/Makefile
 delete mode 100644 certora/applyMunging.patch
 delete mode 100644 certora/helpers/IMorphoHarness.sol

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index f19b9c6..49740dc 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -43,9 +43,6 @@ jobs:
           chmod +x solc-static-linux
           sudo mv solc-static-linux /usr/local/bin/solc-0.8.27
 
-      - name: Apply munging
-        run: make -C certora munged
-
       - name: Verify ${{ matrix.conf }} specification
         run: certoraRun certora/confs/${{ matrix.conf }}.conf
         env:
diff --git a/certora/Makefile b/certora/Makefile
deleted file mode 100644
index 62c3396..0000000
--- a/certora/Makefile
+++ /dev/null
@@ -1,12 +0,0 @@
-munged: $(wildcard ../src/*.sol) applyMunging.patch
-	@rm -rf munged
-	@cp -r ../src munged
-	@patch -p0 -d munged < applyMunging.patch
-
-record:
-	diff -ruN ../src munged | sed 's+\.\./src/++g' | sed 's+munged/++g' > applyMunging.patch
-
-clean:
-	rm -rf munged
-
-.PHONY: help clean # do not add munged here, as it is useful to protect munged edits
diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
deleted file mode 100644
index e953262..0000000
--- a/certora/applyMunging.patch
+++ /dev/null
@@ -1,148 +0,0 @@
-diff -ruN PreLiquidation.sol PreLiquidation.sol
---- PreLiquidation.sol	2024-09-19 08:12:23.000000000 +0200
-+++ PreLiquidation.sol	2024-09-19 13:53:43.000000000 +0200
-@@ -1,20 +1,20 @@
- // SPDX-License-Identifier: GPL-2.0-or-later
- pragma solidity 0.8.27;
- 
--import {Id, MarketParams, IMorpho, Position, Market} from "../lib/morpho-blue/src/interfaces/IMorpho.sol";
--import {IOracle} from "../lib/morpho-blue/src/interfaces/IOracle.sol";
--import {UtilsLib} from "../lib/morpho-blue/src/libraries/UtilsLib.sol";
--import {MarketParamsLib} from "../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
--import "../lib/morpho-blue/src/libraries/ConstantsLib.sol";
--import {MathLib} from "../lib/morpho-blue/src/libraries/MathLib.sol";
--import {SharesMathLib} from "../lib/morpho-blue/src/libraries/SharesMathLib.sol";
--import {SafeTransferLib} from "../lib/solmate/src/utils/SafeTransferLib.sol";
--import {ERC20} from "../lib/solmate/src/tokens/ERC20.sol";
-+import {Id, MarketParams, IMorphoHarness, Position, Market} from "../helpers/IMorphoHarness.sol";
-+import {IOracle} from "../../lib/morpho-blue/src/interfaces/IOracle.sol";
-+import {UtilsLib} from "../../lib/morpho-blue/src/libraries/UtilsLib.sol";
-+import {MarketParamsLib} from "../../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
-+import "../../lib/morpho-blue/src/libraries/ConstantsLib.sol";
-+import {MathLib} from "../../lib/morpho-blue/src/libraries/MathLib.sol";
-+import {SharesMathLib} from "../../lib/morpho-blue/src/libraries/SharesMathLib.sol";
-+import {SafeTransferLib} from "../../lib/solmate/src/utils/SafeTransferLib.sol";
-+import {ERC20} from "../../lib/solmate/src/tokens/ERC20.sol";
- import {EventsLib} from "./libraries/EventsLib.sol";
- import {ErrorsLib} from "./libraries/ErrorsLib.sol";
- import {IPreLiquidationCallback} from "./interfaces/IPreLiquidationCallback.sol";
- import {IPreLiquidation, PreLiquidationParams} from "./interfaces/IPreLiquidation.sol";
--import {IMorphoRepayCallback} from "../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
-+import {IMorphoRepayCallback} from "../../lib/morpho-blue/src/interfaces/IMorphoCallbacks.sol";
- 
- /// @title Morpho
- /// @author Morpho Labs
-@@ -29,7 +29,7 @@
-     using SafeTransferLib for ERC20;
- 
-     /* IMMUTABLE */
--    IMorpho public immutable MORPHO;
-+    IMorphoHarness public immutable MORPHO;
-     Id public immutable marketId;
- 
-     // Market parameters
-@@ -45,7 +45,7 @@
-     uint256 public immutable preLiquidationIncentive;
- 
-     constructor(MarketParams memory _marketParams, PreLiquidationParams memory _preLiquidationParams, address morpho) {
--        MORPHO = IMorpho(morpho);
-+        MORPHO = IMorphoHarness(morpho);
-         marketId = _marketParams.id();
- 
-         require(MORPHO.market(marketId).lastUpdate != 0, ErrorsLib.NonexistentMarket(marketId));
-diff -ruN PreLiquidationFactory.sol PreLiquidationFactory.sol
---- PreLiquidationFactory.sol	2024-09-19 08:12:23.000000000 +0200
-+++ PreLiquidationFactory.sol	2024-09-19 11:30:51.000000000 +0200
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: GPL-2.0-or-later
- pragma solidity 0.8.27;
- 
--import {IMorpho, MarketParams} from "../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {IMorphoHarness, MarketParams} from "../helpers/IMorphoHarness.sol";
- import {PreLiquidation} from "./PreLiquidation.sol";
- import {IPreLiquidation, PreLiquidationParams} from "./interfaces/IPreLiquidation.sol";
- import {ErrorsLib} from "./libraries/ErrorsLib.sol";
-@@ -16,7 +16,7 @@
-     /* IMMUTABLE */
- 
-     /// @inheritdoc IPreLiquidationFactory
--    IMorpho public immutable MORPHO;
-+    IMorphoHarness public immutable MORPHO;
- 
-     /* STORAGE */
- 
-@@ -29,7 +29,7 @@
-     constructor(address morpho) {
-         require(morpho != address(0), ErrorsLib.ZeroAddress());
- 
--        MORPHO = IMorpho(morpho);
-+        MORPHO = IMorphoHarness(morpho);
-     }
- 
-     /* EXTERNAL */
-diff -ruN interfaces/IPreLiquidation.sol interfaces/IPreLiquidation.sol
---- interfaces/IPreLiquidation.sol	2024-09-19 08:12:23.000000000 +0200
-+++ interfaces/IPreLiquidation.sol	2024-09-19 13:56:01.000000000 +0200
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: GPL-2.0-or-later
- pragma solidity >= 0.5.0;
- 
--import {Id, MarketParams, IMorpho} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {Id, MarketParams, IMorphoHarness} from "../../helpers/IMorphoHarness.sol";
- 
- struct PreLiquidationParams {
-     uint256 preLltv;
-@@ -10,7 +10,7 @@
- }
- 
- interface IPreLiquidation {
--    function MORPHO() external view returns (IMorpho);
-+    function MORPHO() external view returns (IMorphoHarness);
- 
-     function marketId() external view returns (Id);
- 
-diff -ruN interfaces/IPreLiquidationFactory.sol interfaces/IPreLiquidationFactory.sol
---- interfaces/IPreLiquidationFactory.sol	2024-09-19 08:12:23.000000000 +0200
-+++ interfaces/IPreLiquidationFactory.sol	2024-09-19 13:55:49.000000000 +0200
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: GPL-2.0-or-later
- pragma solidity >= 0.5.0;
- 
--import {MarketParams, IMorpho} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {MarketParams, IMorpho} from "../../helpers/IMorphoHarness.sol";
- import {IPreLiquidation, PreLiquidationParams} from "./IPreLiquidation.sol";
- 
- /// @title IPreLiquidationFactory
-@@ -10,7 +10,7 @@
- /// @notice Interface of PreLiquidation's factory.
- interface IPreLiquidationFactory {
-     /// @notice The address of the Morpho contract.
--    function MORPHO() external view returns (IMorpho);
-+    function MORPHO() external view returns (IMorphoHarness);
- 
-     /// @notice The contract address created for a specific preLiquidationId.
-     function preLiquidations(bytes32) external view returns (IPreLiquidation);
-diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol
---- libraries/ErrorsLib.sol	2024-09-19 08:12:23.000000000 +0200
-+++ libraries/ErrorsLib.sol	2024-09-19 13:51:28.000000000 +0200
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: GPL-2.0-or-later
- pragma solidity 0.8.27;
- 
--import {Id} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {Id} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
- 
- /// @title ErrorsLib
- /// @author Morpho Labs
-diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
---- libraries/EventsLib.sol	2024-09-19 08:12:23.000000000 +0200
-+++ libraries/EventsLib.sol	2024-09-19 13:51:50.000000000 +0200
-@@ -1,7 +1,7 @@
- // SPDX-License-Identifier: GPL-2.0-or-later
- pragma solidity 0.8.27;
- 
--import {Id, MarketParams} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {Id, MarketParams} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
- import {PreLiquidationParams} from "../interfaces/IPreLiquidation.sol";
- 
- /// @title EventsLib
diff --git a/certora/helpers/IMorphoHarness.sol b/certora/helpers/IMorphoHarness.sol
deleted file mode 100644
index 69ce618..0000000
--- a/certora/helpers/IMorphoHarness.sol
+++ /dev/null
@@ -1,48 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.27;
-
-import {Id, MarketParams, Position, Market, IMorpho} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-
-interface IMorphoHarness is IMorpho {
-    function supplyShares(Id id, address user) external view returns (uint256);
-
-    function borrowShares(Id id, address user) external view returns (uint256);
-
-    function collateral(Id id, address user) external view returns (uint256);
-
-    function totalSupplyAssets(Id id) external view returns (uint256);
-
-    function totalSupplyShares(Id id) external view returns (uint256);
-
-    function totalBorrowAssets(Id id) external view returns (uint256);
-
-    function totalBorrowShares(Id id) external view returns (uint256);
-
-    function lastUpdate(Id id) external view returns (uint256);
-
-    function fee(Id id) external view returns (uint256);
-
-    function expectedMarketBalances(MarketParams memory marketParams)
-        external
-        view
-        returns (uint256, uint256, uint256, uint256);
-
-    function expectedTotalSupplyAssets(MarketParams memory marketParams)
-        external
-        view
-        returns (uint256 totalSupplyAssets);
-
-    function expectedTotalBorrowAssets(MarketParams memory marketParams)
-        external
-        view
-        returns (uint256 totalBorrowAssets);
-
-    function expectedTotalSupplyShares(MarketParams memory marketParams)
-        external
-        view
-        returns (uint256 totalSupplyShares);
-
-    function expectedSupplyAssets(MarketParams memory marketParams, address user) external view returns (uint256);
-
-    function expectedBorrowAssets(MarketParams memory marketParams, address user) external view returns (uint256);
-}
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
index f71de39..ec4719b 100644
--- a/certora/helpers/PreLiquidationHarness.sol
+++ b/certora/helpers/PreLiquidationHarness.sol
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.27;
 
-import {PreLiquidation, Id, MarketParams, PreLiquidationParams} from "../munged/PreLiquidation.sol";
+import {PreLiquidation, Id, MarketParams, PreLiquidationParams} from "../../src/PreLiquidation.sol";
 
 /// @title PreLiquidationHarness
 /// @author Morpho Labs

From 1e77059257330b30fa4fe73118b77e5e03103381 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:43:55 +0200
Subject: [PATCH 13/28] fix: add sload hook

---
 certora/specs/Reentrancy.spec | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
index eba1a06..934cab0 100644
--- a/certora/specs/Reentrancy.spec
+++ b/certora/specs/Reentrancy.spec
@@ -1,11 +1,17 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-// True when storage has been accessed with either a SSTORE or a SLOAD.
+// True when storage has been accessed with either a SSTORE or a
+// SLOAD.
+
 persistent ghost bool hasAccessedStorage;
 
 hook ALL_SSTORE(uint loc, uint v) {
     hasAccessedStorage = true;
 }
 
+hook ALL_SLOAD(uint loc) uint v {
+    hasAccessedStorage = true;
+}
+
 // Check that no function is accessing storage.
 rule reentrancySafe(method f, env e, calldataarg data) {
     // Set up the initial state.

From 9525aa5f1daa8752f439a0387d83cc5a430f2137 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:46:47 +0200
Subject: [PATCH 14/28] fix: add /nl in gitignore

---
 .gitignore | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 42ed0b1..4e898de 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,4 +20,4 @@ docs/
 
 # Certora
 .certora_internal
-certora/munged
\ No newline at end of file
+certora/munged

From d0f2c10b95c5b821f840f43f39ef2f619c0165bf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:51:23 +0200
Subject: [PATCH 15/28] fix: imrpove description of reentrancy verification

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

diff --git a/certora/README.md b/certora/README.md
index 2ae9866..751863f 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -60,8 +60,8 @@ token and the markets of Morpho Blue are trusted.
 The [`certora/specs`](specs) folder contains the following files:
 
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that
-  PreLiquidation is reentrancy safe by making sure that there are no
-  untrusted external calls.
+  PreLiquidation is reentrant by checking that the storage is never
+  used.
 
 The [`certora/confs`](confs) folder contains a configuration file for
 each corresponding specification file.

From d389ee061ab1f0fddfc464988f2c71ae04562417 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 14:54:00 +0200
Subject: [PATCH 16/28] fix: fix description of reentrancy verification

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

diff --git a/certora/README.md b/certora/README.md
index 751863f..85f0c2d 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -47,11 +47,8 @@ liquidations.
 
 ### Reentrancy
 
-PreLiquidation only interacts with Morpho Blue and with the loan token
-of the vault.  This is checked in
-[`Reentrancy.spec`](specs/Reentrancy.spec).  Informally, the loan
-token and the markets of Morpho Blue are trusted.
-
+This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
+Informally, the loan token and the markets of Morpho Blue are trusted.
 
 ## Verification architecture
 

From 83988c4b9f9f2672c6b00ee34f895758f43db288 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 16:32:25 +0200
Subject: [PATCH 17/28] chore: remove certora/munged from gitignore

---
 .gitignore | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 4e898de..8187898 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,4 +20,3 @@ docs/
 
 # Certora
 .certora_internal
-certora/munged

From e3e54e593a8574e30ea002d8eb6203712b332463 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 16:35:22 +0200
Subject: [PATCH 18/28] fix: apply suggestion to README

---
 certora/README.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/certora/README.md b/certora/README.md
index 85f0c2d..1822651 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -48,7 +48,6 @@ liquidations.
 ### Reentrancy
 
 This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
-Informally, the loan token and the markets of Morpho Blue are trusted.
 
 ## Verification architecture
 

From 9aa7aea872ae4b7130c4d4653e0d16f7ecc1070f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 16:36:04 +0200
Subject: [PATCH 19/28] fix: remove natspec from harness

---
 certora/helpers/PreLiquidationHarness.sol | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
index ec4719b..1f2a4db 100644
--- a/certora/helpers/PreLiquidationHarness.sol
+++ b/certora/helpers/PreLiquidationHarness.sol
@@ -3,10 +3,6 @@ pragma solidity 0.8.27;
 
 import {PreLiquidation, Id, MarketParams, PreLiquidationParams} from "../../src/PreLiquidation.sol";
 
-/// @title PreLiquidationHarness
-/// @author Morpho Labs
-/// @custom:contact security@morpho.org
-/// @notice The Pre Liquidation Harness Contract to be used with the Certora prover
 contract PreLiquidationHarness is PreLiquidation {
     constructor(MarketParams memory _marketParams, PreLiquidationParams memory _preLiquidationParams, address morpho)
         PreLiquidation(_marketParams, _preLiquidationParams, morpho)

From c8742e3950fba60c45b2d39dc12ce09a4f84f13c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 16:37:52 +0200
Subject: [PATCH 20/28] fix: reentrant -> reentrancy safe

---
 certora/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/README.md b/certora/README.md
index 1822651..bc8c3fa 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -56,7 +56,7 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 The [`certora/specs`](specs) folder contains the following files:
 
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that
-  PreLiquidation is reentrant by checking that the storage is never
+  PreLiquidation is reentrancy safe by checking that the storage is never
   used.
 
 The [`certora/confs`](confs) folder contains a configuration file for

From 9cb3ee3f32d8438ba879b38da674867dfc7d84c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 16:56:38 +0200
Subject: [PATCH 21/28] fix: remove munging instruction

---
 certora/README.md | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index 42cfa5d..1b5f452 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -18,13 +18,6 @@ following path names:
   - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
     used for `PreLiquidation`.
 
-The verification is performed on modified source files, which can be
-generated by running the following command.
-
-``` shell
-make -C certora munged
-```
-
 ### Installing the Certora Prover
 
 The Certora CLI can be installed by running `python3 -m pip3 install

From 6a913b15eedcb3e3becfabe5ce52973f821219fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 17:06:47 +0200
Subject: [PATCH 22/28] chore: update verif's README

---
 certora/README.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/certora/README.md b/certora/README.md
index 6df5ec7..393b930 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -41,6 +41,10 @@ liquidations.
 
 This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 
+### Immutability
+
+This is checked in [`Immutability.spec`](specs/Immutability.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
@@ -51,6 +55,10 @@ The [`certora/specs`](specs) folder contains the following files:
   PreLiquidation is reentrancy safe by checking that the storage is never
   used.
 
+- [`Immutability.spec`](specs/Immutability.spec) checks that
+  PreLiquidation's storage is safe by checking that the storage is never
+  changed by a delegate call..
+
 The [`certora/confs`](confs) folder contains a configuration file for
 each corresponding specification file.
 

From d079c5c582ae9cd1e4a023e0f4712142076d4fcf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 17:48:49 +0200
Subject: [PATCH 23/28] fix: improve description in README

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

diff --git a/certora/README.md b/certora/README.md
index 393b930..f01cfa2 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -56,8 +56,8 @@ The [`certora/specs`](specs) folder contains the following files:
   used.
 
 - [`Immutability.spec`](specs/Immutability.spec) checks that
-  PreLiquidation's storage is safe by checking that the storage is never
-  changed by a delegate call..
+  PreLiquidation contract is immutable because it doesn't perform any
+  delegate call.
 
 The [`certora/confs`](confs) folder contains a configuration file for
 each corresponding specification file.

From cfa7091c55b26674055785e496ddab7dfbfaaae5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 18:51:57 +0200
Subject: [PATCH 24/28] fix: update PreLiquidationHarness contract interface

---
 certora/confs/Reentrancy.conf             |  1 +
 certora/helpers/PreLiquidationHarness.sol | 14 +++++++++-----
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index b61839d..fd3765a 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -3,6 +3,7 @@
         "certora/helpers/PreLiquidationHarness.sol",
     ],
     "solc": "solc-0.8.27",
+    "solc_via_ir" : true,
     "verify": "PreLiquidationHarness:certora/specs/Reentrancy.spec",
     "loop_iter": "2",
     "optimistic_loop": true,
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
index 1f2a4db..9cb462e 100644
--- a/certora/helpers/PreLiquidationHarness.sol
+++ b/certora/helpers/PreLiquidationHarness.sol
@@ -1,14 +1,18 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.27;
 
-import {PreLiquidation, Id, MarketParams, PreLiquidationParams} from "../../src/PreLiquidation.sol";
+import {PreLiquidation, Id, Market, Position, PreLiquidationParams} from "../../src/PreLiquidation.sol";
 
 contract PreLiquidationHarness is PreLiquidation {
-    constructor(MarketParams memory _marketParams, PreLiquidationParams memory _preLiquidationParams, address morpho)
-        PreLiquidation(_marketParams, _preLiquidationParams, morpho)
+    constructor(Id id, PreLiquidationParams memory _preLiquidationParams, address morpho)
+        PreLiquidation(id, _preLiquidationParams, morpho)
     {}
 
-    function _isPreLiquidatable_(address borrower, uint256 collateralPrice) external view returns (bool) {
-        return _isPreLiquidatable(borrower, collateralPrice);
+    function _isPreLiquidatable_(uint256 collateralPrice, Position memory position, Market memory market)
+        external
+        view
+        returns (bool)
+    {
+        return _isPreLiquidatable(collateralPrice, position, market);
     }
 }

From 25eca6070c9afd753b26e45777f215aa3e1c4b8f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 23 Sep 2024 18:54:16 +0200
Subject: [PATCH 25/28] fix: update immutability conf

---
 certora/confs/Immutability.conf | 1 +
 1 file changed, 1 insertion(+)

diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
index e4e43a1..d9578ab 100644
--- a/certora/confs/Immutability.conf
+++ b/certora/confs/Immutability.conf
@@ -3,6 +3,7 @@
         "certora/helpers/PreLiquidationHarness.sol",
     ],
     "solc": "solc-0.8.27",
+    "solc_via_ir" : true,	
     "verify": "PreLiquidationHarness:certora/specs/Immutability.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

From f17e468defeb41777423ceccc9db2334393e1027 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 24 Sep 2024 10:11:50 +0200
Subject: [PATCH 26/28] fix: readability + simplify certora conf

---
 .github/workflows/certora.yml   | 2 +-
 certora/confs/Immutability.conf | 2 --
 certora/confs/Reentrancy.conf   | 2 --
 3 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 4c177e5..d4c5c3f 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -16,8 +16,8 @@ jobs:
 
       matrix:
         conf:
-          - Reentrancy
           - Immutability
+          - Reentrancy
 
     steps:
       - uses: actions/checkout@v4
diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
index d9578ab..dd47345 100644
--- a/certora/confs/Immutability.conf
+++ b/certora/confs/Immutability.conf
@@ -5,8 +5,6 @@
     "solc": "solc-0.8.27",
     "solc_via_ir" : true,	
     "verify": "PreLiquidationHarness:certora/specs/Immutability.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index fd3765a..41cf094 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -5,8 +5,6 @@
     "solc": "solc-0.8.27",
     "solc_via_ir" : true,
     "verify": "PreLiquidationHarness:certora/specs/Reentrancy.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
     "prover_args": [
         "-enableStorageSplitting false",
         "-depth 3",

From d88bf7e4962d2443833070237b36c67230930140 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Sun, 29 Sep 2024 20:40:06 +0200
Subject: [PATCH 27/28] fix: implement quentin's suggestions

---
 .gitignore                    | 3 ---
 certora/README.md             | 9 +--------
 certora/specs/Reentrancy.spec | 5 +++--
 3 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/.gitignore b/.gitignore
index 71f071c..8c30259 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,8 +13,5 @@ docs/
 # Dotenv file
 .env
 
-# Emacs
-*~
-
 # Certora
 .certora_internal
diff --git a/certora/README.md b/certora/README.md
index f01cfa2..a5ca080 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -18,17 +18,10 @@ following path names:
   - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
     used for `PreLiquidation`.
 
-### Installing the Certora Prover
-
-The Certora CLI can be installed by running `python3 -m pip3 install
-certora-cli`. Detailed installation instructions can be found on
-Certora's official
-[documentation](https://docs.certora.com/en/latest/docs/user-guide/install.html).
-
 To verifying a specification, run the command `certoraRun Spec.conf`
 where `Spec.conf` is the configuration file of the matching CVL
 specification. Configuration files are available in
-[`certora/conf`](./confs). Please ensure that `CERTORA_KEY` is set up
+[`certora/conf`](./confs). Please ensure that `CERTORAKEY` is set up
 in your environment.
 
 ## Overview
diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
index 934cab0..12c808d 100644
--- a/certora/specs/Reentrancy.spec
+++ b/certora/specs/Reentrancy.spec
@@ -1,7 +1,8 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-// True when storage has been accessed with either a SSTORE or a
-// SLOAD.
 
+
+
+// True when storage has been accessed with either a SSTORE or a SLOAD.
 persistent ghost bool hasAccessedStorage;
 
 hook ALL_SSTORE(uint loc, uint v) {

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

---
 certora/confs/Immutability.conf           |  6 +++---
 certora/confs/Reentrancy.conf             |  4 ++--
 certora/helpers/PreLiquidationHarness.sol | 18 ------------------
 3 files changed, 5 insertions(+), 23 deletions(-)
 delete mode 100644 certora/helpers/PreLiquidationHarness.sol

diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
index dd47345..6fae19c 100644
--- a/certora/confs/Immutability.conf
+++ b/certora/confs/Immutability.conf
@@ -1,10 +1,10 @@
 {
     "files": [
-        "certora/helpers/PreLiquidationHarness.sol",
+        "src/PreLiquidation.sol",
     ],
     "solc": "solc-0.8.27",
-    "solc_via_ir" : true,	
-    "verify": "PreLiquidationHarness:certora/specs/Immutability.spec",
+    "solc_via_ir" : true,
+    "verify": "PreLiquidation:certora/specs/Immutability.spec",
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index 41cf094..f217f93 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -1,10 +1,10 @@
 {
     "files": [
-        "certora/helpers/PreLiquidationHarness.sol",
+        "src/PreLiquidation.sol",
     ],
     "solc": "solc-0.8.27",
     "solc_via_ir" : true,
-    "verify": "PreLiquidationHarness:certora/specs/Reentrancy.spec",
+    "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
     "prover_args": [
         "-enableStorageSplitting false",
         "-depth 3",
diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
deleted file mode 100644
index 9cb462e..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, Id, Market, Position, PreLiquidationParams} from "../../src/PreLiquidation.sol";
-
-contract PreLiquidationHarness is PreLiquidation {
-    constructor(Id id, PreLiquidationParams memory _preLiquidationParams, address morpho)
-        PreLiquidation(id, _preLiquidationParams, morpho)
-    {}
-
-    function _isPreLiquidatable_(uint256 collateralPrice, Position memory position, Market memory market)
-        external
-        view
-        returns (bool)
-    {
-        return _isPreLiquidatable(collateralPrice, position, market);
-    }
-}