fix: address more PR reviews

certora/README.md

@@ -1,4 +1,4 @@
-# Bundlers Formal Verification
+# Bundlers formal verification
 
 This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the following bundler contracts:
 

certora/specs/Protected.spec

@@ -1,19 +1,19 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-methods {
-    function initiator() external returns(address) envfree;
-    function MORPHO() external returns(address) envfree;
-}
-
 
 // Check that all methods except those noted below comply with the `protected` modifier when an initiator has been set.
 rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered {
     // Do not check view functions.
+    f -> !f.isView &&
     // Do not check the fallback function.
+    !f.isFallback &&
     // Do not check multicall, which is used to start a new bundle.
-    f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector
+    f.selector != sig:multicall(bytes[]).selector
 }
 {
+    // Safe require because `protected` functions should be callable by the initiator.
+    require e.msg.sender != currentContract._initiator;
+    // Safe require because `protected` functions should be callable by Morpho.
+    require e.msg.sender != currentContract.MORPHO;
     f@withrevert(e,data);
-    bool reverted = lastReverted;
-    assert e.msg.sender != initiator() && e.msg.sender != MORPHO() => reverted;
+    assert lastReverted;
 }