Skip to content

EPF Week 5 - Ivan Anishchuk - a joint proposal with Raj and the verification roadmap upstream

Short version:

  • The verification roadmap went upstream as a PR (#35), twenty proof targets across four tiers.
  • Raj Gill (@irajgill) and I wrote a joint proposal, split by layer. He takes SSZ, I take the consensus layer above it.
  • Three of my PRs are sitting open upstream: the roadmap, the fork-choice throw-faithfulness sweep (#22), and the Heze fork layer (#6) still going through review.

The proposal took most of the week. Raj and I worked on it together and wrote it as one project with two lanes, split by layer. His lane is finishing the three central serialization theorems until they hold for every type the codec actually implements. Mine is everything above SSZ, the arithmetic and structural invariants, merkleization, the shuffle, fork choice, plus keeping conformance green as the forks move and the roadmap both lanes work from. Splitting by layer rather than by ticket keeps us in different packages.

Where the SSZ side stands: the mixed-field container arm is in review (#28, #29). It's the hardest one and the shape BeaconState itself takes, since the decoder has to recover field boundaries from the offset table the encoder wrote. One arm sits behind it, vector and list over variable-size elements, same offset machinery element-wise, scheduled for August. After that the three theorems cover everything the codec implements.

The roadmap PR is up. Twenty targets, four tiers, each pinned to a function and an acceptance criterion, with prior-art tags for what the Dafny and Runtime Verification work covered.

The other two open PRs are older business. #22 is the throw-faithfulness sweep from the week-3 review, converting the fork-choice helpers that can throw in the Python spec into Lean versions that can also fail instead of quietly returning something. #6 is the Heze fork layer, still in review, still the piece the FOCIL inclusion-list proof target sits on. Neither is dramatic, both need to land before the proof work above them means much.

The presentation deck for the proposal is built too.

Next: submit the proposal to the cohort repo, present it, and start on the overflow-safety and slot/epoch invariants while the container arms land underneath.

Resources