Skip to content

Commit 703f890

Browse files
aehyvariaehyvari
committed
Certora formal verification specifications and CI
1 parent 0fb74c2 commit 703f890

37 files changed

+2244
-243
lines changed

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

Lines changed: 29 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -6,37 +6,43 @@ on:
66
types: [closed]
77
branches:
88
- main
9-
9+
1010
# Run on any pushes to certora/* branches
1111
push:
1212
branches:
1313
- 'certora/**'
14-
14+
1515
# Biweekly schedule (1st and 15th of each month at midnight UTC)
1616
schedule:
1717
- cron: '0 0 1,15 * *'
18-
18+
1919
# Manual trigger
2020
workflow_dispatch:
2121

2222
jobs:
23-
# First job: Compile the contracts for Certora verification
24-
compile:
25-
name: Compile
23+
# Compile the contracts and run verification
24+
compile_and_verify:
25+
name: Compile and verify
2626
# Run if it meets one of these conditions:
2727
# 1. It's a merged PR from a feat/* branch to dev
2828
# 2. It's a push to a certora/* branch
2929
# 3. It's a scheduled run
3030
# 4. It's a manually triggered run
3131
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' &&
32+
(github.event_name == 'pull_request' &&
33+
github.event.pull_request.merged == true &&
34+
startsWith(github.head_ref, 'feat/')) ||
35+
(github.event_name == 'push' &&
3636
startsWith(github.ref, 'refs/heads/certora/')) ||
37-
github.event_name == 'schedule' ||
37+
github.event_name == 'schedule' ||
3838
github.event_name == 'workflow_dispatch'
39-
runs-on: protocol-x64-16core
39+
runs-on: ubuntu-latest
40+
# runs-on: protocol-x64-16core
41+
permissions:
42+
contents: read
43+
statuses: write
44+
pull-requests: write
45+
id-token: write
4046
steps:
4147
- uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911
4248
with:
@@ -49,93 +55,29 @@ jobs:
4955
# Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
5056
ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
5157

