test(ethcllib): computational Merkle-branch witnesses #22
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Lean Action CI | |
| on: | |
| push: | |
| pull_request: | |
| workflow_dispatch: | |
| inputs: | |
| pyspec_limit: | |
| description: 'Per-suite case cap for the pyspec run (use "all" for the full sweep)' | |
| default: '1' | |
| required: false | |
| # CI structure mirrors `just` — every step that has a corresponding | |
| # Justfile recipe goes through `just <recipe>`, so local-dev and CI | |
| # can't drift on what they actually run. Adding or renaming a recipe | |
| # updates both sides at once. The only steps that don't go through | |
| # `just` are toolchain installers (elan, uv, python, the `just` | |
| # binary itself) and the `actions/cache` declaration, which is a | |
| # GitHub Actions concern with no local-dev analogue. | |
| jobs: | |
| lint: | |
| # Forbidden-token check on committed Lean source — no Lean | |
| # toolchain needed, just `git grep`. Runs in ~5 s. | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: extractions/setup-just@v3 | |
| - name: Lint Lean sources (sorry / #eval / #check / #print) | |
| run: just lint | |
| test: | |
| # In-Lean property tests: SHA-256 NIST CAVP vectors against both | |
| # the pure-Lean spec (LeanSha256) and the OpenSSL FFI shim | |
| # (LeanHazmatSha256), the FFI ≡ spec equivalence cross-checks, SSZ | |
| # and SSZ library gates (Merkle PRNG, cache machinery on example | |
| # containers). All fire as `native_decide` examples via `lake build`. | |
| # The libraries themselves build transitively, so this job subsumes | |
| # the previous standalone build gate. The consensus-spec libraries | |
| # (EthCLLib / EthCLSpecs) have their own `ethcl` job. | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: extractions/setup-just@v3 | |
| - name: Verify build-time native deps | |
| # See `pyspec` job below for the rationale. | |
| run: just doctor-native | |
| - name: Vendor native crypto sources | |
| # blst (LeanHazmatBls) and c-kzg-4844 (LeanHazmatKzg) are vendored, | |
| # not system packages — fetch them at their pinned tags before the | |
| # Lean build. Offline thereafter. `just test` also self-vendors via | |
| # the `hazmat-bls-test` / `hazmat-kzg-test` recipes; this explicit step keeps the | |
| # fetch visible and ordered first. | |
| run: just hazmat-bls-vendor hazmat-kzg-vendor | |
| # Pinned to the commit `v1` resolves to as of 2026-05-10. Bump deliberately. | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| lake-package-directory: '.' | |
| - name: Unit tests | |
| run: just test | |
| pyspec: | |
| # ssz_generic acceptance: the fork-agnostic SSZ wire-format suite, run via | |
| # the SizzLean pytest harness + `ssz_generic_runner`. The dev-subset smoke | |
| # gate runs on every push / pull_request; `workflow_dispatch` with | |
| # `pyspec_limit: all` upgrades to the full sweep | |
| # (`just sizzlean-pyspec-full`). The per-fork ssz_static container | |
| # vectors run in the `ethcl` job. | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: extractions/setup-just@v3 | |
| - uses: astral-sh/setup-uv@v3 | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.12' | |
| - name: Cache consensus-spec-tests archives | |
| # Cache only the .tar.gz files (the `general` archive ssz_generic uses); | |
| # the extracted trees re-build on each run via `ensure_archive` in the | |
| # SizzLean harness, extraction is ~1 min, much cheaper than the | |
| # GitHub-side cache transfer would be. Keyed on the pinned tag; bumping | |
| # it invalidates and the cache repopulates on first run. | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.cache/sizzlean/v1.7.0-alpha.10-*.tar.gz | |
| key: consensus-spec-tests-v1.7.0-alpha.10-archives | |
| - name: Verify build-time native deps | |
| # `just doctor-native` probes pkg-config + libcrypto (the | |
| # native deps `lakefile.lean` consumes via `pkg-config --libs | |
| # libcrypto`) and prints actionable platform install hints if | |
| # anything is missing. Runs *before* lean-action so a missing | |
| # OpenSSL surfaces here (~1 s) rather than as a cryptic linker | |
| # error 30 s into `lake build`. Uses the `-native` variant | |
| # (not full `just doctor`) because the Lean toolchain isn't | |
| # installed yet at this point — lean-action does that next. | |
| run: just doctor-native | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| lake-package-directory: '.' | |
| # Build the runner the ssz_generic harness drives; SizzLean and the | |
| # LeanHazmat FFI deps compile transitively. | |
| build-args: 'ssz_generic_runner' | |
| - name: Install Python dependencies | |
| run: just setup-python | |
| - name: Run ssz_generic pyspec suite | |
| run: | | |
| set -euo pipefail | |
| LIMIT='${{ github.event.inputs.pyspec_limit || '1' }}' | |
| if [ "$LIMIT" = "all" ]; then | |
| just sizzlean-pyspec-full | |
| else | |
| just sizzlean-pyspec-smoke | |
| fi | |
| ethcl: | |
| # EthCLLib (framework) + EthCLSpecs (Fulu / Gloas) acceptance. `just | |
| # ethcl-test` builds all five libs, firing the framework + spec | |
| # `#guard` / `native_decide` self-tests (inheritance replay, the crypto | |
| # seam, the running step, map-backing equivalence, the signing-root and | |
| # Merkle-branch primitives, the walking-skeleton discharge). Then the | |
| # `pytest-xdist` pyspec smoke gate runs the dev subset at minimal for | |
| # both forks through the per-worker `pyspec_server`. The consensus formats are | |
| # green for both forks (Fulu incl. PeerDAS data availability, standalone | |
| # execution_payload, and get_proposer_head; Gloas the full EIP-7732 ePBS spine, | |
| # operations, fork choice, and transition). The per-fork ssz_static container | |
| # vectors are collected too: the consensus containers pass, and the types | |
| # EthCLSpecs does not model (light-client, gossip, networking helpers) xfail. | |
| # Out of scope and not collected: Electra-parent Fulu fork/transition, | |
| # light_client, networking, merkle_proof, sync. Mainnet and the full sweep run | |
| # on demand (`--preset=mainnet`, `--subset=0`). | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: extractions/setup-just@v3 | |
| - uses: astral-sh/setup-uv@v3 | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.12' | |
| - name: Cache consensus-spec-tests archives | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.cache/sizzlean/v1.7.0-alpha.10-*.tar.gz | |
| key: consensus-spec-tests-v1.7.0-alpha.10-archives | |
| - name: Verify build-time native deps | |
| run: just doctor-native | |
| - name: Vendor native crypto sources | |
| run: just hazmat-bls-vendor hazmat-kzg-vendor | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| lake-package-directory: '.' | |
| # The runner exe; EthCLLib + EthCLSpecs compile transitively as deps. | |
| build-args: 'pyspec_server' | |
| - name: EthCL self-tests (lake build of the test libs) | |
| run: just ethcl-test | |
| - name: Install Python dependencies | |
| run: just setup-python | |
| - name: EthCLSpecs pyspec smoke gate (minimal, both forks) | |
| run: just ethcl-pyspec-smoke | |
| poseidon: | |
| # Poseidon2 differential conformance against the HorizenLabs `zkhash` | |
| # Rust oracle (LeanPoseidon ARCHITECTURE.md §8). This is the ONLY job | |
| # that needs a Rust toolchain (cargo): it builds `poseidon_fuzz` (which | |
| # shells `cargo build` for the oracle) and runs it. The LeanPoseidon | |
| # core and its committed KATs build *without* Rust — the anchor KAT | |
| # already fires in the `test` job via `just test` (`poseidon-test`). | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: extractions/setup-just@v3 | |
| - uses: dtolnay/rust-toolchain@stable | |
| # Same lean-action pin as the other jobs. `build-args: poseidon_fuzz` | |
| # builds the exe, which triggers the `cargo build` + the Rust↔Lean | |
| # link; LeanPoseidon / LeanPoseidonTests compile transitively. | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| lake-package-directory: '.' | |
| build-args: 'poseidon_fuzz' | |
| - name: Committed Poseidon2 KATs (native_decide, no Rust) | |
| run: just poseidon-vectors | |
| - name: Differential conformance vs the zkhash oracle | |
| run: just poseidon-fuzz | |
| poseidon-proofs: | |
| # The mathlib equivalence proof (`permute = permuteRef` — the shipped | |
| # fast layers equal the dense reference). This is the monorepo's ONLY | |
| # mathlib dependency, isolated in the standalone `LeanPoseidonProofs` | |
| # package — no other job (and not the umbrella build) touches mathlib. | |
| # `just poseidon-proofs` runs `lake exe cache get` (the `v4.29.1` | |
| # pin matches the repo toolchain, so prebuilt oleans are used — nothing | |
| # is compiled from scratch) then builds the proofs. | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: extractions/setup-just@v3 | |
| # `auto-config: false` → install the Lean toolchain only; the build + | |
| # mathlib-cache fetch go through the `just` recipe (CI mirrors `just`). | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| - name: Build the fast≡reference equivalence proof (mathlib cache + build) | |
| run: just poseidon-proofs |