refactor: unlink Morpho and summary supply shares

morpho-org · Mar 21, 2024 · 4f49dfa · 4f49dfa
1 parent 79e6c71
commit 4f49dfa
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 11 deletions.
diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
@@ -3,9 +3,6 @@
         "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "parametric_contracts": [
-        "MetaMorphoHarness",
-    ],
     "solc_map": {
         "MorphoHarness": "solc8.19",
         "MetaMorphoHarness": "solc",

diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf
@@ -3,9 +3,6 @@
         "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "parametric_contracts": [
-        "MetaMorphoHarness",
-    ],
     "solc_map": {
         "MorphoHarness": "solc8.19",
         "MetaMorphoHarness": "solc",

diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf
@@ -6,9 +6,6 @@
     "parametric_contracts": [
         "MetaMorphoHarness",
     ],
-    "link": [
-        "MetaMorphoHarness:MORPHO=MorphoHarness",
-    ],
     "solc_map": {
         "MorphoHarness": "solc8.19",
         "MetaMorphoHarness": "solc",

diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec
@@ -6,7 +6,6 @@ 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 Morpho.supplyShares(MorphoHarness.Id, address) external returns(uint256) envfree;
 }
 
 // Check that any market with positive cap is created on Morpho Blue.

diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec
@@ -1,6 +1,18 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 import "LastUpdated.spec";
 
+methods {
+    function _.supplyShares(MetaMorphoHarness.Id id, address user) external => summarySupplyshares(id, user) expect uint256;
+}
+
+ghost lastSupplyShares(MetaMorphoHarness.Id, address) returns uint256;
+
+function summarySupplyshares(MetaMorphoHarness.Id id, address user) returns uint256 {
+    uint256 res;
+    require lastSupplyShares(id, user) == res;
+    return res;
+}
+
 // Show that nextGuardianUpdateTime does not revert.
 rule nextGuardianUpdateTimeDoesNotRevert() {
     // The environment ec yields the current time.
@@ -189,7 +201,7 @@ rule removableTime(env e, method f, calldataarg args) {
 
     if (e.block.timestamp < nextTime)  {
         // Check that no forced removal happened.
-        assert Morpho.supplyShares(id, currentContract) > 0 => config_(id).enabled;
+        assert lastSupplyShares(id, currentContract) > 0 => config_(id).enabled;
         // Increasing nextRemovableTime with an interaction;
         assert nextRemovableTime(e, id) >= nextTime;
     }