From 7d7bfa9d61fd724fba5aedc3335be9b7a0539f43 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 2 Apr 2024 17:34:38 +0200
Subject: [PATCH 01/32] feat: add Halmos test

---
 .github/workflows/halmos.yml | 26 +++++++++++
 .gitmodules                  |  3 ++
 foundry.toml                 |  2 +-
 lib/halmos-cheatcodes        |  1 +
 test/forge/HalmosTest.sol    | 84 ++++++++++++++++++++++++++++++++++++
 5 files changed, 115 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/halmos.yml
 create mode 160000 lib/halmos-cheatcodes
 create mode 100644 test/forge/HalmosTest.sol

diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
new file mode 100644
index 000000000..0d7e10b96
--- /dev/null
+++ b/.github/workflows/halmos.yml
@@ -0,0 +1,26 @@
+name: Halmos
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v4
+
+      - name: Install halmos
+        run: pip install halmos
+
+      - name: Run Halmos
+        run: halmos
diff --git a/.gitmodules b/.gitmodules
index 888d42dcd..455fbae41 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,6 @@
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = git@github.com:a16z/halmos-cheatcodes.git
diff --git a/foundry.toml b/foundry.toml
index 4b0da7556..cd36425af 100644
--- a/foundry.toml
+++ b/foundry.toml
@@ -1,7 +1,7 @@
 [profile.default]
 names = true
 sizes = true
-via-ir = true
+via-ir = false
 optimizer_runs = 999999 # Etherscan does not support verifying contracts with more optimization runs.
 
 [profile.default.invariant]
diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes
new file mode 160000
index 000000000..c0d865508
--- /dev/null
+++ b/lib/halmos-cheatcodes
@@ -0,0 +1 @@
+Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5
diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
new file mode 100644
index 000000000..7249b69a7
--- /dev/null
+++ b/test/forge/HalmosTest.sol
@@ -0,0 +1,84 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+import "../../lib/forge-std/src/Test.sol";
+import {SymTest} from "../../lib/halmos-cheatcodes/src/SymTest.sol";
+
+import {IMorpho} from "../../src/interfaces/IMorpho.sol";
+import {IrmMock} from "../../src/mocks/IrmMock.sol";
+import {ERC20Mock} from "../../src/mocks/ERC20Mock.sol";
+import {OracleMock} from "../../src/mocks/OracleMock.sol";
+
+import "../../src/Morpho.sol";
+import "../../src/libraries/ConstantsLib.sol";
+import {MorphoLib} from "../../src/libraries/periphery/MorphoLib.sol";
+
+contract HalmosTest is SymTest, Test {
+    using MorphoLib for IMorpho;
+    using MarketParamsLib for MarketParams;
+
+    uint256 internal constant BLOCK_TIME = 1;
+    uint256 internal constant DEFAULT_TEST_LLTV = 0.8 ether;
+
+    address internal OWNER;
+    address internal FEE_RECIPIENT;
+
+    IMorpho internal morpho;
+    ERC20Mock internal loanToken;
+    ERC20Mock internal collateralToken;
+    OracleMock internal oracle;
+    IrmMock internal irm;
+
+    MarketParams internal marketParams;
+    Id internal id;
+
+    function setUp() public virtual {
+        OWNER = address(0x10);
+        FEE_RECIPIENT = address(0x11);
+
+        morpho = IMorpho(address(new Morpho(OWNER)));
+
+        loanToken = new ERC20Mock();
+        collateralToken = new ERC20Mock();
+        oracle = new OracleMock();
+        oracle.setPrice(ORACLE_PRICE_SCALE);
+        irm = new IrmMock();
+
+        vm.startPrank(OWNER);
+        morpho.enableIrm(address(0));
+        morpho.enableIrm(address(irm));
+        morpho.enableLltv(0);
+        morpho.setFeeRecipient(FEE_RECIPIENT);
+        vm.stopPrank();
+
+        _setLltv(DEFAULT_TEST_LLTV);
+    }
+
+    function _setLltv(uint256 lltv) internal {
+        marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
+        id = marketParams.id();
+
+        vm.startPrank(OWNER);
+        if (!morpho.isLltvEnabled(lltv)) morpho.enableLltv(lltv);
+        if (morpho.lastUpdate(id) == 0) morpho.createMarket(marketParams);
+        vm.stopPrank();
+
+        _forward(1);
+    }
+
+    /// @dev Rolls & warps the given number of blocks forward the blockchain.
+    function _forward(uint256 blocks) internal {
+        vm.roll(block.number + blocks);
+        vm.warp(block.timestamp + blocks * BLOCK_TIME);
+    }
+
+    function check_fee(bytes4 selector, address caller) public {
+        bytes memory args = svm.createBytes(1024, "data");
+
+        vm.prank(caller);
+        (bool success,) = address(morpho).call(abi.encodePacked(selector, args));
+        vm.assume(success);
+
+        assert(morpho.fee(id) < MAX_FEE);
+    }
+}

From 7aebf2578328ef02a006640580cfbe85816cb40a Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 2 Apr 2024 17:36:51 +0200
Subject: [PATCH 02/32] fix: add foundry to CI for Halmos

---
 .github/workflows/halmos.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
index 0d7e10b96..32f3911dd 100644
--- a/.github/workflows/halmos.yml
+++ b/.github/workflows/halmos.yml
@@ -19,6 +19,9 @@ jobs:
       - name: Install python
         uses: actions/setup-python@v4
 
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
       - name: Install halmos
         run: pip install halmos
 

From 6667451f0e869cf1177dbfe40e473fbf88541a16 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 2 Apr 2024 17:45:02 +0200
Subject: [PATCH 03/32] chore: no timeout on counterexample

---
 test/forge/HalmosTest.sol | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 7249b69a7..4a50fc2d8 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -13,6 +13,7 @@ import "../../src/Morpho.sol";
 import "../../src/libraries/ConstantsLib.sol";
 import {MorphoLib} from "../../src/libraries/periphery/MorphoLib.sol";
 