52-
# Install the Foundry toolchain
53-
- name: Install Foundry
54-
uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de
55-
with:
56-
version: stable
57-
58-
# Install dependencies using Forge
59-
- name: Install forge dependencies
60-
run: forge install
61-
62-
# Run Certora compilation step only
63-
- uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc
64-
with:
65-
# List of configuration files for different contracts to verify
66-
configurations: |-
67-
certora/confs/core/AllocationManager.conf
68-
certora/confs/core/AllocationManagerSanity.conf
69-
certora/confs/core/DelegationManager.conf
70-
certora/confs/core/DelegationManagerValidState.conf
71-
certora/confs/core/StrategyManager.conf
72-
certora/confs/permissions/Pausable.conf
73-
certora/confs/pods/EigenPodManagerRules.conf
74-
certora/confs/strategies/StrategyBase.conf
75-
use-beta: true
76-
solc-versions: 0.8.27
77-
solc-remove-version-prefix: "0."
78-
job-name: "Eigenlayer Contracts"
79-
certora-key: ${{ secrets.CERTORAKEY }}
80-
# Only compile, don't run verification yet
81-
compilation-steps-only: true
82-
env:
83-
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
84-
85-
# Second job: Run the actual verification after compilation succeeds
86-
verify:
87-
name: Verify
88-
runs-on: protocol-x64-16core
89-
# This job depends on the compile job
90-
needs: compile
91-
# Same conditions as the compile job
92-
if: >
93-
(github.event_name == 'pull_request' &&
94-
github.event.pull_request.merged == true &&
95-
startsWith(github.head_ref, 'feat/')) ||
96-
(github.event_name == 'push' &&
97-
startsWith(github.ref, 'refs/heads/certora/')) ||
98-
github.event_name == 'schedule' ||
99-
github.event_name == 'workflow_dispatch'
100-
steps:
101-
- uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911
102-
with:
103-
egress-policy: audit
104-
105-
# Checkout the repository with submodules
106-
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
107-
with:
108-
submodules: recursive
109-
# Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
110-
ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
111-
112-
# Install the Foundry toolchain.
113-
- name: Install Foundry
114-
uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de
115-
with:
116-
version: stable
117-
118-
# Install dependencies using Forge
119-
- name: Install forge dependencies
120-
run: forge install
121-
122-
# Run Certora verification with the same configurations
123-
- uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc
58+
# Run Certora compilation and verification
59+
- name: Run Certora compilation and verification
60+
uses: Certora/certora-run-action@11979c68d2ffab0b1b2fe6c72ec9d7a38855822d
12461
with:
12562
# List of configuration files for different contracts to verify
12663
configurations: |-
64+
certora/confs/multichain/CrossChainRegistry.conf
65+
certora/confs/multichain/KeyRegistrar.conf
66+
certora/confs/multichain/OperatorTableUpdater.conf
67+
certora/confs/multichain/ECDSACertificateVerifier.conf
68+
certora/confs/multichain/BN254CertificateVerifier.conf
12769
certora/confs/core/AllocationManager.conf
70+
certora/confs/core/AllocationManagerOverslashing.conf
71+
certora/confs/core/AllocationManagerValidState.conf
12872
certora/confs/core/AllocationManagerSanity.conf
12973
certora/confs/core/DelegationManager.conf
13074
certora/confs/core/DelegationManagerValidState.conf
13175
certora/confs/core/StrategyManager.conf
13276
certora/confs/permissions/Pausable.conf
13377
certora/confs/pods/EigenPodManagerRules.conf
13478
certora/confs/strategies/StrategyBase.conf
135-
use-beta: true
13679
solc-versions: 0.8.27
137-
solc-remove-version-prefix: "0."
138-
job-name: "Eigenlayer Contracts"
80+
job-name: "Verified Rules"
13981
certora-key: ${{ secrets.CERTORAKEY }}
14082
env:
14183
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.github/workflows/certora.yml‎

Lines changed: 0 additions & 62 deletions
This file was deleted.

‎certora/confs/core/AllocationManager.conf‎

