diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml new file mode 100644 index 00000000..8c64b48b --- /dev/null +++ b/.github/workflows/certora-prover.yml @@ -0,0 +1,63 @@ +name: Certora Prover + +on: + push: + branches: + - master + - release-v* + - formal-verification + 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) }} \ No newline at end of file diff --git a/.gitignore b/.gitignore index e10dbe82..bac8fb01 100644 --- a/.gitignore +++ b/.gitignore @@ -12,5 +12,8 @@ node_modules/ # Dotenv file .env +# Certora Outputs +.certora_internal/ +.certora_recent_jobs.json *.DS_Store diff --git a/certora/config/setup.conf b/certora/config/setup.conf new file mode 100644 index 00000000..027ff637 --- /dev/null +++ b/certora/config/setup.conf @@ -0,0 +1,31 @@ +{ + "files": [ + "certora/harnesses/RegistryCoordinatorHarness.sol", + "certora/harnesses/StakeRegistryHarness.sol", + "certora/harnesses/BLSApkRegistryHarness.sol", + "certora/harnesses/IndexRegistryHarness.sol", + "lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol", + "test/mocks/ServiceManagerMock.sol", + "lib/eigenlayer-contracts/src/contracts/core/Slasher.sol", + "lib/eigenlayer-contracts/src/contracts/core/AVSDirectory.sol" + ], + "verify": "RegistryCoordinatorHarness:certora/specs/setup.spec", + "loop_iter": "2", + "parametric_contracts": ["RegistryCoordinatorHarness"], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable", + "eigenlayer-contracts=lib/eigenlayer-contracts" + ], + "link": [ + "RegistryCoordinatorHarness:serviceManager=ServiceManagerMock", + "ServiceManagerMock:_avsDirectory=AVSDirectory", + "RegistryCoordinatorHarness:blsApkRegistry=BLSApkRegistryHarness", + "RegistryCoordinatorHarness:indexRegistry=IndexRegistryHarness", + "RegistryCoordinatorHarness:stakeRegistry=StakeRegistryHarness" + ], + "optimistic_fallback": true, + "optimistic_loop": true, + "optimistic_hashing": true, + "rule_sanity": "basic" +} diff --git a/certora/harnesses/BLSApkRegistryHarness.sol b/certora/harnesses/BLSApkRegistryHarness.sol new file mode 100644 index 00000000..ac0e0eb8 --- /dev/null +++ b/certora/harnesses/BLSApkRegistryHarness.sol @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity =0.8.12; + +import "src/BLSApkRegistry.sol"; + +contract BLSApkRegistryHarness is BLSApkRegistry { + constructor( + IRegistryCoordinator _registryCoordinator + ) BLSApkRegistry(_registryCoordinator) {} + + function getApkHistory(uint8 quorumNumber) public view returns (ApkUpdate[] memory) { + return apkHistory[quorumNumber]; + } +} diff --git a/certora/harnesses/IndexRegistryHarness.sol b/certora/harnesses/IndexRegistryHarness.sol new file mode 100644 index 00000000..719c8ac6 --- /dev/null +++ b/certora/harnesses/IndexRegistryHarness.sol @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity =0.8.12; + +import "src/IndexRegistry.sol"; + +contract IndexRegistryHarness is IndexRegistry { + constructor( + IRegistryCoordinator _registryCoordinator + ) IndexRegistry(_registryCoordinator) {} + + function operatorIndexHistory(uint8 quorumNumber, uint32 operatorIndex) public view returns (OperatorUpdate[] memory) { + return _operatorIndexHistory[quorumNumber][operatorIndex]; + } + + function operatorCountHistory(uint8 quorumNumber) public view returns (QuorumUpdate[] memory) { + return _operatorCountHistory[quorumNumber]; + } +} diff --git a/certora/harnesses/RegistryCoordinatorHarness.sol b/certora/harnesses/RegistryCoordinatorHarness.sol new file mode 100644 index 00000000..7b8c9ca7 --- /dev/null +++ b/certora/harnesses/RegistryCoordinatorHarness.sol @@ -0,0 +1,59 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity =0.8.12; + +import "src/RegistryCoordinator.sol"; + +contract RegistryCoordinatorHarness is RegistryCoordinator { + constructor( + IServiceManager _serviceManager, + IStakeRegistry _stakeRegistry, + IBLSApkRegistry _blsApkRegistry, + IIndexRegistry _indexRegistry + ) RegistryCoordinator(_serviceManager, _stakeRegistry, _blsApkRegistry, _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.orderedBytesArrayToBitmap(arrayWhichShouldBeASubsetOfTheReference); + if (referenceBitmap | arrayWhichShouldBeASubsetOfTheReferenceBitmap == referenceBitmap) { + return true; + } else { + return false; + } + } + + function quorumInBitmap(uint256 bitmap, uint8 numberToCheckForInclusion) public pure returns (bool) { + return BitmapUtils.isSet(bitmap, numberToCheckForInclusion); + } + + function hashToG1Harness(bytes32 x) public pure returns (BN254.G1Point memory) { + return BN254.G1Point(uint256(keccak256(abi.encodePacked(x))), 2); + } +} diff --git a/certora/harnesses/StakeRegistryHarness.sol b/certora/harnesses/StakeRegistryHarness.sol new file mode 100644 index 00000000..64856b1a --- /dev/null +++ b/certora/harnesses/StakeRegistryHarness.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity =0.8.12; + +import "src/StakeRegistry.sol"; + +contract StakeRegistryHarness is StakeRegistry { + constructor( + IRegistryCoordinator _registryCoordinator, + IDelegationManager _delegationManager + ) StakeRegistry(_registryCoordinator, _delegationManager) {} + + function totalStakeHistory(uint8 quorumNumber) public view returns (StakeUpdate[] memory) { + return _totalStakeHistory[quorumNumber]; + } +} diff --git a/certora/specs/setup.spec b/certora/specs/setup.spec new file mode 100644 index 00000000..6d7ae40d --- /dev/null +++ b/certora/specs/setup.spec @@ -0,0 +1,326 @@ +using ServiceManagerMock as serviceManager; +using StakeRegistryHarness as stakeRegistry; +using BLSApkRegistryHarness as blsApkRegistry; +using IndexRegistryHarness as indexRegistry; +// using DelegationManager as delegation; +// using BN254; +use builtin rule sanity; + +methods { + function _.isValidSignature(bytes32 hash, bytes signature) external => NONDET; // isValidSignatureCVL(hash,signature) expect bytes4; + function _.unpauser() external => unpauser expect address; + function _.isPauser(address user) external => pausers[user] expect bool; + function _.isOperator(address operator) external => operators[operator] expect bool; + + // BN254 Library + function BN254.pairing(BN254.G1Point memory, BN254.G2Point memory, BN254.G1Point memory, BN254.G2Point memory) internal returns (bool) => NONDET; + function BN254.hashToG1(bytes32 x) internal returns (BN254.G1Point memory) => hashToG1Ghost(x); + function BN254.plus(BN254.G1Point memory, BN254.G1Point memory) internal returns (BN254.G1Point memory) => returnG1(); + + // external calls to ServiceManager + function _.registerOperatorToAVS(address, ISignatureUtils.SignatureWithSaltAndExpiry) external => NONDET; + function _.deregisterOperatorFromAVS(address) external => NONDET; + + // Registry contracts + function StakeRegistryHarness.totalStakeHistory(uint8) external returns (IStakeRegistry.StakeUpdate[]) envfree; + function StakeRegistry._weightOfOperatorForQuorum(uint8 quorumNumber, address operator) internal returns (uint96, bool) => weightOfOperatorGhost(quorumNumber, operator); + + function IndexRegistryHarness.operatorCountHistory(uint8) external returns (IIndexRegistry.QuorumUpdate[]) envfree; + + function BLSApkRegistryHarness.getApkHistory(uint8) external returns (IBLSApkRegistry.ApkUpdate[]) envfree; + function BLSApkRegistryHarness.getOperatorId(address) external returns (bytes32) envfree; + function BLSApkRegistryHarness.registerBLSPublicKey(address, IBLSApkRegistry.PubkeyRegistrationParams, BN254.G1Point) external returns (bytes32) => PER_CALLEE_CONSTANT; + + + // RegistryCoordinator + function getOperatorStatus(address operator) external returns (IRegistryCoordinator.OperatorStatus) envfree; + function getOperatorId(address operator) external returns (bytes32) envfree; + function RegistryCoordinator._verifyChurnApproverSignature(address, bytes32, IRegistryCoordinator.OperatorKickParam[] memory, ISignatureUtils.SignatureWithSaltAndExpiry memory) internal => NONDET; + function RegistryCoordinator._validateChurn(uint8, uint96, address, uint96, IRegistryCoordinator.OperatorKickParam memory, IRegistryCoordinator.OperatorSetParam memory) internal => NONDET; + + // harnessed functions + function bytesArrayContainsDuplicates(bytes bytesArray) external returns (bool) envfree; + function bytesArrayIsSubsetOfBitmap(uint256 referenceBitmap, bytes arrayWhichShouldBeASubsetOfTheReference) external returns (bool) envfree; + function quorumInBitmap(uint256 bitmap, uint8 numberToCheckForInclusion) external returns (bool) envfree; + function getQuorumBitmapHistoryLength(bytes32) external returns (uint256) envfree; + function hashToG1Harness(bytes32 x) external returns (BN254.G1Point memory) envfree; + + // BitmapUtils Libraries + function BitmapUtils.orderedBytesArrayToBitmap(bytes memory a) internal returns (uint256) => bytesToBitmapCVL[a]; + function BitmapUtils.orderedBytesArrayToBitmap(bytes memory a, uint8 b) internal returns (uint256) => bytesToBitmapCappedCVL[a][b]; + function BitmapUtils.isArrayStrictlyAscendingOrdered(bytes calldata a) internal returns (bool) => ascendingArrayCVL[a]; + function BitmapUtils.bitmapToBytesArray(uint256 a) internal returns (bytes memory) => returnBytes(); + function BitmapUtils.countNumOnes(uint256 a) internal returns (uint16) => numOnesCVL[a]; +} + +/** Ghost variables **/ + +// BitmapUtils ghost summaries +ghost mapping(bytes => uint256) bytesToBitmapCVL; +ghost mapping(bytes => mapping(uint8 => uint256)) bytesToBitmapCappedCVL; +ghost mapping(bytes => bool) ascendingArrayCVL; +ghost mapping(uint256 => bytes) bitmapToBytesCVL; +ghost mapping(uint256 => uint16) numOnesCVL; + +// Other ghost summaries +ghost address unpauser; +ghost mapping(address => bool) pausers; +ghost mapping(address => bool) operators; +ghost mapping(uint8 => mapping(address => uint96)) operatorWeight; + +/** Functions **/ + +function isPauserCVL(address user) returns bool { + return pausers[user]; +} + +function hashToG1Ghost(bytes32 x) returns BN254.G1Point { + return hashToG1Harness(x); +} + +function weightOfOperatorGhost(uint8 quorumNumber, address operator) returns (uint96, bool) { + bool val = operatorWeight[quorumNumber][operator] >= stakeRegistry.minimumStakeForQuorum[quorumNumber]; + return (operatorWeight[quorumNumber][operator], val); +} + +function returnG1() returns BN254.G1Point { + BN254.G1Point retVal; + return retVal; +} + +function returnG2() returns BN254.G2Point { + BN254.G2Point retVal; + return retVal; +} + +function returnBytes() returns bytes { + bytes retVal; + return retVal; +} + +/** Properties **/ + +/// +// status: verified +invariant initializedQuorumHistories(uint8 quorumNumber) + quorumNumber < currentContract.quorumCount <=> + stakeRegistry.totalStakeHistory(quorumNumber).length != 0 && + indexRegistry.operatorCountHistory(quorumNumber).length != 0 && + blsApkRegistry.getApkHistory(quorumNumber).length != 0; + +// Ensuring that RegistryCoordinator._operatorInfo and BLSApkRegistry.operatorToPubkeyHash operatorIds are consistent +// for the same operator +// status: verified +invariant operatorIdandPubkeyHash(address operator) + getOperatorId(operator) == blsApkRegistry.getOperatorId(operator); + +/// @notice If my Operator status is REGISTERED ⇔ my quorum bitmap MUST BE nonzero +// status: verified +invariant registeredOperatorsHaveNonzeroBitmaps(env e, address operator) + getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED <=> + getCurrentQuorumBitmap(e, getOperatorId(operator)) != 0 && getOperatorId(operator) != to_bytes32(0) + { + preserved with (env e1) { + require e1.msg.sender == e.msg.sender; + // Pushing to history overflows to 0 length and 0 length returns 0 bitmap + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + // If operator and msg.sender are not the same. msg.sender bitmap changing doesn't affect operator bitmap + requireInvariant oneIdPerOperator(operator, e.msg.sender); + // We store operatorId in multiple contracts. Preserves consistency when reading from RegistryCoordinator + // or calling blsApkRegistry.getOperatorId(operator) in _getOrCreateOperatorId + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + requireInvariant operatorIdandPubkeyHash(operator); + } + preserved ejectOperator(address operator1, bytes quorumNumbers) with (env e1) { + requireInvariant oneIdPerOperator(operator1, operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator1)) < max_uint256; + } + preserved registerOperator( + bytes quorumNumbers, + string socket, + IBLSApkRegistry.PubkeyRegistrationParams params, + ISignatureUtils.SignatureWithSaltAndExpiry signature + ) with (env e1) { + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + } + preserved registerOperatorWithChurn( + bytes quorumNumbers, + string socket, + IBLSApkRegistry.PubkeyRegistrationParams params, + IRegistryCoordinator.OperatorKickParam[] kickParams, + ISignatureUtils.SignatureWithSaltAndExpiry churnSignature, + ISignatureUtils.SignatureWithSaltAndExpiry operatorSignature + ) with (env e1) { + require quorumNumbers.length == 1; + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant oneIdPerOperator(operator, kickParams[0].operator); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + } + preserved updateOperators(address[] updatingOperators) with (env e1) { + requireInvariant oneIdPerOperator(operator, updatingOperators[0]); + requireInvariant oneIdPerOperator(updatingOperators[1], operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + } + preserved updateOperatorsForQuorum(address[][] updatingOperators, bytes quorumNumbers) with (env e1) { + require updatingOperators.length == 1 && quorumNumbers.length == 1; + requireInvariant oneIdPerOperator(operator, updatingOperators[0][0]); + requireInvariant oneIdPerOperator(updatingOperators[0][1], operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + } + } + + +/// @notice unique address <=> unique operatorId +// status: verified +invariant oneIdPerOperator(address operator1, address operator2) + operator1 != operator2 + => getOperatorId(operator1) != getOperatorId(operator2) || getOperatorId(operator1) == to_bytes32(0) && getOperatorId(operator2) == to_bytes32(0) + { + preserved { + requireInvariant operatorIdandPubkeyHash(operator1); + requireInvariant operatorIdandPubkeyHash(operator2); + } + } + +/// @notice one way implication as IndexRegistry.currentOperatorIndex does not get updated on operator deregistration +// status: violated +invariant operatorIndexWithinRange(env e, address operator, uint8 quorumNumber, uint256 blocknumber, uint256 index) + quorumInBitmap(assert_uint256(getCurrentQuorumBitmap(e, getOperatorId(operator))), quorumNumber) => + indexRegistry.currentOperatorIndex(e, quorumNumber, getOperatorId(operator)) < indexRegistry.totalOperatorsForQuorum(e, quorumNumber) + { + preserved with (env e1) { + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + requireInvariant operatorIdandPubkeyHash(operator); + } + preserved ejectOperator(address operator1, bytes quorumNumbers) with (env e1) { + requireInvariant oneIdPerOperator(operator1, operator); + requireInvariant operatorIdandPubkeyHash(operator1); + requireInvariant operatorIdandPubkeyHash(operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator1)) < max_uint256; + } + preserved registerOperator( + bytes quorumNumbers, + string socket, + IBLSApkRegistry.PubkeyRegistrationParams params, + ISignatureUtils.SignatureWithSaltAndExpiry signature + ) with (env e1) { + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + requireInvariant operatorIdandPubkeyHash(operator); + + require getCurrentQuorumBitmap(e, getOperatorId(operator)) + bytesToBitmapCVL[quorumNumbers] <= max_uint192; + } + preserved registerOperatorWithChurn( + bytes quorumNumbers, + string socket, + IBLSApkRegistry.PubkeyRegistrationParams params, + IRegistryCoordinator.OperatorKickParam[] kickParams, + ISignatureUtils.SignatureWithSaltAndExpiry churnSignature, + ISignatureUtils.SignatureWithSaltAndExpiry operatorSignature + ) with (env e1) { + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + requireInvariant operatorIdandPubkeyHash(operator); + + require getCurrentQuorumBitmap(e, getOperatorId(operator)) + bytesToBitmapCVL[quorumNumbers] <= max_uint192; + } + preserved updateOperators(address[] updatingOperators) with (env e1) { + requireInvariant oneIdPerOperator(operator, updatingOperators[0]); + requireInvariant oneIdPerOperator(updatingOperators[1], operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + } + preserved updateOperatorsForQuorum(address[][] updatingOperators, bytes quorumNumbers) with (env e1) { + require updatingOperators.length == 1 && quorumNumbers.length == 1; + requireInvariant oneIdPerOperator(operator, updatingOperators[0][0]); + requireInvariant oneIdPerOperator(updatingOperators[0][1], operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + } + } + + +/// @notice if operator is registered for quorum number then operator has stake weight >= minStakeWeight(quorumNumber) +// status: violated +invariant operatorHasNonZeroStakeWeight(env e, address operator, uint8 quorumNumber) + quorumInBitmap(assert_uint256(getCurrentQuorumBitmap(e, getOperatorId(operator))), quorumNumber) => + stakeRegistry.weightOfOperatorForQuorum(e, quorumNumber, operator) >= stakeRegistry.minimumStakeForQuorum(e, quorumNumber) + { + preserved with (env e1) { + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + requireInvariant operatorIdandPubkeyHash(operator); + } + preserved ejectOperator(address operator1, bytes quorumNumbers) with (env e1) { + requireInvariant oneIdPerOperator(operator1, operator); + requireInvariant operatorIdandPubkeyHash(operator1); + requireInvariant operatorIdandPubkeyHash(operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator1)) < max_uint256; + } + preserved registerOperator( + bytes quorumNumbers, + string socket, + IBLSApkRegistry.PubkeyRegistrationParams params, + ISignatureUtils.SignatureWithSaltAndExpiry signature + ) with (env e1) { + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + requireInvariant operatorIdandPubkeyHash(operator); + + require getCurrentQuorumBitmap(e, getOperatorId(operator)) + bytesToBitmapCVL[quorumNumbers] <= max_uint192; + } + preserved registerOperatorWithChurn( + bytes quorumNumbers, + string socket, + IBLSApkRegistry.PubkeyRegistrationParams params, + IRegistryCoordinator.OperatorKickParam[] kickParams, + ISignatureUtils.SignatureWithSaltAndExpiry churnSignature, + ISignatureUtils.SignatureWithSaltAndExpiry operatorSignature + ) with (env e1) { + require e1.msg.sender == e.msg.sender; + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + requireInvariant oneIdPerOperator(operator, e.msg.sender); + requireInvariant operatorIdandPubkeyHash(e.msg.sender); + requireInvariant operatorIdandPubkeyHash(operator); + + require getCurrentQuorumBitmap(e, getOperatorId(operator)) + bytesToBitmapCVL[quorumNumbers] <= max_uint192; + } + preserved updateOperators(address[] updatingOperators) with (env e1) { + requireInvariant oneIdPerOperator(operator, updatingOperators[0]); + requireInvariant oneIdPerOperator(updatingOperators[1], operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + } + preserved updateOperatorsForQuorum(address[][] updatingOperators, bytes quorumNumbers) with (env e1) { + require updatingOperators.length == 1 && quorumNumbers.length == 1; + requireInvariant oneIdPerOperator(operator, updatingOperators[0][0]); + requireInvariant oneIdPerOperator(updatingOperators[0][1], operator); + require getQuorumBitmapHistoryLength(getOperatorId(operator)) < max_uint256; + } + } + +/// Operator cant go from registered to NEVER_REGISTERED. Can write some parametric rule +// status: verified +rule registeredOperatorCantBeNeverRegistered(address operator) { + require(getOperatorStatus(operator) != IRegistryCoordinator.OperatorStatus.NEVER_REGISTERED); + + calldataarg arg; + env e; + method f; + f(e, arg); + + assert(getOperatorStatus(operator) != IRegistryCoordinator.OperatorStatus.NEVER_REGISTERED); +} \ No newline at end of file diff --git a/docs/README.md b/docs/README.md index 62e9dd91..7f95f0f3 100644 --- a/docs/README.md +++ b/docs/README.md @@ -97,6 +97,7 @@ These histories are used by offchain code to query state at particular blocks, a ##### Hooking Into EigenLayer Core The main thing that links an AVS to the EigenLayer core contracts is that when EigenLayer Operators register/deregister with an AVS, the AVS calls these functions in EigenLayer core: + * [`AVSDirectory.registerOperatorToAVS`][core-registerToAVS] * [`AVSDirectory.deregisterOperatorFromAVS`][core-deregisterFromAVS] diff --git a/lib/eigenlayer-contracts b/lib/eigenlayer-contracts index a31a2f3b..75115593 160000 --- a/lib/eigenlayer-contracts +++ b/lib/eigenlayer-contracts @@ -1 +1 @@ -Subproject commit a31a2f3b226faee8a06b8664dd3b16ff95c01071 +Subproject commit 751155931cfb6b5ebcb77ef3cb12dff041329cbc diff --git a/lib/forge-std b/lib/forge-std index bb4ceea9..f73c73d2 160000 --- a/lib/forge-std +++ b/lib/forge-std @@ -1 +1 @@ -Subproject commit bb4ceea94d6f10eeb5b41dc2391c6c8bf8e734ef +Subproject commit f73c73d2018eb6a111f35e4dae7b4f27401e9421 diff --git a/test/integration/CoreRegistration.t.sol b/test/integration/CoreRegistration.t.sol index c655b4e2..655ddd6b 100644 --- a/test/integration/CoreRegistration.t.sol +++ b/test/integration/CoreRegistration.t.sol @@ -6,6 +6,7 @@ import { AVSDirectory } from "eigenlayer-contracts/src/contracts/core/AVSDirecto import { IAVSDirectory } from "eigenlayer-contracts/src/contracts/interfaces/IAVSDirectory.sol"; import { DelegationManager } from "eigenlayer-contracts/src/contracts/core/DelegationManager.sol"; import { IDelegationManager } from "eigenlayer-contracts/src/contracts/interfaces/IDelegationManager.sol"; +import { IAVSDirectory } from "eigenlayer-contracts/src/contracts/interfaces/IAVSDirectory.sol"; contract Test_CoreRegistration is MockAVSDeployer { // Contracts