+/// @custom:halmos --solver-timeout-assertion 0
 contract HalmosTest is SymTest, Test {
     using MorphoLib for IMorpho;
     using MarketParamsLib for MarketParams;

From bb2f9afa891f1c8dbf587877fd43743b52ff2287 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 2 Apr 2024 17:49:13 +0200
Subject: [PATCH 04/32] chore: remove halmos-cheatcode

---
 .gitmodules           | 3 ---
 lib/halmos-cheatcodes | 1 -
 2 files changed, 4 deletions(-)
 delete mode 160000 lib/halmos-cheatcodes

diff --git a/.gitmodules b/.gitmodules
index 455fbae41..888d42dcd 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,6 +1,3 @@
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
-[submodule "lib/halmos-cheatcodes"]
-	path = lib/halmos-cheatcodes
-	url = git@github.com:a16z/halmos-cheatcodes.git
diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes
deleted file mode 160000
index c0d865508..000000000
--- a/lib/halmos-cheatcodes
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5

From b1445fabcc315dcaf09e2ca9cf23d46d047605d7 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 2 Apr 2024 17:50:48 +0200
Subject: [PATCH 05/32] chore: add back halmos-cheatcodes with https

---
 .gitmodules           | 3 +++
 lib/halmos-cheatcodes | 1 +
 2 files changed, 4 insertions(+)
 create mode 160000 lib/halmos-cheatcodes

diff --git a/.gitmodules b/.gitmodules
index 888d42dcd..ba7c98e70 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,6 @@
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes.git
diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes
new file mode 160000
index 000000000..c0d865508
--- /dev/null
+++ b/lib/halmos-cheatcodes
@@ -0,0 +1 @@
+Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5

From 787e15428a32cdc74e064e6ceb44eeb6295201e2 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 2 Apr 2024 17:52:14 +0200
Subject: [PATCH 06/32] fix: test fee

---
 test/forge/HalmosTest.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 4a50fc2d8..32923e884 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -80,6 +80,6 @@ contract HalmosTest is SymTest, Test {
         (bool success,) = address(morpho).call(abi.encodePacked(selector, args));
         vm.assume(success);
 
-        assert(morpho.fee(id) < MAX_FEE);
+        assert(morpho.fee(id) <= MAX_FEE);
     }
 }

From 725c9ee7646df972d630a0aa2d32c0f390fe2c4f Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Wed, 3 Apr 2024 11:36:16 +0200
Subject: [PATCH 07/32] fix: use distinct args for dynamic types

---
 test/forge/HalmosTest.sol | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 32923e884..8d7a17b11 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -13,7 +13,7 @@ import "../../src/Morpho.sol";
 import "../../src/libraries/ConstantsLib.sol";
 import {MorphoLib} from "../../src/libraries/periphery/MorphoLib.sol";
 
