Skip to content

Commit fb9d731

Browse files
IvanAnishchukIvanAnishchuk
committed
docs: add the formal-verification proof-targets roadmap
A tiered catalogue of machine-checkable proof targets over the executable spec (docs/VERIFICATION_ROADMAP.md). It records what the prior efforts proved or stubbed, spells out the axiom and trust story once, and resolves each candidate lemma to the concrete Lean function it would be stated over, with an effort mark and a prior-art flag. So picking the next proof is a lookup rather than a research session. Tier A is SSZ and merkleization, B shuffling and committees, C state-transition invariants and bounds, D deep consensus. The Merkle-branch completeness proof in flight is the worked Tier A example the tiers calibrate against, and the generalized-index library is the dependency gating every Merkle-proof consumer past deposits. A closing section places the adjacent formal efforts that run alongside this without overlapping it, Apalache's bounded 3SF model-checking and Nyx's formal-leanSpec.
1 parent c375a7f commit fb9d731

2 files changed

Lines changed: 290 additions & 0 deletions

File tree

‎docs/VERIFICATION_ROADMAP.md‎

Lines changed: 284 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,284 @@
1+
# Formal-verification proof targets
2+
3+
A menu of proof targets across Etheorem, the SSZ layer, the consensus containers,
4+
and the fork framework. Every target points at code already in the tree and says
5+
whether one of the two prior beacon-chain efforts left a template for it, or whether
6+
it's new ground. They're grouped into four tiers by area and tagged by how novel and
7+
how hard I think each one is.
8+
9+
This is a working doc. I'll reshuffle targets as work lands.
10+
11+
## Prior art
12+
13+
Two earlier efforts verified chunks of the beacon chain, both outside Lean 4. What
14+
they closed tells us what's tractable. What they punted on is where the interesting
15+
work is.
16+
17+
### ConsenSys eth2.0-dafny (Dafny, Phase 0, archived)
18+
19+
- SSZ round-trip proved for the non-composite shapes: `seDesInvolutive`
20+
(`deserialise(serialise s) = s`), `serialiseIsInjective`, and the per-type SeDes
21+
lemmas, bitlist and bitvector included. Both central lemmas carry
22+
`requires !(s.Container? || s.List? || s.Vector?)`, so containers, lists, and
23+
vectors sit outside them. Composite round-trip is open ground for everyone.
24+
- Merkleization: only the chunk-count and length bookkeeping proved. Root-equals-spec
25+
stays differential-tested. `hash()` is uninterpreted.
26+
- State transition proved as refinement. Every `process_*` method carries
27+
`ensures s' == update*(s)`, with slot monotonicity and validator/balance length
28+
sync.
29+
- Overflow bounds assumed, not proved: balance sum `< 2^64`, deposit index
30+
`+1 < 2^64`, registry `<= VALIDATOR_REGISTRY_LIMIT` all ride on `{:axiom}`
31+
`Assume*Overflow` lemmas ("This proof is assumed", per their docstrings). The
32+
transition proofs hold modulo those assumptions; discharging them is open.
33+
- Committee-size bounds (`ActiveValidatorBounds`).
34+
- Fork-choice store invariants: `aValidStoreIsAChain`, slot-monotone ancestry,
35+
accepted-block immutability. No liveness. `filter_block_tree` unimplemented.
36+
- Casper FFG accountable safety (`lemma5`, on the `goal1` branch, never merged to
37+
master): conflicting finalized and justified checkpoints imply a `1/3` slashable
38+
set, under a fixed validator set.
39+
- Never built `is_valid_merkle_branch`. Shuffling stubbed to identity, so no
40+
permutation proof. BLS unimplemented.
41+
42+
### Runtime Verification (K + Coq)
43+
44+
- Deposit-contract incremental Merkle tree: a full proof that the incremental root
45+
equals the naive full-tree root, plus KEVM bytecode refinement against an untrusted
46+
compiler, which surfaced real bugs. This is the canonical incremental-Merkle result.
47+
- Phase 0 state transition: an executable K model, conformance-tested against the
48+
official vectors, not proved.
49+
- Gasper in Coq: accountable safety, plausible liveness, and the slashable bound, with
50+
dynamic validator sets, on an abstract model rather than the executable spec.
51+
- The bridge from the K state-transition model up to Gasper: ongoing, incomplete.
52+
- Shuffling and rewards/penalties: not independently proved.
53+
54+
### Adjacent efforts
55+
56+
- Apalache / TLA+: bounded model-checking of 3SF (three-slot-finality) accountable
57+
safety (Konnov et al. 2025). It checks the property up to a bound, so it finds
58+
counterexamples rather than proving the general case, complementary to a deductive
59+
D2 proof.
60+
- Nyx Foundation `formal-leanSpec`: a parallel Lean 4 formalization, with its own SSZ
61+
layer, of the post-quantum leanSpec (the Beam-chain minimal spec). It tracks the
62+
future PQ spec where Etheorem tracks the production consensus spec, so the two run
63+
alongside each other.
64+
65+
### Takeaways
66+
67+
1. SSZ round-trip on the non-composite shapes and refinement invariants are
68+
known-tractable; Dafny closed both, so we can lean on their shape. Their overflow
69+
bounds were assumed via axiom lemmas, so actually proving those is still open.
70+
2. `is_valid_merkle_branch` soundness and shuffle-is-a-permutation are open ground.
71+
Neither effort proved either, so that's where the novelty is.
72+
3. Our one real edge over both: a verified SHA-256 (`LeanSha256` plus the
73+
FFI-equivalence axioms) and the Poseidon2 proofs. Where Dafny and K could
74+
only differential-test merkleization soundness, we can close it against a
75+
concrete hash.
76+
77+
## Current proof surface
78+
79+
The crypto layer is well proved. Roughly 65 SizzLean theorems (round-trip over
80+
`BasicSupported`, size bounds, injectivity, bit packing, wide-integer codec), 48
81+
Poseidon2, and 23 SHA-256, with zero `sorry`. The axiom footprint is small and named: two
82+
field-primality axioms (`bn254FrModulus_prime`, `blsFrModulus_prime`, LeanPoseidonProofs) and
83+
the three-axiom SHA-256 bridge (`sha256Hash_eq_spec`, `sha256Combine_eq_spec`,
84+
`sha256BatchCombine_eq_spec`, SizzLean), each visible through `#axioms` on any dependent proof.
85+
The Merkle-branch completeness work is symbolic, so it adds none.
86+
The narrow `uintN` arms (8 through 64) close by `bv_decide`, so `Lean.ofReduceBool`
87+
(the compiler axiom) is in that footprint. The wide 128 and 256 arms (PR #18) close by
88+
`Nat`-digit induction and add no axiom.
89+
90+
The consensus layer is mostly bare. Two proof sites sit on main: `uint64ModOfNatToNatLt`,
91+
and the three `bv_decide` builder-index round-trip theorems PR #16 landed
92+
(`EthCLSpecs/Proofs/BuilderIndex.lean`). Alongside them, off main, the in-progress
93+
Merkle-branch stack (roughly 21 theorems in EthCLLib), around 40 `#guard` and
94+
`native_decide` property checks, and roughly 60 `forkdef` state functions with no proofs
95+
attached. A curated function-level candidates list for the Gloas surface lives in
96+
[`CONSENSUS_PROOF_CANDIDATES.md`](../packages/EthCLSpecs/docs/CONSENSUS_PROOF_CANDIDATES.md);
97+
it complements this roadmap one altitude down, per-function where this doc is
98+
per-tier.
99+
100+
A4 is the worked example, already started. The `isValidMerkleBranch` completeness proof
101+
shows a passing verifier accepts the honest opening over a real Merkle tree, down to the
102+
pure-Lean `LeanSha256`, symbolically. Its extension to the mix-in-length root that `processDeposit`
103+
checks is in progress, the prerequisite for **C1**'s deposit arm.
104+
105+
A structural fact shapes the SSZ tier. `SizzLean.Proofs.decode_encode` is
106+
proved over `SSZType.BasicSupported`, which covers every fixed-size shape. PR #18 closed
107+
the last integer widths (`uintN 128/256`, `Proofs/UIntWide.lean`), and `Proofs/BitPack.lean`
108+
folded in the two bit shapes: `packBitsLE_unpackBitsLEAux_inverse` is proved and the
109+
`bitvector`/`bitlist` arms of the central theorems are closed. Variable-size containers
110+
and variable-size lists sit outside `Supported` (the decoder returns `.error` for them);
111+
fixed-element lists are covered and proved (`decode_encode_listFixed`), and `Union` is
112+
not an `SSZType` constructor at all, so it cannot even be stated yet.
113+
114+
## Targets
115+
116+
Legend. Prior art: ✅ template exists, ⚠ partial, ★ greenfield. Difficulty (a guess): L, M, H.
117+
118+
### Tier A, SSZ and merkleization
119+
120+
- **A4 `is_valid_merkle_branch` completeness** ★ M. An honest inclusion proof is always
121+
accepted by the verifier, over a real Merkle tree down to the pure-Lean `LeanSha256`. Started (see the
122+
status paragraph above), symbolic and axiom-clean. The worked Tier A example.
123+
- **A2 bit-packing round-trip** ★ M. Done for the proved direction:
124+
`packBitsLE_unpackBitsLEAux_inverse` (PR #10, `Proofs/BitPack.lean`) recovers
125+
the input bits from their packed bytes, up to false-padding (bits→bytes→bits).
126+
The byte-side composition (`packBitsLE` after unpacking arbitrary bytes) has
127+
no standalone identity and `unpackBitsLE` exists only as the `Aux` form.
128+
- **A1 round-trip on bitvector and bitlist** ⚠ M. Done: PR #10 closed both arms of
129+
`decode_encode` and folded the bit shapes into `BasicSupported`.
130+
- **A5 `merkleRootWithCache ≡ hashTreeRoot`** ⚠ M. The cached tree agrees with the spec
131+
merkleization.
132+
- **A6 zero-hashes tower** and **A7 chunk and length plumbing** ⚠ L–M. The padding and
133+
chunking bookkeeping Dafny proved.
134+
- **A9 generalized-index library** ★ M. Decompose `get_generalized_index` and
135+
`get_subtree_index` into the `(depth, index)` pair the merkleization theorems take, and
136+
bridge a gindex opening to that pair. Greenfield: neither prior effort built it. In
137+
progress. The `(depth, index)` decomposition (`gindex_decompose`,
138+
`getSubtreeIndex`) and `getPowerOfTwoCeil` are proved and axiom-clean;
139+
`getGeneralizedIndex` over `SSZType` is modeled but still miscomputes the chunk position
140+
for packed vectors and lists (it reads the raw element index), so that arm is still
141+
unfinished.
142+
This is the enabling dependency for every Merkle-proof consumer past deposits: the
143+
light-client header branches and the blob and data-column sidecar inclusion proofs all
144+
address leaves by generalized index rather than raw tree position, so each of them waits
145+
on A9. Deposits skip it, their index is a plain tree position.
146+
147+
### Tier B, shuffling and committees
148+
149+
Greenfield, high novelty. Neither prior effort proved a real shuffle. Determinism
150+
needs no target here: the shuffle is a pure function, so same seed, same permutation
151+
holds definitionally, where the informal efforts had to state it as a property.
152+
153+
- **B1 `computeShuffledPermutation` is a bijection** on `[0, count)`.
154+
`EthCLSpecs/Fulu/Committees.lean`. ★ M–H. The flagship result. Dafny stubbed the
155+
shuffle to identity, so no one has proved this.
156+
- **B2 committee partition**: the union of committees is the active set, pairwise
157+
disjoint. Follows B1. ★ M.
158+
- **B3 sampler termination**: the balance-weighted 10M-fuel bound always suffices. ★ M.
159+
160+
### Tier C, state-transition invariants and bounds
161+
162+
The Dafny-proven pattern: templates exist for the statements, but C1's proofs were
163+
assumed there (`{:axiom}`), not carried out.
164+
165+
- **C1 overflow safety**: `increaseBalance` never wraps, total balance `< 2^64`, deposit
166+
index `+1 < 2^64`, registry `<= VALIDATOR_REGISTRY_LIMIT`.
167+
`EthCLSpecs/Fulu/{Balances,Operations}.lean`. ⚠ M. Dafny stated these bounds but
168+
assumed them via `{:axiom}` lemmas, so the template covers the statements, and the proofs
169+
themselves are new work.
170+
- **C2 slot/epoch round-trip and monotonicity**: `computeEpochAtSlot
171+
(computeStartSlotAtEpoch e) = e` for `e < 2^59` (the raw `UInt64` multiply
172+
wraps above that, so the identity is false unbounded), plus slot
173+
monotonicity. `EthCLSpecs/Fulu/Time.lean`. ✅ M; the bound hypothesis is where the
174+
work hides.
175+
- **C3 length invariant**: `|validators| = |balances|` preserved across transitions. ✅ M.
176+
- **C4 committee-size bounds**: an active count in `[32, 2^22]` implies sizes in `(0, MAX]`.
177+
`EthCLSpecs/Fulu/Committees.lean`. ✅ (Dafny `ActiveValidatorBounds`). M.
178+
- **C5 `isSlashableAttestationData` = spec** (double-vote or surround), with the
179+
`strictlySorted` well-formedness. `EthCLSpecs/Fulu/Operations.lean`. ⚠ M.
180+
- **C6 registry-update legality**: a validator flows active to exited at most once, churn
181+
`<=` churn_limit. `EthCLSpecs/Fulu/EpochProcessing.lean`. ⚠ H.
182+
183+
### Tier D, deep consensus
184+
185+
Research-scale.
186+
187+
- **D1 fork-choice store invariants**: a valid store is a chain, ancestry slot-monotone,
188+
accepted blocks immutable. `EthCLSpecs/Fulu/ForkChoice.lean`.
189+
✅ (Dafny `aValidStoreIsAChain`). M. The best entry into Tier D.
190+
- **D2 Casper FFG accountable safety**: conflicting finalized and justified checkpoints
191+
imply a `1/3` slashable set. Needs an abstract FFG layer over
192+
`EthCLSpecs/Fulu/EpochProcessing.lean`.
193+
✅✅ (Dafny `goal1` and RV Coq). H. Both prior efforts closed it, Dafny under a fixed
194+
validator set and RV Coq under dynamic sets, so it is hard yet demonstrably reachable.
195+
Apalache also bounded-model-checked the 3SF form (Konnov et al. 2025), up to a bound. A
196+
Lean version would be a headline result. One approach: extract an abstract
197+
checkpoint/justification-link model from the epoch-processing functions, prove the
198+
two-quorum intersection argument on that, then bridge the abstract model back to
199+
`EthCLSpecs/Fulu/EpochProcessing.lean` by refinement.
200+
- **D3 plausible liveness**: with `>= 2/3` honest, new finalization stays possible. ✅
201+
(RV Coq, dynamic sets). Very H. Sits behind D2 and shares the abstract FFG model D2
202+
builds.
203+
- **D4 Heze/FOCIL inclusion-list validity**: a satisfied inclusion list forces the required
204+
transactions into the block. ★ M–H.
205+
206+
## By function
207+
208+
The same targets, resolved to the concrete definitions they're about, in the layout
209+
[`CONSENSUS_PROOF_CANDIDATES.md`](../packages/EthCLSpecs/docs/CONSENSUS_PROOF_CANDIDATES.md)
210+
uses, so the two docs compare side by side. Line numbers are as of this commit and will drift.
211+
212+
Several candidate rows over there are the same work as targets here: the churn
213+
no-underflow candidates (`computeExitEpochAndUpdateChurn`, `reserveChurn`) are C6, the
214+
fork-choice monotonicity and base-case candidates (`updateCheckpoints`,
215+
`onAttesterSlashing`, `getForkchoiceStore`, `getHead`/`getWeight` determinism) sit
216+
inside D1, and `initiateBuilderExit`'s unguarded exit-epoch arithmetic is a
217+
C1-shaped overflow statement on the Gloas side.
218+
219+
### Tier A
220+
221+
| Target | Function(s) | Location | Status |
222+
| ------ | ----------- | -------- | ------ |
223+
| A4 | `isValidMerkleBranch` | `EthCLLib/Spec/SigningRoot.lean:68` (the verifier) | started; the completeness proof is not yet in-tree |
224+
| A2 | `packBitsLE`, `unpackBitsLEAux` | `SizzLean/Spec/Serialize.lean:223`, `SizzLean/Spec/Deserialize.lean:178`, proof in `SizzLean/Proofs/BitPack.lean` | done |
225+
| A1 | `decode_encode`, bit arms | `SizzLean/Proofs/Roundtrip.lean`, arms in `SizzLean/Proofs/BitPack.lean` | done |
226+
| A5 | `hashTreeRoot` vs `Node.merkleRootWithCache` / `Node.merkleRoot`, `hashTreeRootCached` | `SizzLean/Spec/HashTreeRoot.lean:504`, `SizzLean/Cache/MerkleTree/Merkle.lean:52`, `SizzLean/Cache/TreeBacked.lean:306` | open; reuses the perfect-tree kit shared with the A4 stack |
227+
| A6 | `zeroHashes` (private) | `SizzLean/Cache/MerkleTree/Zero.lean:107` | open |
228+
| A7 | `padToChunk`, `chunkDepth`, `mixInLength` (private) | `SizzLean/Spec/HashTreeRoot.lean:100,288,302` | open |
229+
| A9 | `getGeneralizedIndex`, `getSubtreeIndex`, `floorLog2`, `getPowerOfTwoCeil` | not yet in-tree | in progress; decomposition + `getPowerOfTwoCeil` proved, `getGeneralizedIndex` packed-position fix pending |
230+
231+
### Tier B
232+
233+
All in `EthCLSpecs/Fulu/Committees.lean`.
234+
235+
| Target | Function(s) | Location | Status |
236+
| ------ | ----------- | -------- | ------ |
237+
| B1 | `computeShuffledPermutation` | `Committees.lean:32` | open |
238+
| B2 | `getBeaconCommittee`, on top of B1 | `Committees.lean:83` | open |
239+
| B3 | `computeBalanceWeightedSelection` (the 10M-fuel call is at `:121`) | `Committees.lean:114` | open |
240+
241+
### Tier C
242+
243+
| Target | Function(s) | Location | Status |
244+
| ------ | ----------- | -------- | ------ |
245+
| C1 | `increaseBalance`, `processDeposit`, `processRegistryUpdates` | `Fulu/Balances.lean:29`, `Fulu/Operations.lean:214`, `Fulu/EpochProcessing.lean:165` | open; its deposit-arm Merkle prerequisite (the mix-in-length extension) is in progress, the overflow bounds are not started |
246+
| C2 | `computeEpochAtSlot`, `computeStartSlotAtEpoch` | `Fulu/Time.lean:25,28` | open |
247+
| C3 | `processDeposit` (the append site), then transition-wide preservation | `Fulu/Operations.lean:214` | open; rests on the in-progress mix-in extension, not started |
248+
| C4 | `getBeaconCommittee` | `Fulu/Committees.lean:83` | open |
249+
| C5 | `isSlashableAttestationData`, `strictlySorted` | `Fulu/Operations.lean:38,30` | open |
250+
| C6 | `processRegistryUpdates`, `initiateValidatorExit`, `computeExitEpochAndUpdateChurn` | `Fulu/EpochProcessing.lean:165`, `Fulu/RegistryUpdates.lean:112,78` | open |
251+
252+
### Tier D
253+
254+
| Target | Function(s) | Location | Status |
255+
| ------ | ----------- | -------- | ------ |
256+
| D1 | `getAncestor`, `getHead`, `onBlock` (Gloas twins at `Gloas/ForkChoice.lean:156,446,594`) | `Fulu/ForkChoice.lean:105,200,387` | open |
257+
| D2, D3 | `processJustificationAndFinalization`, behind an abstract FFG layer | `Fulu/EpochProcessing.lean:69` | open |
258+
| D4 | `processInclusionList`, `isPayloadInclusionListSatisfied` | `Heze/ForkChoice.lean` (PR #6, in review) | open; workable now on the in-flight Heze layer, against the current alpha |
259+
260+
## Dependencies and entry points
261+
262+
No strict order here. Some targets rest on others, some are gentler first steps.
263+
264+
- A4 shows the merkleization-completeness shape end to end (status above). A1 and A2 have
265+
since landed on main, which leaves A5 as the natural next SSZ extension.
266+
- A4 is load-bearing beyond Tier A. `processDeposit` accepts a deposit only behind the
267+
`isValidMerkleBranch` assert (`Fulu/Operations.lean:216`),
268+
so C1's deposit arm and C3 lean on the completeness theorem *plus a mix-in-length
269+
extension*: the deposit root mixes in the list length, so it isn't a plain perfect tree
270+
and the base theorem doesn't cover it. That extension is in progress, stated general over
271+
depth so the sidecar inclusion proofs reuse it, a blob or data-column commitment opens a
272+
`List` element that crosses the same length-mix-in node. A5 reuses the same perfect-tree
273+
kit. The `DataColumnSidecar.kzgCommitmentsInclusionProof` field (`Fulu/Blocks.lean:63`)
274+
is the other branch-proof consumer, not modeled yet.
275+
- Tier C holds the quick wins. C1 and C2 are small, self-contained, and follow the Dafny
276+
template closely.
277+
- B1 is the flagship shuffle result. B2 and B3 cluster around it, and B2 follows B1
278+
directly.
279+
- D1 is the doorway into deep consensus and ties into the fork-choice work. D2 is the
280+
long-arc goal of accountable safety, and D3 shares the abstract FFG model D2 builds. D4
281+
follows the FOCIL work.
282+
283+
Both prior efforts closed accountable safety in their own settings, so I'm keeping D2 and
284+
D3 on the list as reachable, although it's arguably deeper research.

‎packages/EthCLSpecs/docs/README.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,9 @@ plus the invariant lemmas they rest on.
2929

3030
[CONSENSUS_PROOF_CANDIDATES.md](CONSENSUS_PROOF_CANDIDATES.md) is a shortlist of Lean
3131
theorem candidates across the Fulu and Gloas specs, to help contributors pick proof targets.
32+
33+
[VERIFICATION_ROADMAP.md](../../../docs/VERIFICATION_ROADMAP.md) (root `docs/`; it spans
34+
the whole monorepo) is a menu of formal-verification proof
35+
targets across the SSZ layer, the consensus containers, and the fork framework, each
36+
cross-referenced against the two prior beacon-chain verification efforts and tagged by
37+
novelty and difficulty. It is where a contributor looks to pick up a proof.

0 commit comments

Comments
 (0)