Multichain setup

Fix path to base conf

Fix paths

Run CI on PRs against eigenlayer/multichain

Link to PauserRegistry in OperatorTableUpdater

Link OperatorTableUpdater to BN254CertificateVerifier

Remove unneeded external wildcard summary for a library with only internal functions

Use Johannes' branch

Refactor the AI specs

Summarize hashToG1, add disale assumeFPStrictlyMonotonic

Refactor AI rules from KeyRegistrar

Remove unnecessary summarization from BN254

Summarize ECDSA _parseSignatures

Switch to master to get all latest fixes

Disable FP monotonicity assumption for now

Switch to eric's fix branch, enable FP monotonicity assumption

Switch to master since eric's branch is merged

Try running without master

initial changes

KeyRegistrar specs

CI setup

multichain rules

Clean the base conf

Keep confs as real jsons

More cleanup on confs

- Remove solc key from confs since everything uses solc-0.8.27
- Unify indentations (4 spaces)
- Unify empty lists (inline)

Remove the empty certora workflow

CI setup path fix

fix compilation error strategyManagerHarness

CI failures fixed

StrategyManager rule adjusted to code

Trigger CI for PRs on eigenlayer/multichain

certora prover workflow for local branch

CI setup

CI

rules updated acc. to code

final adaptations multichain rules

added allocation managers rules from distro project

smt timeout increased on timeout

timeout args changed

overslashing rules

Author: aehyvari

.github/workflows/certora-prover.yml

@@ -1,141 +1,45 @@
-name: Certora
-
 on:
-  # Run when PRs from feat/* branches are merged into dev
   pull_request:
-    types: [closed]
     branches:
       - main
-  
-  # Run on any pushes to certora/* branches
-  push:
-    branches:
-      - 'certora/**'
-  
-  # Biweekly schedule (1st and 15th of each month at midnight UTC)
-  schedule:
-    - cron: '0 0 1,15 * *'
-  
-  # Manual trigger
   workflow_dispatch:
 
 jobs:
-  # First job: Compile the contracts for Certora verification
-  compile:
-    name: Compile
-    # Run if it meets one of these conditions:
-    # 1. It's a merged PR from a feat/* branch to dev
-    # 2. It's a push to a certora/* branch
-    # 3. It's a scheduled run
-    # 4. It's a manually triggered run
-    if: >
-      (github.event_name == 'pull_request' && 
-       github.event.pull_request.merged == true && 
-       startsWith(github.head_ref, 'feat/')) || 
-      (github.event_name == 'push' && 
-       startsWith(github.ref, 'refs/heads/certora/')) ||
-      github.event_name == 'schedule' || 
-      github.event_name == 'workflow_dispatch'
-    runs-on: protocol-x64-16core
+  certora_run_submission:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
     steps:
-      - uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911
-        with:
-          egress-policy: audit
-
-      # Checkout the repository with submodules
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+      - name: Checkout repository
+        uses: actions/checkout@v4
         with:
           submodules: recursive
-          # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
-          ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
-
-      # Install the Foundry toolchain
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de
-        with:
-          version: stable
-
-      # Install dependencies using Forge
-      - name: Install forge dependencies
-        run: forge install
-
-      # Run Certora compilation step only
-      - uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc
-        with:
-          # List of configuration files for different contracts to verify
-          configurations: |-
-            certora/confs/core/AllocationManager.conf
-            certora/confs/core/AllocationManagerSanity.conf
-            certora/confs/core/DelegationManager.conf
-            certora/confs/core/DelegationManagerValidState.conf
-            certora/confs/core/StrategyManager.conf
-            certora/confs/permissions/Pausable.conf
-            certora/confs/pods/EigenPodManagerRules.conf
-            certora/confs/strategies/StrategyBase.conf
-          use-beta: true
-          solc-versions: 0.8.27
-          solc-remove-version-prefix: "0."
-          job-name: "Eigenlayer Contracts"
-          certora-key: ${{ secrets.CERTORAKEY }}
-          # Only compile, don't run verification yet
-          compilation-steps-only: true
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-  # Second job: Run the actual verification after compilation succeeds
-  verify:
-    name: Verify
-    runs-on: protocol-x64-16core
-    # This job depends on the compile job
-    needs: compile
-    # Same conditions as the compile job
-    if: >
-      (github.event_name == 'pull_request' && 
-       github.event.pull_request.merged == true && 
-       startsWith(github.head_ref, 'feat/')) || 
-      (github.event_name == 'push' && 
-       startsWith(github.ref, 'refs/heads/certora/')) ||
-      github.event_name == 'schedule' || 
-      github.event_name == 'workflow_dispatch'
-    steps:
-      - uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911
-        with:
-          egress-policy: audit
-
-      # Checkout the repository with submodules
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
-        with:
-          submodules: recursive
-          # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
-          ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
-          
-      # Install the Foundry toolchain.
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de
-        with:
-          version: stable
-
-      # Install dependencies using Forge
-      - name: Install forge dependencies
-        run: forge install
 
