feat(fc): prove FC-2 the head descends from latest justified

LeanSpec/Forks/Lstar/Store/Ancestry.lean

@@ -12,18 +12,23 @@ only strictly-future block slots, so a stored child always sits strictly
 above its stored parent (`Store.WellFormed.parentSlotLt`,
 leanEthereum/leanSpec#1176 M-context).
 
-Proves FC-4 from `docs/lean4-proof-propositions.md`:
+Proves FC-4 and FC-2 from `docs/lean4-proof-propositions.md`:
   - FC-4: the fork-choice tree is acyclic — on a well-formed store no
     stored block is a proper ancestor of itself (`fork_choice_acyclic`).
     Slots strictly decrease along every proper-ancestor step
     (`properAncestor_slot_lt`), so a cycle would need a slot strictly
     below itself.
+  - FC-2: the head descends from the latest justified checkpoint
+    (`head_descends_from_justified`): the GHOST walk starts at the
+    justified root and only ever steps to stored children
+    (`ghostWalk_ancestorOrEqual`), so the selected head is the anchor
+    itself or a strict descendant (`computeLmdGhostHead_descends`).
 
-The catalog sample decides ancestry with a Boolean `isProperAncestor`;
-the relation is stated here as an inductive `Prop` instead — the walk
-that would decide it is exactly `checkpointIsAncestor`'s, and the
-acyclicity argument needs the derivation structure, not the decision
-procedure.
+The catalog samples decide ancestry with Boolean helpers
+(`isProperAncestor`, `isAncestorOrEqual`); the relations are stated here
+as `Prop`s instead — the walk that would decide them is exactly
+`checkpointIsAncestor`'s, and the acyclicity/descent arguments need the
+derivation structure, not the decision procedure.
 -/
 
 import LeanSpec.Forks.Lstar.Store.Store
@@ -102,5 +107,133 @@ theorem fork_choice_acyclic (st : Store) (hwf : WellFormed st) :
   have := UInt64.lt_iff_toNat_lt.mp hlt
   omega
 
+/-! ## FC-2: the head descends from the latest justified checkpoint -/
+
+/-- `a` is `d` itself or a proper ancestor of it (the catalog's
+`isAncestorOrEqual`, stated relationally like `ProperAncestor`). -/
+def AncestorOrEqual (st : Store) (a d : Root) : Prop :=
+  a = d ∨ ProperAncestor st a d
+
+/-- Proper ancestry composes: a derivation reaching `m` extends by the
+derivation from `m` down to `d`. -/
+theorem ProperAncestor.trans {st : Store} {a : Root} :
+    ∀ {m d : Root}, ProperAncestor st a m → ProperAncestor st m d →
+      ProperAncestor st a d
+  | _, _, h1, .step hd => .tail hd h1
+  | _, _, h1, .tail hd h => .tail hd (ProperAncestor.trans h1 h)
+
+/-- With nodup keys (Python dict semantics), two stored entries sharing
+a root are the same entry. -/
+private theorem mem_unique_of_keys_nodup :
+    ∀ {l : List (Root × Block)}, (l.map (·.1)).Nodup →
+    ∀ {x y : Root × Block}, x ∈ l → y ∈ l → x.1 = y.1 → x = y
+  | [], _, _, _, hx, _, _ => absurd hx (List.not_mem_nil)
+  | p :: t, hnodup, x, y, hx, hy, hxy => by
+    rw [List.map_cons] at hnodup
+    have hnd := List.nodup_cons.mp hnodup
+    cases List.mem_cons.mp hx with
+    | inl hxp =>
+      cases List.mem_cons.mp hy with
+      | inl hyp => rw [hxp, hyp]
+      | inr hyt =>
+        exfalso
+        apply hnd.1
+        rw [hxp] at hxy
+        rw [hxy]
+        exact List.mem_map.mpr ⟨y, hyt, rfl⟩
+    | inr hxt =>
+      cases List.mem_cons.mp hy with
+      | inl hyp =>
+        exfalso
+        apply hnd.1
+        rw [hyp] at hxy
+        rw [← hxy]
+        exact List.mem_map.mpr ⟨x, hxt, rfl⟩
+      | inr hyt => exact mem_unique_of_keys_nodup hnd.2 hxt hyt hxy
+
+/-- With nodup keys, the lookup returns exactly the stored entry (the
+uniqueness half of `getBlock?_eq_some_mem`). -/
+theorem getBlock?_eq_some_of_mem {st : Store}
+    (hnodup : (st.blocks.map (·.1)).Nodup) {r : Root} {b : Block}
+    (h : (r, b) ∈ st.blocks) : st.getBlock? r = some b := by
+  obtain ⟨v, hv⟩ := Option.isSome_iff_exists.mp (getBlock?_isSome_of_mem h)
+  have heq : ((r, v) : Root × Block) = (r, b) :=
+    mem_unique_of_keys_nodup hnodup (getBlock?_eq_some_mem hv) h rfl
+  rw [hv]
+  rw [(Prod.mk.injEq ..).mp heq |>.2]
+
+/-- An eligible child is stored with its parent link at `parent`
+(strengthens `childrenOf_mem` under nodup keys). -/
+theorem childrenOf_parent (st : Store) (weights : Weights)
+    (minScore : Option Nat) (parent c : Root)
+    (hnodup : (st.blocks.map (·.1)).Nodup)
+    (h : c ∈ childrenOf st weights minScore parent) :
+    ∃ b, st.getBlock? c = some b ∧ b.parentRoot = parent := by
+  unfold childrenOf at h
+  rw [List.mem_map] at h
+  obtain ⟨p, hp, rfl⟩ := h
+  have hf := List.mem_filter.mp hp
+  have hpar : p.2.parentRoot = parent :=
+    eq_of_beq ((Bool.and_eq_true ..).mp hf.2).1
+  exact ⟨p.2, getBlock?_eq_some_of_mem hnodup hf.1, hpar⟩
+
+/-- The GHOST descent never leaves the subtree of its start: every step
+moves to a stored child of the current head, so the start is an
+ancestor-or-equal of the result. -/
+theorem ghostWalk_ancestorOrEqual (st : Store) (weights : Weights)
+    (minScore : Option Nat) (hnodup : (st.blocks.map (·.1)).Nodup) :
+    ∀ (fuel : Nat) (head : Root),
+      AncestorOrEqual st head (ghostWalk st weights minScore fuel head)
+  | 0, _ => .inl rfl
+  | fuel + 1, head => by
+    cases hmc : maxChild weights (childrenOf st weights minScore head) with
+    | none =>
+      simp only [ghostWalk, hmc]
+      exact .inl rfl
+    | some best =>
+      have hbmem := maxChild_mem weights _ best hmc
+      obtain ⟨b, hgb, hparent⟩ :=
+        childrenOf_parent st weights minScore head best hnodup hbmem
+      have hstep : ProperAncestor st head best := by
+        rw [← hparent]
+        exact ProperAncestor.step hgb
+      have ih := ghostWalk_ancestorOrEqual st weights minScore hnodup fuel best
+      simp only [ghostWalk, hmc]
+      cases ih with
+      | inl heq => exact .inr (heq ▸ hstep)
+      | inr hpa => exact .inr (hstep.trans hpa)
+
+/-- The selected head sits in the subtree of the anchor it was asked to
+start from — for any vote set and threshold, and regardless of whether
+the anchor is stored (an unknown anchor is returned unchanged). -/
+theorem computeLmdGhostHead_descends (st : Store)
+    (hnodup : (st.blocks.map (·.1)).Nodup) (startRoot : Root)
+    (attestations : List (Nat × AttestationData)) (minScore : Option Nat) :
+    AncestorOrEqual st startRoot
+      (computeLmdGhostHead st startRoot attestations minScore) := by
+  unfold computeLmdGhostHead
+  cases hb : st.getBlock? startRoot with
+  | none => exact .inl rfl
+  | some anchor =>
+    exact ghostWalk_ancestorOrEqual st
+      (accumulateAncestorWeights st attestations anchor.slot) minScore
+      hnodup (st.blocks.length + 1) startRoot
+
+/-- FC-2: the head descends from the latest justified checkpoint — the
+GHOST walk starts at the justified root and only ever steps to stored
+children, so `update_head` selects that root or a strict descendant. -/
+theorem head_descends_from_justified [SSZ.HasHashTreeRoot AttestationData]
+    (st : Store) (hwf : WellFormed st) :
+    AncestorOrEqual st st.latestJustified.root (updateHead st).head := by
+  have hhead : (updateHead st).head =
+      computeLmdGhostHead st st.latestJustified.root
+        (extractAttestationsFromAggregatedPayloads
+          st.latestKnownAggregatedPayloads st.latestFinalized.slot) := rfl
+  rw [hhead]
+  exact computeLmdGhostHead_descends st hwf.blocksKeysNodup
+    st.latestJustified.root
+    (extractAttestationsFromAggregatedPayloads
+      st.latestKnownAggregatedPayloads st.latestFinalized.slot) none
+
 end Store
 end LeanSpec.Forks.Lstar

LeanSpec/Forks/Lstar/Store/Store.lean

@@ -273,8 +273,9 @@ def maxChild (weights : Weights) : List Root → Option Root
     some (cs.foldl (fun best cand => if beats weights best cand then cand else best) c)
 
 /-- Greedy descent to the heaviest leaf (the `while` walk of
-`_compute_lmd_ghost_head`), on explicit fuel. -/
-private def ghostWalk (st : Store) (weights : Weights)
+`_compute_lmd_ghost_head`), on explicit fuel. Public so the descent
+lemmas (FC-2, `Store/Ancestry.lean`) can reason about each step. -/
+def ghostWalk (st : Store) (weights : Weights)
     (minScore : Option Nat) : Nat → Root → Root
   | 0, head => head
   | fuel + 1, head =>

