test: Certora prover specs and CI

.github/workflows/certora-prover.yml

@@ -0,0 +1,75 @@
+name: Certora Prover Workflow
+
+on:
+  push:
+    branches:
+      - dev
+  pull_request:
+    branches:
+      - dev
+  workflow_dispatch:
+
+jobs:
+  compile:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: stable
+      - name: Install forge dependencies
+        run: forge install
+      - uses: Certora/certora-run-action@v1
+        with:
+          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 }}
+          compilation-steps-only: true
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+  verify:
+    runs-on: ubuntu-latest
+    needs: compile
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+      - name: Install forge dependencies
+        run: forge install
+      - uses: Certora/certora-run-action@v1
+        with:
+          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 }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -50,4 +50,7 @@ surya_report.md
 
 *state.json
 deployed_strategies.json
-populate_src*
+populate_src*
+
+# cerota
+.certora_internal/*

certora/.bin/verify.sh

@@ -0,0 +1,75 @@
+#!/bin/bash
+#
+# This script should not be run directly but instead through a link
+#
+
+usage="$0 [-hd] [-f '<fun1> <fun2> ...'] [-l <bytes>] [<msg>] [<rule>]"
+
+usage_long="\
+Script for verifying contracts.\n\
+\n\
+ -h|--help        Print this message and exit\n\
+ -d|--dev         Use dev mode: send to staging and run on master using
+                  certoraRun.py\n\
+ -f|--functions   Verify the listed functions only (for parametric rules)\n\
+ -l|--hash-length hash bound length in bytes\n\
+"
+
+script=$0
+
+scriptDir=$(cd $(dirname $script); pwd)
+scriptName=$(basename $0 .sh)
+contractName=$(echo $scriptName |sed 's/^verify//g')
+module=$(basename $scriptDir)
+projectBase=$scriptDir/../../..
+confDir=$projectBase/certora/confs/$module
+
+devFlags=""
+certoraRun="certoraRun"
+
+while [ $# -gt 0 ]; do
+    case $1 in
+        -h|--help)
+            printf -- "${usage_long}\nIn summary:\n\n  $usage\n\n"
+            exit 1
+            ;;
+        -d|--dev)
+            devFlags="--server staging --commit_sha1 d6b1d13a2e01dda0b070d7c12a94f3d4bf27885c" # 7.25.2
+            certoraRun=certoraRun.py
+            ;;
+        -f|--functions)
+            methods=$2;
+            shift
+            ;;
+        -l|--hash-length)
+            hashLength=$2;
+            shift
+            ;;
+        -*)
+            echo "Error: invalid option '$1'"
+            exit 1
+            ;;
+        *)
+            break
+    esac
+    shift;
+done
+
+ARGS=
+
+if [[ "$2" ]]; then
+    ARGS+="--rule $2"
+fi
+
+if [[ $methods ]]; then
+    ARGS+=" --method $methods"
+fi
+
+if [[ $hashLength ]]; then
+    ARGS+=" --hashing_length_bound $hashLength"
+fi
+
+(
+  cd $projectBase
+  $certoraRun $confDir/$contractName.conf $ARGS --msg "$contractName $1 $2" $devFlags
+)

certora/confs/core/AllocationManager.conf

@@ -0,0 +1,45 @@
+{
+    "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"
+    ],
+    "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",
+}

certora/confs/core/AllocationManagerSanity.conf

@@ -0,0 +1,45 @@
+{
+    "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"
+    ],
+    "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": "2",
+    "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",
+    "solc_via_ir": true,
+    "verify": "AllocationManager:certora/specs/core/AllocationManagerSanity.spec"
+}

certora/confs/core/DelegationManager.conf

@@ -0,0 +1,50 @@
+{
+    "files": [
+        "certora/harnesses/DelegationManagerHarness.sol",
+        "certora/harnesses/ShortStringsUpgradeableHarness.sol",
+        "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
+        "lib/openzeppelin-contracts-v4.9.0/contracts/mocks/ERC1271WalletMock.sol",
+        "src/contracts/pods/EigenPodManager.sol",
+        "src/contracts/pods/EigenPod.sol",
+        "src/contracts/strategies/StrategyBase.sol",
+        "src/contracts/core/StrategyManager.sol",
+        "src/contracts/permissions/PauserRegistry.sol",
+        "src/contracts/core/DelegationManager.sol",
+        "src/contracts/permissions/PermissionController.sol",
+        "src/contracts/core/AllocationManager.sol"
+    ],
+    "link": [
+        "AllocationManager:delegation=DelegationManagerHarness",
+        "DelegationManagerHarness:permissionController=PermissionController",
+        "DelegationManagerHarness:allocationManager=AllocationManager",
+        "AllocationManager:permissionController=PermissionController",
+        "DelegationManagerHarness:strategyManager=StrategyManager",
+        "EigenPodManager:delegationManager=DelegationManagerHarness",
+        "DelegationManagerHarness:eigenPodManager=EigenPodManager"
+    ],
+    "loop_iter": "2",
+    "optimistic_fallback": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "320",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-destructiveOptimizations twostage",
+        "-mediumTimeout 20",
+        "-lowTimeout 20",
+        "-tinyTimeout 20",
+        "-depth 20"
+    ],
+    "packages": [
+        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
+        "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
+    ],
+    "parametric_contracts": [
+        "DelegationManagerHarness"
+    ],
+    "rule_sanity": "basic",
+    "process": "emv",
+    "solc": "solc8.27",
+    "solc_optimize": "1",
+    "solc_via_ir": true,
+    "verify": "DelegationManagerHarness:certora/specs/core/DelegationManager.spec"
+}

certora/confs/core/DelegationManagerValidState.conf

@@ -0,0 +1,43 @@
+{
+    "files": [
+        "certora/harnesses/DelegationManagerHarness.sol",
+        "certora/harnesses/ShortStringsUpgradeableHarness.sol",
+        "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
+        "lib/openzeppelin-contracts-v4.9.0/contracts/mocks/ERC1271WalletMock.sol",
+        "src/contracts/pods/EigenPodManager.sol",
+        "src/contracts/pods/EigenPod.sol",
+        "src/contracts/strategies/StrategyBase.sol",
+        "src/contracts/core/StrategyManager.sol",
+        "src/contracts/permissions/PauserRegistry.sol",
+        "src/contracts/core/DelegationManager.sol",
+        "src/contracts/permissions/PermissionController.sol",
+        "src/contracts/core/AllocationManager.sol"
+    ],
+    "link": [
+        "AllocationManager:delegation=DelegationManagerHarness",
+        "DelegationManagerHarness:permissionController=PermissionController",
+        "DelegationManagerHarness:allocationManager=AllocationManager",
+        "AllocationManager:permissionController=PermissionController",
+        "DelegationManagerHarness:strategyManager=StrategyManager",
+        "EigenPodManager:delegationManager=DelegationManagerHarness",
+        "DelegationManagerHarness:eigenPodManager=EigenPodManager"
+    ],
+    "loop_iter": "1",
+    "optimistic_fallback": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "320",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
+        "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
+    ],
+    "parametric_contracts": [
+        "DelegationManagerHarness"
+    ],
+   "rule_sanity": "basic",
+    "process": "emv",
+    "solc": "solc8.27",
+    "solc_optimize": "1",
+    "solc_via_ir": true,
+    "verify": "DelegationManagerHarness:certora/specs/core/DelegationManagerValidState.spec"
+}

certora/confs/core/StrategyManager.conf

@@ -0,0 +1,37 @@
+{
+    "files": [
+        "certora/harnesses/ShortStringsUpgradeableHarness.sol",
+        "certora/harnesses/StrategyManagerHarness.sol",
+        "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
+        "lib/openzeppelin-contracts-v4.9.0/contracts/mocks/ERC1271WalletMock.sol",
+        "src/contracts/pods/EigenPodManager.sol",
+        "src/contracts/pods/EigenPod.sol",
+        "src/contracts/strategies/StrategyBase.sol",
+        "src/contracts/core/DelegationManager.sol",
+        "src/contracts/permissions/PauserRegistry.sol",
+        "src/contracts/core/AllocationManager.sol"
+    ],
+    "link": [
+        "DelegationManager:allocationManager=AllocationManager",
+        "DelegationManager:eigenPodManager=EigenPodManager",
+        "StrategyManagerHarness:delegation=DelegationManager"
+    ],
+    "loop_iter": "2",
+    "optimistic_fallback": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "320",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
+        "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
+    ],
+    "parametric_contracts": [
+        "StrategyManagerHarness"
+    ],
+    "process": "emv",
+    "solc": "solc8.27",
+    "solc_optimize": "1",
+    "solc_via_ir": true,
+    "verify": "StrategyManagerHarness:certora/specs/core/StrategyManager.spec",
+    "rule_sanity": "basic"
+}