-      # Run Certora verification with the same configurations
-      - uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc
+      - name: Submit verification jobs to Certora Prover
+        uses: Certora/certora-run-action@v2
         with:
           # List of configuration files for different contracts to verify
           configurations: |-
+            certora/confs/multichain/CrossChainRegistry.conf
+            certora/confs/multichain/KeyRegistrar.conf
+            certora/confs/multichain/OperatorTableUpdater.conf
+            certora/confs/multichain/ECDSACertificateVerifier.conf
+            certora/confs/multichain/BN254CertificateVerifier.conf
             certora/confs/core/AllocationManager.conf
+            certora/confs/core/AllocationManagerOverslashing.conf
+            certora/confs/core/AllocationManagerValidState.conf
             certora/confs/core/AllocationManagerSanity.conf
             certora/confs/core/DelegationManager.conf
             certora/confs/core/DelegationManagerValidState.conf
             certora/confs/core/StrategyManager.conf
             certora/confs/permissions/Pausable.conf
             certora/confs/pods/EigenPodManagerRules.conf
             certora/confs/strategies/StrategyBase.conf
-          use-beta: true
           solc-versions: 0.8.27
-          solc-remove-version-prefix: "0."
-          job-name: "Eigenlayer Contracts"
+          job-name: "Verified Rules"
           certora-key: ${{ secrets.CERTORAKEY }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora.yml

@@ -1,45 +1,56 @@
 {
-    "assert_autofinder_success": true,
-    "files": [
-        "src/contracts/core/AllocationManager.sol",
-        "src/contracts/permissions/PauserRegistry.sol",
-        "src/contracts/permissions/PermissionController.sol",
-        "src/contracts/core/DelegationManager.sol",
-        "src/contracts/pods/EigenPodManager.sol",
-        "src/contracts/core/StrategyManager.sol",
-        "src/contracts/strategies/StrategyBase.sol",
-        "certora/mocks/CertoraAVSRegistrar.sol",
-        "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
-        "src/contracts/libraries/OperatorSetLib.sol"
+	"assert_autofinder_success": true,
+	// "build_cache": true,
+	"files": [
+		"certora/harnesses/AllocationManagerHarness.sol",
+		"src/contracts/permissions/PauserRegistry.sol",
+		"src/contracts/permissions/PermissionController.sol",
+		"src/contracts/core/DelegationManager.sol",
+		"src/contracts/pods/EigenPodManager.sol",
+		"src/contracts/core/StrategyManager.sol",
+		"src/contracts/strategies/StrategyBase.sol",
+		"certora/mocks/CertoraAVSRegistrar.sol",
+		"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
+		"src/contracts/libraries/OperatorSetLib.sol",
+		"certora/harnesses/ShortStringsUpgradeableHarness.sol"
+	],
+	"java_args": [],
+	"link": [
+		"AllocationManagerHarness:pauserRegistry=PauserRegistry",
+		"DelegationManager:permissionController=PermissionController",
+		"DelegationManager:allocationManager=AllocationManagerHarness",
+		"AllocationManagerHarness:permissionController=PermissionController",
+		"DelegationManager:strategyManager=StrategyManager",
+		"AllocationManagerHarness:delegation=DelegationManager",
+		"EigenPodManager:delegationManager=DelegationManager",
+		"DelegationManager:eigenPodManager=EigenPodManager"
+	],
+	"loop_iter": "1",
+	"msg": "AllocationManager",
+	"optimistic_fallback": true,
+	"optimistic_loop": true,
+	"packages": [
+		"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
+		"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
+	],
+	"parametric_contracts": [
+		"AllocationManagerHarness"
+	],
+    "rule": [
+        "pendingDiffStateTransitions",
+        "pendingDiffStateTransitionModifyAllocations",
+        "redistributionRecipientCannotBeDeadAddress"
     ],
-    "java_args": [
-    ],
-    "link": [
-        "AllocationManager:pauserRegistry=PauserRegistry",
-        "DelegationManager:permissionController=PermissionController",
-        "DelegationManager:allocationManager=AllocationManager",
-        "AllocationManager:permissionController=PermissionController",
-        "DelegationManager:strategyManager=StrategyManager",
-        "AllocationManager:delegation=DelegationManager",
-        "EigenPodManager:delegationManager=DelegationManager",
-        "DelegationManager:eigenPodManager=EigenPodManager"
-    ],
-    "loop_iter": "1",
-    "optimistic_fallback": true,
-    "optimistic_loop": true,
-    "packages": [
-        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
-        "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
-    ],
-    "parametric_contracts": [
-        "AllocationManager"
-    ],
-    "process": "emv",
-    "prover_args": [
-        " -recursionErrorAsAssert false -recursionEntryLimit 3"
-    ],
-    "solc": "solc8.27",
-    "solc_optimize": "1",
-    "verify": "AllocationManager:certora/specs/core/AllocationManagerRules.spec",
-    "server": "production",
-}
+	"process": "emv",
+	"prover_args": [
+		"-recursionErrorAsAssert false -recursionEntryLimit 3",
+		"-splitParallel true",
+		"-dontStopAtFirstSplitTimeout true"
+	],
+	"rule_sanity": "basic",
+	"server": "production",
+    // "solc_via_ir": true,
+	"solc_optimize": "1",
+	"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
+	"wait_for_results": "none"
+}

certora/confs/core/AllocationManager.conf

@@ -0,0 +1,62 @@
+{
+	// "build_cache": true,
+	"files": [
+		"certora/harnesses/AllocationManagerHarness.sol",
+		"src/contracts/permissions/PauserRegistry.sol",
+		"src/contracts/permissions/PermissionController.sol",
+		"src/contracts/core/DelegationManager.sol",
+		"src/contracts/pods/EigenPodManager.sol",
+		"src/contracts/core/StrategyManager.sol",
+		"src/contracts/strategies/StrategyBase.sol",
+		"certora/mocks/CertoraAVSRegistrar.sol",
+		"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
+		"src/contracts/libraries/OperatorSetLib.sol",
+		"certora/harnesses/ShortStringsUpgradeableHarness.sol"
+	],
+	"java_args": [],
+	"link": [
+		"AllocationManagerHarness:pauserRegistry=PauserRegistry",
+		"DelegationManager:permissionController=PermissionController",
+		"DelegationManager:allocationManager=AllocationManagerHarness",
+		"AllocationManagerHarness:permissionController=PermissionController",
+		"DelegationManager:strategyManager=StrategyManager",
+		"AllocationManagerHarness:delegation=DelegationManager",
+		"EigenPodManager:delegationManager=DelegationManager",
+		"DelegationManager:eigenPodManager=EigenPodManager"
+	],
+	"loop_iter": "1",
+	"msg": "AllocationManager No Overslashing",
+	"optimistic_fallback": true,
+	"optimistic_loop": true,
+	"packages": [
+		"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
+		"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
+	],
+	"parametric_contracts": [
+		"AllocationManagerHarness"
+	],
+    "rule": [
+        "noOverslashingOfShares",
+		"noOverslashingOfOperatorShares",
+		"overslashingOfSharesAtMostOne",
+    ],
+	"process": "emv",
+	"prover_args": [
+		"-recursionErrorAsAssert",
+		"false",
+		"-recursionEntryLimit",
+		"3",
+		"-dontStopAtFirstSplitTimeout",
+		"true",
+		"-split",
+		"false"
+	],
+	"smt_timeout": "7200",
+	"rule_sanity": "basic",
+	"server": "production",
+    "solc_via_ir": true,
+	"solc_optimize": "1",
+	"disable_solc_optimizers": ["cse" , "peephole"],
+	"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
+	"wait_for_results": "none"
+}