docs: add Lean4 proof propositions catalog (JP + EN)#696
Open
adust09 wants to merge 2 commits intoleanEthereum:mainfrom
Open
docs: add Lean4 proof propositions catalog (JP + EN)#696adust09 wants to merge 2 commits intoleanEthereum:mainfrom
adust09 wants to merge 2 commits intoleanEthereum:mainfrom
Conversation
Catalog of propositions to be formally verified in Lean4 to support safe client specification design. Organized into Tier 1/2/3 by proof difficulty across four domains: consensus core, SSZ/base types, validator duties, and networking/sync. Each proposition includes a natural-language statement, a semi-formal (∀/⇒) form, and a Lean4 theorem skeleton. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add docs/lean4-proof-propositions-en.md as an English sibling to the existing Japanese catalog. The English version states 51 propositions with literal constants (MAX_REQUEST_BLOCKS=1024, MAX_PAYLOAD_SIZE=10 MiB, D_low=6, P=2^31-2^24+1) and exact source line ranges so each proposition maps directly to a Lean4 theorem skeleton. Coverage: - Tier 1 (24): SSZ round-trips, range/length invariants, slot/checkpoint algebra, validator dual-key, networking bounds - Tier 2 (19): state-transition monotonicity, supermajority threshold, forkchoice topology, sync FSM, gossipsub mesh bounds, slashing avoidance - Tier 3 (8): forkchoice acyclicity, finalization irreversibility, state_transition purity, hash collision-resistance axiom, Fp ring axioms, XMSS sign/verify round-trip
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds a prioritized catalog of propositions to formally verify the Lean Ethereum consensus spec in Lean4. Two parallel artifacts:
docs/lean4-proof-propositions.md— Japanese version (initial draft).docs/lean4-proof-propositions-en.md— English version, deliberately more concrete: literal constants (MAX_REQUEST_BLOCKS=1024,MAX_PAYLOAD_SIZE=10 MiB,D_low=6, D_high=12,P = 2^31 − 2^24 + 1), exact field names, andfile:lineanchors for every proposition.51 proposition entries total in the English doc, organized by tier:
justified.slot,finalized.slot), supermajority threshold (3v ≥ 2N), forkchoice topology, sync FSM transitions, gossipsub mesh[6,12]bound, slashing avoidance, XMSS prepared-window advancement.state_transitionpurity, hash collision-resistance axiom,Fpcommutative ring + Fermat inverse, XMSS sign/verify round-trip.Each entry has natural-language description, semi-formal
∀/⇒statement, and a Lean4theorem … := by sorryskeleton. The doc also proposes aproofs/lean4/LeanSpec/...file layout and a source-to-propositions cross-reference table.This is a planning artifact only — no Lean4 code is added in this PR. The first proof PRs will discharge Tier 1 lemmas in a follow-up.
Test plan
title,last_updated: 2026-05-01, kebab-casetags)file_path:line_numberreferences point to real files in the working tree