From e997f43d0787f6ce0e1a35a302666284375419fe Mon Sep 17 00:00:00 2001
From: Adrien Husson <adhusson@gmail.com>
Date: Tue, 29 Oct 2024 23:02:45 +0100
Subject: [PATCH] fix: remove unset_initiator require

---
 certora/confs/AaveV2MigrationBundlerV2.conf          | 3 +--
 certora/confs/AaveV3MigrationBundlerV2.conf          | 3 +--
 certora/confs/AaveV3OptimizerMigrationBundlerV2.conf | 3 +--
 certora/confs/ChainAgnosticBundlerV2.conf            | 3 +--
 certora/confs/CompoundV2MigrationBundlerV2.conf      | 3 +--
 certora/confs/CompoundV3MigrationBundlerV2.conf      | 3 +--
 certora/confs/EthereumBundlerV2.conf                 | 3 +--
 certora/harness/Constants.sol                        | 8 --------
 certora/specs/Protected.spec                         | 4 ----
 9 files changed, 7 insertions(+), 26 deletions(-)
 delete mode 100644 certora/harness/Constants.sol

diff --git a/certora/confs/AaveV2MigrationBundlerV2.conf b/certora/confs/AaveV2MigrationBundlerV2.conf
index bf9c9c0a..3661f225 100644
--- 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
index 7dc2f5b5..02346908 100644
--- 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
index f2a0ccb2..783266a1 100644
--- 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
index 082951a7..5a6ba6b3 100644
--- 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
index 51b0a45f..58b938a5 100644
--- 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
index 06a390fb..5a379797 100644
--- 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
index 4e3e2369..2d144f99 100644
--- 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
deleted file mode 100644
index a524aefe..00000000
--- a/certora/harness/Constants.sol
+++ /dev/null
@@ -1,8 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.24;
-
-import "../../src/libraries/ConstantsLib.sol" as ConstantsLib;
-
-contract Constants {
-    address public constant UNSET_INITIATOR = ConstantsLib.UNSET_INITIATOR;
-}
diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec
index 9d266df7..3a6237a5 100644
--- 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);