Skip to content

Commit d13239d

Browse files
aehyvariaehyvari
committed
test: Certora specs for redistribution
1 parent 4c928cf commit d13239d

23 files changed

+1085
-274
lines changed

‎.github/workflows/certora-prover.yml‎

Lines changed: 12 additions & 100 deletions
Original file line numberDiff line numberDiff line change
@@ -1,122 +1,35 @@
11
name: Certora
22

33
on:
4-
# Run when PRs from feat/* branches are merged into dev
54
pull_request:
6-
types: [closed]
75
branches:
8-
- main
9-
10-
# Run on any pushes to certora/* branches
11-
push:
12-
branches:
13-
- 'certora/**'
14-
15-
# Biweekly schedule (1st and 15th of each month at midnight UTC)
16-
schedule:
17-
- cron: '0 0 1,15 * *'
18-
19-
# Manual trigger
6+
- certora/distro
207
workflow_dispatch:
218

229
jobs:
23-
# First job: Compile the contracts for Certora verification
24-
compile:
25-
name: Compile
26-
# Run if it meets one of these conditions:
27-
# 1. It's a merged PR from a feat/* branch to dev
28-
# 2. It's a push to a certora/* branch
29-
# 3. It's a scheduled run
30-
# 4. It's a manually triggered run
31-
if: >
32-
(github.event_name == 'pull_request' &&
33-
github.event.pull_request.merged == true &&
34-
startsWith(github.head_ref, 'feat/')) ||
35-
(github.event_name == 'push' &&
36-
startsWith(github.ref, 'refs/heads/certora/')) ||
37-
github.event_name == 'schedule' ||
38-
github.event_name == 'workflow_dispatch'
39-
runs-on: protocol-x64-16core
40-
steps:
41-
# Checkout the repository with submodules
42-
- uses: actions/checkout@v4
43-
with:
44-
submodules: recursive
45-
# Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
46-
ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
47-
48-
# Install the Foundry toolchain
49-
- name: Install Foundry
50-
uses: foundry-rs/foundry-toolchain@v1
51-
with:
52-
version: stable
53-
54-
# Install dependencies using Forge
55-
- name: Install forge dependencies
56-
run: forge install
57-
58-
# Run Certora compilation step only
59-
- uses: Certora/certora-run-action@v1
60-
with:
61-
# List of configuration files for different contracts to verify
62-
configurations: |-
63-
certora/confs/core/AllocationManager.conf
64-
certora/confs/core/AllocationManagerSanity.conf
65-
certora/confs/core/DelegationManager.conf
66-
certora/confs/core/DelegationManagerValidState.conf
67-
certora/confs/core/StrategyManager.conf
68-
certora/confs/permissions/Pausable.conf
69-
certora/confs/pods/EigenPodManagerRules.conf
70-
certora/confs/strategies/StrategyBase.conf
71-
use-beta: true
72-
solc-versions: 0.8.27
73-
solc-remove-version-prefix: "0."
74-
job-name: "Eigenlayer Contracts"
75-
certora-key: ${{ secrets.CERTORAKEY }}
76-
# Only compile, don't run verification yet
77-
compilation-steps-only: true
78-
env:
79-
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
80-
81-
# Second job: Run the actual verification after compilation succeeds
82-
verify:
83-
name: Verify
84-
runs-on: protocol-x64-16core
85-
# This job depends on the compile job
86-
needs: compile
87-
# Same conditions as the compile job
88-
if: >
89-
(github.event_name == 'pull_request' &&
90-
github.event.pull_request.merged == true &&
91-
startsWith(github.head_ref, 'feat/')) ||
92-
(github.event_name == 'push' &&
93-
startsWith(github.ref, 'refs/heads/certora/')) ||
94-
github.event_name == 'schedule' ||
95-
github.event_name == 'workflow_dispatch'
10+
certora_run:
11+
runs-on: ubuntu-latest
12+
permissions:
13+
contents: read
14+
statuses: write
15+
pull-requests: write
9616
steps:
97-
# Checkout the repository with submodules
98-
- uses: actions/checkout@v4
17+
- name: Checkout repository
18+
uses: actions/checkout@v4
9919
with:
10020
submodules: recursive
101-
# Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
102-
ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
103-
104-
# Install the Foundry toolchain.
10521
- name: Install Foundry
10622
uses: foundry-rs/foundry-toolchain@v1
10723
with:
10824
version: stable
109-
110-
# Install dependencies using Forge
11125
- name: Install forge dependencies
11226
run: forge install
113-
114-
# Run Certora verification with the same configurations
115-
- uses: Certora/certora-run-action@v1
27+
- name: Run Certora pipeline
28+
uses: Certora/certora-run-action@v1
11629
with:
117-
# List of configuration files for different contracts to verify
11830
configurations: |-
11931
certora/confs/core/AllocationManager.conf
32+
certora/confs/core/AllocationManagerValidState.conf
12033
certora/confs/core/AllocationManagerSanity.conf
12134
certora/confs/core/DelegationManager.conf
12235
certora/confs/core/DelegationManagerValidState.conf
@@ -126,7 +39,6 @@ jobs:
12639
certora/confs/strategies/StrategyBase.conf
12740
use-beta: true
12841
solc-versions: 0.8.27
129-
solc-remove-version-prefix: "0."
13042
job-name: "Eigenlayer Contracts"
13143
certora-key: ${{ secrets.CERTORAKEY }}
13244
env:

