Skip to content

EPF Week 6 - Ivan Anishchuk - the merkle-branch completeness proof goes upstream

Short version:

  • The merkle-branch completeness proof went upstream as #42, the first consensus-layer proof off the roadmap.
  • It's the bottom of a three-branch stack. Layer 2 (generalized index) goes up next, layer 3 (hash_tree_root agreement) is held behind a spec divergence I filed as #40.
  • Co-presented the proposal with Raj on 29 July. Video and slides linked below. The proposal itself is merged into the cohort repo.
  • Side quest: packaged jitsi-meet-desktop as an ebuild and presented on it. Guest mode only so far.

The proof went up

#42 is the result I've been promising since week 4: is_valid_merkle_branch accepts every honest opening of an openable tree, machine-checked. That's the check processDeposit runs against eth1Data.depositRoot, so the deposit path is covered directly. Eighteen files. Most of that is the tree and path vocabulary the statement quantifies over, not the theorem itself.

Fixed a divergence from the spec while I was in there. merkleBranchRoot now takes depth ≤ branch.size, so a short branch can't fold in Inhabited defaults where upstream's compute_merkle_branch_root raises IndexError. External signature unchanged, processDeposit needed no edit.

Trust footprint: propext, Classical.choice, Quot.sound, nothing else. The Sha256Spec corollaries add sha256Combine_eq_spec, the one named FFI-equals-spec bridge. No sorry anywhere.

The stack behind it

#42 is the bottom of three stacked branches, roadmap items A4, A9 and A5, against the roadmap in #35. Layer 2 models get_generalized_index and proves it names the position Node.ofShape actually puts a container field at, which reaches the data-column sidecar inclusion proof, FINALIZED_ROOT_GINDEX, EXECUTION_BLOCK_HASH_GINDEX and both sync-committee gindices. Layer 3 proves hash_tree_root equals the root of the cached Node tree.

The value is back-loaded. Layers 1 and 2 are stated over Node.merkleRoot, our own construction, not Ethereum's hash_tree_root, so neither says anything about spec behaviour until layer 3 bridges them.

Layer 3 is held, blocked on #40: our zero-hash table stops at 65 entries where the pyspec builds 100, and clamps out of range where the spec raises. That divergence is why layer 3's headline theorem carries a depth ≤ 64 side condition. Fixing the table removes the side condition and rewrites layer 3's central argument, so it has to land first.

Completeness only, throughout. The check accepts every honest opening, which rules out rejecting valid data, the failure mode that forks a light client off its peers. Binding, that a forged branch gets rejected, has no sound statement under a real 64-to-32 combine. It squeezes sixty-four bytes into thirty-two, so colliding branches exist by pigeonhole, and what's left is a hardness assumption rather than something you prove.

Proposal presented and merged

Raj and I co-presented the proposal on 29 July, in EPF7 Project Presentations 3 (our segment starts at 1:19:03), and here is the proposal deck.

The proposal is merged into the cohort repo as projects/etheorem-consensus-proofs-lean4.md.

Aside: jitsi-meet-desktop

Unrelated to the proofs. I packaged jitsi-meet-desktop as an ebuild in my overlay, net-im/jitsi-meet-desktop-2026.7.0, and gave the presentation above on it. Worked well, screen share included.

It joins OIDC-gated rooms as a guest, which is what got me through the call. Non-guest mode is another matter. It doesn't look like the desktop client supports authentication the way the Ethereum server does it, so that needs more investigation before it's usable as a properly logged-in client.

Next: get #42 through review, put layer 2 up behind it, and fix the zero-hash table so layer 3 can move.

Resources