fix: remove unset_initiator require

morpho-org · Oct 29, 2024 · e997f43 · e997f43
1 parent 8603571
commit e997f43
Show file tree

Hide file tree

Showing 9 changed files with 7 additions and 26 deletions.
diff --git a/certora/confs/AaveV2MigrationBundlerV2.conf b/certora/confs/AaveV2MigrationBundlerV2.conf
@@ -1,7 +1,6 @@
 {
   "files": [
-    "src/migration/AaveV2MigrationBundlerV2.sol",
-    "certora/harness/Constants.sol"
+    "src/migration/AaveV2MigrationBundlerV2.sol"
   ],
   "verify": "AaveV2MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",

diff --git a/certora/confs/AaveV3MigrationBundlerV2.conf b/certora/confs/AaveV3MigrationBundlerV2.conf
@@ -1,7 +1,6 @@
 {
   "files": [
-    "src/migration/AaveV3MigrationBundlerV2.sol",
-    "certora/harness/Constants.sol"
+    "src/migration/AaveV3MigrationBundlerV2.sol"
   ],
   "verify": "AaveV3MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",

diff --git a/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf
@@ -1,7 +1,6 @@
 {
   "files": [
-    "src/migration/AaveV3OptimizerMigrationBundlerV2.sol",
-    "certora/harness/Constants.sol"
+    "src/migration/AaveV3OptimizerMigrationBundlerV2.sol"
   ],
   "verify": "AaveV3OptimizerMigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",

diff --git a/certora/confs/ChainAgnosticBundlerV2.conf b/certora/confs/ChainAgnosticBundlerV2.conf
@@ -1,7 +1,6 @@
 {
   "files": [
-    "src/chain-agnostic/ChainAgnosticBundlerV2.sol",
-    "certora/harness/Constants.sol"
+    "src/chain-agnostic/ChainAgnosticBundlerV2.sol"
   ],
   "verify": "ChainAgnosticBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",

diff --git a/certora/confs/CompoundV2MigrationBundlerV2.conf b/certora/confs/CompoundV2MigrationBundlerV2.conf
@@ -1,7 +1,6 @@
 {
   "files": [
-    "src/migration/CompoundV2MigrationBundlerV2.sol",
-    "certora/harness/Constants.sol"
+    "src/migration/CompoundV2MigrationBundlerV2.sol"
   ],
   "verify": "CompoundV2MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",

diff --git a/certora/confs/CompoundV3MigrationBundlerV2.conf b/certora/confs/CompoundV3MigrationBundlerV2.conf
@@ -1,7 +1,6 @@
 {
   "files": [
-    "src/migration/CompoundV3MigrationBundlerV2.sol",
-    "certora/harness/Constants.sol"
+    "src/migration/CompoundV3MigrationBundlerV2.sol"
   ],
   "verify": "CompoundV3MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",

diff --git a/certora/confs/EthereumBundlerV2.conf b/certora/confs/EthereumBundlerV2.conf
@@ -1,7 +1,6 @@
 {
   "files": [
-    "src/ethereum/EthereumBundlerV2.sol",
-    "certora/harness/Constants.sol"
+    "src/ethereum/EthereumBundlerV2.sol"
   ],
   "verify": "EthereumBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",

diff --git a/certora/harness/Constants.sol b/certora/harness/Constants.sol
diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec
@@ -1,10 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-using Constants as constants;
-
 methods {
     function initiator() external returns(address) envfree;
     function MORPHO() external returns(address) envfree;
-    function constants.UNSET_INITIATOR() external returns(address) envfree;
 }
 
 
@@ -16,7 +13,6 @@ rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered {
     f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector
 }
 {
-    require e.msg.sender != constants.UNSET_INITIATOR();
     require e.msg.sender != initiator();
     require e.msg.sender != MORPHO();
     f@withrevert(e,data);