From 6220852b667f5089ab3d263d43b4a1938cc15ba7 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 16:40:49 +0100
Subject: [PATCH 01/15] feat: market interactions

---
 .github/workflows/certora.yml         |  1 +
 certora/confs/MarketInteractions.conf | 27 +++++++++++++++++++++
 certora/specs/MarketInteractions.spec | 34 +++++++++++++++++++++++++++
 3 files changed, 62 insertions(+)
 create mode 100644 certora/confs/MarketInteractions.conf
 create mode 100644 certora/specs/MarketInteractions.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index ee4b0f75..b171d91a 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -22,6 +22,7 @@ jobs:
           - Immutability
           - LastUpdated
           - Liveness
+          - MarketInteractions
           - PendingValues
           - Range
           - Reentrancy
diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf
new file mode 100644
index 00000000..beb5574d
--- /dev/null
+++ b/certora/confs/MarketInteractions.conf
@@ -0,0 +1,27 @@
+{
+    "files": [
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/helpers/MetaMorphoHarness.sol",
+    ],
+    "link": [
+        "MetaMorphoHarness:MORPHO=MorphoHarness",
+    ],
+    "solc_map": {
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
+    },
+    "parametric_contracts": [
+        "MetaMorphoHarness",
+    ],
+    "verify": "MetaMorphoHarness:certora/specs/MarketInteractions.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho Market Interactions"
+}
diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
new file mode 100644
index 00000000..c9f58034
--- /dev/null
+++ b/certora/specs/MarketInteractions.spec
@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+import "Enabled.spec";
+
+using MorphoHarness as Morpho;
+
+methods {
+    function Morpho.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) => summarySupply(marketParams, assets, shares, onBehalf, data);
+    function Morpho.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver);
+    function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
+}
+
+function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) {
+    assert shares == 0;
+    assert onBehalf == currentContract;
+    assert data.length == 0;
+
+    // Compile using the following line instead
+    // return (assets, shares);
+    return Morpho.supply(marketParams, assets, shares, onBehalf, data);
+}
+
+function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) {
+    assert onBehalf == currentContract;
+    assert receiver == currentContract;
+
+    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+
+    // Compile using the following line instead
+    // return (assets, shares);
+    return Morpho.withdraw(marketParams, assets, shares, onBehalf, receiver);
+}
+
+invariant checkSummaries()
+    true;

From 6af7170978a8d7d4aad3be276ea845ac041bbcb2 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 16:53:01 +0100
Subject: [PATCH 02/15] refactor: remove sanity on market interactions

---
 certora/confs/MarketInteractions.conf | 1 -
 1 file changed, 1 deletion(-)

diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf
index beb5574d..a66f8678 100644
--- a/certora/confs/MarketInteractions.conf
+++ b/certora/confs/MarketInteractions.conf
@@ -21,7 +21,6 @@
         "-mediumTimeout 20",
         "-timeout 120",
     ],
-    "rule_sanity": "basic",
     "server": "production",
     "msg": "MetaMorpho Market Interactions"
 }

From fe7cc929a95e7de9942eed2d8652e2814a2cdf82 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 16:57:02 +0100
Subject: [PATCH 03/15] docs: comment failure

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

diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index c9f58034..3c5a1bbe 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -14,20 +14,20 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse
     assert onBehalf == currentContract;
     assert data.length == 0;
 
+    // What environment parameter should I give ?
+    return Morpho.supply(marketParams, assets, shares, onBehalf, data);
     // Compile using the following line instead
     // return (assets, shares);
-    return Morpho.supply(marketParams, assets, shares, onBehalf, data);
 }
 
 function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) {
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
-
+    // What environment parameter should I give ?
+    return Morpho.withdraw(marketParams, assets, shares, onBehalf, receiver);
     // Compile using the following line instead
     // return (assets, shares);
-    return Morpho.withdraw(marketParams, assets, shares, onBehalf, receiver);
 }
 
 invariant checkSummaries()

From d0d7e8b9605d4660fed8600091c18af3f4978e14 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 17:07:13 +0100
Subject: [PATCH 04/15] fix: compile using environment

---
 certora/specs/MarketInteractions.spec | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index 3c5a1bbe..ecf18251 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -4,30 +4,28 @@ import "Enabled.spec";
 using MorphoHarness as Morpho;
 
 methods {
-    function Morpho.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) => summarySupply(marketParams, assets, shares, onBehalf, data);
-    function Morpho.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver);
+    function Morpho.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) with (env e) => summarySupply(e, marketParams, assets, shares, onBehalf, data);
+    function Morpho.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) with (env e) => summaryWithdraw(e, marketParams, assets, shares, onBehalf, receiver);
     function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
 }
 
