etheoremEtheorem

Etheorem

Etheorem

Status — early-stage, experimental, single-developer; personal project, not an EF release. The libraries here pass the upstream consensus-spec test corpus and ship the three central SSZ theorems on a BasicSupported cut, but production-grade stability and a stable release line are not implied.

A Lean 4 monorepo for Ethereum consensus-spec types and SSZ (Simple Serialize) with machine-checked correctness on the verified core.

Upstream repository: https://github.com/etheorem/etheorem.

Layout

LeanSha256 ─────────────┐
                        ├─→ SizzLean  ←  LeanEthCS
LeanHazmatSha256 ───────┘   (SSZ +        (consensus
   (FFI SHA-256)            cache)        containers,
                                          Phase0…Gloas)

LeanHazmat* (FFI crypto family):  Sha256 · Bls · Kzg   (consumed à la carte)

LeanPoseidon (pure Poseidon2, standalone island — nothing depends on it yet)

Lake subpackages under packages/, each with its own lakefile and independent build target:

  • packages/LeanSha256/ — pure-Lean SHA-256 reference. NIST CAVP-validated, kernel-reducible. No FFI.
  • packages/SizzLean/ — SSZ library: spec types, serialization, deserialization, Merkleization, the SSZRepr deriving handler, the cache layer, the sszUpdate macro, plus the Hasher typeclass + Sha256 instance (delegating to the LeanHazmatSha256 FFI binding) and the FFI ≡ spec equivalence axioms — the one layer importing both the FFI binding and the spec.
  • packages/LeanEthCS/ — Ethereum consensus-spec containers from Phase 0 through Gloas, the preset-struct macro, and the ssz_static CLI runner (eth_ssz_vector_runner, driven by scripts/run_conformance.py).
  • packages/LeanHazmat*/ — the FFI crypto family: one package per primitive family wrapping a battle-tested native library behind @[extern]. Consensus families ship today — LeanHazmatSha256 (OpenSSL), LeanHazmatBls (blst), LeanHazmatKzg (c-kzg-4844), consumed à la carte. The aggregator meta-packages (LeanHazmatConsensus, …) and execution-layer families are deferred. See hazmat-docs/.
  • packages/LeanPoseidon/ — pure-Lean Poseidon2 algebraic hash (BN254 and BLS12-381 scalar fields, t = 3): the permutation, the 2-to-1 compress, and a sponge. A standalone island parallel to LeanSha256 — depends on nothing in the monorepo and nothing depends on it yet. Conformance-validated by a differential test against the HorizenLabs zkhash Rust oracle (test-only) plus committed KATs; the kernel-/native_decide-reducible core needs no Rust. A sibling LeanPoseidonProofs package (mathlib, standalone) proves permute = permuteRef (the shipped fast layers equal the textbook dense reference) with a clean axiom footprint.

The umbrella lakefile.toml declares no Lean libraries of its own — it just coordinates the subpackages via [[require]] blocks (LeanPoseidonProofs is built on its own, keeping mathlib out of the root). Per-package publication repos will exist later; this is a development monorepo.

Status: conformance-validated. The Layer 1 spec (total serialize / deserialize / hashTreeRoot), the SSZRepr typeclass + deriving handler, the FFI SHA-256 backend, the pure-Lean Sha256Spec reference, and the cache layer (persistent Node, Node.ofShape, cached merkle walker, gindex-driven setManyAt, fused commit Node.commitAndHash, closure-based pending overlay, sszUpdate macro, SSZ.Box user surface) are all landed. Consensus containers cover Phase 0 through Gloas, including Fulu's proposer_lookahead and the full Gloas ePBS BeaconState (nine EIP-7732 fields plus the supporting Builder / ExecutionPayloadBid types). Conformance pinned at consensus-spec-tests v1.6.0-beta.0 in scripts/run_conformance.py. The universal proof set (decode_encode, serialize_injective, encode_size_le_max over SSZType.Supported) and the AVX-512 SIMD inner loop for sha256BatchCombine remain as planned follow-ups; see packages/SizzLean/docs/PLAN.md for the staged roadmap.

Documents

Per-subpackage design docs live next to the code they describe:

Repo-wide docs:

  • docs/monorepo-arch.md — how the monorepo is laid out: the three-subpackage shape, which lakefiles are TOML vs procedural, where the FFI C shim lives, the LeanSha256 standalone mirror, and the naming / dep / build conventions.
  • CLAUDE.md — style and discipline conventions, project-wide.
  • CONTRIBUTING.md — PR / issue workflow, toolchain setup, code-style pointers.
  • SECURITY.md — vulnerability-disclosure policy.
  • CODE_OF_CONDUCT.md — community guidelines.

Prerequisites

