Skip to content

EPF Week 2 - Ivan Anishchuk - expanding etheorem with Heze/FOCIL and cross-client conformance harness experimentation

Week 2 I shifted off the Charon+Aeneas extraction experiments and onto etheorem's conformance layer, the Lean 4 spec-container models that get checked against the official test vectors. That work landed:

  • Two PRs merged, the consensus-specs re-pin to v1.7.0-alpha.11 with the new EIP-8282 builder containers (#5) plus a small cross-distro build fix (#4). My first merged PRs there.
  • The big one is the Heze fork layer (FOCIL, EIP-7805), published as #6 and now up for review. ~2.2k lines across 36 files; the spec delta over Gloas at this pin is compact (the inclusion-list containers plus the FOCIL fork-choice machinery), so most of the work was the fork-choice layer and keeping everything conformance-green (6770 passed / 0 failed on minimal, 997 / 0 on mainnet). One catch: alpha.11 ships no vectors that actually drive FOCIL behavior, so I pinned the vectorless fork-choice code with build-enforced #guard examples worked out by hand.

The other half of the week was research. How do we use etheorem to verify actual clients, starting with moonglass? Two candidate shapes. Differential testing (fuzzing-flavored), where you run both implementations over the same inputs and diff the verdicts, cheap and wide. Or proving by extraction, pulling the Rust through Charon/Aeneas into Lean and proving it equivalent to etheorem's definitions. Slower, way more painful, but you end up with an actual theorem. I settled on a 50/50 balance, the differential harness for breadth plus extraction proofs for the small pure kernels where a real theorem is within reach. (The extraction side already has an anchor from the week-1 experiments: the machine-checked proof that the extracted Rust u64 SSZ encoder is byte-equal to etheorem's now checks against SizzLean's actual definition instead of a pinned copy.)

In practice that meant fixing a few minor toolchain issues (the usual yaks) and getting an initial harness/runner implementation going. It drives etheorem and moonglass side by side over the official vectors and compares the two verdict streams, a real cross-implementation diff rather than each checked against the fixtures alone. On everything both currently cover (the gloas operations family) it finds zero divergences, which is the boring kind of result you actually want. The coverage edge is the runner's scope, not the harness's. The code is public now, consensus-diff (the harness) and moonglass-runner (the moonglass-side adapter). They're deliberately two repos, for a stupid copywrongs reason (the runner links moonglass's AGPL core so it has to be AGPL itself; the harness only talks to backends over a subprocess wire protocol, carries no moonglass code, and stays tri-licensed CC0/Apache/WTFPL). And the runner might hopefully get upstreamed into moonglass itself eventually anyway.

Next: handle whatever review lands on #6, then widen the moonglass runner past operations so the differential covers more of the suite. After that probably mutation-fuzzing inputs with etheorem as the oracle. I still need to shape what I'm doing into a more specific and presentable project proposal, too. To be continued.

Resources