docs/lean4-proof-propositions.md

@@ -71,12 +71,12 @@ 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 |
-| FC | 2 | 3 | 0 | 5 |
+| FC | 3 | 2 | 0 | 5 |
 | VAL | 2 | 3 | 0 | 5 |
 | NET | 0 | 2 | 0 | 2 |
 | STOR | 0 | 2 | 0 | 2 |
 | SYNC | 0 | 2 | 0 | 2 |
-| **Total** | **18** | **12** | **1** | **31** |
+| **Total** | **19** | **11** | **1** | **31** |
 
 ## SSZ & primitive types
 
@@ -308,15 +308,19 @@ The propositions here guarantee **fork-choice consistency**: `compute_head` is d
     --    `Store.updateHead_head_in_store`)
     ```
 
-- [ ] **FC-2: The head descends from the latest justified checkpoint**
-  - Source: `compute_head` (derived property; same function as FC-1)
-  - Note: Confirm that the head is a descendant of justified using the helper `isAncestorOrEqual` (decides whether `a` is an ancestor of, or equal to, `b`).
+- [x] **FC-2: The head descends from the latest justified checkpoint**
+  - Source: `compute_head` (derived property; same function as FC-1 — upstream `update_head` / `_compute_lmd_ghost_head`)
+  - Note: Confirm that the head is a descendant of justified using the helper `isAncestorOrEqual` (decides whether `a` is an ancestor of, or equal to, `b`). Modeled relationally as `Store.AncestorOrEqual` (`a = d ∨ ProperAncestor st a d`), like FC-4's `ProperAncestor`.
+  - Proved at: `LeanSpec/Forks/Lstar/Store/Ancestry.lean` (`Store.head_descends_from_justified`, via `Store.ghostWalk_ancestorOrEqual` — every walk step moves to a stored child — and `Store.computeLmdGhostHead_descends`; `ProperAncestor.trans` composes the steps)
   - Sample code:
 
     ```lean
     theorem head_descends_from_justified (st : Store) (h : Bytes32)
         (hh : Store.computeHead st = h) :
         Store.isAncestorOrEqual st st.latestJustified.root h := by sorry
+    -- ✅ proved in LeanSpec/Forks/Lstar/Store/Ancestry.lean as
+    --    `Store.head_descends_from_justified` (stated directly on
+    --    `(Store.updateHead st).head` under `Store.WellFormed`)
     ```
 
 - [ ] **FC-3: An attestation's source / target / head are slot-ordered**