Fix invariant (Thanks Nurit)

certora/specs/CER-2-Operator/CER-68-Operator-authorization.spec

@@ -49,15 +49,28 @@ rule onlyOwnerCanCallSetOperator() {
     assert(getOperator(addressPrefix, operator) == operatorBitField);
 }
 
+
+// a copy of the internal ownerLookup
+persistent ghost mapping(bytes19 => address) ownerLookupGhost {
+    init_state axiom forall bytes19 prefix. ownerLookupGhost[prefix] == 0;
+}
+// makes sure the ownerLookupGhost is updated properly
+hook Sstore EthereumVaultConnectorHarness.ownerLookup[KEY bytes19 prefix] address value STORAGE {
+    ownerLookupGhost[prefix] = value;
+}
+// makes sure that reads from ownerLookup after havocs are correct
+hook Sload address value EthereumVaultConnectorHarness.ownerLookup[KEY bytes19 prefix] STORAGE {
+    require(ownerLookupGhost[prefix] == value);
+}
+
 // check that an owner of a prefix is always from that prefix
 invariant OwnerIsFromPrefix(bytes19 prefix)
-    getOwnerOf(prefix) == 0 || getAddressPrefix(getOwnerOf(prefix)) == prefix
+    // Assume: In the inductive step, for the precondition,
+    // we are assuming that the low-level `CALL`s that are
+    // reachable in batch/call will not affect the state of ownerLookup
+    ownerLookupGhost[prefix] == 0 || getAddressPrefix(ownerLookupGhost[prefix]) == prefix
     filtered { 
-        f -> !isMustRevertFunction(f) &&
-        // We can't handle these functions since they have `CALL`s in them
-        f.selector != sig:batch(IEVC.BatchItem[] calldata).selector
-        && 
-        f.selector != sig:call(address, address, uint256, bytes calldata).selector
+        f -> !isMustRevertFunction(f)
     }
 
 /**