From a901a0727b7261e33431d7ec499a778e653a9875 Mon Sep 17 00:00:00 2001 From: adust09 Date: Mon, 20 Jul 2026 20:41:57 +0900 Subject: [PATCH] feat(fc): prove FC-6 update_head preserves the store invariants The head-walk theorems (FC-2/FC-4) assumed Store.WellFormed without any proof that the store's own operations maintain it. This closes the gap for update_head, the one modeled mutator: all six clauses survive. Five clauses carry over untouched (update_head rewrites only head and latest_finalized). The substantive clause is justifiedDescendsFromFinalized, proved from: - descendToSlot_ancestorOrEqual: the finalized re-derivation walk never leaves the head's ancestor chain. - properAncestor_comparable / ancestors_comparable: parent links are unique, so two ancestors of one block sit on one chain; the wrong order is killed by slot arithmetic. - ancestorWalk_complete: completeness of the Boolean _checkpoint_is_ancestor walk against the relational ancestry. The fuel argument counts distinct stored blocks at or below the walk's position (slotCount), which strictly shrinks every step, so blocks.length + 1 fuel always suffices. - checkpointIsAncestor_of_ancestorOrEqual packages the walk guard and completeness into the stored clause. Two store invariants that on_block maintains outside update_head's reach enter as explicit hypotheses rather than growing WellFormed: the justified checkpoint records its own block's slot, and no stored post-state finalizes past the store's justified slot (backed by ST-4). ancestorWalk and descendToSlot are de-privatized so the lemmas can reason about each step, mirroring the earlier ghostWalk treatment. Catalog: FC-6 entry added; progress table now 32 proved / 1 axiom. --- LeanSpec/Forks/Lstar/Store/Ancestry.lean | 415 ++++++++++++++++++++++- LeanSpec/Forks/Lstar/Store/Store.lean | 10 +- docs/lean4-proof-propositions.md | 21 +- 3 files changed, 439 insertions(+), 7 deletions(-) diff --git a/LeanSpec/Forks/Lstar/Store/Ancestry.lean b/LeanSpec/Forks/Lstar/Store/Ancestry.lean index 7d665a4..a597eda 100644 --- a/LeanSpec/Forks/Lstar/Store/Ancestry.lean +++ b/LeanSpec/Forks/Lstar/Store/Ancestry.lean @@ -12,7 +12,7 @@ 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 and FC-2 from `docs/lean4-proof-propositions.md`: +Proves FC-4, FC-2, and FC-6 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 @@ -29,6 +29,12 @@ The catalog samples decide ancestry with Boolean helpers 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. + +Also proves FC-6: `update_head` preserves the store invariants +(`updateHead_wellFormed`) — only `head` and `latest_finalized` change, +and the re-derived finalized checkpoint stays on the justified chain; +see the FC-6 section docstring below for the argument and the two +`on_block`-maintained hypotheses. -/ import LeanSpec.Forks.Lstar.Store.Store @@ -235,5 +241,412 @@ theorem head_descends_from_justified [SSZ.HasHashTreeRoot AttestationData] (extractAttestationsFromAggregatedPayloads st.latestKnownAggregatedPayloads st.latestFinalized.slot) none +/-! ## FC-6: `update_head` preserves the store invariants + +`updateHead` rewrites only `head` and `latestFinalized`, so five of the +six `WellFormed` clauses carry over untouched. The substantive one is +`justifiedDescendsFromFinalized`: the re-derived finalized checkpoint — +the head chain's ancestor at the head state's finalized slot — must +still sit on the justified checkpoint's chain. The argument: the head +descends from the justified root (FC-2), the re-derived root is an +ancestor of the head (`descendToSlot_ancestorOrEqual`), parent links +are unique so two ancestors of one block are comparable +(`properAncestor_comparable`), and the wrong order is killed by slots. +Completeness of the Boolean `ancestorWalk` against the relational +ancestry (`ancestorWalk_complete`) turns that into the stored clause; +its fuel argument counts distinct stored blocks below the walk's +position, which strictly shrinks every step. -/ + +/-- Parent links are unique, so two proper ancestors of one block are +comparable: one is an ancestor-or-equal of the other. -/ +theorem properAncestor_comparable {st : Store} : + ∀ {a j d : Root}, ProperAncestor st a d → ProperAncestor st j d → + AncestorOrEqual st a j ∨ ProperAncestor st j a + | _, _, _, @ProperAncestor.step _ _ b₁ hd₁, + @ProperAncestor.step _ _ b₂ hd₂ => by + have hb : b₂ = b₁ := Option.some.inj (hd₂.symm.trans hd₁) + exact .inl (.inl (by rw [hb])) + | _, _, _, @ProperAncestor.step _ _ b₁ hd₁, + @ProperAncestor.tail _ _ _ b₂ hd₂ h₂ => by + have hb : b₂ = b₁ := Option.some.inj (hd₂.symm.trans hd₁) + exact .inr (hb ▸ h₂) + | _, _, _, @ProperAncestor.tail _ _ _ b₁ hd₁ h₁, + @ProperAncestor.step _ _ b₂ hd₂ => by + have hb : b₂ = b₁ := Option.some.inj (hd₂.symm.trans hd₁) + exact .inl (.inr (hb ▸ h₁)) + | _, _, _, @ProperAncestor.tail _ _ _ b₁ hd₁ h₁, + @ProperAncestor.tail _ _ _ b₂ hd₂ h₂ => by + have hb : b₂ = b₁ := Option.some.inj (hd₂.symm.trans hd₁) + exact properAncestor_comparable h₁ (hb ▸ h₂) + +/-- Comparability lifted to ancestor-or-equal: two ancestors of one +block sit on one chain. -/ +theorem ancestors_comparable {st : Store} {a j d : Root} + (ha : AncestorOrEqual st a d) (hj : AncestorOrEqual st j d) : + AncestorOrEqual st a j ∨ ProperAncestor st j a := by + cases ha with + | inl heq => + cases hj with + | inl heq' => exact .inl (.inl (heq.trans heq'.symm)) + | inr hpj => exact .inr (heq ▸ hpj) + | inr hpa => + cases hj with + | inl heq' => exact .inl (.inr (heq' ▸ hpa)) + | inr hpj => exact properAncestor_comparable hpa hpj + +/-- The finalized re-derivation walk never leaves the ancestor chain of +its start: every step follows a stored parent link. -/ +theorem descendToSlot_ancestorOrEqual (st : Store) (finalizedSlot : Slot) : + ∀ (fuel : Nat) (r : Root), + AncestorOrEqual st (descendToSlot st finalizedSlot fuel r) r + | 0, r => .inl rfl + | fuel + 1, r => by + unfold descendToSlot + cases hr : st.getBlock? r with + | none => exact .inl rfl + | some b => + dsimp only + split + · cases hp : st.getBlock? b.parentRoot with + | none => exact .inl rfl + | some bp => + dsimp only + have hstep : ProperAncestor st b.parentRoot r := + ProperAncestor.step hr + have ih := + descendToSlot_ancestorOrEqual st finalizedSlot fuel b.parentRoot + cases ih with + | inl heq => exact .inr (by rw [heq]; exact hstep) + | inr hpa => exact .inr (hpa.trans hstep) + · exact .inl rfl + +/-- Dropping entries can only shorten a filter. -/ +private theorem filter_length_mono {α : Type} (p q : α → Bool) : + ∀ (l : List α), (∀ x ∈ l, p x = true → q x = true) → + (l.filter p).length ≤ (l.filter q).length + | [], _ => Nat.le_refl _ + | x :: t, himp => by + have ht := filter_length_mono p q t + (fun y hy => himp y (List.mem_cons_of_mem x hy)) + cases hp : p x with + | true => + rw [List.filter_cons_of_pos hp, + List.filter_cons_of_pos (himp x List.mem_cons_self hp)] + exact Nat.succ_le_succ ht + | false => + rw [List.filter_cons_of_neg (by simp [hp])] + cases hq : q x with + | true => + rw [List.filter_cons_of_pos hq] + exact Nat.le_succ_of_le ht + | false => + rw [List.filter_cons_of_neg (by simp [hq])] + exact ht + +/-- A member kept by `q` but dropped by `p` makes the `p`-filter +strictly shorter. -/ +private theorem filter_length_lt {α : Type} (p q : α → Bool) : + ∀ (l : List α), (∀ x ∈ l, p x = true → q x = true) → + ∀ w ∈ l, q w = true → p w = false → + (l.filter p).length < (l.filter q).length + | [], _, w, hw, _, _ => absurd hw (List.not_mem_nil) + | x :: t, himp, w, hw, hqw, hpw => by + have himpt : ∀ y ∈ t, p y = true → q y = true := + fun y hy => himp y (List.mem_cons_of_mem x hy) + cases List.mem_cons.mp hw with + | inl hwx => + subst hwx + rw [List.filter_cons_of_neg (by simp [hpw]), + List.filter_cons_of_pos hqw] + exact Nat.lt_succ_of_le (filter_length_mono p q t himpt) + | inr hwt => + have ht := filter_length_lt p q t himpt w hwt hqw hpw + cases hp : p x with + | true => + rw [List.filter_cons_of_pos hp, + List.filter_cons_of_pos (himp x List.mem_cons_self hp)] + exact Nat.succ_lt_succ ht + | false => + rw [List.filter_cons_of_neg (by simp [hp])] + cases hq : q x with + | true => + rw [List.filter_cons_of_pos hq] + exact Nat.lt_succ_of_lt ht + | false => + rw [List.filter_cons_of_neg (by simp [hq])] + exact ht + +/-- Stored entries at or below a slot — the fuel measure of +`ancestorWalk_complete`. Every walk step strictly shrinks it: the +current block leaves the count and parent steps strictly lower the +slot. -/ +private def slotCount (st : Store) (s : Slot) : Nat := + (st.blocks.filter (fun p => decide (p.2.slot.toNat ≤ s.toNat))).length + +private theorem slotCount_le (st : Store) (s : Slot) : + slotCount st s ≤ st.blocks.length := + List.length_filter_le _ _ + +/-- A parent step strictly shrinks the measure: the child's entry +counts for the child's slot but not for the strictly lower parent +slot. -/ +private theorem slotCount_lt {st : Store} {d : Root} {bd : Block} + (hd : st.getBlock? d = some bd) {s : Slot} + (hlt : s.toNat < bd.slot.toNat) : + slotCount st s < slotCount st bd.slot := by + apply filter_length_lt _ _ st.blocks + · intro x _ hx + have h1 := of_decide_eq_true hx + exact decide_eq_true (Nat.le_trans h1 (Nat.le_of_lt hlt)) + · exact getBlock?_eq_some_mem hd + · exact decide_eq_true (Nat.le_refl _) + · exact decide_eq_false (show ¬(bd.slot.toNat ≤ s.toNat) by omega) + +/-- Completeness of the `_checkpoint_is_ancestor` walk against the +relational ancestry: starting anywhere on a chain that contains the +ancestor — whose stored block sits exactly at the checkpoint's slot — +the walk finds it, given fuel for the stored blocks at or below the +start. Slots strictly decrease along the chain, so the walk can neither +stop early at the ancestor's slot on a different root nor jump past +it. -/ +theorem ancestorWalk_complete {st : Store} (hwf : WellFormed st) + (anc : Checkpoint) {ar : Root} (har : anc.root = ar) {ba : Block} + (hba : st.getBlock? ar = some ba) (hslot : ba.slot = anc.slot) : + ∀ (fuel : Nat) (d : Root) (bd : Block), + st.getBlock? d = some bd → + AncestorOrEqual st ar d → + slotCount st bd.slot ≤ fuel → + ancestorWalk st anc fuel d = true + | 0, d, bd, hbd, _, hfuel => by + exfalso + have hmem : (d, bd) ∈ st.blocks := getBlock?_eq_some_mem hbd + have : 0 < slotCount st bd.slot := by + apply List.length_pos_of_mem + exact List.mem_filter.mpr ⟨hmem, decide_eq_true (Nat.le_refl _)⟩ + omega + | fuel + 1, d, bd, hbd, hanc, hfuel => by + unfold ancestorWalk + rw [hbd] + dsimp only + by_cases hslots : bd.slot = anc.slot + · rw [if_pos hslots] + -- At the ancestor's slot the chain position is the ancestor + -- itself: a proper ancestor would sit strictly below. + cases hanc with + | inl heq => + rw [← heq, har] + exact beq_self_eq_true ar + | inr hpa => + exfalso + have hlt := properAncestor_slot_lt hwf hpa ba bd hba hbd + have h1 := UInt64.lt_iff_toNat_lt.mp hlt + have h2 : ba.slot = bd.slot := by rw [hslot, hslots] + rw [h2] at h1 + omega + · rw [if_neg hslots] + by_cases hbelow : bd.slot < anc.slot + · exfalso + -- The chain cannot start below the ancestor it contains. + cases hanc with + | inl heq => + rw [heq] at hba + have : ba = bd := Option.some.inj (hba.symm.trans hbd) + rw [this] at hslot + exact hslots hslot + | inr hpa => + have hlt := properAncestor_slot_lt hwf hpa ba bd hba hbd + have h1 := UInt64.lt_iff_toNat_lt.mp hlt + have h2 := UInt64.lt_iff_toNat_lt.mp hbelow + have h3 : ba.slot.toNat = anc.slot.toNat := by rw [hslot] + omega + · rw [if_neg hbelow] + -- Strictly above the ancestor: the position cannot be the + -- ancestor itself, so the derivation steps to the parent. + have hne : ar ≠ d := by + intro heq + rw [heq] at hba + have : ba = bd := Option.some.inj (hba.symm.trans hbd) + rw [this] at hslot + exact hslots hslot + cases hanc with + | inl heq => exact absurd heq hne + | inr hpa => + cases hpa with + | @step _ b' hd' => + -- The ancestor is the parent link itself. + have hb' : bd = b' := Option.some.inj (hbd.symm.trans hd') + subst hb' + have hplt : ba.slot < bd.slot := + hwf.parentSlotLt (d, bd) (getBlock?_eq_some_mem hbd) + (bd.parentRoot, ba) (getBlock?_eq_some_mem hba) rfl + exact ancestorWalk_complete hwf anc har hba hslot fuel + bd.parentRoot ba hba (.inl rfl) + (by + have := slotCount_lt hbd (UInt64.lt_iff_toNat_lt.mp hplt) + omega) + | @tail _ _ b' hd' hpa' => + have hb' : bd = b' := Option.some.inj (hbd.symm.trans hd') + subst hb' + obtain ⟨bp, hbp⟩ := hpa'.descendant_block + have hplt : bp.slot < bd.slot := + hwf.parentSlotLt (d, bd) (getBlock?_eq_some_mem hbd) + (bd.parentRoot, bp) (getBlock?_eq_some_mem hbp) rfl + exact ancestorWalk_complete hwf anc har hba hslot fuel + bd.parentRoot bp hbp (.inr hpa') + (by + have := slotCount_lt hbd (UInt64.lt_iff_toNat_lt.mp hplt) + omega) + +/-- The stored `checkpointIsAncestor` clause from relational ancestry: +an ancestor whose block sits exactly at its slot, on the chain of a +descendant checkpoint no earlier than it, is found by the walk. -/ +theorem checkpointIsAncestor_of_ancestorOrEqual {st : Store} + (hwf : WellFormed st) (anc desc : Checkpoint) {ba bd : Block} + (hba : st.getBlock? anc.root = some ba) (hslot : ba.slot = anc.slot) + (hbd : st.getBlock? desc.root = some bd) + (hanc : AncestorOrEqual st anc.root desc.root) + (hle : anc.slot ≤ desc.slot) : + checkpointIsAncestor st anc desc = true := by + unfold checkpointIsAncestor + rw [if_neg (UInt64.not_lt.mpr hle)] + exact ancestorWalk_complete hwf anc rfl hba hslot (st.blocks.length + 1) + desc.root bd hbd hanc + (Nat.le_trans (slotCount_le st bd.slot) (Nat.le_succ _)) + +/-- `checkpointIsAncestor` reads only the block map, which `updateHead` +never touches. -/ +private theorem ancestorWalk_congr {st st' : Store} + (hblocks : st'.blocks = st.blocks) (anc : Checkpoint) : + ∀ (fuel : Nat) (r : Root), + ancestorWalk st' anc fuel r = ancestorWalk st anc fuel r + | 0, _ => rfl + | fuel + 1, r => by + unfold ancestorWalk + have hget : st'.getBlock? r = st.getBlock? r := by + unfold getBlock? + rw [hblocks] + rw [hget] + cases st.getBlock? r with + | none => rfl + | some b => + dsimp only + split + · rfl + · split + · rfl + · exact ancestorWalk_congr hblocks anc fuel b.parentRoot + +private theorem checkpointIsAncestor_congr {st st' : Store} + (hblocks : st'.blocks = st.blocks) (anc desc : Checkpoint) : + checkpointIsAncestor st' anc desc = checkpointIsAncestor st anc desc := by + unfold checkpointIsAncestor + rw [hblocks, ancestorWalk_congr hblocks] + +/-- FC-6: `update_head` preserves the store invariants. Only `head` and +`latestFinalized` change, so the block/state clauses carry over; the +re-derived finalized checkpoint stays on the justified chain because it +is the head chain's ancestor at the head state's finalized slot, the +head descends from the justified root (FC-2), and one chain orders its +ancestors by slot. + +The two extra hypotheses are store invariants upstream's `on_block` +maintains outside `update_head`'s reach, stated explicitly rather than +grown into `WellFormed`: + - `hjslot` — the justified checkpoint records the slot of its own + block (`validate_attestation` enforces exactly this shape for every + vote checkpoint; `on_block` builds `latest_justified` from + checkpoints produced by the STF, which pairs each root with its + block's slot). + - `hdom` — no stored post-state finalizes past the store's justified + slot (`on_block` advances `store.latest_justified` over every + stored state's justified checkpoint, and ST-4 bounds each state's + finalized slot by its justified slot). -/ +theorem updateHead_wellFormed [SSZ.HasHashTreeRoot AttestationData] + (st : Store) (hwf : WellFormed st) + (hjslot : ∀ bj, st.getBlock? st.latestJustified.root = some bj → + bj.slot = st.latestJustified.slot) + (hdom : ∀ r s₀, st.getState? r = some s₀ → + s₀.latestFinalized.slot ≤ st.latestJustified.slot) : + WellFormed (updateHead st) := by + have hblocks : (updateHead st).blocks = st.blocks := rfl + have hjust : (updateHead st).latestJustified = st.latestJustified := rfl + refine ⟨hwf.blocksKeysNodup, hwf.statesKeysNodup, + hwf.blocksStatesAligned, hwf.parentSlotLt, hwf.justifiedInBlocks, ?_⟩ + rw [checkpointIsAncestor_congr hblocks, hjust] + -- The new finalized checkpoint, by the cases of `update_head`'s + -- re-derivation. + show checkpointIsAncestor st + (match st.getState? + (computeLmdGhostHead st st.latestJustified.root + (extractAttestationsFromAggregatedPayloads + st.latestKnownAggregatedPayloads st.latestFinalized.slot)) with + | none => st.latestFinalized + | some headState => + let finalizedSlot := headState.latestFinalized.slot + let finalizedRoot := + descendToSlot st finalizedSlot (st.blocks.length + 1) + (computeLmdGhostHead st st.latestJustified.root + (extractAttestationsFromAggregatedPayloads + st.latestKnownAggregatedPayloads st.latestFinalized.slot)) + match st.getBlock? finalizedRoot with + | none => st.latestFinalized + | some b => + if b.slot = finalizedSlot then + { root := finalizedRoot, slot := finalizedSlot } + else st.latestFinalized) + st.latestJustified = true + cases hstate : st.getState? + (computeLmdGhostHead st st.latestJustified.root + (extractAttestationsFromAggregatedPayloads + st.latestKnownAggregatedPayloads st.latestFinalized.slot)) with + | none => exact hwf.justifiedDescendsFromFinalized + | some headState => + dsimp only + cases hfb : st.getBlock? + (descendToSlot st headState.latestFinalized.slot + (st.blocks.length + 1) + (computeLmdGhostHead st st.latestJustified.root + (extractAttestationsFromAggregatedPayloads + st.latestKnownAggregatedPayloads st.latestFinalized.slot))) with + | none => exact hwf.justifiedDescendsFromFinalized + | some b => + dsimp only + by_cases hbslot : b.slot = headState.latestFinalized.slot + · rw [if_pos hbslot] + -- The substantive case: the re-derived checkpoint. + obtain ⟨bj, hbj⟩ := + Option.isSome_iff_exists.mp hwf.justifiedInBlocks + have hbjslot := hjslot bj hbj + have hfslot := hdom _ _ hstate + -- The head descends from the justified root; the re-derived + -- root is an ancestor of the head. + have hhead := computeLmdGhostHead_descends st hwf.blocksKeysNodup + st.latestJustified.root + (extractAttestationsFromAggregatedPayloads + st.latestKnownAggregatedPayloads st.latestFinalized.slot) none + have hdesc := descendToSlot_ancestorOrEqual st + headState.latestFinalized.slot (st.blocks.length + 1) + (computeLmdGhostHead st st.latestJustified.root + (extractAttestationsFromAggregatedPayloads + st.latestKnownAggregatedPayloads st.latestFinalized.slot)) + -- Two ancestors of the head are comparable; the justified root + -- below the re-derived one would order the slots backwards. + cases ancestors_comparable hdesc hhead with + | inl hanc => + exact checkpointIsAncestor_of_ancestorOrEqual hwf _ _ hfb hbslot + hbj hanc hfslot + | inr hpj => + exfalso + have hlt := properAncestor_slot_lt hwf hpj bj b hbj hfb + have h1 := UInt64.lt_iff_toNat_lt.mp hlt + have h2 := UInt64.le_iff_toNat_le.mp hfslot + have h3 : bj.slot.toNat = st.latestJustified.slot.toNat := by + rw [hbjslot] + have h4 : b.slot.toNat = headState.latestFinalized.slot.toNat := by + rw [hbslot] + omega + · rw [if_neg hbslot] + exact hwf.justifiedDescendsFromFinalized + end Store end LeanSpec.Forks.Lstar diff --git a/LeanSpec/Forks/Lstar/Store/Store.lean b/LeanSpec/Forks/Lstar/Store/Store.lean index d273874..0d3bb4f 100644 --- a/LeanSpec/Forks/Lstar/Store/Store.lean +++ b/LeanSpec/Forks/Lstar/Store/Store.lean @@ -143,8 +143,9 @@ theorem getBlock?_eq_some_mem {st : Store} {r : Root} {b : Block} ancestor checkpoint (the loop of `_checkpoint_is_ancestor`): landing on the ancestor's slot decides by root equality, climbing past it without landing means the ancestor is off this chain, and leaving the known tree -ends the search. -/ -private def ancestorWalk (st : Store) (ancestor : Checkpoint) : +ends the search. Public so the completeness lemma (FC-6, +`Store/Ancestry.lean`) can reason about each step. -/ +def ancestorWalk (st : Store) (ancestor : Checkpoint) : Nat → Root → Bool | 0, _ => false | fuel + 1, current => @@ -395,8 +396,9 @@ def computeLmdGhostHead (st : Store) (startRoot : Root) /-- Climb from `current` to its ancestor at `finalizedSlot` (the finalized re-derivation loop of `update_head`); the walk stops early -when the parent leaves the known tree. -/ -private def descendToSlot (st : Store) (finalizedSlot : Slot) : +when the parent leaves the known tree. Public so the descent lemma +(FC-6, `Store/Ancestry.lean`) can reason about each step. -/ +def descendToSlot (st : Store) (finalizedSlot : Slot) : Nat → Root → Root | 0, current => current | fuel + 1, current => diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index 7466f06..0b4626f 100644 --- a/docs/lean4-proof-propositions.md +++ b/docs/lean4-proof-propositions.md @@ -71,12 +71,12 @@ Format: `-`. `DOMAIN` is the abbreviation of the owning area: | SSZ | 6 | 0 | 1 | 7 | | CONT | 2 | 0 | 0 | 2 | | ST | 7 | 0 | 0 | 7 | -| FC | 5 | 0 | 0 | 5 | +| FC | 6 | 0 | 0 | 6 | | VAL | 5 | 0 | 0 | 5 | | NET | 2 | 0 | 0 | 2 | | STOR | 2 | 0 | 0 | 2 | | SYNC | 2 | 0 | 0 | 2 | -| **Total** | **31** | **0** | **1** | **32** | +| **Total** | **32** | **0** | **1** | **33** | ## SSZ & primitive types @@ -386,6 +386,23 @@ The propositions here guarantee **fork-choice consistency**: `compute_head` is d -- `build_block_selection_terminates` (pass count ≤ candidates + 1) ``` +- [x] **FC-6: `update_head` preserves the store invariants** + - Source: `update_head` (`src/lean_spec/spec/forks/lstar/fork_choice.py`; the finalized re-derivation loop, with the `Checkpoint.advance_to` / `Store.latest_finalized` invariant notes of leanEthereum/leanSpec#1182) + - Note: `update_head` rewrites only `head` and `latest_finalized`, so five of the six `Store.WellFormed` clauses carry over untouched. The substantive clause is `justifiedDescendsFromFinalized`: the re-derived finalized checkpoint — the head chain's ancestor at the head state's finalized slot — must still sit on the justified chain. Proved from FC-2 (the head descends from the justified root), a descent lemma for the re-derivation walk, comparability of two ancestors of one block (parent links are unique), and completeness of the Boolean `_checkpoint_is_ancestor` walk against the relational ancestry (the fuel argument counts distinct stored blocks at or below the walk's position, which strictly shrinks each step). Two store invariants that `on_block` maintains outside `update_head`'s reach enter as explicit hypotheses rather than growing `WellFormed`: the justified checkpoint records its own block's slot, and no stored post-state finalizes past the store's justified slot (via ST-4). + - Proved at: `LeanSpec/Forks/Lstar/Store/Ancestry.lean` (`Store.updateHead_wellFormed`; via `properAncestor_comparable` / `ancestors_comparable`, `descendToSlot_ancestorOrEqual`, `ancestorWalk_complete`, and `checkpointIsAncestor_of_ancestorOrEqual`) + - Sample code: + + ```lean + theorem updateHead_wellFormed (st : Store) (hwf : Store.WellFormed st) + (hjslot : ∀ bj, st.getBlock? st.latestJustified.root = some bj → + bj.slot = st.latestJustified.slot) + (hdom : ∀ r s₀, st.getState? r = some s₀ → + s₀.latestFinalized.slot ≤ st.latestJustified.slot) : + Store.WellFormed (Store.updateHead st) := by sorry + -- ✅ proved in LeanSpec/Forks/Lstar/Store/Ancestry.lean as + -- `Store.updateHead_wellFormed` + ``` + ## Validator A **Validator** is an entity that stakes ETH and participates in consensus. At each slot it executes its assigned **duties**: (1) propose a new block if selected as `proposer`, and (2) vote on the current head as an `attester`. The validator service locally manages its keys (a dual-key configuration with a proposal key and an attestation key) and signed history.