Fast Confirmation Rule (Lean)

A Lean 4 / mathlib formalization of Ethereum's Fast Confirmation Rule — arXiv:2405.00549 and consensus-specs PR #4747. FCR gives ~12-second synchronous confirmation on top of Gasper (LMD-GHOST-HFC fork choice + FFG-Casper finality).

Status

Item	Status
Lean toolchain	v4.30.0-rc2 (mathlib pinned to match)
Scope	§3.1 LMD-GHOST confirmation rule + §4 LMD-GHOST-HFC / FFG-Casper layer
§3.1 (defs, statements, proofs)	done; all three public theorems proved
§4 HFC (defs, statements, proofs)	done; safety + monotonicity proved in both the semantic-gate and the literal Algorithm-1 forms
sorry / admit / project axioms	none (#print axioms = propext, Classical.choice, Quot.sound)
§5 (validator-set changes)	reserved seam; not built

lake build is green (one mathlib standard-set linter pass; no errors).

Quick start

lake exe cache get
lake build

What is proved

§3.1 — LMD-GHOST (FastConfirmation/LMDGhost/TheoremStatements.lean)

Statement	Paper	Informal content
Theorem1_Safety	Thm 1 / Def 4	A confirmed block is, from some time on, on every honest validator's LMD-GHOST head.
Theorem1_Monotonicity	Thm 1 / Def 4	Once confirmed, always confirmed.
HeadFutureAgreement	Lemma 6	Reusable, filter-generic, arbitrary-anchor engine: isLMDGHOSTSafe + NeverFiltered + GJ-weight-non-increase ⇒ head agreement from the next slot. The §4 layer reuses this verbatim.

§4 — LMD-GHOST-HFC / FFG-Casper (FastConfirmation/HFC/TheoremStatements.lean)

Statement	Paper	Informal content
HFC_Safety_Alg1 / HFC_Monotonicity_Alg1	§4.1, Algorithm 1	The headline §4 theorems. Same guarantees as Theorem 1, using the HFC wrapper isConfirmedAlg1, whose selector ranges over the paper's literal per-block rule isConfirmedNoCaching (Algorithm 1, both branches). The semantic conflict gate is eliminated; the remaining AU/Gasper obligations are explicit in Alg1SelectorSafetyInterface / Alg1SafetyInterface / SafeConfirmedAlg1Inputs.
HFC_Safety / HFC_Monotonicity	§4.1 / Def 4	The earlier forms over the combined predicate isHFCConfirmed (LMD-safe + the semantic gate WillNoConflictingChkpBeJustified). Superseded by the _Alg1 pair; kept as a stepping-stone.

The proved facade constants live in FastConfirmation/HFC/ProvenTheorems.lean (HFC_Safety_Alg1_proved, HFC_Monotonicity_Alg1_proved, and the gate-based HFC_Safety_proved, HFC_Monotonicity_proved) and FastConfirmation/LMDGhost/ProvenTheorems.lean (Theorem1_Safety_proved, Theorem1_Monotonicity_proved, HeadFutureAgreement_proved).

These rest on the Definition 8 predicate (isLMDGHOSTSafe/isOneConfirmed), Algorithm 4 (isConfirmed, highestConfirmedSinceEpoch, sg), Algorithm 1 (gjblock, willChkpBeJustified, isConfirmedNoCaching, isConfirmedAlg1), the weights (S, W, Wp, Q, safetyThreshold), the LMD-GHOST head (forkChoiceHead), the FFG layer (Justified/Finalized/votingSource/checkpointOf, plus block-contained AU/GU/GF), and the axiomatized Synchrony bundle including block relay.

A paper-to-Lean correspondence (every definition and statement side-by-side) is in docs/model-annotation.md.

Layout

FastConfirmation/
  Core/        shared vocabulary: Time, Blocks, Validators, Vote, View, Filter, ForkChoice
  LMDGhost/    §3.1: Model/{Weights,Confirm,Rule,Assumptions} + TheoremStatements + Proof + ProvenTheorems
  HFC/         §4: Model (incl. Algorithm 1 isConfirmedAlg1/AU) + TheoremStatements + Proof + ProvenTheorems
docs/
  project-design.md         design decisions, paper mapping, as-built notes
  model-annotation.md       paper ↔ Lean correspondence (defs + statements)
  algorithm1-gate-discharge.md   the semantic-gate elimination (Algorithm-1 path)
  ffg-delivery-abstraction.md    the block-contained FFG vote model and AU visibility bridge

Each layer follows the four-file discipline: Model/ (executable defs) · TheoremStatements.lean (proof-free public Props — the review surface) · Proof/ (internal lemmas) · ProvenTheorems.lean (proved facade).

Reading order

1. docs/project-design.md — design and the paper mapping.
2. FastConfirmation/LMDGhost/TheoremStatements.lean — the §3.1 public claims.
3. FastConfirmation/HFC/Model/FFGRule.lean — the literal rule isConfirmedNoCaching and the isConfirmedAlg1 wrapper.
4. FastConfirmation/HFC/TheoremStatements.lean — the §4 public claims (the headline HFC_Safety_Alg1 / HFC_Monotonicity_Alg1).
5. docs/algorithm1-gate-discharge.md — the gate-elimination rationale.
6. FastConfirmation/{Core,LMDGhost,HFC}/Model/ — the definitions.

Verification

rg -n '\b(sorry|admit|axiom)\b' FastConfirmation --glob '*.lean'   # should find nothing
lake build                                                         # elaborates + verifies all defs, statements, and proofs (§3.1 and §4)