From 2b41b036a752f7c43a060cf38ce127a7bb56212d Mon Sep 17 00:00:00 2001 From: adust09 Date: Mon, 20 Jul 2026 20:08:49 +0900 Subject: [PATCH 1/2] feat(val): re-align VAL-2 checked insertion with merged leanSpec#1185 Upstream leanEthereum/leanSpec#1185 (closes #1184) now rejects a manifest whose attestation and proposal public keys coincide, at load time and without touching secret bytes. The model's addChecked previously compared PRF seeds as a placeholder for the invited fix; re-align it with the merged shape: - addChecked now compares public keys, with the Arklib-side derivation entering as the publicKeyOf parameter (the repo's crypto-as-parameter pattern). - addChecked_wellFormed holds for every derivation: distinct public keys imply distinct secret keys by congruence alone. - addChecked_seed_distinct keeps the OTS-reuse core of #1184: for seed-fingerprinting derivations an accepted entry's keys have distinct master seeds. - Registry.lean and catalog docstrings drop the stale 'upstream does not enforce' caveat: WellFormed is established by construction since #1185. --- LeanSpec/Validator/Registry.lean | 103 ++++++++++++++++++++----------- docs/lean4-proof-propositions.md | 11 ++-- 2 files changed, 72 insertions(+), 42 deletions(-) diff --git a/LeanSpec/Validator/Registry.lean b/LeanSpec/Validator/Registry.lean index c6ae6e6..2275f7f 100644 --- a/LeanSpec/Validator/Registry.lean +++ b/LeanSpec/Validator/Registry.lean @@ -11,15 +11,19 @@ Mirrors `src/lean_spec/node/validator/registry.py`: `entry.index` at every insertion site, so the model stores the entries directly and looks them up by their own index. -Upstream states the dual-key separation but does not enforce it: -`add` is a bare assignment and `from_yaml` raises only for missing -files and decode failures — a same-key manifest loads silently and -then signs a proposal and an attestation for one slot with one -stateful XMSS key (OTS state reuse; found by attempting VAL-2, an -"invariant maintained only by convention" of the same class as -leanEthereum/leanSpec#1176, reported as #1184). The distinctness -therefore enters as `WellFormed`, and `WellFormed.add` shows the -suggested fix — validating at insertion — preserves it. +Upstream originally stated the dual-key separation but did not +enforce it: `add` was a bare assignment and `from_yaml` raised only +for missing files and decode failures — a same-key manifest loaded +silently and then signed a proposal and an attestation for one slot +with one stateful XMSS key (OTS state reuse; found by attempting +VAL-2, an "invariant maintained only by convention" of the same class +as leanEthereum/leanSpec#1176, reported as #1184). Since +leanEthereum/leanSpec#1185 the loader rejects such a manifest by +comparing its two public keys (the secret bytes stay untouched), so +every loaded registry satisfies the distinctness by construction. +The distinctness enters the theorems as `WellFormed`; `WellFormed.add` +shows unchecked insertion preserves it, and `addChecked` mirrors the +merged load-time check. Proves VAL-2 from `docs/lean4-proof-propositions.md`: - VAL-2: on a well-formed registry, every lookup returns an entry @@ -63,11 +67,11 @@ def get? (reg : ValidatorRegistry) (index : ValidatorIndex) : Option ValidatorEntry := reg.validators.find? (fun e => e.index == index) -/-- The dual-key separation `ValidatorEntry` documents but upstream -does not enforce: every entry's proposal key differs from its -attestation key. A same-key entry would let one slot's proposal and -attestation signatures consume overlapping XMSS one-time-signature -state (see the module docstring). -/ +/-- The dual-key separation `ValidatorEntry` documents and the loader +enforces since leanEthereum/leanSpec#1185: every entry's proposal key +differs from its attestation key. A same-key entry would let one +slot's proposal and attestation signatures consume overlapping XMSS +one-time-signature state (see the module docstring). -/ def WellFormed (reg : ValidatorRegistry) : Prop := ∀ e ∈ reg.validators, e.proposalSecretKey ≠ e.attestationSecretKey @@ -93,36 +97,42 @@ theorem WellFormed.add (reg : ValidatorRegistry) (entry : ValidatorEntry) | inl heq => rw [heq]; exact hentry | inr hmem => exact hwf e (List.mem_filter.mp hmem).1 -/-! ## Checked insertion (the fix shape of leanEthereum/leanSpec#1184) - -Tracks the fix suggested in leanEthereum/leanSpec#1184 (invited by the -maintainers): reject a same-key entry where the check is one -comparison, at insertion. Every one-time key of an XMSS secret key -derives from its master PRF seed, so two keys collide in OTS state -exactly when their seeds coincide — the check compares the seeds -(upstream will compare the manifest's two public keys, which -equivalently fingerprint the seeds). Re-align the shape with the merged -fix when it lands upstream. -/ - -/-- Add a validator entry only when its two keys are distinct — the -load-time validation of leanEthereum/leanSpec#1184. `none` mirrors the -`ValueError` the loader raises on a same-seed manifest. -/ -def addChecked (reg : ValidatorRegistry) (entry : ValidatorEntry) : +/-! ## Checked insertion (the merged fix of leanEthereum/leanSpec#1185) + +Mirrors the fix merged upstream as leanEthereum/leanSpec#1185 (closes +#1184): `from_yaml` rejects a manifest entry whose attestation and +proposal public keys coincide, before any secret key is decoded. The +public-key derivation is Arklib-side crypto, so it enters the model as +the `publicKeyOf` parameter. Distinct public keys imply distinct +secret keys for *every* derivation (a function maps equal inputs to +equal outputs), so `WellFormed` follows with no cryptographic +assumption; the OTS-level content — distinct master seeds — follows +for derivations that fingerprint the seed +(`addChecked_seed_distinct`). -/ + +/-- Add a validator entry only when its two public keys differ — the +load-time validation of leanEthereum/leanSpec#1185. `none` mirrors the +`ValueError` the loader raises on a same-key manifest; the comparison +touches only public material. -/ +def addChecked (publicKeyOf : SecretKey → ByteArray) + (reg : ValidatorRegistry) (entry : ValidatorEntry) : Option ValidatorRegistry := - if entry.proposalSecretKey.prfKey.data == - entry.attestationSecretKey.prfKey.data then + if (publicKeyOf entry.attestationSecretKey).data == + (publicKeyOf entry.proposalSecretKey).data then none else some (reg.add entry) /-- The checked insertion discharges the `WellFormed` distinctness at -construction: an accepted entry passed the seed comparison, and keys -sharing no seed are distinct. Once upstream enforces the check, every -loaded registry is well-formed by construction — closing the loop the -way leanEthereum/leanSpec#1179 did for the store invariants. -/ -theorem addChecked_wellFormed (reg reg' : ValidatorRegistry) +construction, for every public-key derivation: an accepted entry has +distinct public keys, and equal secret keys cannot derive distinct +public keys. Upstream now enforces the check, so every loaded registry +is well-formed by construction — closing the loop the way +leanEthereum/leanSpec#1179 did for the store invariants. -/ +theorem addChecked_wellFormed (publicKeyOf : SecretKey → ByteArray) + (reg reg' : ValidatorRegistry) (entry : ValidatorEntry) (hwf : WellFormed reg) - (h : addChecked reg entry = some reg') : + (h : addChecked publicKeyOf reg entry = some reg') : WellFormed reg' := by unfold addChecked at h split at h @@ -133,5 +143,24 @@ theorem addChecked_wellFormed (reg reg' : ValidatorRegistry) exact WellFormed.add reg entry hwf fun hc => hne (by rw [hc]; exact beq_self_eq_true _) +/-- The OTS-reuse core of leanEthereum/leanSpec#1184: when the +derivation fingerprints the master seed (Arklib derives the public +root from the PRF seed), an accepted entry's two keys have distinct +seeds, so one slot's proposal and attestation signatures can never +consume overlapping one-time-signature state. -/ +theorem addChecked_seed_distinct (publicKeyOf : SecretKey → ByteArray) + (hdet : ∀ k₁ k₂ : SecretKey, k₁.prfKey.data = k₂.prfKey.data → + publicKeyOf k₁ = publicKeyOf k₂) + (reg reg' : ValidatorRegistry) (entry : ValidatorEntry) + (h : addChecked publicKeyOf reg entry = some reg') : + entry.proposalSecretKey.prfKey.data ≠ + entry.attestationSecretKey.prfKey.data := by + unfold addChecked at h + split at h + · simp at h + · next hne => + intro hseed + exact hne (by rw [hdet _ _ hseed]; exact beq_self_eq_true _) + end ValidatorRegistry end LeanSpec.Validator diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index 6784a95..e87bd44 100644 --- a/docs/lean4-proof-propositions.md +++ b/docs/lean4-proof-propositions.md @@ -1,6 +1,6 @@ --- title: leanSpec → Lean4 Theorem Proving Proposition Catalog -last_updated: 2026-07-05 +last_updated: 2026-07-20 tags: - lean4 - formal-verification @@ -388,8 +388,8 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr - [x] **VAL-2: Proposal key and attestation key are distinct** - Source: `proposalKey` / `attestationKey` (ValidatorService; realized as the `attestation_secret_key` / `proposal_secret_key` fields of `ValidatorEntry`, `src/lean_spec/node/validator/registry.py`) - - Note: Each validator manages two separate signing keys, one for block proposal and one for attestations — documented upstream as "without OTS conflict", but **not enforced**: `ValidatorRegistry.add` assigns without validation and `from_yaml` compares nothing, so a same-key manifest loads silently and one slot's proposal + attestation signatures would consume overlapping XMSS one-time-signature state. Found by attempting this proposition; reported upstream as leanEthereum/leanSpec#1184 (the "invariant maintained only by convention" class of #1176). The theorem is therefore proved relative to `ValidatorRegistry.WellFormed`. - - Proved at: `LeanSpec/Validator/Registry.lean` (`ValidatorRegistry.dual_key_distinct`, relative to `WellFormed`; `WellFormed.add` shows the suggested fix — validate at insertion — preserves the invariant) + - Note: Each validator manages two separate signing keys, one for block proposal and one for attestations — documented upstream as "without OTS conflict". Originally **not enforced** (`ValidatorRegistry.add` assigned without validation, `from_yaml` compared nothing, so a same-key manifest loaded silently and one slot's proposal + attestation signatures would consume overlapping XMSS one-time-signature state); found by attempting this proposition and reported upstream as leanEthereum/leanSpec#1184 (the "invariant maintained only by convention" class of #1176). **Enforced since leanEthereum/leanSpec#1185**: the loader rejects a manifest whose two public keys coincide, before touching secret bytes, so every loaded registry satisfies `WellFormed` by construction. + - Proved at: `LeanSpec/Validator/Registry.lean` (`ValidatorRegistry.dual_key_distinct`, relative to `WellFormed`; `WellFormed.add` shows unchecked insertion preserves the invariant; `addChecked` mirrors the merged #1185 public-key check with the derivation as a parameter — `addChecked_wellFormed` for every derivation, `addChecked_seed_distinct` for seed-fingerprinting ones) - Sample code: ```lean @@ -397,8 +397,9 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr reg.proposalKey vid ≠ reg.attestationKey vid := by sorry -- ✅ proved in LeanSpec/Validator/Registry.lean as -- `ValidatorRegistry.dual_key_distinct` (relative to - -- `ValidatorRegistry.WellFormed` — upstream does not enforce the - -- distinctness, so it cannot be derived from construction) + -- `ValidatorRegistry.WellFormed` — established at load time by + -- upstream since leanEthereum/leanSpec#1185, mirrored as + -- `addChecked_wellFormed`) ``` - [x] **VAL-3: Each slot has exactly one proposer** From d4652a884594391fd386caed9ff10e81dfab111c Mon Sep 17 00:00:00 2001 From: adust09 Date: Mon, 20 Jul 2026 20:21:53 +0900 Subject: [PATCH 2/2] feat(st): prove ST-7 checkpoint replacement is strictly forward ST-3/ST-6 bound only the checkpoint slots, so they still admitted a transition that swaps latest_justified / latest_finalized to a different root at the same slot. ST-7 closes that gap at the STF level: across a successful transition each checkpoint is either unchanged as a whole value (root included) or replaced by one at a strictly higher slot, mirroring Checkpoint.advance_to's strict comparison and the finalized < source.slot finalization guard. - New LeanSpec/Forks/Lstar/CheckpointForward.lean with the per-phase chain applyJustification_forward -> processAttestation_forward -> foldlM -> processAttestations_forward, plus processBlockHeader_checkpoints_of_ne_zero (past genesis anchoring the header stage leaves both checkpoints untouched) and the top-level checkpoint_forward. - Genesis anchoring (the first block filling in its parent root at slot 0) is the one designed same-slot replacement; it is excluded by the latestBlockHeader.slot != 0 hypothesis and documented in the catalog entry. - Root ancestry across branches stays a store invariant per upstream leanSpec#1182's Checkpoint.advance_to / Store.latest_finalized notes; it is future FC work, not an STF property. - Catalog: ST-7 entry added, progress table now 31 proved / 1 axiom. --- LeanSpec.lean | 1 + LeanSpec/Forks/Lstar/CheckpointForward.lean | 238 ++++++++++++++++++++ docs/lean4-proof-propositions.md | 23 +- 3 files changed, 260 insertions(+), 2 deletions(-) create mode 100644 LeanSpec/Forks/Lstar/CheckpointForward.lean diff --git a/LeanSpec.lean b/LeanSpec.lean index 1879925..aa6f4fc 100644 --- a/LeanSpec.lean +++ b/LeanSpec.lean @@ -1,4 +1,5 @@ import LeanSpec.Aliases +import LeanSpec.Forks.Lstar.CheckpointForward import LeanSpec.Forks.Lstar.Config import LeanSpec.Forks.Lstar.Containers.Aggregation import LeanSpec.Forks.Lstar.Containers.Attestation diff --git a/LeanSpec/Forks/Lstar/CheckpointForward.lean b/LeanSpec/Forks/Lstar/CheckpointForward.lean new file mode 100644 index 0000000..e14a26c --- /dev/null +++ b/LeanSpec/Forks/Lstar/CheckpointForward.lean @@ -0,0 +1,238 @@ +/- +Strictly-forward checkpoint replacement. + +Mirrors `src/lean_spec/spec/forks/lstar/state_transition.py` in leanSpec: + - `Checkpoint.advance_to` replaces a checkpoint only when the candidate's + slot is strictly higher (`containers/checkpoint.py`; modeled inline as + the strict comparison in `applyJustification`). + - The finalization arm of `process_attestations` replaces + `latest_finalized` only under the `finalized < source.slot` guard. + +ST-3/ST-6 bound only the checkpoint *slots*: they admit a transition that +swaps a checkpoint to a different root at the same slot. This file closes +that gap: across a successful transition each of `latest_justified` / +`latest_finalized` is either unchanged as a whole value — root included — +or replaced by a checkpoint at a strictly higher slot. The one designed +exception is genesis anchoring (the first block fills in its parent root +at slot 0), excluded by the `latestBlockHeader.slot ≠ 0` hypothesis. + +Cross-branch root *ancestry* is deliberately out of the STF's reach: +leanEthereum/leanSpec#1182 documents on `Checkpoint.advance_to` that +"selection is by slot only" and on `Store.latest_finalized` that the +ancestry is a separate store invariant. + +Proves ST-7 from `docs/lean4-proof-propositions.md`: + - ST-7: `State.transition s b = .ok s'` with a non-genesis latest header + implies each checkpoint is unchanged or strictly slot-advanced + (`checkpoint_forward`). +-/ + +import LeanSpec.Forks.Lstar.StateTransition + +namespace LeanSpec.Forks.Lstar +namespace State + +/-- "Unchanged or strictly forward" composes: stepping `a → b → c` where +each step keeps the checkpoint or strictly raises its slot yields the same +disjunction end to end. -/ +private theorem forward_trans {a b c : Checkpoint} + (h₁ : b = a ∨ a.slot < b.slot) (h₂ : c = b ∨ b.slot < c.slot) : + c = a ∨ a.slot < c.slot := by + cases h₁ with + | inl hba => + cases h₂ with + | inl hcb => exact .inl (hcb.trans hba) + | inr hlt => exact .inr (by rw [← hba]; exact hlt) + | inr hlt₁ => + cases h₂ with + | inl hcb => exact .inr (by rw [hcb]; exact hlt₁) + | inr hlt₂ => + exact .inr (UInt64.lt_iff_toNat_lt.mpr + (Nat.lt_trans (UInt64.lt_iff_toNat_lt.mp hlt₁) + (UInt64.lt_iff_toNat_lt.mp hlt₂))) + +/-- `applyJustification` replaces each checkpoint only strictly forward: +the justified checkpoint moves only to a strictly later target, the +finalized checkpoint only to a source strictly past the old finalized +slot; otherwise both are returned unchanged, root included. -/ +theorem applyJustification_forward (rootSlot : Root → Option Nat) + (acc : JFAcc) (src tgt : Checkpoint) : + ((applyJustification rootSlot acc src tgt).latestJustified + = acc.latestJustified ∨ + acc.latestJustified.slot < + (applyJustification rootSlot acc src tgt).latestJustified.slot) ∧ + ((applyJustification rootSlot acc src tgt).latestFinalized + = acc.latestFinalized ∨ + acc.latestFinalized.slot < + (applyJustification rootSlot acc src tgt).latestFinalized.slot) := by + unfold applyJustification + dsimp only + split + · next hfin => + refine ⟨?_, .inr hfin.1⟩ + split + · next hlt => exact .inr hlt + · exact .inl rfl + · refine ⟨?_, .inl rfl⟩ + split + · next hlt => exact .inr hlt + · exact .inl rfl + +/-- One attestation step keeps each checkpoint or strictly advances its +slot: the vote filters and a stored tally leave both untouched, and the +supermajority path is `applyJustification`. -/ +theorem processAttestation_forward (validatorCount : Nat) (hist : Array Root) + (rootSlot : Root → Option Nat) (acc acc' : JFAcc) + (att : AggregatedAttestation) + (h : processAttestation validatorCount hist rootSlot acc att = .ok acc') : + (acc'.latestJustified = acc.latestJustified ∨ + acc.latestJustified.slot < acc'.latestJustified.slot) ∧ + (acc'.latestFinalized = acc.latestFinalized ∨ + acc.latestFinalized.slot < acc'.latestFinalized.slot) := by + unfold processAttestation at h + dsimp only at h + split at h + · simp at h + · injection h with h' + subst h' + exact ⟨.inl rfl, .inl rfl⟩ + · split at h + · simp at h + · injection h with h' + subst h' + exact ⟨.inl rfl, .inl rfl⟩ + · split at h + · injection h with h' + subst h' + exact ⟨.inl rfl, .inl rfl⟩ + · split at h + · injection h with h' + subst h' + exact ⟨.inl rfl, .inl rfl⟩ + · split at h + · injection h with h' + subst h' + exact ⟨.inl rfl, .inl rfl⟩ + · split at h + · simp at h + · split at h + · simp at h + · split at h + · injection h with h' + subst h' + exact ⟨.inl rfl, .inl rfl⟩ + · injection h with h' + subst h' + exact applyJustification_forward rootSlot acc + att.data.source att.data.target + +/-- Folding attestation steps preserves strictly-forward replacement. -/ +theorem foldlM_processAttestation_forward (validatorCount : Nat) + (hist : Array Root) (rootSlot : Root → Option Nat) : + ∀ (atts : List AggregatedAttestation) (acc acc' : JFAcc), + List.foldlM (processAttestation validatorCount hist rootSlot) acc atts + = .ok acc' → + (acc'.latestJustified = acc.latestJustified ∨ + acc.latestJustified.slot < acc'.latestJustified.slot) ∧ + (acc'.latestFinalized = acc.latestFinalized ∨ + acc.latestFinalized.slot < acc'.latestFinalized.slot) + | [], acc, acc', h => by + injection h with h' + subst h' + exact ⟨.inl rfl, .inl rfl⟩ + | att :: atts, acc, acc', h => by + rw [List.foldlM_cons] at h + cases hstep : processAttestation validatorCount hist rootSlot acc att with + | error e => + rw [hstep] at h + injection h + | ok acc₁ => + rw [hstep] at h + have hrest : + List.foldlM (processAttestation validatorCount hist rootSlot) acc₁ + atts = .ok acc' := h + have h1 := processAttestation_forward validatorCount hist rootSlot acc + acc₁ att hstep + have h2 := foldlM_processAttestation_forward validatorCount hist + rootSlot atts acc₁ acc' hrest + exact ⟨forward_trans h1.1 h2.1, forward_trans h1.2 h2.2⟩ + +/-- `processAttestations` keeps each checkpoint or strictly advances its +slot — never a same-slot root swap. -/ +theorem processAttestations_forward (s s' : State) + (atts : List AggregatedAttestation) + (h : processAttestations s atts = .ok s') : + (s'.latestJustified = s.latestJustified ∨ + s.latestJustified.slot < s'.latestJustified.slot) ∧ + (s'.latestFinalized = s.latestFinalized ∨ + s.latestFinalized.slot < s'.latestFinalized.slot) := by + unfold processAttestations at h + dsimp only at h + split at h + · simp at h + · split at h + · simp at h + · split at h + · simp at h + · split at h + · simp at h + · split at h + · simp at h + · next acc heq => + injection h with h' + subst h' + exact foldlM_processAttestation_forward _ _ _ atts _ acc heq + +/-- Past genesis anchoring, `processBlockHeader` leaves both checkpoints +untouched: the anchor branch fires only when the latest header still sits +at slot 0. -/ +theorem processBlockHeader_checkpoints_of_ne_zero (s s' : State) (b : Block) + (hnz : s.latestBlockHeader.slot ≠ 0) + (h : processBlockHeader s b = .ok s') : + s'.latestJustified = s.latestJustified ∧ + s'.latestFinalized = s.latestFinalized := by + unfold processBlockHeader at h + dsimp only at h + split at h + · simp at h + · split at h + · simp at h + · split at h + · simp at h + · split at h + · simp at h + · injection h with h' + subst h' + exact ⟨rfl, rfl⟩ + +/-- ST-7: checkpoint replacement is strictly forward across a successful +transition on a post-anchoring state — each of `latestJustified` / +`latestFinalized` is unchanged as a whole checkpoint (root included) or +moves to a strictly higher slot. A same-slot root swap is impossible. -/ +theorem checkpoint_forward (s s' : State) (b : Block) + (hnz : s.latestBlockHeader.slot ≠ 0) + (h : transition s b = .ok s') : + (s'.latestJustified = s.latestJustified ∨ + s.latestJustified.slot < s'.latestJustified.slot) ∧ + (s'.latestFinalized = s.latestFinalized ∨ + s.latestFinalized.slot < s'.latestFinalized.slot) := by + unfold transition at h + split at h + · simp at h + · unfold processBlock at h + split at h + · simp at h + · next s₁ hh => + have hps := processSlots_checkpoints s b.slot + have hnz' : (processSlots s b.slot).latestBlockHeader.slot ≠ 0 := by + rw [hps.2.2]; exact hnz + have hhdr := + processBlockHeader_checkpoints_of_ne_zero _ _ b hnz' hh + rw [hps.1] at hhdr + rw [hps.2.1] at hhdr + have hatt := processAttestations_forward _ _ _ h + rw [hhdr.1, hhdr.2] at hatt + exact hatt + +end State +end LeanSpec.Forks.Lstar diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index e87bd44..7466f06 100644 --- a/docs/lean4-proof-propositions.md +++ b/docs/lean4-proof-propositions.md @@ -70,13 +70,13 @@ Format: `-`. `DOMAIN` is the abbreviation of the owning area: |---|---:|---:|---:|---:| | SSZ | 6 | 0 | 1 | 7 | | CONT | 2 | 0 | 0 | 2 | -| ST | 6 | 0 | 0 | 6 | +| ST | 7 | 0 | 0 | 7 | | FC | 5 | 0 | 0 | 5 | | VAL | 5 | 0 | 0 | 5 | | NET | 2 | 0 | 0 | 2 | | STOR | 2 | 0 | 0 | 2 | | SYNC | 2 | 0 | 0 | 2 | -| **Total** | **30** | **0** | **1** | **31** | +| **Total** | **31** | **0** | **1** | **32** | ## SSZ & primitive types @@ -286,6 +286,25 @@ The propositions here guarantee that **the STF advances state as expected**: aft -- `State.finalization_irreversible` (with `hwf : AnchorWF s`) ``` +- [x] **ST-7: Checkpoint replacement is strictly forward (no same-slot root swap)** + - Source: `process_attestations` / `process_block_header` (the `Checkpoint.advance_to` strict slot comparison and the `finalized < source.slot` finalization guard; `src/lean_spec/spec/forks/lstar/state_transition.py`) + - Note: ST-3/ST-6 bound only the checkpoint **slots** — they would still admit a transition that swaps `latest_justified` / `latest_finalized` to a different root at the same slot. This proposition closes that gap at the STF level: a successful transition either leaves each checkpoint unchanged **as a whole value (root included)** or replaces it with one at a strictly higher slot. The one designed exception is genesis anchoring (the first block force-assigns both checkpoints to its parent root at slot 0, filling in the genesis root), excluded by the `latestBlockHeader.slot ≠ 0` hypothesis. Cross-branch root *ancestry* is deliberately not an STF property — upstream leanEthereum/leanSpec#1182 documents on `Checkpoint.advance_to` that "selection is by slot only" and on `Store.latest_finalized` that the ancestry is a separate store invariant (future FC work). + - Proved at: `LeanSpec/Forks/Lstar/CheckpointForward.lean` (`State.checkpoint_forward`; per-phase lemmas `applyJustification_forward`, `processAttestation_forward`, `processAttestations_forward`, and `processBlockHeader_checkpoints_of_ne_zero`) + - Sample code: + + ```lean + theorem checkpoint_forward + (s s' : State) (b : Block) + (hnz : s.latestBlockHeader.slot ≠ 0) + (h : State.transition s b = .ok s') : + (s'.latestJustified = s.latestJustified ∨ + s.latestJustified.slot < s'.latestJustified.slot) ∧ + (s'.latestFinalized = s.latestFinalized ∨ + s.latestFinalized.slot < s'.latestFinalized.slot) := by sorry + -- ✅ proved in LeanSpec/Forks/Lstar/CheckpointForward.lean as + -- `State.checkpoint_forward` + ``` + ## Fork Choice **Fork choice** is the algorithm that decides which branch is the canonical chain when multiple valid block candidates exist. Lean Ethereum (lstar) is **LMD-GHOST**-based: it tallies the weight of the latest attestations and selects the heaviest branch downstream of the justified checkpoint as the head. The `Store` is the state holding fork-choice inputs — the block set, the attestation cache, and the latest justified/finalized checkpoints.