chore(deps): bump leanSpec to f12000b (pre-devnet5), rename fork to Lstar

[MegaRedHand]

Summary

The pinned LEAN_SPEC_COMMIT_HASH (18fe71f, 2026-04-29) can no longer generate fixtures: the released latest test keys moved to the new key JSON schema (attestation_keypair.public_key etc.), so the old code fails with KeyError: 'attestation_public' during fixture generation.

The fix bumps the pin to f12000b (leanSpec PR #725, 2026-05-17), which reads the new key schema. This is the commit just before leanSpec's devnet5 work, chosen deliberately:

• An earlier draft of this PR pinned to 825bec6 (the #745 download fix). That commit unavoidably includes leanSpec PR #717 (ac5f259), which switched the aggregated-proof wire format to devnet5. The Rust client still runs leanMultisig@5eba3b1 (pre-devnet5), so the forkchoice spec tests failed with AggregateVerificationFailed(DeserializationFailed). The devnet5 proof format requires the full crypto-stack migration tracked in feat: add devnet 5 support #378/feat: integrate leanMultisig devnet5 + leanSpec PR #717 wire format #370, which is not yet on main.
• f12000b predates #717, so fixtures keep the old proof format that the current crypto stack deserializes correctly. No Rust changes are needed.

Also rename --fork devnet → --fork Lstar to match the upstream fork rename (already in effect at f12000b).

Download workaround

f12000b predates leanSpec PR #745, whose download_keys reads the still-open (unflushed) download tempfile, intermittently truncating the gzip tail and aborting with EOFError (surfaced as Aborted!). Both the Makefile and CI now fetch+extract the prod keys with curl+tar before fill, which fully writes the archive before reading it; fill then sees the keys present and skips its own buggy download. Both blocks are commented Remove once the pin moves past PR #745.

Why not 825bec6 / devnet5?

The devnet5 aggregated-proof wire format and the matching ethlambda-crypto rewrite live in #378 / #370 and are not yet merged to main. Bumping fixtures to a devnet5 leanSpec commit here would require duplicating that crypto work. This PR stays scoped to "unbreak fixture generation on main" and remains on the pre-devnet5 format until the devnet5 PRs land.

Test plan

• rm -rf leanSpec && make leanSpec/fixtures — clean download (via curl+tar) + extract, 554 fixtures generated, no Aborted!.
• cargo test -p ethlambda-blockchain --test forkchoice_spectests — 84/0.
• cargo test -p ethlambda-blockchain --test signature_spectests — 11/0.
• make test — full workspace suite, 421/0.
• CI runs green.

[github-actions]

🤖 Kimi Code Review

Makefile (lines 27-33)

1. Security - Commit hash verification: Changing the LEAN_SPEC_COMMIT_HASH introduces supply chain risk. Verify that 825bec6bf278920cfc56730d64a7c90522a0bb6c is the legitimate commit from the leanEthereum/leanSpec repository and review the diff between the old and new commits for any malicious changes to test fixtures or consensus logic.

2. Consensus compatibility - Fork transition: The change from --fork devnet to --fork Lstar (line 33) is significant. Ensure that:

   • The client implementation actually supports the Lstar fork rules (state transition, validation, XMSS parameters)
   • This isn't just a test configuration change but reflects actual consensus logic updates in src/

3. Style: The removal of = in --scheme prod (line 33) is consistent with POSIX argument styles, but verify the fill command accepts both formats to avoid argument parsing errors.

4. Date comment: Good practice updating the date comment (line 27) to match the new commit timestamp.

Recommendation: Before merging, run the full test suite against the new Lstar fixtures to ensure state transition functions and XMSS signature verification pass, as fixture format may have changed between devnet and Lstar.

---

Automated review by Kimi (Moonshot AI) · kimi-k2.5 · custom prompt

[github-actions]

🤖 Claude Code Review

PR #391 — chore(deps): bump leanSpec to 825bec6, rename fork to Lstar

Overview

Minimal Makefile-only change (3 additions, 3 deletions) that bumps the pinned leanSpec commit from 18fe71f → 825bec6 and renames the --fork argument from devnet → Lstar to unblock make test.

---

Change-by-change analysis

Commit hash bump

The PR description traces the breakage precisely to two upstream commits and pins to the exact fix. Pinning by full SHA (not a branch/tag) is the right approach here — it's reproducible and auditable.

Fork rename (devnet → Lstar)

Matches the upstream rename. Straightforward.

--scheme=prod → --scheme prod

This change is not mentioned in the PR description. Both forms are equivalent in Click (which uv run uses), so it is functionally harmless, but it's a small undocumented delta worth noting for completeness.

---

Potential concerns

• Fixture regeneration time is ~22 min (as noted in the test plan). This is expected for 496 fixtures, but it's worth ensuring CI caches leanSpec/fixtures between runs to avoid paying this cost on every pipeline invocation.
• The change affects only test fixture generation — no runtime code is touched, so the security/consensus-correctness blast radius is zero.

---

Verdict

Approve. The PR is well-motivated, the diff is minimal and correct, the test plan covers the critical paths (rm -rf leanSpec && make leanSpec/fixtures + make test), and pinning by full SHA is sound practice. The only nit is that the --scheme=prod → --scheme prod style tweak could be mentioned in the PR description for completeness.

---

Automated review by Claude (Anthropic) · sonnet · custom prompt

[greptile-apps]

Greptile Summary

This PR updates the pinned leanSpec commit from 18fe71f to 825bec6 to incorporate two upstream fixes that were breaking make test, and renames the fork argument to match the upstream rename.

• Bumps LEAN_SPEC_COMMIT_HASH to 825bec6 (2026-05-21), which brings in a tempfile-close fix (EOFError during tarfile.open) and a JSON schema key rename fix (attestation_public → attestation_keypair.public_key).
• Renames --fork devnet → --fork Lstar to match the upstream fork rename, and removes the = from --scheme=prod (making it --scheme prod), which is an equivalent form for most CLI parsers.

Confidence Score: 5/5

Safe to merge — the change is a targeted commit-hash bump and a matching fork rename, both directly tied to documented upstream breakage.

The only touched file is the Makefile, and every line changed has a clear upstream motivation described in the PR. The commit hash, fork name, and scheme flag syntax all line up with the referenced upstream PRs (#725, #745). The author verified the fix locally with a full clean run of fixture generation and the complete test suite.

No files require special attention.

Important Files Changed

Filename	Overview
Makefile	Bumps LEAN_SPEC_COMMIT_HASH to 825bec6, renames --fork devnet → --fork Lstar, and switches --scheme=prod to --scheme prod to align with upstream leanSpec breaking changes

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[make test] --> B[leanSpec/fixtures]
    B --> C[leanSpec target]
    C --> D[git clone leanSpec.git]
    D --> E[git checkout 825bec6]
    E --> F[uv run fill\n--fork Lstar\n-n auto\n--scheme prod\n-o fixtures]
    F --> G{496 fixtures\ngenerated}
    G --> H[cargo test --workspace --release]

Loading

_{Reviews (1): Last reviewed commit: "chore(deps): bump leanSpec to 825bec6, r..." | Re-trigger Greptile}

[github-actions]

🤖 Codex Code Review

1. Makefile:28-35 — the LEAN_SPEC_COMMIT_HASH bump is not actually enforced once leanSpec/ already exists. Because leanSpec is a file target backed by a directory, make will skip the clone/checkout recipe on subsequent runs, so make test can keep using an older checkout while appearing to use commit 825bec6…. That makes this PR’s main change non-deterministic in cached CI/dev environments. Mark leanSpec/leanSpec/fixtures as .PHONY, or better, key the checkout/generation off a stamp file that includes the pinned hash.

2. Makefile:34-35 — switching fixture generation from devnet to Lstar without clearing leanSpec/fixtures can leave stale JSON from the previous fork in place. The datatest harness walks the fixture directories directly, so deleted/renamed cases from devnet may still run and mix with Lstar outputs. The recipe should remove or recreate the output directory before uv run fill.

No consensus, fork-choice, attestation, STF, XMSS, or SSZ implementation code changes are in this PR; the review surface is limited to fixture reproducibility. Other than the cache/staleness problems above, the update is straightforward.

---

Automated review by OpenAI Codex · gpt-5.4 · custom prompt