‎certora/confs/core/AllocationManager.conf‎

Lines changed: 17 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
{
22
"assert_autofinder_success": true,
33
"files": [
4-
"src/contracts/core/AllocationManager.sol",
4+
"certora/harnesses/AllocationManagerHarness.sol",
55
"src/contracts/permissions/PauserRegistry.sol",
66
"src/contracts/permissions/PermissionController.sol",
77
"src/contracts/core/DelegationManager.sol",
@@ -10,19 +10,19 @@
1010
"src/contracts/strategies/StrategyBase.sol",
1111
"certora/mocks/CertoraAVSRegistrar.sol",
1212
"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
13-
"src/contracts/libraries/OperatorSetLib.sol"
14-
],
15-
"java_args": [
13+
"src/contracts/libraries/OperatorSetLib.sol",
14+
"certora/harnesses/ShortStringsUpgradeableHarness.sol",
1615
],
16+
"java_args": [],
1717
"link": [
18-
"AllocationManager:pauserRegistry=PauserRegistry",
18+
"AllocationManagerHarness:pauserRegistry=PauserRegistry",
1919
"DelegationManager:permissionController=PermissionController",
20-
"DelegationManager:allocationManager=AllocationManager",
21-
"AllocationManager:permissionController=PermissionController",
20+
"DelegationManager:allocationManager=AllocationManagerHarness",
21+
"AllocationManagerHarness:permissionController=PermissionController",
2222
"DelegationManager:strategyManager=StrategyManager",
23-
"AllocationManager:delegation=DelegationManager",
23+
"AllocationManagerHarness:delegation=DelegationManager",
2424
"EigenPodManager:delegationManager=DelegationManager",
25-
"DelegationManager:eigenPodManager=EigenPodManager"
25+
"DelegationManager:eigenPodManager=EigenPodManager",
2626
],
2727
"loop_iter": "1",
2828
"optimistic_fallback": true,
@@ -32,14 +32,18 @@
3232
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
3333
],
3434
"parametric_contracts": [
35-
"AllocationManager"
35+
"AllocationManagerHarness"
3636
],
37+
"msg": "AllocationManager Rules",
3738
"process": "emv",
3839
"prover_args": [
39-
" -recursionErrorAsAssert false -recursionEntryLimit 3"
40+
"-recursionErrorAsAssert false -recursionEntryLimit 3",
41+
"-splitParallel true",
42+
"-dontStopAtFirstSplitTimeout true",
4043
],
41-
"solc": "solc8.27",
4244
"solc_optimize": "1",
43-
"verify": "AllocationManager:certora/specs/core/AllocationManagerRules.spec",
45+
"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
4446
"server": "production",
47+
"rule_sanity": "basic",
48+
"build_cache": true
4549
}

