-
Notifications
You must be signed in to change notification settings - Fork 92
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
migrate Prover functionality from core repo
had to modify some paths / folder structure / etc
- Loading branch information
1 parent
5b1b729
commit 16fef83
Showing
35 changed files
with
961 additions
and
0 deletions.
There are no files selected for viewing
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| { | ||
| "topics": [] | ||
| } |
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| { | ||
| "topics": [] | ||
| } |
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| { | ||
| "topics": [] | ||
| } |
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| { | ||
| "topics": [] | ||
| } |
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| { | ||
| "topics": [] | ||
| } |
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| { | ||
| "topics": [] | ||
| } |
54 changes: 54 additions & 0 deletions
54
.certora_internal/23_10_18_12_26_27_032/.certora_metadata.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
169 changes: 169 additions & 0 deletions
169
...nal/23_10_18_12_26_27_032/.certora_sources/.0_BLSRegistryCoordinatorWithIndices.spec.spec
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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)); | ||
| } | ||
| } | ||
| } | ||
| */ |
10 changes: 10 additions & 0 deletions
10
.certora_internal/23_10_18_12_26_27_032/.certora_verify.cvl1.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } | ||
| ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
36 changes: 36 additions & 0 deletions
36
.certora_internal/23_10_18_12_26_27_032/certora_debug_log.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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"; | ||
| | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
|
|
||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| { | ||
| "topics": [] | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
Oops, something went wrong.