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 1/9] 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 From cdcf5764dda77138a8f7bbd15ae447739ee714c3 Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Thu, 19 Oct 2023 11:43:34 -0700 Subject: [PATCH 2/9] clean up trash and add the folder to gitignore --- .../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 - .gitignore | 4 + 28 files changed, 4 insertions(+), 625 deletions(-) delete mode 100644 .certora_internal/23_10_18_12_21_12_640/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_21_12_640/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_23_12_641/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_23_12_641/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_24_19_683/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_24_19_683/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_25_21_966/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_25_21_966/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_25_45_316/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_25_45_316/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_26_04_818/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_26_04_818/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_metadata.json delete mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec delete mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json delete mode 100644 .certora_internal/23_10_18_12_26_27_032/.certora_verify.json delete mode 100644 .certora_internal/23_10_18_12_26_27_032/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_26_27_032/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_26_27_032/run.conf delete mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_metadata.json delete mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec delete mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_verify.cvl1.json delete mode 100644 .certora_internal/23_10_18_12_29_48_001/.certora_verify.json delete mode 100644 .certora_internal/23_10_18_12_29_48_001/certora_debug_log.txt delete mode 100644 .certora_internal/23_10_18_12_29_48_001/resource_errors.json delete mode 100644 .certora_internal/23_10_18_12_29_48_001/run.conf delete mode 120000 .certora_internal/latest 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 deleted file mode 100644 index e69de29b..00000000 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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_21_12_640/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index e69de29b..00000000 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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_23_12_641/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index e69de29b..00000000 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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_24_19_683/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index e69de29b..00000000 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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_25_21_966/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index e69de29b..00000000 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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_25_45_316/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index e69de29b..00000000 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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_26_04_818/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index a2848b4c..00000000 --- a/.certora_internal/23_10_18_12_26_27_032/.certora_metadata.json +++ /dev/null @@ -1,54 +0,0 @@ -{ - "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 deleted file mode 100644 index 2ca61c0c..00000000 --- a/.certora_internal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec +++ /dev/null @@ -1,169 +0,0 @@ - -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 deleted file mode 100644 index 0a3774e7..00000000 --- a/.certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json +++ /dev/null @@ -1,10 +0,0 @@ -[ - { - "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 deleted file mode 100644 index 1c5ff4ef..00000000 --- a/.certora_internal/23_10_18_12_26_27_032/.certora_verify.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "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 deleted file mode 100644 index 8d41e8d9..00000000 --- a/.certora_internal/23_10_18_12_26_27_032/certora_debug_log.txt +++ /dev/null @@ -1,36 +0,0 @@ -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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_26_27_032/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index 52def0f3..00000000 --- a/.certora_internal/23_10_18_12_26_27_032/run.conf +++ /dev/null @@ -1,23 +0,0 @@ -{ - "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 deleted file mode 100644 index 15f9ee79..00000000 --- a/.certora_internal/23_10_18_12_29_48_001/.certora_metadata.json +++ /dev/null @@ -1,54 +0,0 @@ -{ - "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 deleted file mode 100644 index 2ca61c0c..00000000 --- a/.certora_internal/23_10_18_12_29_48_001/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec +++ /dev/null @@ -1,169 +0,0 @@ - -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 deleted file mode 100644 index 59d2a181..00000000 --- a/.certora_internal/23_10_18_12_29_48_001/.certora_verify.cvl1.json +++ /dev/null @@ -1,10 +0,0 @@ -[ - { - "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 deleted file mode 100644 index 1c5ff4ef..00000000 --- a/.certora_internal/23_10_18_12_29_48_001/.certora_verify.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "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 deleted file mode 100644 index 68fc570f..00000000 --- a/.certora_internal/23_10_18_12_29_48_001/certora_debug_log.txt +++ /dev/null @@ -1,36 +0,0 @@ -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 deleted file mode 100644 index d9bd7923..00000000 --- a/.certora_internal/23_10_18_12_29_48_001/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "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 deleted file mode 100644 index 52def0f3..00000000 --- a/.certora_internal/23_10_18_12_29_48_001/run.conf +++ /dev/null @@ -1,23 +0,0 @@ -{ - "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 deleted file mode 120000 index 402a8cd1..00000000 --- a/.certora_internal/latest +++ /dev/null @@ -1 +0,0 @@ -23_10_18_12_29_48_001 \ No newline at end of file diff --git a/.gitignore b/.gitignore index 5a7b7747..433499ae 100644 --- a/.gitignore +++ b/.gitignore @@ -14,4 +14,8 @@ docs/ # Dotenv file .env +# Certora Outputs +.certora_internal/ +.certora_recent_jobs.json + *.DS_Store From a91ec690bb3cac8f3ebc2e8f85f97e9f97965ed3 Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Mon, 23 Oct 2023 11:26:23 -0700 Subject: [PATCH 3/9] fix script to use correct remapping and remove double forward-slash behavior from YAML file --- .github/workflows/certora-prover.yml | 2 +- certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh | 2 +- lib/eigenlayer-contracts | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml index a464608e..46fb679c 100644 --- a/.github/workflows/certora-prover.yml +++ b/.github/workflows/certora-prover.yml @@ -18,7 +18,7 @@ jobs: 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]') + 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 diff --git a/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh b/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh index 0a980d00..a6e7e171 100644 --- a/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh +++ b/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh @@ -15,7 +15,7 @@ certoraRun certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol \ --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 \ + --packages @openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts @openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable eigenlayer-contracts=lib/eigenlayer-contracts \ --msg "BLSRegistryCoordinatorWithIndices $1 $2" \ # TODO: import a ServiceManager contract \ No newline at end of file diff --git a/lib/eigenlayer-contracts b/lib/eigenlayer-contracts index 2a3ec30a..ad980b5b 160000 --- a/lib/eigenlayer-contracts +++ b/lib/eigenlayer-contracts @@ -1 +1 @@ -Subproject commit 2a3ec30ad1cfd844d19855bab619cd4e4ecfc2d9 +Subproject commit ad980b5b02f8e9a6bcc3ff8dd0b574649a065285 From d762ddcf3bc346a69d28073d9dc4df4afb7f5281 Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Mon, 23 Oct 2023 13:12:15 -0700 Subject: [PATCH 4/9] fix duplicate run issue we were using the wrong syntax, resulting in listing scripts twice instead of once --- .github/workflows/certora-prover.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml index 46fb679c..f3d07a0d 100644 --- a/.github/workflows/certora-prover.yml +++ b/.github/workflows/certora-prover.yml @@ -6,7 +6,6 @@ on: - master - release-v* - formal-verification - - fix-ci-errors pull_request: {} workflow_dispatch: {} @@ -18,7 +17,7 @@ jobs: 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]') + 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 From be6479cdb6d4c31eddf5e3a77ff2308c831038cb Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Fri, 27 Oct 2023 10:12:33 -0700 Subject: [PATCH 5/9] try using more NONDET summaries This spec is failing with unexpected havocs. Trying out using more NONDET summaries to see if this fixes it. --- certora/specs/BLSRegistryCoordinatorWithIndices.spec | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/certora/specs/BLSRegistryCoordinatorWithIndices.spec b/certora/specs/BLSRegistryCoordinatorWithIndices.spec index 2ca61c0c..a4eaeb01 100644 --- a/certora/specs/BLSRegistryCoordinatorWithIndices.spec +++ b/certora/specs/BLSRegistryCoordinatorWithIndices.spec @@ -5,14 +5,16 @@ methods { 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 _.registerOperator(address, bytes32, bytes) external => DISPATCHER(true); + function _.registerOperator(address, bytes32, bytes) external => NONDET; 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 _.registerOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); + function _.registerOperator(address, bytes, BN254.G1Point) external => NONDET; function _.deregisterOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true); // external calls to ServiceManager @@ -20,12 +22,14 @@ methods { function _.recordLastStakeUpdateAndRevokeSlashingAbility(address, uint256) external => DISPATCHER(true); // external calls to IndexRegistry - function _.registerOperator(bytes32, bytes) external => DISPATCHER(true); + // function _.registerOperator(bytes32, bytes) external => DISPATCHER(true); + function _.registerOperator(bytes32, bytes) external => NONDET; 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); + // function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true); + function _.isValidSignature(bytes32, bytes) external => NONDET; // external calls to BLSPubkeyCompendium function _.pubkeyHashToOperator(bytes32) external => DISPATCHER(true); From 4f7e77d6e927599ab1ba76dffd49e5661830522a Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Fri, 27 Oct 2023 10:34:33 -0700 Subject: [PATCH 6/9] temporarily delete submodule in order to force upgrade --- .gitmodules | 3 --- lib/eigenlayer-contracts | 1 - 2 files changed, 4 deletions(-) delete mode 160000 lib/eigenlayer-contracts diff --git a/.gitmodules b/.gitmodules index 635af195..4b4c42b7 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,9 +1,6 @@ [submodule "lib/forge-std"] path = lib/forge-std url = https://github.com/foundry-rs/forge-std -[submodule "lib/eigenlayer-contracts"] - path = lib/eigenlayer-contracts - url = https://github.com/Layr-labs/eigenlayer-contracts [submodule "lib/ds-test"] path = lib/ds-test url = https://github.com/dapphub/ds-test diff --git a/lib/eigenlayer-contracts b/lib/eigenlayer-contracts deleted file mode 160000 index ad980b5b..00000000 --- a/lib/eigenlayer-contracts +++ /dev/null @@ -1 +0,0 @@ -Subproject commit ad980b5b02f8e9a6bcc3ff8dd0b574649a065285 From 3a83c4e2dff136ccd01eb28f19dbcc5edd7d23cb Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Fri, 27 Oct 2023 10:35:03 -0700 Subject: [PATCH 7/9] remove other submodules --- .gitmodules | 6 ------ lib/ds-test | 1 - lib/forge-std | 1 - 3 files changed, 8 deletions(-) delete mode 160000 lib/ds-test delete mode 160000 lib/forge-std diff --git a/.gitmodules b/.gitmodules index 4b4c42b7..e69de29b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +0,0 @@ -[submodule "lib/forge-std"] - path = lib/forge-std - url = https://github.com/foundry-rs/forge-std -[submodule "lib/ds-test"] - path = lib/ds-test - url = https://github.com/dapphub/ds-test diff --git a/lib/ds-test b/lib/ds-test deleted file mode 160000 index e282159d..00000000 --- a/lib/ds-test +++ /dev/null @@ -1 +0,0 @@ -Subproject commit e282159d5170298eb2455a6c05280ab5a73a4ef0 diff --git a/lib/forge-std b/lib/forge-std deleted file mode 160000 index f73c73d2..00000000 --- a/lib/forge-std +++ /dev/null @@ -1 +0,0 @@ -Subproject commit f73c73d2018eb6a111f35e4dae7b4f27401e9421 From 0001b4320b31e07d8c01f2d3827fbb6f5d60fafb Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Fri, 27 Oct 2023 10:39:30 -0700 Subject: [PATCH 8/9] forge install: eigenlayer-contracts 97a2ddf --- .gitmodules | 3 +++ lib/eigenlayer-contracts | 1 + 2 files changed, 4 insertions(+) create mode 160000 lib/eigenlayer-contracts diff --git a/.gitmodules b/.gitmodules index e69de29b..6c719165 100644 --- a/.gitmodules +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "lib/eigenlayer-contracts"] + path = lib/eigenlayer-contracts + url = https://github.com/Layr-Labs/eigenlayer-contracts diff --git a/lib/eigenlayer-contracts b/lib/eigenlayer-contracts new file mode 160000 index 00000000..97a2ddff --- /dev/null +++ b/lib/eigenlayer-contracts @@ -0,0 +1 @@ +Subproject commit 97a2ddff40b99a94ff79e7fdfc0bd2783dc8338e From dcca0b6dee6a13d3e5a7f62c6041f6a5700d0e48 Mon Sep 17 00:00:00 2001 From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com> Date: Fri, 27 Oct 2023 10:45:38 -0700 Subject: [PATCH 9/9] chore: switch remappings to use more of the eigenlayer-contracts submodules --- remappings.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/remappings.txt b/remappings.txt index 26950b6a..25d27daf 100644 --- a/remappings.txt +++ b/remappings.txt @@ -1,7 +1,7 @@ @openzeppelin-upgrades/=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable/ @openzeppelin/=lib/eigenlayer-contracts/lib/openzeppelin-contracts/ -ds-test/=lib/ds-test/src/ +ds-test/=lib/eigenlayer-contracts/lib/ds-test/src/ eigenlayer-contracts/=lib/eigenlayer-contracts/ -forge-std/=lib/forge-std/src/ +forge-std/=lib/eigenlayer-contracts/lib/forge-std/src/ openzeppelin-contracts-upgradeable/=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable/ openzeppelin-contracts/=lib/eigenlayer-contracts/lib/openzeppelin-contracts/