feat: updated certora rules

.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) }}

.gitignore

@@ -12,5 +12,8 @@ node_modules/
 # Dotenv file
 .env
 
+# Certora Outputs
+.certora_internal/
+.certora_recent_jobs.json
 
 *.DS_Store

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"
+}

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];
+    }
+}

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];
+    }
+}

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);
+    }
+}

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];
+    }
+}