-function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) {
+function summarySupply(env e, MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) {
     assert shares == 0;
     assert onBehalf == currentContract;
     assert data.length == 0;
 
-    // What environment parameter should I give ?
-    return Morpho.supply(marketParams, assets, shares, onBehalf, data);
-    // Compile using the following line instead
-    // return (assets, shares);
+    uint256 retAssets; uint256 retShares;
+    retAssets, retShares = Morpho.supply(e, marketParams, assets, shares, onBehalf, data);
+    return (retAssets, retShares);
 }
 
-function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) {
+function summaryWithdraw(env e, MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) {
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
-    // What environment parameter should I give ?
-    return Morpho.withdraw(marketParams, assets, shares, onBehalf, receiver);
-    // Compile using the following line instead
-    // return (assets, shares);
+    uint256 retAssets; uint256 retShares;
+    retAssets, retShares = Morpho.withdraw(e, marketParams, assets, shares, onBehalf, receiver);
+    return (retAssets, retShares);
 }
 
 invariant checkSummaries()

From 3ecfb32648ec5efb45a55d3c2e9ec8074e2b9e4e Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 20:45:56 +0100
Subject: [PATCH 05/15] feat: verify enabled on all supply and withdraw

---
 certora/specs/MarketInteractions.spec | 28 +++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index ecf18251..efb9b650 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -7,6 +7,19 @@ methods {
     function Morpho.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) with (env e) => summarySupply(e, marketParams, assets, shares, onBehalf, data);
     function Morpho.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) with (env e) => summaryWithdraw(e, marketParams, assets, shares, onBehalf, receiver);
     function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
+    function Morpho.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
+}
+
+function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
+    MetaMorphoHarness.MarketParams marketParams;
+    uint256 lastUpdated = Morpho.lastUpdate(id);
+
+    // Safe require because markets in the supply/withdraw queue have positive last update (see LastUpdated.spec).
+    require lastUpdated > 0;
+    // Safe require because it is a verified invariant in Morpho Blue.
+    require lastUpdated > 0 => Morpho.libId(marketParams) == id;
+
+    return marketParams;
 }
 
 function summarySupply(env e, MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) {
@@ -14,6 +27,13 @@ function summarySupply(env e, MetaMorphoHarness.MarketParams marketParams, uint2
     assert onBehalf == currentContract;
     assert data.length == 0;
 
+    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    // Safe require because it is a verified invariant
+    require hasSupplyCapIsEnabled(id);
+
+    // Check that all markets on which MetaMorpho supplies are enabled markets.
+    assert config_(id).enabled;
+
     uint256 retAssets; uint256 retShares;
     retAssets, retShares = Morpho.supply(e, marketParams, assets, shares, onBehalf, data);
     return (retAssets, retShares);
@@ -23,6 +43,14 @@ function summaryWithdraw(env e, MetaMorphoHarness.MarketParams marketParams, uin
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
+    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    uint256 rank = withdrawRank(id);
+    // Safe require because it is a verified invariant.
+    require isInWithdrawQueueIsEnabled(assert_uint256(rank - 1));
+
+    // Check that all markets from which MetaMorpho withdraws are enabled markets.
+    assert config_(id).enabled;
+
     uint256 retAssets; uint256 retShares;
     retAssets, retShares = Morpho.withdraw(e, marketParams, assets, shares, onBehalf, receiver);
     return (retAssets, retShares);

From 0afab89e720239ef48d8c93093c9e851b5e7b9c2 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 20:50:11 +0100
Subject: [PATCH 06/15] fix: add is withdraw rank correct

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

diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index efb9b650..35a7a295 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -7,7 +7,7 @@ methods {
     function Morpho.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) with (env e) => summarySupply(e, marketParams, assets, shares, onBehalf, data);
     function Morpho.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) with (env e) => summaryWithdraw(e, marketParams, assets, shares, onBehalf, receiver);
     function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
-    function Morpho.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
+    function Morpho.idToMarketParams(MetaMorphoHarness.Id id) external returns(MetaMorphoHarness.MarketParams) => summaryIdToMarketParams(id);
 }
 
 function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
@@ -47,6 +47,8 @@ function summaryWithdraw(env e, MetaMorphoHarness.MarketParams marketParams, uin
     uint256 rank = withdrawRank(id);
     // Safe require because it is a verified invariant.
     require isInWithdrawQueueIsEnabled(assert_uint256(rank - 1));
+    // Safe require because it is a verified invariant
+    require isWithdrawRankCorrect(id);
 
     // Check that all markets from which MetaMorpho withdraws are enabled markets.
     assert config_(id).enabled;

From d0acbe2bd990fb1d85381ec44a52d5a327815f06 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 21:06:20 +0100
Subject: [PATCH 07/15] fix: target ConsistentState to have access to
 hasSupplyCapIsEnabled

---
 certora/specs/MarketInteractions.spec | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index 35a7a295..2fdbbb3b 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -1,23 +1,24 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "Enabled.spec";
+import "ConsistentState.spec";
 
-using MorphoHarness as Morpho;
+using MorphoHarness as M;
 
 methods {
-    function Morpho.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) with (env e) => summarySupply(e, marketParams, assets, shares, onBehalf, data);
-    function Morpho.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) with (env e) => summaryWithdraw(e, marketParams, assets, shares, onBehalf, receiver);
-    function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
-    function Morpho.idToMarketParams(MetaMorphoHarness.Id id) external returns(MetaMorphoHarness.MarketParams) => summaryIdToMarketParams(id);
+    function M.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) with (env e) => summarySupply(e, marketParams, assets, shares, onBehalf, data);
+    function M.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) with (env e) => summaryWithdraw(e, marketParams, assets, shares, onBehalf, receiver);
+    function M.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
+    function M.lastUpdate(MetaMorphoHarness.Id) external returns(uint256) envfree;
+    function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
 }
 
 function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
     MetaMorphoHarness.MarketParams marketParams;
-    uint256 lastUpdated = Morpho.lastUpdate(id);
+    uint256 lastUpdated = M.lastUpdate(id);
 
     // Safe require because markets in the supply/withdraw queue have positive last update (see LastUpdated.spec).
     require lastUpdated > 0;