‎certora/confs/core/AllocationManagerSanity.conf‎

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
{
22
"assert_autofinder_success": true,
33
"files": [
4-
"src/contracts/core/AllocationManager.sol",
4+
"certora/harnesses/AllocationManagerHarness.sol",
55
"src/contracts/permissions/PauserRegistry.sol",
66
"src/contracts/permissions/PermissionController.sol",
77
"src/contracts/core/DelegationManager.sol",
@@ -12,17 +12,16 @@
1212
"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
1313
"src/contracts/libraries/OperatorSetLib.sol"
1414
],
15-
"java_args": [
16-
],
15+
"java_args": [],
1716
"link": [
18-
"AllocationManager:pauserRegistry=PauserRegistry",
17+
"AllocationManagerHarness:pauserRegistry=PauserRegistry",
1918
"DelegationManager:permissionController=PermissionController",
20-
"DelegationManager:allocationManager=AllocationManager",
21-
"AllocationManager:permissionController=PermissionController",
19+
"DelegationManager:allocationManager=AllocationManagerHarness",
20+
"AllocationManagerHarness:permissionController=PermissionController",
2221
"DelegationManager:strategyManager=StrategyManager",
23-
"AllocationManager:delegation=DelegationManager",
22+
"AllocationManagerHarness:delegation=DelegationManager",
2423
"EigenPodManager:delegationManager=DelegationManager",
25-
"DelegationManager:eigenPodManager=EigenPodManager"
24+
"DelegationManager:eigenPodManager=EigenPodManager",
2625
],
2726
"loop_iter": "2",
2827
"optimistic_fallback": true,
@@ -32,14 +31,14 @@
3231
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
3332
],
3433
"parametric_contracts": [
35-
"AllocationManager"
34+
"AllocationManagerHarness"
3635
],
3736
"process": "emv",
3837
"prover_args": [
3938
" -recursionErrorAsAssert false -recursionEntryLimit 3"
4039
],
41-
"solc": "solc8.27",
4240
"solc_optimize": "1",
4341
"solc_via_ir": true,
44-
"verify": "AllocationManager:certora/specs/core/AllocationManagerSanity.spec"
42+
"server": "production",
43+
"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerSanity.spec"
4544
}

‎certora/confs/core/AllocationManagerValidState.conf‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
{
2+
"assert_autofinder_success": true,
3+
"files": [
4+
"certora/harnesses/AllocationManagerHarness.sol",
5+
"src/contracts/permissions/PauserRegistry.sol",
6+
"src/contracts/permissions/PermissionController.sol",
7+
"src/contracts/core/DelegationManager.sol",
8+
"src/contracts/pods/EigenPodManager.sol",
9+
"src/contracts/core/StrategyManager.sol",
10+
"src/contracts/strategies/StrategyBase.sol",
11+
"certora/mocks/CertoraAVSRegistrar.sol",
12+
"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
13+
"src/contracts/libraries/OperatorSetLib.sol"
14+
],
15+
"java_args": [],
16+
"link": [
17+
"AllocationManagerHarness:pauserRegistry=PauserRegistry",
18+
"DelegationManager:permissionController=PermissionController",
19+
"DelegationManager:allocationManager=AllocationManagerHarness",
20+
"AllocationManagerHarness:permissionController=PermissionController",
21+
"DelegationManager:strategyManager=StrategyManager",
22+
"AllocationManagerHarness:delegation=DelegationManager",
23+
"EigenPodManager:delegationManager=DelegationManager",
24+
"DelegationManager:eigenPodManager=EigenPodManager",
25+
],
26+
"loop_iter": "1",
27+
"optimistic_fallback": true,
28+
"optimistic_loop": true,
29+
"packages": [
30+
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
31+
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
32+
],
33+
"parametric_contracts": [
34+
"AllocationManagerHarness"
35+
],
36+
"process": "emv",
37+
"msg": "AllocationManager Valid State Invariants",
38+
"prover_args": [
39+
" -recursionErrorAsAssert false -recursionEntryLimit 3"
40+
],
41+
"solc_optimize": "1",
42+
"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerValidState.spec",
43+
"rule_sanity": "basic",
44+
"server": "production",
45+
}