-/// @custom:halmos --solver-timeout-assertion 0
+/// @custom:halmos --symbolic-storage --solver-timeout-assertion 0
 contract HalmosTest is SymTest, Test {
     using MorphoLib for IMorpho;
     using MarketParamsLib for MarketParams;
@@ -74,7 +74,30 @@ contract HalmosTest is SymTest, Test {
     }
 
     function check_fee(bytes4 selector, address caller) public {
-        bytes memory args = svm.createBytes(1024, "data");
+        vm.assume(selector != morpho.extSloads.selector);
+
+        bytes memory emptyData = hex"";
+        uint256 assets = svm.createUint256("assets");
+        uint256 shares = svm.createUint256("shares");
+        address onBehalf = svm.createAddress("onBehalf");
+
+        bytes memory args;
+
+        if (selector == morpho.supply.selector) {
+            args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
+        } else if (selector == morpho.repay.selector) {
+            args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
+        } else if (selector == morpho.supplyCollateral.selector) {
+            args = abi.encode(marketParams, assets, onBehalf, emptyData);
+        } else if (selector == morpho.liquidate.selector) {
+            address borrower = svm.createAddress("borrower");
+            args = abi.encode(marketParams, borrower, assets, shares, emptyData);
+        } else if (selector == morpho.flashLoan.selector) {
+            address token = svm.createAddress("token");
+            args = abi.encode(marketParams, token, assets, emptyData);
+        } else {
+            args = svm.createBytes(1024, "data");
+        }
 
         vm.prank(caller);
         (bool success,) = address(morpho).call(abi.encodePacked(selector, args));

From 7a71b6295348301a4f35cc23c8fe6701b7b65f7d Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 4 Apr 2024 16:54:30 +0200
Subject: [PATCH 08/32] chore: simpler setup

---
 test/forge/HalmosTest.sol | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 8d7a17b11..95aee72b5 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -83,6 +83,7 @@ contract HalmosTest is SymTest, Test {
 
         bytes memory args;
 
+        // Todo: make it possible to call any market
         if (selector == morpho.supply.selector) {
             args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
         } else if (selector == morpho.repay.selector) {
@@ -93,7 +94,8 @@ contract HalmosTest is SymTest, Test {
             address borrower = svm.createAddress("borrower");
             args = abi.encode(marketParams, borrower, assets, shares, emptyData);
         } else if (selector == morpho.flashLoan.selector) {
-            address token = svm.createAddress("token");
+            // Todo: make it more general
+            address token = address(loanToken);
             args = abi.encode(marketParams, token, assets, emptyData);
         } else {
             args = svm.createBytes(1024, "data");

From 848940714b4b7abb39674df0a8216b52c5c1ceb4 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 4 Apr 2024 17:19:46 +0200
Subject: [PATCH 09/32] feat: pass all market params

---
 test/forge/HalmosTest.sol | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 95aee72b5..df0bda393 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -75,21 +75,30 @@ contract HalmosTest is SymTest, Test {
 
     function check_fee(bytes4 selector, address caller) public {
         vm.assume(selector != morpho.extSloads.selector);
+        vm.assume(selector != morpho.createMarket.selector);
 
         bytes memory emptyData = hex"";
+        uint256 amount = svm.createUint256("amount");
         uint256 assets = svm.createUint256("assets");
         uint256 shares = svm.createUint256("shares");
         address onBehalf = svm.createAddress("onBehalf");
+        address receiver = svm.createAddress("receiver");
 
         bytes memory args;
 
         // Todo: make it possible to call any market
         if (selector == morpho.supply.selector) {
             args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
+        } else if (selector == morpho.withdraw.selector) {
+            args = abi.encode(marketParams, assets, shares, onBehalf, receiver);
+        } else if (selector == morpho.borrow.selector) {
+            args = abi.encode(marketParams, assets, shares, onBehalf, receiver);
         } else if (selector == morpho.repay.selector) {
             args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
         } else if (selector == morpho.supplyCollateral.selector) {
             args = abi.encode(marketParams, assets, onBehalf, emptyData);
+        } else if (selector == morpho.withdrawCollateral.selector) {
+            args = abi.encode(marketParams, assets, onBehalf, receiver);
         } else if (selector == morpho.liquidate.selector) {
             address borrower = svm.createAddress("borrower");
             args = abi.encode(marketParams, borrower, assets, shares, emptyData);
@@ -97,6 +106,10 @@ contract HalmosTest is SymTest, Test {
             // Todo: make it more general
             address token = address(loanToken);
             args = abi.encode(marketParams, token, assets, emptyData);
+        } else if (selector == morpho.accrueInterest.selector) {
+            args = abi.encode(marketParams);
+        } else if (selector == morpho.setFee.selector) {
+            args = abi.encode(marketParams, amount);
         } else {
             args = svm.createBytes(1024, "data");
         }

From 49a1ca08e142228b5fbfc5c6859dbcd31144caa8 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 5 Apr 2024 12:04:36 +0200
Subject: [PATCH 10/32] feat: generalize token for flashLoan

---
 test/forge/HalmosTest.sol | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index df0bda393..861619891 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -78,7 +78,6 @@ contract HalmosTest is SymTest, Test {
         vm.assume(selector != morpho.createMarket.selector);
 
         bytes memory emptyData = hex"";
-        uint256 amount = svm.createUint256("amount");
         uint256 assets = svm.createUint256("assets");
         uint256 shares = svm.createUint256("shares");
         address onBehalf = svm.createAddress("onBehalf");
@@ -86,7 +85,6 @@ contract HalmosTest is SymTest, Test {
 
         bytes memory args;
 
-        // Todo: make it possible to call any market
         if (selector == morpho.supply.selector) {
             args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
         } else if (selector == morpho.withdraw.selector) {
@@ -103,8 +101,16 @@ contract HalmosTest is SymTest, Test {
             address borrower = svm.createAddress("borrower");
             args = abi.encode(marketParams, borrower, assets, shares, emptyData);
         } else if (selector == morpho.flashLoan.selector) {
-            // Todo: make it more general
-            address token = address(loanToken);
+            uint256 rand = svm.createUint256("rand");
+            address token;
+            if (rand == 0) {
+                token = address(loanToken);
+            } else if (rand == 1) {
+                token = address(collateralToken);
+            } else {
+                ERC20Mock otherToken = new ERC20Mock();
+                token = address(otherToken);
+            }
             args = abi.encode(marketParams, token, assets, emptyData);
         } else if (selector == morpho.accrueInterest.selector) {
             args = abi.encode(marketParams);

From b6f96c797b455080b942ff998beb3c5c693f0abd Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 5 Apr 2024 14:26:12 +0200
Subject: [PATCH 11/32] fix: svm create newFee

---
 test/forge/HalmosTest.sol | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 861619891..11f3df5d2 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -115,7 +115,8 @@ contract HalmosTest is SymTest, Test {
         } else if (selector == morpho.accrueInterest.selector) {
             args = abi.encode(marketParams);
         } else if (selector == morpho.setFee.selector) {
-            args = abi.encode(marketParams, amount);
+            uint256 newFee = svm.createUint256("newFee");
+            args = abi.encode(marketParams, newFee);
         } else {
             args = svm.createBytes(1024, "data");
         }

From 3e546e5eeec615079a22ba351a07e43a4ba579b3 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Wed, 10 Apr 2024 15:27:30 +0200
Subject: [PATCH 12/32] feat: borrow less than supply and last updated
 invariant

---
 test/forge/HalmosTest.sol | 32 ++++++++++++++++++++++++++++----
 1 file changed, 28 insertions(+), 4 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 11f3df5d2..ca8941710 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -73,10 +73,7 @@ contract HalmosTest is SymTest, Test {
         vm.warp(block.timestamp + blocks * BLOCK_TIME);
     }
 
-    function check_fee(bytes4 selector, address caller) public {
-        vm.assume(selector != morpho.extSloads.selector);
-        vm.assume(selector != morpho.createMarket.selector);
-
+    function _callMorpho(bytes4 selector, address caller) internal {
         bytes memory emptyData = hex"";
         uint256 assets = svm.createUint256("assets");
         uint256 shares = svm.createUint256("shares");
@@ -124,7 +121,34 @@ contract HalmosTest is SymTest, Test {
         vm.prank(caller);
         (bool success,) = address(morpho).call(abi.encodePacked(selector, args));
         vm.assume(success);
+    }
+
+    function check_feeInRange(bytes4 selector, address caller) public {
+        vm.assume(selector != morpho.extSloads.selector);
+        vm.assume(selector != morpho.createMarket.selector);
+
+        _callMorpho(selector, caller);
 
         assert(morpho.fee(id) <= MAX_FEE);
     }
+
+    function check_borrowLessThanSupply(bytes4 selector, address caller) public {
+        vm.assume(selector != morpho.extSloads.selector);
+        vm.assume(selector != morpho.createMarket.selector);
+
+        _callMorpho(selector, caller);
+
+        assert(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id));
+    }
+
+    function check_lastUpdatedInvariant(bytes4 selector, address caller) public {
+        vm.assume(selector != morpho.extSloads.selector);
+        vm.assume(selector != morpho.createMarket.selector);
+
+        vm.assume(morpho.lastUpdated(id) != 0);
+
+        _callMorpho(selector, caller);
+
+        assert(morpho.lastUpdated(id) != 0);
+    }
 }

From 2b69597cda45fc2a271820f585e953cf75415aa5 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Wed, 10 Apr 2024 15:32:09 +0200
Subject: [PATCH 13/32] fix: lastUpdate name

---
 test/forge/HalmosTest.sol | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index ca8941710..dd16b0cad 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -145,10 +145,10 @@ contract HalmosTest is SymTest, Test {
         vm.assume(selector != morpho.extSloads.selector);
         vm.assume(selector != morpho.createMarket.selector);
 
-        vm.assume(morpho.lastUpdated(id) != 0);
+        vm.assume(morpho.lastUpdate(id) != 0);
 
         _callMorpho(selector, caller);
 
-        assert(morpho.lastUpdated(id) != 0);
+        assert(morpho.lastUpdate(id) != 0);
     }
 }

From 72d70b2b3f5cc9820093842af6e5013f89cb0fae Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 16 Apr 2024 17:16:13 +0200
Subject: [PATCH 14/32] chore: specify python-version

---
 .github/workflows/certora.yml | 2 ++
 .github/workflows/halmos.yml  | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 47e091715..81d64a0c4 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -35,6 +35,8 @@ jobs:
 
       - name: Install python
         uses: actions/setup-python@v4
+        with:
+          python-version: ">=3.9"
 
       - name: Install certora
         run: pip install certora-cli
diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
index 32f3911dd..f32231fea 100644
--- a/.github/workflows/halmos.yml
+++ b/.github/workflows/halmos.yml
@@ -18,6 +18,8 @@ jobs:
 
       - name: Install python
         uses: actions/setup-python@v4
+        with:
+          python-version: ">=3.9"
 
       - name: Install Foundry
         uses: foundry-rs/foundry-toolchain@v1

From ff1427a1614daa4278f76dae98ff0750fc513b89 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 16 Apr 2024 17:20:21 +0200
Subject: [PATCH 15/32] chore: bump action setup python

---
 .github/workflows/certora.yml | 2 +-
 .github/workflows/halmos.yml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 81d64a0c4..1ed55f2ec 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -34,7 +34,7 @@ jobs:
           submodules: recursive
 
       - name: Install python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: ">=3.9"
 
diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
index f32231fea..ef6b6fe28 100644
--- a/.github/workflows/halmos.yml
+++ b/.github/workflows/halmos.yml
@@ -17,7 +17,7 @@ jobs:
           submodules: recursive
 
       - name: Install python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: ">=3.9"
 

From fd6adac927e6ad84695d0b47d8799f051526d42c Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 16 Apr 2024 17:24:42 +0200
Subject: [PATCH 16/32] chore: add setuptools

---
 .github/workflows/certora.yml | 2 +-
 .github/workflows/halmos.yml  | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 1ed55f2ec..6203f6f31 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -29,7 +29,7 @@ jobs:
           - Transfer
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
index ef6b6fe28..5eeff430e 100644
--- a/.github/workflows/halmos.yml
+++ b/.github/workflows/halmos.yml
@@ -12,7 +12,7 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
@@ -25,7 +25,7 @@ jobs:
         uses: foundry-rs/foundry-toolchain@v1
 
       - name: Install halmos
-        run: pip install halmos
+        run: pip install halmos setuptools
 
       - name: Run Halmos
         run: halmos

From a71df2da9dc56b5ca8d4c75876670897013e66c5 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 16 Apr 2024 17:39:16 +0200
Subject: [PATCH 17/32] feat: symbolic LLTV

---
 test/forge/HalmosTest.sol | 31 ++++++++-----------------------
 1 file changed, 8 insertions(+), 23 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index dd16b0cad..0a339aa50 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -19,7 +19,6 @@ contract HalmosTest is SymTest, Test {
     using MarketParamsLib for MarketParams;
 
     uint256 internal constant BLOCK_TIME = 1;
-    uint256 internal constant DEFAULT_TEST_LLTV = 0.8 ether;
 
     address internal OWNER;
     address internal FEE_RECIPIENT;
@@ -52,28 +51,23 @@ contract HalmosTest is SymTest, Test {
         morpho.setFeeRecipient(FEE_RECIPIENT);
         vm.stopPrank();
 
-        _setLltv(DEFAULT_TEST_LLTV);
-    }
-
-    function _setLltv(uint256 lltv) internal {
+        uint256 lltv = svm.createUint256("lltv");
         marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
         id = marketParams.id();
 
         vm.startPrank(OWNER);
-        if (!morpho.isLltvEnabled(lltv)) morpho.enableLltv(lltv);
-        if (morpho.lastUpdate(id) == 0) morpho.createMarket(marketParams);
+        morpho.enableLltv(lltv);
+        morpho.createMarket(marketParams);
         vm.stopPrank();
 
-        _forward(1);
-    }
-
-    /// @dev Rolls & warps the given number of blocks forward the blockchain.
-    function _forward(uint256 blocks) internal {
-        vm.roll(block.number + blocks);
-        vm.warp(block.timestamp + blocks * BLOCK_TIME);
+        vm.roll(block.number + 1);
+        vm.warp(block.timestamp + 1 * BLOCK_TIME);
     }
 
     function _callMorpho(bytes4 selector, address caller) internal {
+        vm.assume(selector != morpho.extSloads.selector);
+        vm.assume(selector != morpho.createMarket.selector);
+
         bytes memory emptyData = hex"";
         uint256 assets = svm.createUint256("assets");
         uint256 shares = svm.createUint256("shares");
@@ -124,27 +118,18 @@ contract HalmosTest is SymTest, Test {
     }
 
     function check_feeInRange(bytes4 selector, address caller) public {
-        vm.assume(selector != morpho.extSloads.selector);
-        vm.assume(selector != morpho.createMarket.selector);
-
         _callMorpho(selector, caller);
 
         assert(morpho.fee(id) <= MAX_FEE);
     }
 
     function check_borrowLessThanSupply(bytes4 selector, address caller) public {
-        vm.assume(selector != morpho.extSloads.selector);
-        vm.assume(selector != morpho.createMarket.selector);
-
         _callMorpho(selector, caller);
 
         assert(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id));
     }
 
     function check_lastUpdatedInvariant(bytes4 selector, address caller) public {
-        vm.assume(selector != morpho.extSloads.selector);
-        vm.assume(selector != morpho.createMarket.selector);
-
         vm.assume(morpho.lastUpdate(id) != 0);
 
         _callMorpho(selector, caller);

From 62fc02e0c04dbd20810a49bab3200836f6711b40 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 19 Apr 2024 09:37:35 +0200
Subject: [PATCH 18/32] chore: remove setuptools

---
 .github/workflows/halmos.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
index 5eeff430e..d631346a6 100644
--- a/.github/workflows/halmos.yml
+++ b/.github/workflows/halmos.yml
@@ -25,7 +25,7 @@ jobs:
         uses: foundry-rs/foundry-toolchain@v1
 
       - name: Install halmos
-        run: pip install halmos setuptools
+        run: pip install halmos
 
       - name: Run Halmos
         run: halmos

From 6ef5c7a5b32e6bbccfd45c018a56f32691826273 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 19 Apr 2024 13:00:20 +0200
Subject: [PATCH 19/32] feat: check lltv smaller than WAD

---
 test/forge/HalmosTest.sol | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 0a339aa50..8d44eec59 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -136,4 +136,12 @@ contract HalmosTest is SymTest, Test {
 
         assert(morpho.lastUpdate(id) != 0);
     }
+
+    function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 lltv) public {
+        vm.assume(!morpho.isLltvEnabled(lltv) || lltv < 1e18);
+
+        _callMorpho(selector, caller);
+
+        assert(!morpho.isLltvEnabled(lltv) || lltv < 1e18);
+    }
 }

From c29c3bc1ee1e137eef05aeb2237807a78cb136a7 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 19 Apr 2024 13:40:40 +0200
Subject: [PATCH 20/32] refactor: use test profile for Halmos

---
 .github/workflows/halmos.yml | 2 +-
 foundry.toml                 | 2 +-
 package.json                 | 1 +
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
index d631346a6..fe56f888a 100644
--- a/.github/workflows/halmos.yml
+++ b/.github/workflows/halmos.yml
@@ -28,4 +28,4 @@ jobs:
         run: pip install halmos
 
       - name: Run Halmos
-        run: halmos
+        run: FOUNDRY_PROFILE=test halmos
diff --git a/foundry.toml b/foundry.toml
index 900bf246f..9b7733f1b 100644
--- a/foundry.toml
+++ b/foundry.toml
@@ -2,7 +2,7 @@
 libs = ["lib"]
 names = true
 sizes = true
-via-ir = false
+via-ir = true
 optimizer_runs = 999999 # Etherscan does not support verifying contracts with more optimization runs.
 
 [profile.default.invariant]
diff --git a/package.json b/package.json
index 1d942bfe8..bcc0e8d00 100644
--- a/package.json
+++ b/package.json
@@ -16,6 +16,7 @@
     "test:forge:invariant": "FOUNDRY_MATCH_CONTRACT=InvariantTest yarn test:forge",
     "test:forge:integration": "FOUNDRY_MATCH_CONTRACT=IntegrationTest yarn test:forge",
     "test:hardhat": "npx hardhat test",
+    "test:halmos": "FOUNDRY_PROFILE=test halmos",
     "lint": "yarn lint:forge && yarn lint:hardhat",
     "lint:forge": "forge fmt --check",
     "lint:hardhat": "prettier --check test/hardhat",

From 5a41d5dc63b7e3ef165cea97d6998c330e247d50 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 19 Apr 2024 15:22:05 +0200
Subject: [PATCH 21/32] docs: add description of invariants

---
 test/forge/HalmosTest.sol | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 8d44eec59..96f24ed35 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -55,6 +55,7 @@ contract HalmosTest is SymTest, Test {
         marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
         id = marketParams.id();
 
+        vm.assume(block.timestamp != 0);
         vm.startPrank(OWNER);
         morpho.enableLltv(lltv);
         morpho.createMarket(marketParams);
@@ -64,6 +65,7 @@ contract HalmosTest is SymTest, Test {
         vm.warp(block.timestamp + 1 * BLOCK_TIME);
     }
 
+    // Call Morpho, assuming interacting with only the defined market for performance reasons.
     function _callMorpho(bytes4 selector, address caller) internal {
         vm.assume(selector != morpho.extSloads.selector);
         vm.assume(selector != morpho.createMarket.selector);
@@ -117,26 +119,28 @@ contract HalmosTest is SymTest, Test {
         vm.assume(success);
     }
 
+    // Check that the fee is always smaller than the max fee.
     function check_feeInRange(bytes4 selector, address caller) public {
         _callMorpho(selector, caller);
 
         assert(morpho.fee(id) <= MAX_FEE);
     }
 
+    // Check that there is always less borrow than supply on the market.
     function check_borrowLessThanSupply(bytes4 selector, address caller) public {
         _callMorpho(selector, caller);
 
         assert(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id));
     }
 
-    function check_lastUpdatedInvariant(bytes4 selector, address caller) public {
-        vm.assume(morpho.lastUpdate(id) != 0);
-
+    // Check that the market cannot be "destroyed".
+    function check_lastUpdatedNonZero(bytes4 selector, address caller) public {
         _callMorpho(selector, caller);
 
         assert(morpho.lastUpdate(id) != 0);
     }
 
+    // Check that enabled LLTVs are necessarily less than 1.
     function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 lltv) public {
         vm.assume(!morpho.isLltvEnabled(lltv) || lltv < 1e18);
 

From 1221cce8fc1c8dacb43579ecfd1715d9c408fbbe Mon Sep 17 00:00:00 2001
From: MathisGD <mathis@morpho.xyz>
Date: Mon, 22 Apr 2024 12:26:16 +0200
Subject: [PATCH 22/32] test: halmost irm and ltv can't be disabled

---
 test/forge/HalmosTest.sol | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 96f24ed35..9d4962398 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -28,6 +28,7 @@ contract HalmosTest is SymTest, Test {
     ERC20Mock internal collateralToken;
     OracleMock internal oracle;
     IrmMock internal irm;
+    uint256 internal lltv;
 
     MarketParams internal marketParams;
     Id internal id;
@@ -51,7 +52,7 @@ contract HalmosTest is SymTest, Test {
         morpho.setFeeRecipient(FEE_RECIPIENT);
         vm.stopPrank();
 
-        uint256 lltv = svm.createUint256("lltv");
+        lltv = svm.createUint256("lltv");
         marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
         id = marketParams.id();
 
@@ -141,11 +142,26 @@ contract HalmosTest is SymTest, Test {
     }
 
     // Check that enabled LLTVs are necessarily less than 1.
-    function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 lltv) public {
-        vm.assume(!morpho.isLltvEnabled(lltv) || lltv < 1e18);
+    function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 _lltv) public {
+        vm.assume(!morpho.isLltvEnabled(_lltv) || _lltv < 1e18);
 
         _callMorpho(selector, caller);
 
-        assert(!morpho.isLltvEnabled(lltv) || lltv < 1e18);
+        assert(!morpho.isLltvEnabled(_lltv) || _lltv < 1e18);
+    }
+
+    // Check that LLTVs can't be disabled.
+    function check_lltvCannotBeDisabled(bytes4 selector, address caller) public {
+        _callMorpho(selector, caller);
+
+        assert(morpho.isLltvEnabled(lltv));
+    }
+
+    // Check that IRMs can't be disabled.
+    // Note: IRM is not symbolic, that is not ideal.
+    function check_irmCannotBeDisabled(bytes4 selector, address caller) public {
+        _callMorpho(selector, caller);
+
+        assert(morpho.isIrmEnabled(address(irm)));
     }
 }

From 46c6f463f46d59bfd9a80c5fdbd8eb7ba3e99deb Mon Sep 17 00:00:00 2001
From: MathisGD <mathis@morpho.xyz>
Date: Mon, 22 Apr 2024 12:35:24 +0200
Subject: [PATCH 23/32] test: halmos nonce can't decrease

---
 test/forge/HalmosTest.sol | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 9d4962398..cb445774f 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -164,4 +164,14 @@ contract HalmosTest is SymTest, Test {
 
         assert(morpho.isIrmEnabled(address(irm)));
     }
+
+    // Check that the nonce of users cannot decrease.
+    function check_nonceCannotDecrease(bytes4 selector, address caller, address user) public {
+        uint256 nonceBefore = morpho.nonce(user);
+
+        _callMorpho(selector, caller);
+
+        uint256 nonceAfter = morpho.nonce(user);
+        assert(nonceAfter == nonceBefore);
+    }
 }

From ba6386e90656943fcde7c97bececf00ce09c41fa Mon Sep 17 00:00:00 2001
From: MathisGD <mathis@morpho.xyz>
Date: Mon, 22 Apr 2024 12:39:58 +0200
Subject: [PATCH 24/32] test: halmos fix nonceCannotDecrease

---
 test/forge/HalmosTest.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index cb445774f..8e20ccb2e 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -172,6 +172,6 @@ contract HalmosTest is SymTest, Test {
         _callMorpho(selector, caller);
 
         uint256 nonceAfter = morpho.nonce(user);
-        assert(nonceAfter == nonceBefore);
+        assert(nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1);
     }
 }

From a3bfab074d269d5ae51675def59810c03d821881 Mon Sep 17 00:00:00 2001
From: MathisGD <mathis@morpho.xyz>
Date: Mon, 22 Apr 2024 13:44:12 +0200
Subject: [PATCH 25/32] test: halmos add two little rules

---
 test/forge/HalmosTest.sol | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 8e20ccb2e..0d02143d4 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -135,12 +135,22 @@ contract HalmosTest is SymTest, Test {
     }
 
     // Check that the market cannot be "destroyed".
-    function check_lastUpdatedNonZero(bytes4 selector, address caller) public {
+    function check_lastUpdateNonZero(bytes4 selector, address caller) public {
         _callMorpho(selector, caller);
 
         assert(morpho.lastUpdate(id) != 0);
     }
 
+    // Check that the lastUpdate can only increase.
+    function check_lastUpdateCannotDecrease(bytes4 selector, address caller) public {
+        uint256 lastUpdateBefore = morpho.lastUpdate(id);
+
+        _callMorpho(selector, caller);
+
+        uint256 lastUpdateAfter = morpho.lastUpdate(id);
+        assert(lastUpdateAfter >= lastUpdateBefore);
+    }
+
     // Check that enabled LLTVs are necessarily less than 1.
     function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 _lltv) public {
         vm.assume(!morpho.isLltvEnabled(_lltv) || _lltv < 1e18);
@@ -174,4 +184,13 @@ contract HalmosTest is SymTest, Test {
         uint256 nonceAfter = morpho.nonce(user);
         assert(nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1);
     }
+
+    function check_idToMarketParamsForCreatedMarketCannotChange(bytes4 selector, address caller) public {
+        MarketParams memory itmpBefore = morpho.idToMarketParams(id);
+
+        _callMorpho(selector, caller);
+
+        MarketParams memory itmpAfter = morpho.idToMarketParams(id);
+        assert(Id.unwrap(itmpBefore.id()) == Id.unwrap(itmpAfter.id()));
+    }
 }

From 53f3e28e8ce85e0798f3d8d0041e115446b8638a Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 22 Apr 2024 14:48:17 +0200
Subject: [PATCH 26/32] refactor: simplify setup

---
 test/forge/HalmosTest.sol | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 0d02143d4..fffce5c2d 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -44,26 +44,17 @@ contract HalmosTest is SymTest, Test {
         oracle = new OracleMock();
         oracle.setPrice(ORACLE_PRICE_SCALE);
         irm = new IrmMock();
-
-        vm.startPrank(OWNER);
-        morpho.enableIrm(address(0));
-        morpho.enableIrm(address(irm));
-        morpho.enableLltv(0);
-        morpho.setFeeRecipient(FEE_RECIPIENT);
-        vm.stopPrank();
-
         lltv = svm.createUint256("lltv");
+
         marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
         id = marketParams.id();
 
         vm.assume(block.timestamp != 0);
         vm.startPrank(OWNER);
+        morpho.enableIrm(address(irm));
         morpho.enableLltv(lltv);
         morpho.createMarket(marketParams);
         vm.stopPrank();
-
-        vm.roll(block.number + 1);
-        vm.warp(block.timestamp + 1 * BLOCK_TIME);
     }
 
     // Call Morpho, assuming interacting with only the defined market for performance reasons.
@@ -182,7 +173,7 @@ contract HalmosTest is SymTest, Test {
         _callMorpho(selector, caller);
 
         uint256 nonceAfter = morpho.nonce(user);
-        assert(nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1);
+        assert(nonceAfter == nonceBefore);
     }
 
     function check_idToMarketParamsForCreatedMarketCannotChange(bytes4 selector, address caller) public {

From 4b96f6aa502fde85cc70cd1ad05b22145745a0c9 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 22 Apr 2024 14:53:01 +0200
Subject: [PATCH 27/32] refactor: merge dispatch borrow-withdraw

---
 test/forge/HalmosTest.sol | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index fffce5c2d..ff80bc251 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -70,14 +70,10 @@ contract HalmosTest is SymTest, Test {
 
         bytes memory args;
 
-        if (selector == morpho.supply.selector) {
+        if (selector == morpho.supply.selector || selector == morpho.repay.selector) {
             args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
-        } else if (selector == morpho.withdraw.selector) {
+        } else if (selector == morpho.withdraw.selector || selector == morpho.borrow.selector) {
             args = abi.encode(marketParams, assets, shares, onBehalf, receiver);
-        } else if (selector == morpho.borrow.selector) {
-            args = abi.encode(marketParams, assets, shares, onBehalf, receiver);
-        } else if (selector == morpho.repay.selector) {
-            args = abi.encode(marketParams, assets, shares, onBehalf, emptyData);
         } else if (selector == morpho.supplyCollateral.selector) {
             args = abi.encode(marketParams, assets, onBehalf, emptyData);
         } else if (selector == morpho.withdrawCollateral.selector) {

From dc2c664496962331445b2c0bc9ba40e4fd77ae46 Mon Sep 17 00:00:00 2001
From: MathisGD <mathis@morpho.xyz>
Date: Mon, 22 Apr 2024 15:33:48 +0200
Subject: [PATCH 28/32] test: halmos document
 check_idToMarketParamsForCreatedMarketCannotChange

---
 test/forge/HalmosTest.sol | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index ff80bc251..c2649cb43 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -172,6 +172,8 @@ contract HalmosTest is SymTest, Test {
         assert(nonceAfter == nonceBefore);
     }
 
+    // Check that idToMarketParams cannot change.
+    // Note: ok because createMarket is never called by _callMorpho.
     function check_idToMarketParamsForCreatedMarketCannotChange(bytes4 selector, address caller) public {
         MarketParams memory itmpBefore = morpho.idToMarketParams(id);
 

From da3ebee920aecb30e7df0ab77aa1382f4aa127e6 Mon Sep 17 00:00:00 2001
From: MathisGD <mathis@morpho.xyz>
Date: Mon, 22 Apr 2024 15:36:45 +0200
Subject: [PATCH 29/32] test: (halmos) fix check_nonceCannotDecrease

---
 test/forge/HalmosTest.sol | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index c2649cb43..bbf9293a6 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -169,7 +169,7 @@ contract HalmosTest is SymTest, Test {
         _callMorpho(selector, caller);
 
         uint256 nonceAfter = morpho.nonce(user);
-        assert(nonceAfter == nonceBefore);
+        assert(nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1);
     }
 
     // Check that idToMarketParams cannot change.

From 0bdca52a44fdc5e5cc0fa290f3e72cc36930af7d Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 22 Apr 2024 18:26:18 +0200
Subject: [PATCH 30/32] refactor: simplify setup, and generalize id

---
 test/forge/HalmosTest.sol | 38 +++++++++++++++++++-------------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index bbf9293a6..3d0e1604b 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -18,10 +18,7 @@ contract HalmosTest is SymTest, Test {
     using MorphoLib for IMorpho;
     using MarketParamsLib for MarketParams;
 
-    uint256 internal constant BLOCK_TIME = 1;
-
-    address internal OWNER;
-    address internal FEE_RECIPIENT;
+    address internal owner;
 
     IMorpho internal morpho;
     ERC20Mock internal loanToken;
@@ -34,10 +31,8 @@ contract HalmosTest is SymTest, Test {
     Id internal id;
 
     function setUp() public virtual {
-        OWNER = address(0x10);
-        FEE_RECIPIENT = address(0x11);
-
-        morpho = IMorpho(address(new Morpho(OWNER)));
+        owner = svm.createAddress("owner");
+        morpho = IMorpho(address(new Morpho(owner)));
 
         loanToken = new ERC20Mock();
         collateralToken = new ERC20Mock();
@@ -49,8 +44,7 @@ contract HalmosTest is SymTest, Test {
         marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
         id = marketParams.id();
 
-        vm.assume(block.timestamp != 0);
-        vm.startPrank(OWNER);
+        vm.startPrank(owner);
         morpho.enableIrm(address(irm));
         morpho.enableLltv(lltv);
         morpho.createMarket(marketParams);
@@ -108,33 +102,39 @@ contract HalmosTest is SymTest, Test {
     }
 
     // Check that the fee is always smaller than the max fee.
-    function check_feeInRange(bytes4 selector, address caller) public {
+    function check_feeInRange(bytes4 selector, address caller, Id _id) public {
+        vm.assume(morpho.fee(_id) <= MAX_FEE);
+
         _callMorpho(selector, caller);
 
-        assert(morpho.fee(id) <= MAX_FEE);
+        assert(morpho.fee(_id) <= MAX_FEE);
     }
 
     // Check that there is always less borrow than supply on the market.
-    function check_borrowLessThanSupply(bytes4 selector, address caller) public {
+    function check_borrowLessThanSupply(bytes4 selector, address caller, Id _id) public {
+        vm.assume(morpho.totalBorrowAssets(_id) <= morpho.totalSupplyAssets(id));
+
         _callMorpho(selector, caller);
 
-        assert(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id));
+        assert(morpho.totalBorrowAssets(_id) <= morpho.totalSupplyAssets(_id));
     }
 
     // Check that the market cannot be "destroyed".
-    function check_lastUpdateNonZero(bytes4 selector, address caller) public {
+    function check_lastUpdateNonZero(bytes4 selector, address caller, Id _id) public {
+        vm.assume(morpho.lastUpdate(_id) != 0);
+
         _callMorpho(selector, caller);
 
-        assert(morpho.lastUpdate(id) != 0);
+        assert(morpho.lastUpdate(_id) != 0);
     }
 
     // Check that the lastUpdate can only increase.
-    function check_lastUpdateCannotDecrease(bytes4 selector, address caller) public {
-        uint256 lastUpdateBefore = morpho.lastUpdate(id);
+    function check_lastUpdateCannotDecrease(bytes4 selector, address caller, Id _id) public {
+        uint256 lastUpdateBefore = morpho.lastUpdate(_id);
 
         _callMorpho(selector, caller);
 
-        uint256 lastUpdateAfter = morpho.lastUpdate(id);
+        uint256 lastUpdateAfter = morpho.lastUpdate(_id);
         assert(lastUpdateAfter >= lastUpdateBefore);
     }
 

From 0618762067acea0de197d43fb627cc1fd504e4f8 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 22 Apr 2024 18:50:18 +0200
Subject: [PATCH 31/32] refactor: make id completely symbolic

---
 test/forge/HalmosTest.sol | 28 +++++++++++++---------------
 1 file changed, 13 insertions(+), 15 deletions(-)

diff --git a/test/forge/HalmosTest.sol b/test/forge/HalmosTest.sol
index 3d0e1604b..f9ddc5ec8 100644
--- a/test/forge/HalmosTest.sol
+++ b/test/forge/HalmosTest.sol
@@ -28,7 +28,6 @@ contract HalmosTest is SymTest, Test {
     uint256 internal lltv;
 
     MarketParams internal marketParams;
-    Id internal id;
 
     function setUp() public virtual {
         owner = svm.createAddress("owner");
@@ -42,7 +41,6 @@ contract HalmosTest is SymTest, Test {
         lltv = svm.createUint256("lltv");
 
         marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv);
-        id = marketParams.id();
 
         vm.startPrank(owner);
         morpho.enableIrm(address(irm));
@@ -102,39 +100,39 @@ contract HalmosTest is SymTest, Test {
     }
 
     // Check that the fee is always smaller than the max fee.
-    function check_feeInRange(bytes4 selector, address caller, Id _id) public {
-        vm.assume(morpho.fee(_id) <= MAX_FEE);
+    function check_feeInRange(bytes4 selector, address caller, Id id) public {
+        vm.assume(morpho.fee(id) <= MAX_FEE);
 
         _callMorpho(selector, caller);
 
-        assert(morpho.fee(_id) <= MAX_FEE);
+        assert(morpho.fee(id) <= MAX_FEE);
     }
 
     // Check that there is always less borrow than supply on the market.
-    function check_borrowLessThanSupply(bytes4 selector, address caller, Id _id) public {
-        vm.assume(morpho.totalBorrowAssets(_id) <= morpho.totalSupplyAssets(id));
+    function check_borrowLessThanSupply(bytes4 selector, address caller, Id id) public {
+        vm.assume(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id));
 
         _callMorpho(selector, caller);
 
-        assert(morpho.totalBorrowAssets(_id) <= morpho.totalSupplyAssets(_id));
+        assert(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id));
     }
 
     // Check that the market cannot be "destroyed".
-    function check_lastUpdateNonZero(bytes4 selector, address caller, Id _id) public {
-        vm.assume(morpho.lastUpdate(_id) != 0);
+    function check_lastUpdateNonZero(bytes4 selector, address caller, Id id) public {
+        vm.assume(morpho.lastUpdate(id) != 0);
 
         _callMorpho(selector, caller);
 
-        assert(morpho.lastUpdate(_id) != 0);
+        assert(morpho.lastUpdate(id) != 0);
     }
 
     // Check that the lastUpdate can only increase.
-    function check_lastUpdateCannotDecrease(bytes4 selector, address caller, Id _id) public {
-        uint256 lastUpdateBefore = morpho.lastUpdate(_id);
+    function check_lastUpdateCannotDecrease(bytes4 selector, address caller, Id id) public {
+        uint256 lastUpdateBefore = morpho.lastUpdate(id);
 
         _callMorpho(selector, caller);
 
-        uint256 lastUpdateAfter = morpho.lastUpdate(_id);
+        uint256 lastUpdateAfter = morpho.lastUpdate(id);
         assert(lastUpdateAfter >= lastUpdateBefore);
     }
 
@@ -174,7 +172,7 @@ contract HalmosTest is SymTest, Test {
 
     // Check that idToMarketParams cannot change.
     // Note: ok because createMarket is never called by _callMorpho.
-    function check_idToMarketParamsForCreatedMarketCannotChange(bytes4 selector, address caller) public {
+    function check_idToMarketParamsForCreatedMarketCannotChange(bytes4 selector, address caller, Id id) public {
         MarketParams memory itmpBefore = morpho.idToMarketParams(id);
 
         _callMorpho(selector, caller);

From 5a79282a4e109fcc067d88f3d178f5ad16f8a985 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 22 Apr 2024 18:54:19 +0200
Subject: [PATCH 32/32] refactor: move Halmos test to its own folder

---
 test/{forge => halmos}/HalmosTest.sol | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename test/{forge => halmos}/HalmosTest.sol (100%)

diff --git a/test/forge/HalmosTest.sol b/test/halmos/HalmosTest.sol
similarity index 100%
rename from test/forge/HalmosTest.sol
rename to test/halmos/HalmosTest.sol