-    // Safe require because it is a verified invariant in Morpho Blue.
-    require lastUpdated > 0 => Morpho.libId(marketParams) == id;
+    // Safe require because it is a verified invariant in M Blue.
+    require lastUpdated > 0 => M.libId(marketParams) == id;
 
     return marketParams;
 }
@@ -27,7 +28,7 @@ function summarySupply(env e, MetaMorphoHarness.MarketParams marketParams, uint2
     assert onBehalf == currentContract;
     assert data.length == 0;
 
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    MetaMorphoHarness.Id id = M.libId(marketParams);
     // Safe require because it is a verified invariant
     require hasSupplyCapIsEnabled(id);
 
@@ -35,7 +36,7 @@ function summarySupply(env e, MetaMorphoHarness.MarketParams marketParams, uint2
     assert config_(id).enabled;
 
     uint256 retAssets; uint256 retShares;
-    retAssets, retShares = Morpho.supply(e, marketParams, assets, shares, onBehalf, data);
+    retAssets, retShares = M.supply(e, marketParams, assets, shares, onBehalf, data);
     return (retAssets, retShares);
 }
 
@@ -43,7 +44,7 @@ function summaryWithdraw(env e, MetaMorphoHarness.MarketParams marketParams, uin
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    MetaMorphoHarness.Id id = M.libId(marketParams);
     uint256 rank = withdrawRank(id);
     // Safe require because it is a verified invariant.
     require isInWithdrawQueueIsEnabled(assert_uint256(rank - 1));
@@ -54,7 +55,7 @@ function summaryWithdraw(env e, MetaMorphoHarness.MarketParams marketParams, uin
     assert config_(id).enabled;
 
     uint256 retAssets; uint256 retShares;
-    retAssets, retShares = Morpho.withdraw(e, marketParams, assets, shares, onBehalf, receiver);
+    retAssets, retShares = M.withdraw(e, marketParams, assets, shares, onBehalf, receiver);
     return (retAssets, retShares);
 }
 

From ef187d1c1ec7e1c8f8583956a9ee01f40720f78d Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 21:14:06 +0100
Subject: [PATCH 08/15] docs: update with market interactions

---
 certora/README.md         | 3 +++
 certora/specs/Tokens.spec | 4 +---
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index 44ddb86a..d04b82ae 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -103,6 +103,7 @@ function isEnabledHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams
 ```
 
 This checks that each market in the withdraw queue has a consistent asset.
+Additionally, every supply and withdraw on Morpho Blue is checked to target an enabled market in [`MarketInteractions.spec`](specs/MarketInteractions.spec).
 
 ### Enabled flag
 
@@ -192,6 +193,7 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`Immutability.spec`](specs/Immutability.spec) checks that MetaMorpho is immutable.
 - [`LastUpdated.spec`](specs/LastUpdated.spec) checks that all Morpho Blue markets that MetaMorpho interacts with are created markets.
 - [`Liveness.spec`](specs/Liveness.spec) checks some liveness properties of MetaMorpho, notably that some emergency procedures are always available.
+- [`MarketInteractions.spec`](specs/MarketInteractions.spec) checks that every supply and withdraw from MetaMorpho is targeting an enabled market.
 - [`PendingValues.spec`](specs/PendingValues.spec) checks properties on the values that are still under timelock. Those properties are notably useful to prove that actual storage variables, when set to the pending value, use a consistent value.
 - [`Range.spec`](specs/Range.spec) checks the bounds (if any) of storage variables.
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that MetaMorpho is reentrancy safe by making sure that there are no untrusted external calls.
@@ -214,6 +216,7 @@ graph
 Tokens --> ConsistentState
 Liveness --> ConsistentState
 Reverts --> ConsistentState
+MarketInteractions --> ConsistentState
 ConsistentState --> Timelock
 Timelock --> LastUpdated
 LastUpdated --> Enabled
diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec
index fa9a19ab..29842886 100644
--- a/certora/specs/Tokens.spec
+++ b/certora/specs/Tokens.spec
@@ -54,9 +54,7 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
 
     MetaMorphoHarness.Id id = Morpho.libId(marketParams);
 
-    // Safe require because:
-    // - for reallocate this is checked in the code
-    // - for withdraw, it is verified that markets in the withdraw queue are enabled.
+    // Safe require because it is verifed in MarketInteractions.
     require config_(id).enabled;
     // Safe require because it is a verified invariant.
     require isEnabledHasConsistentAsset(marketParams);

From 70eea432c386ca6bc9ebcf1734de97a5d56e3991 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 21 Mar 2024 23:59:35 +0100
Subject: [PATCH 09/15] feat: add MorphoHavoc

---
 certora/confs/MarketInteractions.conf |  7 ++----
 certora/helpers/MorphoHavoc.sol       | 14 ++++++++++++
 certora/specs/MarketInteractions.spec | 33 ++++++++++++---------------
 3 files changed, 31 insertions(+), 23 deletions(-)
 create mode 100644 certora/helpers/MorphoHavoc.sol

diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf
index a66f8678..24dee0d4 100644
--- a/certora/confs/MarketInteractions.conf
+++ b/certora/confs/MarketInteractions.conf
@@ -1,13 +1,10 @@
 {
     "files": [
-        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/helpers/MorphoHavoc.sol",
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "link": [
-        "MetaMorphoHarness:MORPHO=MorphoHarness",
-    ],
     "solc_map": {
-        "MorphoHarness": "solc-0.8.19",
+        "MorphoHavoc": "solc-0.8.19",
         "MetaMorphoHarness": "solc-0.8.21",
     },
     "parametric_contracts": [
diff --git a/certora/helpers/MorphoHavoc.sol b/certora/helpers/MorphoHavoc.sol
new file mode 100644
index 00000000..c590672d
--- /dev/null
+++ b/certora/helpers/MorphoHavoc.sol
@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.19;
+
+import "../../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
+
+contract MorphoHavoc {
+    using MarketParamsLib for MarketParams;
+
+    function havocDummy() external pure {}
+
+    function libId(MarketParams memory marketParams) external pure returns (Id) {
+        return marketParams.id();
+    }
+}
diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index 2fdbbb3b..c6b8f05b 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -1,29 +1,28 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 import "ConsistentState.spec";
 
-using MorphoHarness as M;
+using MorphoHavoc as M;
 
 methods {
-    function M.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external returns (uint256, uint256) with (env e) => summarySupply(e, marketParams, assets, shares, onBehalf, data);
-    function M.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external returns (uint256, uint256) with (env e) => summaryWithdraw(e, marketParams, assets, shares, onBehalf, receiver);
-    function M.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
-    function M.lastUpdate(MetaMorphoHarness.Id) external returns(uint256) envfree;
+    function _.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summarySupply(marketParams, assets, shares, onBehalf, data) expect (uint256, uint256) ALL;
+    function _.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver) expect (uint256, uint256) ALL;
     function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
+
+    function M.libId(MetaMorphoHarness.MarketParams marketParams) external returns(MetaMorphoHarness.Id) envfree;
 }
 
 function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
     MetaMorphoHarness.MarketParams marketParams;
-    uint256 lastUpdated = M.lastUpdate(id);
 
-    // Safe require because markets in the supply/withdraw queue have positive last update (see LastUpdated.spec).
-    require lastUpdated > 0;
-    // Safe require because it is a verified invariant in M Blue.
-    require lastUpdated > 0 => M.libId(marketParams) == id;
+    // Safe require because:
+    // - markets in the supply/withdraw queue have positive lastUpdate (see LastUpdated.spec)
+    // - lastUpdate(id) > 0 => marketParams.id() == id is a verified invariant in Morpho Blue.
+    require M.libId(marketParams) == id;
 
     return marketParams;
 }
 
-function summarySupply(env e, MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) {
+function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) {
     assert shares == 0;
     assert onBehalf == currentContract;
     assert data.length == 0;
@@ -35,12 +34,11 @@ function summarySupply(env e, MetaMorphoHarness.MarketParams marketParams, uint2
     // Check that all markets on which MetaMorpho supplies are enabled markets.
     assert config_(id).enabled;
 
-    uint256 retAssets; uint256 retShares;
-    retAssets, retShares = M.supply(e, marketParams, assets, shares, onBehalf, data);
-    return (retAssets, retShares);
+    // NONDET summary, which is sound because all non view functions in Morpho Blue are abstracted away.
+    return (_, _);
 }
 
-function summaryWithdraw(env e, MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) {
+function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) {
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
@@ -54,9 +52,8 @@ function summaryWithdraw(env e, MetaMorphoHarness.MarketParams marketParams, uin
     // Check that all markets from which MetaMorpho withdraws are enabled markets.
     assert config_(id).enabled;
 
-    uint256 retAssets; uint256 retShares;
-    retAssets, retShares = M.withdraw(e, marketParams, assets, shares, onBehalf, receiver);
-    return (retAssets, retShares);
+    // NONDET summary, which is sound because all non view functions in Morpho Blue are abstracted away.
+    return (_, _);
 }
 
 invariant checkSummaries()

From e9d75b6109c3634644548d833e3c1d99a16d9f63 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 10:07:24 +0100
Subject: [PATCH 10/15] fix: import Util in configuration

---
 certora/README.md                     |  2 +-
 certora/confs/ConsistentState.conf    |  7 ++-----
 certora/confs/LastUpdated.conf        |  2 ++
 certora/confs/MarketInteractions.conf |  7 ++-----
 certora/helpers/MorphoHavoc.sol       | 14 --------------
 certora/helpers/Util.sol              | 16 +++++++++++++++-
 certora/specs/ConsistentState.spec    | 22 ++++++++++------------
 certora/specs/LastUpdated.spec        | 15 +++++++++++++--
 certora/specs/Liveness.spec           |  2 +-
 certora/specs/MarketInteractions.spec | 10 +++-------
 certora/specs/Reverts.spec            | 13 ++++---------
 certora/specs/Timelock.spec           |  2 +-
 certora/specs/Tokens.spec             | 14 ++++----------
 13 files changed, 58 insertions(+), 68 deletions(-)
 delete mode 100644 certora/helpers/MorphoHavoc.sol

diff --git a/certora/README.md b/certora/README.md
index d04b82ae..fbe2dc21 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -199,7 +199,7 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that MetaMorpho is reentrancy safe by making sure that there are no untrusted external calls.
 - [`Reverts.spec`](specs/Reverts.spec) checks the revert conditions on entrypoints.
 - [`Roles.spec`](specs/Roles.spec) checks the access control and authorization granted by the respective MetaMorpho roles. In particular it checks the hierarchy of roles.
-- [`Timelock.spec`](specs/Timelock.spec) gives computations (and verifies them) for periods during which we know the values are under timelock.
+- [`Timelock.spec`](specs/Timelock.spec) verifies computations for periods during which we know the values are under timelock.
 - [`Tokens.spec`](specs/Tokens.spec) checks that tokens are not kept on the MetaMorpho contract. Any deposit ends up in Morpho Blue and any withdrawal is forwarded to the user.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
index 366d4e4c..5da45284 100644
--- a/certora/confs/ConsistentState.conf
+++ b/certora/confs/ConsistentState.conf
@@ -1,12 +1,9 @@
 {
     "files": [
-        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
+        "certora/helpers/Util.sol",
     ],
-    "solc_map": {
-        "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-    },
+    "solc": "solc-0.8.21",
     "parametric_contracts": [
         "MetaMorphoHarness",
     ],
diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf
index 855c7359..81bc168c 100644
--- a/certora/confs/LastUpdated.conf
+++ b/certora/confs/LastUpdated.conf
@@ -2,10 +2,12 @@
     "files": [
         "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
+        "certora/helpers/Util.sol",
     ],
     "solc_map": {
         "MorphoHarness": "solc-0.8.19",
         "MetaMorphoHarness": "solc-0.8.21",
+        "Util": "solc-0.8.21",
     },
     "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec",
     "loop_iter": "2",
diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf
index 24dee0d4..02b6ea2e 100644
--- a/certora/confs/MarketInteractions.conf
+++ b/certora/confs/MarketInteractions.conf
@@ -1,12 +1,9 @@
 {
     "files": [
-        "certora/helpers/MorphoHavoc.sol",
         "certora/helpers/MetaMorphoHarness.sol",
+        "certora/helpers/Util.sol",
     ],
-    "solc_map": {
-        "MorphoHavoc": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-    },
+    "solc": "solc-0.8.21",
     "parametric_contracts": [
         "MetaMorphoHarness",
     ],
diff --git a/certora/helpers/MorphoHavoc.sol b/certora/helpers/MorphoHavoc.sol
deleted file mode 100644
index c590672d..00000000
--- a/certora/helpers/MorphoHavoc.sol
+++ /dev/null
@@ -1,14 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.19;
-
-import "../../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
-
-contract MorphoHavoc {
-    using MarketParamsLib for MarketParams;
-
-    function havocDummy() external pure {}
-
-    function libId(MarketParams memory marketParams) external pure returns (Id) {
-        return marketParams.id();
-    }
-}
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
index e713bd38..b38f9e03 100644
--- a/certora/helpers/Util.sol
+++ b/certora/helpers/Util.sol
@@ -1,11 +1,21 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.21;
 
-import {IERC20, SafeERC20, IMorphoHarness, SharesMathLib, Id, Market} from "../munged/MetaMorpho.sol";
+import {
+    MarketParams,
+    MarketParamsLib,
+    IERC20,
+    SafeERC20,
+    IMorphoHarness,
+    SharesMathLib,
+    Id,
+    Market
+} from "../munged/MetaMorpho.sol";
 
 contract Util {
     using SafeERC20 for IERC20;
     using SharesMathLib for uint256;
+    using MarketParamsLib for MarketParams;
 
     function balanceOf(address token, address user) external view returns (uint256) {
         return IERC20(token).balanceOf(user);
@@ -31,4 +41,8 @@ contract Util {
             return shares.toAssetsDown(market.totalSupplyAssets, market.totalSupplyShares);
         }
     }
+
+    function libId(MarketParams memory marketParams) external pure returns (Id) {
+        return marketParams.id();
+    }
 }
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
index 8185f85b..c9a20a75 100644
--- a/certora/specs/ConsistentState.spec
+++ b/certora/specs/ConsistentState.spec
@@ -1,16 +1,14 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 import "Timelock.spec";
 
-function hasCuratorRole(address user) returns bool {
-    return user == owner() || user == curator();
-}
-
-function hasAllocatorRole(address user) returns bool {
-    return user == owner() || user == curator() || isAllocator(user);
-}
-
-function hasGuardianRole(address user) returns bool {
-    return user == owner() || user == guardian();
+using Util as Util;
+
+methods {
+    function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
+    function Util.balanceOf(address, address) external returns(uint256) envfree;
+    function Util.totalSupply(address) external returns(uint256) envfree;
+    function Util.safeTransferFrom(address, address, address, uint256) external envfree;
+    function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree;
 }
 
 // Check that fee cannot accrue to an unset fee recipient.
@@ -29,7 +27,7 @@ invariant supplyCapIsEnabled(MetaMorphoHarness.Id id)
     hasSupplyCapIsEnabled(id);
 
 function hasPendingSupplyCapHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams) returns bool {
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
 
     return pendingCap_(id).validAt > 0 => marketParams.loanToken == asset();
 }
@@ -39,7 +37,7 @@ invariant pendingSupplyCapHasConsistentAsset(MetaMorphoHarness.MarketParams mark
     hasPendingSupplyCapHasConsistentAsset(marketParams);
 
 function isEnabledHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams) returns bool {
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
 
     return config_(id).enabled => marketParams.loanToken == asset();
 }
diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec
index d123cfc7..a7a75001 100644
--- a/certora/specs/LastUpdated.spec
+++ b/certora/specs/LastUpdated.spec
@@ -1,11 +1,22 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "Enabled.spec";
+import "ConsistentState.spec";
 
 using MorphoHarness as Morpho;
 
 methods {
     function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree;
-    function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
+}
+
+function hasCuratorRole(address user) returns bool {
+    return user == owner() || user == curator();
+}
+
+function hasAllocatorRole(address user) returns bool {
+    return user == owner() || user == curator() || isAllocator(user);
+}
+
+function hasGuardianRole(address user) returns bool {
+    return user == owner() || user == guardian();
 }
 
 // Check that any market with positive cap is created on Morpho Blue.
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index d8abb025..025263a9 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -25,7 +25,7 @@ rule canPauseSupply() {
 }
 
 rule canForceRemoveMarket(MetaMorphoHarness.MarketParams marketParams) {
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
 
     // Safe require because it is a verified invariant.
     require hasSupplyCapIsEnabled(id);
diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index c6b8f05b..8d650bcb 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -1,14 +1,10 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 import "ConsistentState.spec";
 
-using MorphoHavoc as M;
-
 methods {
     function _.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summarySupply(marketParams, assets, shares, onBehalf, data) expect (uint256, uint256) ALL;
     function _.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver) expect (uint256, uint256) ALL;
     function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
-
-    function M.libId(MetaMorphoHarness.MarketParams marketParams) external returns(MetaMorphoHarness.Id) envfree;
 }
 
 function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
@@ -17,7 +13,7 @@ function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarn
     // Safe require because:
     // - markets in the supply/withdraw queue have positive lastUpdate (see LastUpdated.spec)
     // - lastUpdate(id) > 0 => marketParams.id() == id is a verified invariant in Morpho Blue.
-    require M.libId(marketParams) == id;
+    require Util.libId(marketParams) == id;
 
     return marketParams;
 }
@@ -27,7 +23,7 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse
     assert onBehalf == currentContract;
     assert data.length == 0;
 
-    MetaMorphoHarness.Id id = M.libId(marketParams);
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
     // Safe require because it is a verified invariant
     require hasSupplyCapIsEnabled(id);
 
@@ -42,7 +38,7 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
-    MetaMorphoHarness.Id id = M.libId(marketParams);
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
     uint256 rank = withdrawRank(id);
     // Safe require because it is a verified invariant.
     require isInWithdrawQueueIsEnabled(assert_uint256(rank - 1));
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 9e91e6f4..5394efe9 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -1,12 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "ConsistentState.spec";
-
-using Util as Util;
+import "LastUpdated.spec";
 
 methods {
-    function Util.totalSupply(address) external returns(uint256) envfree;
-    function Util.balanceOf(address, address) external returns(uint256) envfree;
-
     function _.transfer(address, uint256) external => DISPATCHER(true);
     function _.balanceOf(address) external => DISPATCHER(true);
 }
@@ -104,7 +99,7 @@ rule submitGuardianRevertCondition(env e, address newGuardian) {
 
 // Check all the revert conditions of the submitCap function.
 rule submitCapRevertCondition(env e, MetaMorphoHarness.MarketParams marketParams, uint256 newSupplyCap) {
-    MorphoHarness.Id id = Morpho.libId(marketParams);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     bool hasCuratorRole = hasCuratorRole(e.msg.sender);
     address asset = asset();
@@ -134,7 +129,7 @@ rule submitCapRevertCondition(env e, MetaMorphoHarness.MarketParams marketParams
 
 // Check all the revert conditions of the submitMarketRemoval function.
 rule submitMarketRemovalRevertCondition(env e, MetaMorphoHarness.MarketParams marketParams) {
-    MorphoHarness.Id id = Morpho.libId(marketParams);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     bool hasCuratorRole = hasCuratorRole(e.msg.sender);
     uint256 pendingCapValidAt = pendingCap_(id).validAt;
@@ -283,7 +278,7 @@ rule acceptGuardianRevertCondition(env e) {
 // Check the input validation conditions under which the acceptCap function reverts.
 // This function can also revert if interest accrual reverts or if it would lead to growing the withdraw queue past the max length.
 rule acceptCapInputValidation(env e, MetaMorphoHarness.MarketParams marketParams) {
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
 
     uint256 pendingCapValidAt = pendingCap_(id).validAt;
 
diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec
index cc7d7af4..0f7cf5a9 100644
--- a/certora/specs/Timelock.spec
+++ b/certora/specs/Timelock.spec
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "LastUpdated.spec";
+import "Enabled.spec";
 
 methods {
     function _.supplyShares(MetaMorphoHarness.Id id, address user) external => summarySupplyshares(id, user) expect uint256;
diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec
index 29842886..703e874c 100644
--- a/certora/specs/Tokens.spec
+++ b/certora/specs/Tokens.spec
@@ -1,13 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "ConsistentState.spec";
-
-using Util as Util;
+import "LastUpdated.spec";
 
 methods {
-    function Util.balanceOf(address, address) external returns(uint256) envfree;
-    function Util.safeTransferFrom(address, address, address, uint256) external envfree;
-    function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree;
-
     function _.transfer(address, uint256) external => DISPATCHER(true);
     function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
     function _.balanceOf(address) external => DISPATCHER(true);
@@ -27,7 +21,7 @@ function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarn
     // Safe require because markets in the supply/withdraw queue have positive last update (see LastUpdated.spec).
     require lastUpdated > 0;
     // Safe require because it is a verified invariant in Morpho Blue.
-    require lastUpdated > 0 => Morpho.libId(marketParams) == id;
+    require lastUpdated > 0 => Util.libId(marketParams) == id;
 
     return marketParams;
 }
@@ -38,7 +32,7 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse
     assert data.length == 0;
 
     // Safe require because it is a verified invariant.
-    require hasSupplyCapIsEnabled(Morpho.libId(marketParams));
+    require hasSupplyCapIsEnabled(Util.libId(marketParams));
     // Safe require because it is a verified invariant.
     require isEnabledHasConsistentAsset(marketParams);
 
@@ -52,7 +46,7 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
-    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
 
     // Safe require because it is verifed in MarketInteractions.
     require config_(id).enabled;

From 5f50dc9aed03c1a7e2059f49798f87da808bf3a5 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 10:11:39 +0100
Subject: [PATCH 11/15] fix: dependency and update graph

---
 certora/README.md           | 10 +++++-----
 certora/specs/Liveness.spec |  2 +-
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/certora/README.md b/certora/README.md
index fbe2dc21..e2246f95 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -213,13 +213,13 @@ The [`certora/dispatch`](dispatch) folder contains different contracts similar
 
 ```mermaid
 graph
-Tokens --> ConsistentState
-Liveness --> ConsistentState
-Reverts --> ConsistentState
+Tokens --> LastUpdated
+Liveness --> LastUpdated
+Reverts --> LastUpdated
+LastUpdated --> ConsistentState
 MarketInteractions --> ConsistentState
 ConsistentState --> Timelock
-Timelock --> LastUpdated
-LastUpdated --> Enabled
+Timelock --> Enabled
 Enabled --> DistinctIdentifiers
 DistinctIdentifiers --> PendingValues
 PendingValues --> Range
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 025263a9..fe3160e5 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "ConsistentState.spec";
+import "LastUpdated.spec";
 
 // Check that having the allocator role allows to pause supply on the vault.
 rule canPauseSupply() {

From d7cfaf0e7b58352a90e7d829a3531ccc06ba3977 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 11:27:27 +0100
Subject: [PATCH 12/15] feat: harness last index withdraw

---
 certora/applyMunging.patch            | 40 ++++++++++++++++++---------
 certora/specs/MarketInteractions.spec |  6 ++--
 2 files changed, 31 insertions(+), 15 deletions(-)

diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
index b77f8391..095d407a 100644
--- a/certora/applyMunging.patch
+++ b/certora/applyMunging.patch
@@ -1,6 +1,6 @@
 diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol
---- interfaces/IMetaMorpho.sol	2024-01-03 14:41:15.012185229 +0100
-+++ interfaces/IMetaMorpho.sol	2024-03-04 17:27:18.336468241 +0100
+--- interfaces/IMetaMorpho.sol	2024-03-20 15:13:25.818251404 +0100
++++ interfaces/IMetaMorpho.sol	2024-03-22 11:22:35.598510490 +0100
 @@ -1,9 +1,9 @@
  // SPDX-License-Identifier: GPL-2.0-or-later
  pragma solidity >=0.5.0;
@@ -24,8 +24,8 @@ diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol
  
      /// @notice The address of the curator.
 diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol
---- libraries/ErrorsLib.sol	2024-01-03 14:27:38.058744959 +0100
-+++ libraries/ErrorsLib.sol	2024-02-13 10:07:21.879957695 +0100
+--- libraries/ErrorsLib.sol	2024-03-20 15:13:25.802251714 +0100
++++ libraries/ErrorsLib.sol	2024-03-22 11:22:35.598510490 +0100
 @@ -1,7 +1,7 @@
  // SPDX-License-Identifier: GPL-2.0-or-later
  pragma solidity ^0.8.0;
@@ -36,8 +36,8 @@ diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol
  /// @title ErrorsLib
  /// @author Morpho Labs
 diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
---- libraries/EventsLib.sol	2023-11-27 12:37:13.369852625 +0100
-+++ libraries/EventsLib.sol	2024-02-13 10:07:21.879957695 +0100
+--- libraries/EventsLib.sol	2024-03-20 15:13:25.802251714 +0100
++++ libraries/EventsLib.sol	2024-03-22 11:22:35.598510490 +0100
 @@ -1,7 +1,7 @@
  // SPDX-License-Identifier: GPL-2.0-or-later
  pragma solidity ^0.8.0;
@@ -48,8 +48,8 @@ diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
  import {PendingAddress} from "./PendingLib.sol";
  
 diff -ruN MetaMorpho.sol MetaMorpho.sol
---- MetaMorpho.sol	2024-02-02 13:00:21.238074050 +0100
-+++ MetaMorpho.sol	2024-03-04 23:26:21.562604750 +0100
+--- MetaMorpho.sol	2024-03-20 15:13:25.862250553 +0100
++++ MetaMorpho.sol	2024-03-22 11:25:47.991055286 +0100
 @@ -9,24 +9,22 @@
      IMetaMorphoBase,
      IMetaMorphoStaticTyping
@@ -114,10 +114,14 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
  
      /// @notice OpenZeppelin decimals offset used by the ERC4626 implementation.
      /// @dev Calculated to be max(0, 18 - underlyingDecimals) at construction, so the initial conversion rate maximizes
-@@ -107,6 +103,15 @@
+@@ -107,6 +103,19 @@
      /// @inheritdoc IMetaMorphoBase
      uint256 public lastTotalAssets;
  
++    // HARNESS
++    // The index of the identifier of the last market withdrawn.
++    uint256 lastIndexWithdraw;
++
 +    // HARNESS
 +    // The rank of a market identifier in the withdraw queue.
 +    // Returns 0 if the corresponding market is not in the withdraw queue.
@@ -130,7 +134,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
      /* CONSTRUCTOR */
  
      /// @dev Initializes the contract.
-@@ -126,7 +131,7 @@
+@@ -126,7 +135,7 @@
      ) ERC4626(IERC20(_asset)) ERC20Permit(_name) ERC20(_name, _symbol) Ownable(owner) {
          if (morpho == address(0)) revert ErrorsLib.ZeroAddress();
  
@@ -139,7 +143,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          DECIMALS_OFFSET = uint8(uint256(18).zeroFloorSub(IERC20Metadata(_asset).decimals()));
  
          _checkTimelockBounds(initialTimelock);
-@@ -338,6 +343,9 @@
+@@ -338,6 +347,9 @@
              seen[prevIndex] = true;
  
              newWithdrawQueue[i] = id;
@@ -149,7 +153,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          }
  
          for (uint256 i; i < currLength; ++i) {
-@@ -355,6 +363,10 @@
+@@ -355,6 +367,10 @@
                      }
                  }
  
@@ -160,7 +164,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  delete config[id];
              }
          }
