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.

Author: adust09

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

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

docs/lean4-proof-propositions.md

@@ -70,13 +70,13 @@ Format: `<DOMAIN>-<number>`. `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.