Lines changed: 54 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -1,45 +1,56 @@
11
{
2-
"assert_autofinder_success": true,
3-
"files": [
4-
"src/contracts/core/AllocationManager.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"
2+
"assert_autofinder_success": true,
3+
// "build_cache": true,
4+
"files": [
5+
"certora/harnesses/AllocationManagerHarness.sol",
6+
"src/contracts/permissions/PauserRegistry.sol",
7+
"src/contracts/permissions/PermissionController.sol",
8+
"src/contracts/core/DelegationManager.sol",
9+
"src/contracts/pods/EigenPodManager.sol",
10+
"src/contracts/core/StrategyManager.sol",
11+
"src/contracts/strategies/StrategyBase.sol",
12+
"certora/mocks/CertoraAVSRegistrar.sol",
13+
"lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
14+
"src/contracts/libraries/OperatorSetLib.sol",
15+
"certora/harnesses/ShortStringsUpgradeableHarness.sol"
16+
],
17+
"java_args": [],
18+
"link": [
19+
"AllocationManagerHarness:pauserRegistry=PauserRegistry",
20+
"DelegationManager:permissionController=PermissionController",
21+
"DelegationManager:allocationManager=AllocationManagerHarness",
22+
"AllocationManagerHarness:permissionController=PermissionController",
23+
"DelegationManager:strategyManager=StrategyManager",
24+
"AllocationManagerHarness:delegation=DelegationManager",
25+
"EigenPodManager:delegationManager=DelegationManager",
26+
"DelegationManager:eigenPodManager=EigenPodManager"
27+
],
28+
"loop_iter": "1",
29+
"msg": "AllocationManager",
30+
"optimistic_fallback": true,
31+
"optimistic_loop": true,
32+
"packages": [
33+
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
34+
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
35+
],
36+
"parametric_contracts": [
37+
"AllocationManagerHarness"
38+
],
39+
"rule": [
40+
"pendingDiffStateTransitions",
41+
"pendingDiffStateTransitionModifyAllocations",
42+
"redistributionRecipientCannotBeDeadAddress"
1443
],
15-
"java_args": [
16-
],
17-
"link": [
18-
"AllocationManager:pauserRegistry=PauserRegistry",
19-
"DelegationManager:permissionController=PermissionController",
20-
"DelegationManager:allocationManager=AllocationManager",
21-
"AllocationManager:permissionController=PermissionController",
22-
"DelegationManager:strategyManager=StrategyManager",
23-
"AllocationManager:delegation=DelegationManager",
24-
"EigenPodManager:delegationManager=DelegationManager",
25-
"DelegationManager:eigenPodManager=EigenPodManager"
26-
],
27-
"loop_iter": "1",
28-
"optimistic_fallback": true,
29-
"optimistic_loop": true,
30-
"packages": [
31-
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
32-
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
33-
],
34-
"parametric_contracts": [
35-
"AllocationManager"
36-
],
37-
"process": "emv",
38-
"prover_args": [
39-
" -recursionErrorAsAssert false -recursionEntryLimit 3"
40-
],
41-
"solc": "solc8.27",
42-
"solc_optimize": "1",
43-
"verify": "AllocationManager:certora/specs/core/AllocationManagerRules.spec",
44-
"server": "production",
45-
}
44+
"process": "emv",
45+
"prover_args": [
46+
"-recursionErrorAsAssert false -recursionEntryLimit 3",
47+
"-splitParallel true",
48+
"-dontStopAtFirstSplitTimeout true"
49+
],
50+
"rule_sanity": "basic",
51+
"server": "production",
52+
// "solc_via_ir": true,
53+
"solc_optimize": "1",
54+
"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
55+
"wait_for_results": "none"
56+
}

‎certora/confs/core/AllocationManagerOverslashing.conf‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
{
2+
// "build_cache": 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+
"certora/harnesses/ShortStringsUpgradeableHarness.sol"
15+
],
16+
"java_args": [],
17+
"link": [
18+
"AllocationManagerHarness:pauserRegistry=PauserRegistry",
19+
"DelegationManager:permissionController=PermissionController",
20+
"DelegationManager:allocationManager=AllocationManagerHarness",
21+
"AllocationManagerHarness:permissionController=PermissionController",
22+
"DelegationManager:strategyManager=StrategyManager",
23+
"AllocationManagerHarness:delegation=DelegationManager",
24+
"EigenPodManager:delegationManager=DelegationManager",
25+
"DelegationManager:eigenPodManager=EigenPodManager"
26+
],
27+
"loop_iter": "1",
28+
"msg": "AllocationManager No Overslashing",
29+
"optimistic_fallback": true,
30+
"optimistic_loop": true,
31+
"packages": [
32+
"@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
33+
"@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
34+
],
35+
"parametric_contracts": [
36+
"AllocationManagerHarness"
37+
],
38+
"rule": [
39+
"noOverslashingOfShares",
40+
"noOverslashingOfOperatorShares",
41+
"overslashingOfSharesAtMostOne",
42+
],
43+
"process": "emv",
44+
"prover_args": [
45+
"-recursionErrorAsAssert",
46+
"false",
47+
"-recursionEntryLimit",
48+
"3",
49+
"-dontStopAtFirstSplitTimeout",
50+
"true",
51+
"-split",
52+
"false"
53+
],
54+
"smt_timeout": "7200",
55+
"rule_sanity": "basic",
56+
"server": "production",
57+
"solc_via_ir": true,
58+
"solc_optimize": "1",
59+
"disable_solc_optimizers": ["cse" , "peephole"],
60+
"verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
61+
"wait_for_results": "none"
62+
}

0 commit comments

Comments
 (0)