-@@ -743,6 +755,9 @@
+@@ -743,6 +759,9 @@
  
          if (supplyCap > 0) {
              if (!marketConfig.enabled) {
@@ -170,3 +174,13 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  withdrawQueue.push(id);
  
                  if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded();
+@@ -802,6 +821,9 @@
+     /// @dev Withdraws `assets` from Morpho.
+     function _withdrawMorpho(uint256 assets) internal {
+         for (uint256 i; i < withdrawQueue.length; ++i) {
++            // HARNESS
++            lastIndexWithdraw = i;
++
+             Id id = withdrawQueue[i];
+             MarketParams memory marketParams = _marketParams(id);
+             (uint256 supplyAssets,, Market memory market) = _accruedSupplyBalance(marketParams, id);
diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index 8d650bcb..6659f6c4 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -5,6 +5,8 @@ methods {
     function _.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summarySupply(marketParams, assets, shares, onBehalf, data) expect (uint256, uint256) ALL;
     function _.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver) expect (uint256, uint256) ALL;
     function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
+
+    function lastIndexWithdraw() external returns(uint256) envfree;
 }
 
 function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
@@ -39,9 +41,9 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     assert receiver == currentContract;
 
     MetaMorphoHarness.Id id = Util.libId(marketParams);
-    uint256 rank = withdrawRank(id);
+    uint256 index = lastIndexWithdraw();
     // Safe require because it is a verified invariant.
-    require isInWithdrawQueueIsEnabled(assert_uint256(rank - 1));
+    require isInWithdrawQueueIsEnabled(index);
     // Safe require because it is a verified invariant
     require isWithdrawRankCorrect(id);
 

From deda832a19727cbb0f18d422774ff965dbca46d2 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 14:27:48 +0100
Subject: [PATCH 13/15] fix: public lastIndexWithdraw

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

diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
index 095d407a..31937cc4 100644
--- a/certora/applyMunging.patch
+++ b/certora/applyMunging.patch
@@ -49,7 +49,7 @@ diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
  
 diff -ruN MetaMorpho.sol MetaMorpho.sol
 --- MetaMorpho.sol	2024-03-20 15:13:25.862250553 +0100
-+++ MetaMorpho.sol	2024-03-22 11:25:47.991055286 +0100
++++ MetaMorpho.sol	2024-03-22 14:27:33.670423544 +0100
 @@ -9,24 +9,22 @@
      IMetaMorphoBase,
      IMetaMorphoStaticTyping
@@ -120,7 +120,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
  
 +    // HARNESS
 +    // The index of the identifier of the last market withdrawn.
-+    uint256 lastIndexWithdraw;
++    uint256 public lastIndexWithdraw;
 +
 +    // HARNESS
 +    // The rank of a market identifier in the withdraw queue.

From 4f186ca93fe8df28110d64e46df3c9b5b898f1a5 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Mar 2024 14:30:40 +0100
Subject: [PATCH 14/15] docs: document checkSummaries

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

diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index 6659f6c4..d357a7a2 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -54,5 +54,7 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     return (_, _);
 }
 
+// Check assertions in the summaries.
+// This requires to turn off sanity checks for this invariant that appears vacuous.
 invariant checkSummaries()
     true;

From 6c6a2d5e34864dcd6a8ed226136df68bd7d0c261 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Mon, 25 Mar 2024 09:39:55 +0100
Subject: [PATCH 15/15] feat: assets and shares conditions

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

diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
index d357a7a2..cbfc6d09 100644
--- a/certora/specs/MarketInteractions.spec
+++ b/certora/specs/MarketInteractions.spec
@@ -22,6 +22,7 @@ function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarn
 
 function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) {
     assert shares == 0;
+    assert assets != 0;
     assert onBehalf == currentContract;
     assert data.length == 0;
 
@@ -37,6 +38,7 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse
 }
 
 function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) {
+    assert shares == 0 <=> assets != 0;
     assert onBehalf == currentContract;
     assert receiver == currentContract;
 
@@ -44,8 +46,6 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     uint256 index = lastIndexWithdraw();
     // Safe require because it is a verified invariant.
     require isInWithdrawQueueIsEnabled(index);
-    // Safe require because it is a verified invariant
-    require isWithdrawRankCorrect(id);
 
     // Check that all markets from which MetaMorpho withdraws are enabled markets.
     assert config_(id).enabled;