From 16fef83757c245e9aeb0873f7fc486b2a933fd33 Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Wed, 18 Oct 2023 12:37:15 -0700 Subject: [PATCH] migrate Prover functionality from core repo had to modify some paths / folder structure / etc --- .../certora_debug_log.txt | 0 .../resource_errors.json | 3 + .../certora_debug_log.txt | 0 .../resource_errors.json | 3 + .../certora_debug_log.txt | 0 .../resource_errors.json | 3 + .../certora_debug_log.txt | 0 .../resource_errors.json | 3 + .../certora_debug_log.txt | 0 .../resource_errors.json | 3 + .../certora_debug_log.txt | 0 .../resource_errors.json | 3 + .../.certora_metadata.json | 54 ++++++ ...LSRegistryCoordinatorWithIndices.spec.spec | 169 ++++++++++++++++++ .../.certora_verify.cvl1.json | 10 ++ .../.certora_verify.json | 8 + .../certora_debug_log.txt | 36 ++++ .../resource_errors.json | 3 + .../23_10_18_12_26_27_032/run.conf | 23 +++ .../.certora_metadata.json | 54 ++++++ ...LSRegistryCoordinatorWithIndices.spec.spec | 169 ++++++++++++++++++ .../.certora_verify.cvl1.json | 10 ++ .../.certora_verify.json | 8 + .../certora_debug_log.txt | 36 ++++ .../resource_errors.json | 3 + .../23_10_18_12_29_48_001/run.conf | 23 +++ .certora_internal/latest | 1 + .github/workflows/certora-prover.yml | 64 +++++++ .gitignore | 2 + certora/.gitignore | 1 + certora/Makefile | 25 +++ certora/applyHarness.patch | 0 ...SRegistryCoordinatorWithIndicesHarness.sol | 54 ++++++ ...verifyBLSRegistryCoordinatorWithIndices.sh | 21 +++ .../BLSRegistryCoordinatorWithIndices.spec | 169 ++++++++++++++++++ 35 files changed, 961 insertions(+) create mode 100644 .certora_internal/23_10_18_12_21_12_640/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_21_12_640/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_23_12_641/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_23_12_641/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_24_19_683/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_24_19_683/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_25_21_966/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_25_21_966/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_25_45_316/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_25_45_316/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_26_04_818/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_26_04_818/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_metadata.json create mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec create mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json create mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_verify.json create mode 100644 .certora_internal/23_10_18_12_26_27_032/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_26_27_032/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_26_27_032/run.conf create mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_metadata.json create mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec create mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_verify.cvl1.json create mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_verify.json create mode 100644 .certora_internal/23_10_18_12_29_48_001/certora_debug_log.txt create mode 100644 .certora_internal/23_10_18_12_29_48_001/resource_errors.json create mode 100644 .certora_internal/23_10_18_12_29_48_001/run.conf create mode 120000 .certora_internal/latest create mode 100644 .github/workflows/certora-prover.yml create mode 100644 certora/.gitignore create mode 100644 certora/Makefile create mode 100644 certora/applyHarness.patch create mode 100644 certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol create mode 100644 certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh create mode 100644 certora/specs/BLSRegistryCoordinatorWithIndices.spec diff --git a/.certora_internal/23_10_18_12_21_12_640/certora_debug_log.txt b/.certora_internal/23_10_18_12_21_12_640/certora_debug_log.txt new file mode 100644 index 00000000..e69de29b diff --git a/.certora_internal/23_10_18_12_21_12_640/resource_errors.json b/.certora_internal/23_10_18_12_21_12_640/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_21_12_640/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_23_12_641/certora_debug_log.txt b/.certora_internal/23_10_18_12_23_12_641/certora_debug_log.txt new file mode 100644 index 00000000..e69de29b diff --git a/.certora_internal/23_10_18_12_23_12_641/resource_errors.json b/.certora_internal/23_10_18_12_23_12_641/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_23_12_641/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_24_19_683/certora_debug_log.txt b/.certora_internal/23_10_18_12_24_19_683/certora_debug_log.txt new file mode 100644 index 00000000..e69de29b diff --git a/.certora_internal/23_10_18_12_24_19_683/resource_errors.json b/.certora_internal/23_10_18_12_24_19_683/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_24_19_683/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_25_21_966/certora_debug_log.txt b/.certora_internal/23_10_18_12_25_21_966/certora_debug_log.txt new file mode 100644 index 00000000..e69de29b diff --git a/.certora_internal/23_10_18_12_25_21_966/resource_errors.json b/.certora_internal/23_10_18_12_25_21_966/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_25_21_966/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_25_45_316/certora_debug_log.txt b/.certora_internal/23_10_18_12_25_45_316/certora_debug_log.txt new file mode 100644 index 00000000..e69de29b diff --git a/.certora_internal/23_10_18_12_25_45_316/resource_errors.json b/.certora_internal/23_10_18_12_25_45_316/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_25_45_316/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_26_04_818/certora_debug_log.txt b/.certora_internal/23_10_18_12_26_04_818/certora_debug_log.txt new file mode 100644 index 00000000..e69de29b diff --git a/.certora_internal/23_10_18_12_26_04_818/resource_errors.json b/.certora_internal/23_10_18_12_26_04_818/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_26_04_818/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_26_27_032/.certora_metadata.json b/.certora_internal/23_10_18_12_26_27_032/.certora_metadata.json new file mode 100644 index 00000000..a2848b4c --- /dev/null +++ b/.certora_internal/23_10_18_12_26_27_032/.certora_metadata.json @@ -0,0 +1,54 @@ +{ + "CLI_version": "4.13.1", + "branch": "add-certora-rules", + "conf": { + "files": [ + "certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol", + "lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol", + "certora/munged/StakeRegistry.sol", + "certora/munged/BLSPubkeyRegistry.sol", + "certora/munged/IndexRegistry.sol", + "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol" + ], + "loop_iter": "2", + "msg": "BLSRegistryCoordinatorWithIndices ", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable", + "@openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts" + ], + "process": "emv", + "prover_args": [ + " -optimisticFallback true -recursionEntryLimit 2 " + ], + "verify": "BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec" + }, + "cwd_relative": ".", + "dirty": true, + "origin": "https://github.com/Layr-Labs/eigenlayer-middleware.git", + "raw_args": [ + "/Library/Frameworks/Python.framework/Versions/3.11/bin/certoraRun", + "certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol", + "lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol", + "certora/munged/StakeRegistry.sol", + "certora/munged/BLSPubkeyRegistry.sol", + "certora/munged/IndexRegistry.sol", + "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol", + "--verify", + "BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "--optimistic_loop", + "--optimistic_hashing", + "--prover_args", + "-optimisticFallback true -recursionEntryLimit 2 ", + "--loop_iter", + "2", + "--packages", + "@openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts", + "@openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable", + "--msg", + "BLSRegistryCoordinatorWithIndices " + ], + "revision": "5b1b7296bde76b86ad40378db416bd2719f65a53", + "timestamp": "1697682387.833124" +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec b/.certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec new file mode 100644 index 00000000..2ca61c0c --- /dev/null +++ b/.certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec @@ -0,0 +1,169 @@ + +methods { + //// External Calls + // external calls to StakeRegistry + function _.quorumCount() external => DISPATCHER(true); + function _.getCurrentTotalStakeForQuorum(uint8 quorumNumber) external => DISPATCHER(true); + function _.getCurrentOperatorStakeForQuorum(bytes32 operatorId, uint8 quorumNumber) external => DISPATCHER(true); + function _.registerOperator(address, bytes32, bytes) external => DISPATCHER(true); + function _.deregisterOperator(bytes32, bytes) external => DISPATCHER(true); + + // external calls to Slasher + function _.contractCanSlashOperatorUntilBlock(address, address) external => DISPATCHER(true); + + // external calls to BLSPubkeyRegistry + function _.registerOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); + function _.deregisterOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); + + // external calls to ServiceManager + function _.latestServeUntilBlock() external => DISPATCHER(true); + function _.recordLastStakeUpdateAndRevokeSlashingAbility(address, uint256) external => DISPATCHER(true); + + // external calls to IndexRegistry + function _.registerOperator(bytes32, bytes) external => DISPATCHER(true); + function _.deregisterOperator(bytes32, bytes, bytes32[]) external => DISPATCHER(true); + + // external calls to ERC1271 (can import OpenZeppelin mock implementation) + // isValidSignature(bytes32 hash, bytes memory signature) returns (bytes4 magicValue) => DISPATCHER(true) + function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true); + + // external calls to BLSPubkeyCompendium + function _.pubkeyHashToOperator(bytes32) external => DISPATCHER(true); + + //envfree functions + function OPERATOR_CHURN_APPROVAL_TYPEHASH() external returns (bytes32) envfree; + function slasher() external returns (address) envfree; + function serviceManager() external returns (address) envfree; + function blsPubkeyRegistry() external returns (address) envfree; + function stakeRegistry() external returns (address) envfree; + function indexRegistry() external returns (address) envfree; + function registries(uint256) external returns (address) envfree; + function churnApprover() external returns (address) envfree; + function isChurnApproverSaltUsed(bytes32) external returns (bool) envfree; + function getOperatorSetParams(uint8 quorumNumber) external returns (IBLSRegistryCoordinatorWithIndices.OperatorSetParam) envfree; + function getOperator(address operator) external returns (IRegistryCoordinator.Operator) envfree; + function getOperatorId(address operator) external returns (bytes32) envfree; + function getOperatorStatus(address operator) external returns (IRegistryCoordinator.OperatorStatus) envfree; + function getQuorumBitmapIndicesByOperatorIdsAtBlockNumber(uint32 blockNumber, bytes32[] operatorIds) + external returns (uint32[]) envfree; + function getQuorumBitmapByOperatorIdAtBlockNumberByIndex(bytes32 operatorId, uint32 blockNumber, uint256 index) external returns (uint192) envfree; + function getQuorumBitmapUpdateByOperatorIdByIndex(bytes32 operatorId, uint256 index) + external returns (IRegistryCoordinator.QuorumBitmapUpdate) envfree; + function getCurrentQuorumBitmapByOperatorId(bytes32 operatorId) external returns (uint192) envfree; + function getQuorumBitmapUpdateByOperatorIdLength(bytes32 operatorId) external returns (uint256) envfree; + function numRegistries() external returns (uint256) envfree; + function calculateOperatorChurnApprovalDigestHash( + bytes32 registeringOperatorId, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[] operatorKickParams, + bytes32 salt, + uint256 expiry + ) external returns (bytes32) envfree; + + // harnessed functions + function bytesArrayContainsDuplicates(bytes bytesArray) external returns (bool) envfree; + function bytesArrayIsSubsetOfBitmap(uint256 referenceBitmap, bytes arrayWhichShouldBeASubsetOfTheReference) external returns (bool) envfree; +} + +// If my Operator status is REGISTERED ⇔ my quorum bitmap MUST BE nonzero +invariant registeredOperatorsHaveNonzeroBitmaps(address operator) + getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED <=> + getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)) != 0; + +// if two operators have different addresses, then they have different IDs +// excludes the case in which the operator is not registered, since then they can both have ID zero (the default) +invariant operatorIdIsUnique(address operator1, address operator2) + operator1 != operator2 => + (getOperatorStatus(operator1) == IRegistryCoordinator.OperatorStatus.REGISTERED => getOperatorId(operator1) != getOperatorId(operator2)); + +definition methodCanModifyBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector + || f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector; + +definition methodCanAddToBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector + || f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector; + +// `registerOperatorWithCoordinator` with kick params also meets this definition due to the 'churn' mechanism +definition methodCanRemoveFromBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector; + +// verify that quorumNumbers provided as an input to deregister operator MUST BE a subset of the operator’s current quorums +rule canOnlyDeregisterFromExistingQuorums(address operator) { + requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator); + + // TODO: store this status, verify that all calls to `deregisterOperatorWithCoordinator` *fail* if the operator is not registered first! + require(getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED); + + uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + + bytes quorumNumbers; + BN254.G1Point pubkey; + bytes32[] operatorIdsToSwap; + env e; + + deregisterOperatorWithCoordinator(e, quorumNumbers, pubkey, operatorIdsToSwap); + + // if deregistration is successful, verify that `quorumNumbers` input was proper + if (getOperatorStatus(operator) != IRegistryCoordinator.OperatorStatus.REGISTERED) { + assert(bytesArrayIsSubsetOfBitmap(bitmapBefore, quorumNumbers)); + } else { + assert(true); + } +} + +/* TODO: this is a Work In Progress +rule canOnlyModifyBitmapWithSpecificFunctions(address operator) { + requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator); + uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + // prepare to perform arbitrary function call + method f; + env e; + // TODO: need to ensure that if the function can modify the bitmap, then we are using the operator as an input + if (!methodCanModifyBitmap(f)) { + // perform arbitrary function call + calldataarg arg; + f(e, arg); + uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + assert(bitmapAfter == bitmapBefore); + } else if ( + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + ) { + if (e.msg.sender != operator) { + uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + assert(bitmapAfter == bitmapBefore); + } + } + + // if method did not remove from bitmap, it must have added + if (bitmapAfter & bitmapBefore == bitmapBefore) { + assert(methodCanAddToBitmap(f)); + } else { + assert(methodCanRemoveFromBitmap(f)); + } + } +} +*/ \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json b/.certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json new file mode 100644 index 00000000..0a3774e7 --- /dev/null +++ b/.certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json @@ -0,0 +1,10 @@ +[ + { + "importFilesToOrigRelpaths": {}, + "primary_contract": "BLSRegistryCoordinatorWithIndicesHarness", + "specfile": ".certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec", + "specfileOrigRelpath": "certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "specfilesToImportDecls": {}, + "type": "spec" + } +] \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_26_27_032/.certora_verify.json b/.certora_internal/23_10_18_12_26_27_032/.certora_verify.json new file mode 100644 index 00000000..1c5ff4ef --- /dev/null +++ b/.certora_internal/23_10_18_12_26_27_032/.certora_verify.json @@ -0,0 +1,8 @@ +{ + "importFilesToOrigRelpaths": {}, + "primary_contract": "BLSRegistryCoordinatorWithIndicesHarness", + "specfile": "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "specfileOrigRelpath": "certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "specfilesToImportDecls": {}, + "type": "spec" +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_26_27_032/certora_debug_log.txt b/.certora_internal/23_10_18_12_26_27_032/certora_debug_log.txt new file mode 100644 index 00000000..8d41e8d9 --- /dev/null +++ b/.certora_internal/23_10_18_12_26_27_032/certora_debug_log.txt @@ -0,0 +1,36 @@ +Saving last configuration file to .certora_internal/23_10_18_12_26_27_032/run.conf +There is no TAC file. Going to script EVMVerifier/certoraBuild.py to main_with_args() +Creating dir /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_config +In /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec, found the imports: [] +copying spec file /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec to /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec +In /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec, found the imports: [] +writing /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_verify.json +writing /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json +Path to typechecker is /Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/certora_jars/Typechecker.jar +running ['java', '-jar', '/Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/certora_jars/Typechecker.jar', '-buildDirectory', '/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032'] + +building file certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol +Running cmd /Library/Frameworks/Python.framework/Versions/3.11/bin/solc -o "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0/" --overwrite --allow-paths "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync","lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable","lib/eigenlayer-contracts/lib/openzeppelin-contracts",. --standard-json +stdout, stderr = /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0.standard.json.stdout, /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0.standard.json.stderr +Exitcode 0 +Solc run /Library/Frameworks/Python.framework/Versions/3.11/bin/solc -o "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0/" --overwrite --allow-paths "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync","lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable","lib/eigenlayer-contracts/lib/openzeppelin-contracts",. --standard-json time: 0.1566 +reading standard json data from /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_26_27_032/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0.standard.json.stdout +build failed +Failure traceback: +Shared.certoraUtils.CertoraUserInputError: /Library/Frameworks/Python.framework/Versions/3.11/bin/solc had an error: +ParserError: Source "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/munged/middleware/BLSRegistryCoordinatorWithIndices.sol" not found: File not found. Searched the following locations: "". + --> /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol:4:1: + | +4 | import "../munged/middleware/BLSRegistryCoordinatorWithIndices.sol"; + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Encountered an error running Certora Prover: +/Library/Frameworks/Python.framework/Versions/3.11/bin/solc had an error: +ParserError: Source "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/munged/middleware/BLSRegistryCoordinatorWithIndices.sol" not found: File not found. Searched the following locations: "". + --> /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol:4:1: + | +4 | import "../munged/middleware/BLSRegistryCoordinatorWithIndices.sol"; + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + diff --git a/.certora_internal/23_10_18_12_26_27_032/resource_errors.json b/.certora_internal/23_10_18_12_26_27_032/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_26_27_032/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_26_27_032/run.conf b/.certora_internal/23_10_18_12_26_27_032/run.conf new file mode 100644 index 00000000..52def0f3 --- /dev/null +++ b/.certora_internal/23_10_18_12_26_27_032/run.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol", + "lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol", + "certora/munged/StakeRegistry.sol", + "certora/munged/BLSPubkeyRegistry.sol", + "certora/munged/IndexRegistry.sol", + "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol" + ], + "loop_iter": "2", + "msg": "BLSRegistryCoordinatorWithIndices ", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable", + "@openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts" + ], + "process": "emv", + "prover_args": [ + " -optimisticFallback true -recursionEntryLimit 2 " + ], + "verify": "BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec" +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_29_48_001/.certora_metadata.json b/.certora_internal/23_10_18_12_29_48_001/.certora_metadata.json new file mode 100644 index 00000000..15f9ee79 --- /dev/null +++ b/.certora_internal/23_10_18_12_29_48_001/.certora_metadata.json @@ -0,0 +1,54 @@ +{ + "CLI_version": "4.13.1", + "branch": "add-certora-rules", + "conf": { + "files": [ + "certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol", + "lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol", + "certora/munged/StakeRegistry.sol", + "certora/munged/BLSPubkeyRegistry.sol", + "certora/munged/IndexRegistry.sol", + "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol" + ], + "loop_iter": "2", + "msg": "BLSRegistryCoordinatorWithIndices ", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable", + "@openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts" + ], + "process": "emv", + "prover_args": [ + " -optimisticFallback true -recursionEntryLimit 2 " + ], + "verify": "BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec" + }, + "cwd_relative": ".", + "dirty": true, + "origin": "https://github.com/Layr-Labs/eigenlayer-middleware.git", + "raw_args": [ + "/Library/Frameworks/Python.framework/Versions/3.11/bin/certoraRun", + "certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol", + "lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol", + "certora/munged/StakeRegistry.sol", + "certora/munged/BLSPubkeyRegistry.sol", + "certora/munged/IndexRegistry.sol", + "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol", + "--verify", + "BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "--optimistic_loop", + "--optimistic_hashing", + "--prover_args", + "-optimisticFallback true -recursionEntryLimit 2 ", + "--loop_iter", + "2", + "--packages", + "@openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts", + "@openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable", + "--msg", + "BLSRegistryCoordinatorWithIndices " + ], + "revision": "5b1b7296bde76b86ad40378db416bd2719f65a53", + "timestamp": "1697682588.610295" +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec b/.certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec new file mode 100644 index 00000000..2ca61c0c --- /dev/null +++ b/.certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec @@ -0,0 +1,169 @@ + +methods { + //// External Calls + // external calls to StakeRegistry + function _.quorumCount() external => DISPATCHER(true); + function _.getCurrentTotalStakeForQuorum(uint8 quorumNumber) external => DISPATCHER(true); + function _.getCurrentOperatorStakeForQuorum(bytes32 operatorId, uint8 quorumNumber) external => DISPATCHER(true); + function _.registerOperator(address, bytes32, bytes) external => DISPATCHER(true); + function _.deregisterOperator(bytes32, bytes) external => DISPATCHER(true); + + // external calls to Slasher + function _.contractCanSlashOperatorUntilBlock(address, address) external => DISPATCHER(true); + + // external calls to BLSPubkeyRegistry + function _.registerOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); + function _.deregisterOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); + + // external calls to ServiceManager + function _.latestServeUntilBlock() external => DISPATCHER(true); + function _.recordLastStakeUpdateAndRevokeSlashingAbility(address, uint256) external => DISPATCHER(true); + + // external calls to IndexRegistry + function _.registerOperator(bytes32, bytes) external => DISPATCHER(true); + function _.deregisterOperator(bytes32, bytes, bytes32[]) external => DISPATCHER(true); + + // external calls to ERC1271 (can import OpenZeppelin mock implementation) + // isValidSignature(bytes32 hash, bytes memory signature) returns (bytes4 magicValue) => DISPATCHER(true) + function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true); + + // external calls to BLSPubkeyCompendium + function _.pubkeyHashToOperator(bytes32) external => DISPATCHER(true); + + //envfree functions + function OPERATOR_CHURN_APPROVAL_TYPEHASH() external returns (bytes32) envfree; + function slasher() external returns (address) envfree; + function serviceManager() external returns (address) envfree; + function blsPubkeyRegistry() external returns (address) envfree; + function stakeRegistry() external returns (address) envfree; + function indexRegistry() external returns (address) envfree; + function registries(uint256) external returns (address) envfree; + function churnApprover() external returns (address) envfree; + function isChurnApproverSaltUsed(bytes32) external returns (bool) envfree; + function getOperatorSetParams(uint8 quorumNumber) external returns (IBLSRegistryCoordinatorWithIndices.OperatorSetParam) envfree; + function getOperator(address operator) external returns (IRegistryCoordinator.Operator) envfree; + function getOperatorId(address operator) external returns (bytes32) envfree; + function getOperatorStatus(address operator) external returns (IRegistryCoordinator.OperatorStatus) envfree; + function getQuorumBitmapIndicesByOperatorIdsAtBlockNumber(uint32 blockNumber, bytes32[] operatorIds) + external returns (uint32[]) envfree; + function getQuorumBitmapByOperatorIdAtBlockNumberByIndex(bytes32 operatorId, uint32 blockNumber, uint256 index) external returns (uint192) envfree; + function getQuorumBitmapUpdateByOperatorIdByIndex(bytes32 operatorId, uint256 index) + external returns (IRegistryCoordinator.QuorumBitmapUpdate) envfree; + function getCurrentQuorumBitmapByOperatorId(bytes32 operatorId) external returns (uint192) envfree; + function getQuorumBitmapUpdateByOperatorIdLength(bytes32 operatorId) external returns (uint256) envfree; + function numRegistries() external returns (uint256) envfree; + function calculateOperatorChurnApprovalDigestHash( + bytes32 registeringOperatorId, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[] operatorKickParams, + bytes32 salt, + uint256 expiry + ) external returns (bytes32) envfree; + + // harnessed functions + function bytesArrayContainsDuplicates(bytes bytesArray) external returns (bool) envfree; + function bytesArrayIsSubsetOfBitmap(uint256 referenceBitmap, bytes arrayWhichShouldBeASubsetOfTheReference) external returns (bool) envfree; +} + +// If my Operator status is REGISTERED ⇔ my quorum bitmap MUST BE nonzero +invariant registeredOperatorsHaveNonzeroBitmaps(address operator) + getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED <=> + getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)) != 0; + +// if two operators have different addresses, then they have different IDs +// excludes the case in which the operator is not registered, since then they can both have ID zero (the default) +invariant operatorIdIsUnique(address operator1, address operator2) + operator1 != operator2 => + (getOperatorStatus(operator1) == IRegistryCoordinator.OperatorStatus.REGISTERED => getOperatorId(operator1) != getOperatorId(operator2)); + +definition methodCanModifyBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector + || f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector; + +definition methodCanAddToBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector + || f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector; + +// `registerOperatorWithCoordinator` with kick params also meets this definition due to the 'churn' mechanism +definition methodCanRemoveFromBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector; + +// verify that quorumNumbers provided as an input to deregister operator MUST BE a subset of the operator’s current quorums +rule canOnlyDeregisterFromExistingQuorums(address operator) { + requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator); + + // TODO: store this status, verify that all calls to `deregisterOperatorWithCoordinator` *fail* if the operator is not registered first! + require(getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED); + + uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + + bytes quorumNumbers; + BN254.G1Point pubkey; + bytes32[] operatorIdsToSwap; + env e; + + deregisterOperatorWithCoordinator(e, quorumNumbers, pubkey, operatorIdsToSwap); + + // if deregistration is successful, verify that `quorumNumbers` input was proper + if (getOperatorStatus(operator) != IRegistryCoordinator.OperatorStatus.REGISTERED) { + assert(bytesArrayIsSubsetOfBitmap(bitmapBefore, quorumNumbers)); + } else { + assert(true); + } +} + +/* TODO: this is a Work In Progress +rule canOnlyModifyBitmapWithSpecificFunctions(address operator) { + requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator); + uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + // prepare to perform arbitrary function call + method f; + env e; + // TODO: need to ensure that if the function can modify the bitmap, then we are using the operator as an input + if (!methodCanModifyBitmap(f)) { + // perform arbitrary function call + calldataarg arg; + f(e, arg); + uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + assert(bitmapAfter == bitmapBefore); + } else if ( + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + ) { + if (e.msg.sender != operator) { + uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + assert(bitmapAfter == bitmapBefore); + } + } + + // if method did not remove from bitmap, it must have added + if (bitmapAfter & bitmapBefore == bitmapBefore) { + assert(methodCanAddToBitmap(f)); + } else { + assert(methodCanRemoveFromBitmap(f)); + } + } +} +*/ \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_29_48_001/.certora_verify.cvl1.json b/.certora_internal/23_10_18_12_29_48_001/.certora_verify.cvl1.json new file mode 100644 index 00000000..59d2a181 --- /dev/null +++ b/.certora_internal/23_10_18_12_29_48_001/.certora_verify.cvl1.json @@ -0,0 +1,10 @@ +[ + { + "importFilesToOrigRelpaths": {}, + "primary_contract": "BLSRegistryCoordinatorWithIndicesHarness", + "specfile": ".certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec", + "specfileOrigRelpath": "certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "specfilesToImportDecls": {}, + "type": "spec" + } +] \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_29_48_001/.certora_verify.json b/.certora_internal/23_10_18_12_29_48_001/.certora_verify.json new file mode 100644 index 00000000..1c5ff4ef --- /dev/null +++ b/.certora_internal/23_10_18_12_29_48_001/.certora_verify.json @@ -0,0 +1,8 @@ +{ + "importFilesToOrigRelpaths": {}, + "primary_contract": "BLSRegistryCoordinatorWithIndicesHarness", + "specfile": "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "specfileOrigRelpath": "certora/specs/BLSRegistryCoordinatorWithIndices.spec", + "specfilesToImportDecls": {}, + "type": "spec" +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_29_48_001/certora_debug_log.txt b/.certora_internal/23_10_18_12_29_48_001/certora_debug_log.txt new file mode 100644 index 00000000..68fc570f --- /dev/null +++ b/.certora_internal/23_10_18_12_29_48_001/certora_debug_log.txt @@ -0,0 +1,36 @@ +Saving last configuration file to .certora_internal/23_10_18_12_29_48_001/run.conf +There is no TAC file. Going to script EVMVerifier/certoraBuild.py to main_with_args() +Creating dir /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_config +In /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec, found the imports: [] +copying spec file /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec to /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec +In /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/specs/BLSRegistryCoordinatorWithIndices.spec, found the imports: [] +writing /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_verify.json +writing /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_verify.cvl1.json +Path to typechecker is /Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/certora_jars/Typechecker.jar +running ['java', '-jar', '/Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/certora_jars/Typechecker.jar', '-buildDirectory', '/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001'] + +building file certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol +Running cmd /Library/Frameworks/Python.framework/Versions/3.11/bin/solc -o "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0/" --overwrite --allow-paths "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync","lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable","lib/eigenlayer-contracts/lib/openzeppelin-contracts",. --standard-json +stdout, stderr = /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0.standard.json.stdout, /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0.standard.json.stderr +Exitcode 0 +Solc run /Library/Frameworks/Python.framework/Versions/3.11/bin/solc -o "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0/" --overwrite --allow-paths "/Users/Jeffrey/Desktop/eigenlayer-middleware.nosync","lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable","lib/eigenlayer-contracts/lib/openzeppelin-contracts",. --standard-json time: 0.1383 +reading standard json data from /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/.certora_internal/23_10_18_12_29_48_001/.certora_config/BLSRegistryCoordinatorWithIndicesHarness.sol_0.standard.json.stdout +build failed +Failure traceback: +Shared.certoraUtils.CertoraUserInputError: /Library/Frameworks/Python.framework/Versions/3.11/bin/solc had an error: +ParserError: Source "eigenlayer-contracts/src/contracts/interfaces/IPauserRegistry.sol" not found: File not found. Searched the following locations: "". + --> /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/munged/BLSRegistryCoordinatorWithIndices.sol:7:1: + | +7 | import {IPauserRegistry} from "eigenlayer-contracts/src/contracts/interfaces/IPauserRegistry.sol"; + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + +Encountered an error running Certora Prover: +/Library/Frameworks/Python.framework/Versions/3.11/bin/solc had an error: +ParserError: Source "eigenlayer-contracts/src/contracts/interfaces/IPauserRegistry.sol" not found: File not found. Searched the following locations: "". + --> /Users/Jeffrey/Desktop/eigenlayer-middleware.nosync/certora/munged/BLSRegistryCoordinatorWithIndices.sol:7:1: + | +7 | import {IPauserRegistry} from "eigenlayer-contracts/src/contracts/interfaces/IPauserRegistry.sol"; + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + diff --git a/.certora_internal/23_10_18_12_29_48_001/resource_errors.json b/.certora_internal/23_10_18_12_29_48_001/resource_errors.json new file mode 100644 index 00000000..d9bd7923 --- /dev/null +++ b/.certora_internal/23_10_18_12_29_48_001/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/.certora_internal/23_10_18_12_29_48_001/run.conf b/.certora_internal/23_10_18_12_29_48_001/run.conf new file mode 100644 index 00000000..52def0f3 --- /dev/null +++ b/.certora_internal/23_10_18_12_29_48_001/run.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol", + "lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol", + "certora/munged/StakeRegistry.sol", + "certora/munged/BLSPubkeyRegistry.sol", + "certora/munged/IndexRegistry.sol", + "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol" + ], + "loop_iter": "2", + "msg": "BLSRegistryCoordinatorWithIndices ", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable", + "@openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts" + ], + "process": "emv", + "prover_args": [ + " -optimisticFallback true -recursionEntryLimit 2 " + ], + "verify": "BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec" +} \ No newline at end of file diff --git a/.certora_internal/latest b/.certora_internal/latest new file mode 120000 index 00000000..402a8cd1 --- /dev/null +++ b/.certora_internal/latest @@ -0,0 +1 @@ +23_10_18_12_29_48_001 \ No newline at end of file diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml new file mode 100644 index 00000000..a464608e --- /dev/null +++ b/.github/workflows/certora-prover.yml @@ -0,0 +1,64 @@ +name: Certora Prover + +on: + push: + branches: + - master + - release-v* + - formal-verification + - fix-ci-errors + pull_request: {} + workflow_dispatch: {} + +jobs: + list-scripts: + runs-on: ubuntu-latest + outputs: + matrix: ${{ steps.set-matrix.outputs.matrix }} + steps: + - uses: actions/checkout@v2 + - id: set-matrix + run: echo ::set-output name=matrix::$(ls certora/scripts/{,**}/*.sh | grep -v '\WnoCI\W' | jq -Rsc 'split("\n")[:-1]') + verify: + runs-on: ubuntu-latest + needs: list-scripts + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + - name: Install forge dependencies + run: forge install + - name: Install python + uses: actions/setup-python@v2 + with: + python-version: '3.10' + cache: 'pip' + - name: Install java + uses: actions/setup-java@v2 + with: + distribution: temurin + java-version: '17' + - name: Install certora + run: pip install certora-cli + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.12/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc + chmod +x /usr/local/bin/solc + - name: Verify rule ${{ matrix.params }} + run: | + touch certora/applyHarness.patch + make -C certora munged + bash ${{ matrix.params }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 4 + matrix: + params: ${{ fromJson(needs.list-scripts.outputs.matrix) }} diff --git a/.gitignore b/.gitignore index d4dfc4c9..5a7b7747 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,5 @@ docs/ # Dotenv file .env + +*.DS_Store diff --git a/certora/.gitignore b/certora/.gitignore new file mode 100644 index 00000000..28437922 --- /dev/null +++ b/certora/.gitignore @@ -0,0 +1 @@ +munged \ No newline at end of file diff --git a/certora/Makefile b/certora/Makefile new file mode 100644 index 00000000..77c6375b --- /dev/null +++ b/certora/Makefile @@ -0,0 +1,25 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../src +MUNGED_DIR = munged + +help: + @echo "usage:" + @echo " make clean: remove all generated files (those ignored by git)" + @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" + @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" + +munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) + rm -rf $@ + cp -r $(CONTRACTS_DIR) $@ + patch -p0 -d $@ < $(PATCH) + +record: + diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH) + +refresh: munged record + +clean: + git clean -fdX + touch $(PATCH) diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch new file mode 100644 index 00000000..e69de29b diff --git a/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol b/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol new file mode 100644 index 00000000..54330ea1 --- /dev/null +++ b/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity =0.8.12; + +import "../munged/BLSRegistryCoordinatorWithIndices.sol"; + +contract BLSRegistryCoordinatorWithIndicesHarness is BLSRegistryCoordinatorWithIndices { + constructor( + ISlasher _slasher, + IServiceManager _serviceManager, + IStakeRegistry _stakeRegistry, + IBLSPubkeyRegistry _blsPubkeyRegistry, + IIndexRegistry _indexRegistry + ) + BLSRegistryCoordinatorWithIndices(_slasher, _serviceManager, _stakeRegistry, _blsPubkeyRegistry, _indexRegistry) + {} + + // @notice function based upon `BitmapUtils.bytesArrayToBitmap`, used to determine if an array contains any duplicates + function bytesArrayContainsDuplicates(bytes memory bytesArray) public pure returns (bool) { + // sanity-check on input. a too-long input would fail later on due to having duplicate entry(s) + if (bytesArray.length > 256) { + return false; + } + + // initialize the empty bitmap, to be built inside the loop + uint256 bitmap; + // initialize an empty uint256 to be used as a bitmask inside the loop + uint256 bitMask; + + // loop through each byte in the array to construct the bitmap + for (uint256 i = 0; i < bytesArray.length; ++i) { + // construct a single-bit mask from the numerical value of the next byte out of the array + bitMask = uint256(1 << uint8(bytesArray[i])); + // check that the entry is not a repeat + if (bitmap & bitMask != 0) { + return false; + } + // add the entry to the bitmap + bitmap = (bitmap | bitMask); + } + + // if the loop is completed without returning early, then the array contains no duplicates + return true; + } + + // @notice verifies that a bytes array is a (non-strict) subset of a bitmap + function bytesArrayIsSubsetOfBitmap(uint256 referenceBitmap, bytes memory arrayWhichShouldBeASubsetOfTheReference) public pure returns (bool) { + uint256 arrayWhichShouldBeASubsetOfTheReferenceBitmap = BitmapUtils.bytesArrayToBitmap(arrayWhichShouldBeASubsetOfTheReference); + if (referenceBitmap | arrayWhichShouldBeASubsetOfTheReferenceBitmap == referenceBitmap) { + return true; + } else { + return false; + } + } +} \ No newline at end of file diff --git a/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh b/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh new file mode 100644 index 00000000..0a980d00 --- /dev/null +++ b/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh @@ -0,0 +1,21 @@ +if [[ "$2" ]] +then + RULE="--rule $2" +fi + +solc-select use 0.8.12 + +certoraRun certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol \ + lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol \ + certora/munged/StakeRegistry.sol certora/munged/BLSPubkeyRegistry.sol certora/munged/IndexRegistry.sol \ + lib/eigenlayer-contracts/src/contracts/core/Slasher.sol \ + --verify BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec \ + --optimistic_loop \ + --optimistic_hashing \ + --prover_args '-optimisticFallback true -recursionEntryLimit 2 ' \ + $RULE \ + --loop_iter 2 \ + --packages @openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts @openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable \ + --msg "BLSRegistryCoordinatorWithIndices $1 $2" \ + +# TODO: import a ServiceManager contract \ No newline at end of file diff --git a/certora/specs/BLSRegistryCoordinatorWithIndices.spec b/certora/specs/BLSRegistryCoordinatorWithIndices.spec new file mode 100644 index 00000000..2ca61c0c --- /dev/null +++ b/certora/specs/BLSRegistryCoordinatorWithIndices.spec @@ -0,0 +1,169 @@ + +methods { + //// External Calls + // external calls to StakeRegistry + function _.quorumCount() external => DISPATCHER(true); + function _.getCurrentTotalStakeForQuorum(uint8 quorumNumber) external => DISPATCHER(true); + function _.getCurrentOperatorStakeForQuorum(bytes32 operatorId, uint8 quorumNumber) external => DISPATCHER(true); + function _.registerOperator(address, bytes32, bytes) external => DISPATCHER(true); + function _.deregisterOperator(bytes32, bytes) external => DISPATCHER(true); + + // external calls to Slasher + function _.contractCanSlashOperatorUntilBlock(address, address) external => DISPATCHER(true); + + // external calls to BLSPubkeyRegistry + function _.registerOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); + function _.deregisterOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); + + // external calls to ServiceManager + function _.latestServeUntilBlock() external => DISPATCHER(true); + function _.recordLastStakeUpdateAndRevokeSlashingAbility(address, uint256) external => DISPATCHER(true); + + // external calls to IndexRegistry + function _.registerOperator(bytes32, bytes) external => DISPATCHER(true); + function _.deregisterOperator(bytes32, bytes, bytes32[]) external => DISPATCHER(true); + + // external calls to ERC1271 (can import OpenZeppelin mock implementation) + // isValidSignature(bytes32 hash, bytes memory signature) returns (bytes4 magicValue) => DISPATCHER(true) + function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true); + + // external calls to BLSPubkeyCompendium + function _.pubkeyHashToOperator(bytes32) external => DISPATCHER(true); + + //envfree functions + function OPERATOR_CHURN_APPROVAL_TYPEHASH() external returns (bytes32) envfree; + function slasher() external returns (address) envfree; + function serviceManager() external returns (address) envfree; + function blsPubkeyRegistry() external returns (address) envfree; + function stakeRegistry() external returns (address) envfree; + function indexRegistry() external returns (address) envfree; + function registries(uint256) external returns (address) envfree; + function churnApprover() external returns (address) envfree; + function isChurnApproverSaltUsed(bytes32) external returns (bool) envfree; + function getOperatorSetParams(uint8 quorumNumber) external returns (IBLSRegistryCoordinatorWithIndices.OperatorSetParam) envfree; + function getOperator(address operator) external returns (IRegistryCoordinator.Operator) envfree; + function getOperatorId(address operator) external returns (bytes32) envfree; + function getOperatorStatus(address operator) external returns (IRegistryCoordinator.OperatorStatus) envfree; + function getQuorumBitmapIndicesByOperatorIdsAtBlockNumber(uint32 blockNumber, bytes32[] operatorIds) + external returns (uint32[]) envfree; + function getQuorumBitmapByOperatorIdAtBlockNumberByIndex(bytes32 operatorId, uint32 blockNumber, uint256 index) external returns (uint192) envfree; + function getQuorumBitmapUpdateByOperatorIdByIndex(bytes32 operatorId, uint256 index) + external returns (IRegistryCoordinator.QuorumBitmapUpdate) envfree; + function getCurrentQuorumBitmapByOperatorId(bytes32 operatorId) external returns (uint192) envfree; + function getQuorumBitmapUpdateByOperatorIdLength(bytes32 operatorId) external returns (uint256) envfree; + function numRegistries() external returns (uint256) envfree; + function calculateOperatorChurnApprovalDigestHash( + bytes32 registeringOperatorId, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[] operatorKickParams, + bytes32 salt, + uint256 expiry + ) external returns (bytes32) envfree; + + // harnessed functions + function bytesArrayContainsDuplicates(bytes bytesArray) external returns (bool) envfree; + function bytesArrayIsSubsetOfBitmap(uint256 referenceBitmap, bytes arrayWhichShouldBeASubsetOfTheReference) external returns (bool) envfree; +} + +// If my Operator status is REGISTERED ⇔ my quorum bitmap MUST BE nonzero +invariant registeredOperatorsHaveNonzeroBitmaps(address operator) + getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED <=> + getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)) != 0; + +// if two operators have different addresses, then they have different IDs +// excludes the case in which the operator is not registered, since then they can both have ID zero (the default) +invariant operatorIdIsUnique(address operator1, address operator2) + operator1 != operator2 => + (getOperatorStatus(operator1) == IRegistryCoordinator.OperatorStatus.REGISTERED => getOperatorId(operator1) != getOperatorId(operator2)); + +definition methodCanModifyBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector + || f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector; + +definition methodCanAddToBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector + || f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector; + +// `registerOperatorWithCoordinator` with kick params also meets this definition due to the 'churn' mechanism +definition methodCanRemoveFromBitmap(method f) returns bool = + f.selector == sig:registerOperatorWithCoordinator( + bytes, + BN254.G1Point, + string, + IBLSRegistryCoordinatorWithIndices.OperatorKickParam[], + ISignatureUtils.SignatureWithSaltAndExpiry + ).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector + || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector; + +// verify that quorumNumbers provided as an input to deregister operator MUST BE a subset of the operator’s current quorums +rule canOnlyDeregisterFromExistingQuorums(address operator) { + requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator); + + // TODO: store this status, verify that all calls to `deregisterOperatorWithCoordinator` *fail* if the operator is not registered first! + require(getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED); + + uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + + bytes quorumNumbers; + BN254.G1Point pubkey; + bytes32[] operatorIdsToSwap; + env e; + + deregisterOperatorWithCoordinator(e, quorumNumbers, pubkey, operatorIdsToSwap); + + // if deregistration is successful, verify that `quorumNumbers` input was proper + if (getOperatorStatus(operator) != IRegistryCoordinator.OperatorStatus.REGISTERED) { + assert(bytesArrayIsSubsetOfBitmap(bitmapBefore, quorumNumbers)); + } else { + assert(true); + } +} + +/* TODO: this is a Work In Progress +rule canOnlyModifyBitmapWithSpecificFunctions(address operator) { + requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator); + uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + // prepare to perform arbitrary function call + method f; + env e; + // TODO: need to ensure that if the function can modify the bitmap, then we are using the operator as an input + if (!methodCanModifyBitmap(f)) { + // perform arbitrary function call + calldataarg arg; + f(e, arg); + uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + assert(bitmapAfter == bitmapBefore); + } else if ( + f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector + ) { + if (e.msg.sender != operator) { + uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)); + assert(bitmapAfter == bitmapBefore); + } + } + + // if method did not remove from bitmap, it must have added + if (bitmapAfter & bitmapBefore == bitmapBefore) { + assert(methodCanAddToBitmap(f)); + } else { + assert(methodCanRemoveFromBitmap(f)); + } + } +} +*/ \ No newline at end of file