chore: bump leanSpec commit to e9ddede (2026-04-16)

[MegaRedHand]

Summary

• Updates LEAN_SPEC_COMMIT_HASH in the Makefile from 76d4792 (2026-04-14) to e9ddede (2026-04-16), picking up the latest upstream leanSpec changes used to regenerate fork choice, signature, and state transition test fixtures.

Test plan

• rm -rf leanSpec && make test passes locally against the refreshed fixtures
• CI is green

[greptile-apps]

Greptile Summary

Routine leanSpec fixture bump: updates LEAN_SPEC_COMMIT_HASH in the Makefile from 76d4792 (2026-04-14) to e9ddede (2026-04-16) to pull in the latest upstream fork choice, signature, and state transition test fixtures. No logic or code changes are included.

Confidence Score: 5/5

Safe to merge — single-line hash bump with no code changes.

The entire PR is a two-line diff updating a commit hash and its date comment. No logic, no security surface, no breaking changes. CI passing confirms the new fixtures are compatible.

No files require special attention.

Important Files Changed

Filename	Overview
Makefile	Bumps LEAN_SPEC_COMMIT_HASH from 76d4792 (2026-04-14) to e9ddede (2026-04-16) to pick up the latest upstream leanSpec test fixtures; no logic changes.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[Makefile\nLEAN_SPEC_COMMIT_HASH bump] --> B[e9ddede\n2026-04-16]
    B --> C[rm -rf leanSpec &&\nmake leanSpec/fixtures]
    C --> D[Regenerated test fixtures\nforkchoice / signature / stf]
    D --> E[make test\ncargo test --workspace --release]

Loading

_{Reviews (1): Last reviewed commit: "chore: bump leanSpec commit to e9ddede (..." | Re-trigger Greptile}

[github-actions]

🤖 Kimi Code Review

Makefile: Dependency Update Review

This is a high-risk change for a consensus client. Updating the formal specification commit hash affects protocol correctness guarantees.

Security & Correctness Issues:

1. Unused Variable Risk (Line 28)
   The LEAN_SPEC_COMMIT_HASH variable is defined but the visible leanSpec target (lines 30-31) performs git clone without checking out this specific commit. Ensure the Makefile executes git checkout $(LEAN_SPEC_COMMIT_HASH) after cloning, or the pin is ineffective.

2. Supply Chain Verification Missing
   No GPG signature verification or checksum validation for the external leanEthereum/leanSpec repository. For consensus-critical code, add:

   # Verify commit signature if available
   git verify-commit $(LEAN_SPEC_COMMIT_HASH) || (echo "Signature check failed"; exit 1)

3. Opaque Specification Change
   The diff between 76d4792... and e9ddede... is not documented. For consensus spec updates, the PR description should include:

   • Link to the spec diff: https://github.com/leanEthereum/leanSpec/compare/76d4792...e9ddede
   • Summary of consensus logic changes (fork choice, state transition, or XMSS signature rules)
   • Impact analysis on existing test vectors

Minor:

• Line 27: Date format 2026-04-16 appears to be futuristic (relative to current date). Verify this is intentional versioning and not a system clock error or placeholder.

Recommendation:
Block merge until the PR description documents what changed in the Lean spec and confirms the new commit hash is from the official leanEthereum repository (verify committer GPG keys).

---

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

[github-actions]

🤖 Claude Code Review

PR #294 Review: chore: bump leanSpec commit to e9ddede (2026-04-16)

Author: Tomás Grüner | Type: Dependency/Fixture bump

---

Overview

This PR updates a single Makefile variable — LEAN_SPEC_COMMIT_HASH — to pin the upstream leanSpec test fixture repository to a newer commit (76d4792 → e9ddede, 2026-04-14 → 2026-04-16). No application logic is modified.

---

Analysis

The change itself is clean and correct:

• The diff is exactly what it claims: two lines changed, one being the date comment and one being the commit hash.
• The commit hash is a full 40-character SHA, which is the safe and correct way to pin an external dependency in a Makefile (versus a branch or tag, which can move).
• The accompanying date comment (# 2026-04-16) is kept in sync, which aids auditability.

---

Considerations

• No changelog or spec diff included. It would be useful to know what changed in leanSpec between 76d4792 and e9ddede. If upstream made breaking spec changes, that could silently affect test behavior. Consider linking to the leanSpec commit range (e.g., 76d4792...e9ddede) in the PR description.

• Test plan checkbox is unchecked. Both items (rm -rf leanSpec && make test locally, CI green) are listed but not checked off. The PR should not be merged until CI is confirmed green, especially since fixture changes can expose latent spec divergences.

• No fixture files are committed. The .gitignore or workflow presumably regenerates leanSpec/ on demand. This is consistent with the project pattern (rm -rf leanSpec && make leanSpec/fixtures), so no concern here.

---

Verdict

Low-risk, routine maintenance. Ready to merge once CI passes. The only optional improvement would be adding the leanSpec commit range URL to the PR description for traceability.

---

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

[github-actions]

🤖 Codex Code Review

No findings in the repo diff.

The PR only updates the pinned external leanSpec commit in Makefile and the checkout used by Makefile. There are no direct changes here to fork choice, attestation validation, justification/finalization, state transition logic, XMSS handling, SSZ code, or Rust memory/error-handling paths.

Residual risk: this does change the upstream fixture/spec baseline indirectly, so the real behavior change lives outside this repo. I could not validate the contents of commit e9ddede89f87a46da585bcbce6b5080fad08d5de or regenerate leanSpec fixtures in this environment because leanSpec/ is not present locally and network access is restricted.

---

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