On a fresh machine you need four things before lake build will work. The Lean toolchain and just itself aren't installed by the project — they're external tools the recipes assume.

  1. elan (the Lean toolchain manager — provides lake / lean). The version in lean-toolchain is installed on first use.

    curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

  2. just (task runner — every workflow below is wrapped in a just recipe; just doctor won't run until just itself is installed). Install via your platform's package manager: brew install just (macOS), cargo install just (anywhere with Rust), or see https://just.systems for distro packages.

  3. OpenSSL 3.x + pkg-config (system-level build deps for the SHA-256 FFI shim — see Native dependencies below for the per-platform one-liners). The Justfile's doctor-native recipe pinpoints what's missing.

  4. python3 + uv (only for official-ssz-vector-tests*). Run just setup-python once to create .venv/ and install the harness deps.

Verify everything in one shot:

just doctor          # checks elan/lake/lean + pkg-config/OpenSSL + python3/uv

just doctor prints actionable platform-specific install hints if anything's missing. The CI runs the slimmer just doctor-native gate (build-time native deps only — the Lean toolchain is installed by leanprover/lean-action later in the workflow).

Build

Toolchain pinned in lean-toolchain (elan picks it up).

# From the repo root — common targets by name:
lake build LeanSha256
lake build SizzLean
lake build LeanEthCS
lake build LeanPoseidon     # standalone Poseidon2 island (fires its anchor KAT)

# Test suites (per package, run on demand):
lake build LeanSha256Tests
lake build SizzLeanTests
lake build LeanEthCSTests
lake build LeanPoseidonTests # committed Poseidon2 KATs (no Rust)
lake exe   poseidon_fuzz     # Poseidon2 differential test vs the zkhash oracle (needs cargo)
just test-poseidon-proofs    # mathlib equivalence proof permute = permuteRef (standalone; fetches olean cache)

# Bench + profile executables:
lake build ssz_bench       # microbench grid, S1–S7 (see SizzLeanBench.lean)
lake build ssz_profile     # phase-by-phase profile of one workload

# ssz_static / ssz_generic CLI driver (consumed by scripts/run_conformance.py):
lake build eth_ssz_vector_runner

# Or build a single subpackage in isolation:
cd packages/SizzLean && lake build

The repo's Justfile wraps the common workflows (just build, just test, just bench, just official-ssz-vector-tests-static, …) — see just --list for the full set.

CI runs lake build for each named library on the pinned toolchain via leanprover/lean-action.

Native dependencies

The FFI SHA-256 shim (packages/LeanHazmatSha256/csrc/sha256_shim.c, used by SizzLean's hash path) links against OpenSSL's libcrypto, discovered via pkg-config (Debian/Ubuntu fallback baked in). The Lake build expects:

  • Linux (Debian/Ubuntu, including CI): libssl-dev for the headers (/usr/include/openssl/evp.h) and the versioned libcrypto.so.3 shared library, plus pkg-config. Install via:

    sudo apt-get install libssl-dev pkg-config

  • macOS: openssl@3 + pkg-config via Homebrew (the pkg-config discovery handles the keg-only include/lib paths).

Run just doctor-native to verify the build-time native deps (cc, git, pkg-config, OpenSSL 3.x).

Vendored crypto (the LeanHazmat BLS / KZG families). LeanHazmatBls (blst) and LeanHazmatKzg (c-kzg-4844) wrap vendored native libraries, fetched at pinned tags by just vendor-bls / just vendor-kzg into gitignored vendor/ trees before lake build (never git submodules; see hazmat-docs/ARCHITECTURE.md §6). just build runs both vendor steps for you. The C / C++ compilers are invoked through the Lean toolchain's cc wrapper — no separate configuration required.

Conformance harness

scripts/run_conformance.py drives the Lean eth_ssz_vector_runner CLI against ethereum/consensus-spec-tests release archives. Default mode runs the ssz_generic suite (type-agnostic SSZ tests for uints, basic_vector, bitvector, bitlist, boolean, containers), with a --limit N subset cap by default.

# One-time: create `.venv/` with the harness deps (cramjam + PyYAML).
# Wraps `uv venv` + `uv pip install -r scripts/requirements.txt`.
just setup-python

# Default: ssz_generic subset (5 cases per handler/suite)
.venv/bin/python scripts/run_conformance.py

# Full ssz_generic sweep
.venv/bin/python scripts/run_conformance.py --all

# Switch to ssz_static (per-fork consensus types)
.venv/bin/python scripts/run_conformance.py --suite static

# Single-shape focus
.venv/bin/python scripts/run_conformance.py --include 'generic:uints/*'

Current dispatch coverage

Numbers below are against consensus-spec-tests v1.6.0-beta.0 (the tag pinned in scripts/run_conformance.py). Both presets green across every fork Phase 0 → Fulu — Gloas and EIP-7805 test vectors exist in the corpus but aren't yet in the CLI dispatch table or the harness's FORKS list.

  • ssz_generic: 2188 / 2188 in-scope cases pass across all handlers (uints, basic_vector, bitvector, bitlist, boolean, containers). 292 progressive-container cases are deliberately out of scope. The test-only structs (SingleFieldTestStruct, SmallTestStruct, FixedTestStruct, VarTestStruct, ComplexTestStruct, BitsStruct) have their SSZ shapes hardcoded in packages/LeanEthCS/LeanEthCS/Cli/Main.lean.
  • ssz_static --config mainnet --all: 1585 / 1585 cases pass across every fork Phase 0 → Fulu.
  • ssz_static --config minimal --all: 38991 / 38991 cases pass across every fork Phase 0 → Fulu — including variable-size composites (Attestation, BeaconBlockBody, BeaconState) and all fork deltas (Altair / Bellatrix / Capella / Deneb / Electra / Fulu).
  • One-command full sweep: just official-ssz-vector-tests-all drives generic + static-mainnet + static-minimal end-to-end.