test: certora config

certora/config/registryCoordinator.conf

@@ -0,0 +1,40 @@
+{
+    "files": [
+        "certora/harnesses/RegistryCoordinatorHarness.sol",
+        "lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol",
+        "test/mocks/ServiceManagerMock.sol",
+        "src/StakeRegistry.sol",
+        "src/BLSApkRegistry.sol",
+        "src/IndexRegistry.sol",
+        "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol",
+        "lib/eigenlayer-contracts/src/contracts/core/AVSDirectory.sol",
+        "lib/eigenlayer-contracts/src/contracts/core/DelegationManager.sol"
+    ],
+    "verify": "RegistryCoordinatorHarness:certora/specs/RegistryCoordinator.spec",
+    "loop_iter": "2",
+    "parametric_contracts": ["RegistryCoordinatorHarness"],
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts",
+        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable",
+        "eigenlayer-contracts=lib/eigenlayer-contracts"
+    ],
+    "link": [
+        "RegistryCoordinatorHarness:serviceManager=ServiceManagerMock",
+        "AVSDirectory:delegation=DelegationManager",
+        "StakeRegistry:delegation=DelegationManager",
+        "ServiceManagerMock:_avsDirectory=AVSDirectory",
+        "RegistryCoordinatorHarness:blsApkRegistry=BLSApkRegistry",
+        "RegistryCoordinatorHarness:indexRegistry=IndexRegistry",
+        "RegistryCoordinatorHarness:stakeRegistry=StakeRegistry"
+    ],
+    "prover_args": [
+        "-optimisticFallback true",
+        "-recursionEntryLimit 2",
+        // "-splitParallel true",
+        "-mediumTimeout 30",
+        "-depth 5"
+    ],
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "rule_sanity": "basic"
+}

certora/specs/RegistryCoordinator.spec

@@ -59,6 +59,7 @@ methods {
     function registries(uint256) external returns (address) envfree;
     function numRegistries() external returns (uint256) envfree;
     function calculateOperatorChurnApprovalDigestHash(
+        address registeringOperator,
         bytes32 registeringOperatorId,
         IRegistryCoordinator.OperatorKickParam[] operatorKickParams,
         bytes32 salt,

certora/specs/setup.spec

@@ -0,0 +1,16 @@
+using ServiceManagerMock as serviceManager;
+using StakeRegistry as stakeRegistry;
+using BLSApkRegistry as blsApkRegistry;
+using IndexRegistry as indexRegistry;
+using DelegationManager as delegation;
+methods {
+    function _.isValidSignature(bytes32 hash, bytes signature) external => NONDET; // isValidSignatureCVL(hash,signature) expect bytes4;
+    function _.unpauser() external => unpauser expect address;
+    function _.isPauser(address user) external => isPauserCVL(user) expect bool;
+}
+ghost address unpauser;
+ghost mapping(address => bool) pausers;
+function isPauserCVL(address user) returns bool {
+    return pausers[user];
+}
+use builtin rule sanity;