‎certora/confs/core/DelegationManager.conf‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
"src/contracts/strategies/StrategyBase.sol",
1010
"src/contracts/core/StrategyManager.sol",
1111
"src/contracts/permissions/PauserRegistry.sol",
12-
"src/contracts/core/DelegationManager.sol",
1312
"src/contracts/permissions/PermissionController.sol",
1413
"src/contracts/core/AllocationManager.sol"
1514
],
@@ -20,7 +19,7 @@
2019
"AllocationManager:permissionController=PermissionController",
2120
"DelegationManagerHarness:strategyManager=StrategyManager",
2221
"EigenPodManager:delegationManager=DelegationManagerHarness",
23-
"DelegationManagerHarness:eigenPodManager=EigenPodManager"
22+
"DelegationManagerHarness:eigenPodManager=EigenPodManager",
2423
],
2524
"loop_iter": "2",
2625
"optimistic_fallback": true,
@@ -34,6 +33,7 @@
3433
"-tinyTimeout 20",
3534
"-depth 20"
3635
],
36+
"msg": "DelegationManager Rules",
3737
"packages": [
3838
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
3939
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
@@ -43,8 +43,9 @@
4343
],
4444
"rule_sanity": "basic",
4545
"process": "emv",
46-
"solc": "solc8.27",
4746
"solc_optimize": "1",
4847
"solc_via_ir": true,
48+
"build_cache": true,
49+
"server": "production",
4950
"verify": "DelegationManagerHarness:certora/specs/core/DelegationManager.spec"
5051
}

‎certora/confs/core/DelegationManagerValidState.conf‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,9 @@
99
"src/contracts/strategies/StrategyBase.sol",
1010
"src/contracts/core/StrategyManager.sol",
1111
"src/contracts/permissions/PauserRegistry.sol",
12-
"src/contracts/core/DelegationManager.sol",
1312
"src/contracts/permissions/PermissionController.sol",
14-
"src/contracts/core/AllocationManager.sol"
13+
"src/contracts/core/AllocationManager.sol",
14+
"certora/mocks/CertoraAVSRegistrar.sol",
1515
],
1616
"link": [
1717
"AllocationManager:delegation=DelegationManagerHarness",
@@ -20,7 +20,7 @@
2020
"AllocationManager:permissionController=PermissionController",
2121
"DelegationManagerHarness:strategyManager=StrategyManager",
2222
"EigenPodManager:delegationManager=DelegationManagerHarness",
23-
"DelegationManagerHarness:eigenPodManager=EigenPodManager"
23+
"DelegationManagerHarness:eigenPodManager=EigenPodManager",
2424
],
2525
"loop_iter": "1",
2626
"optimistic_fallback": true,
@@ -31,13 +31,15 @@
3131
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
3232
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
3333
],
34+
"msg": "DelegationManager Valid State Invariants",
3435
"parametric_contracts": [
35-
"DelegationManagerHarness"
36+
"DelegationManagerHarness",
3637
],
37-
"rule_sanity": "basic",
38+
"rule_sanity": "basic",
3839
"process": "emv",
39-
"solc": "solc8.27",
4040
"solc_optimize": "1",
4141
"solc_via_ir": true,
42+
"build_cache": true,
43+
"server": "production",
4244
"verify": "DelegationManagerHarness:certora/specs/core/DelegationManagerValidState.spec"
4345
}

0 commit comments

Comments
 (0)