feat(stor): track upstream #1182 block-horizon guards in insertBlock (#57)

Mirror the pending leanEthereum/leanSpec#1182 (head 5e1b7b51, fixing
issue #1171): on_block bounds a block's slot right after the parent
lookup, before the state transition's empty-slot loop can run - at
most HISTORICAL_ROOTS_LIMIT beyond the parent state
(BLOCK_SLOT_GAP_TOO_LARGE) and at most one slot past the store clock
(BLOCK_TOO_FAR_IN_FUTURE). STError gains both reasons and Config gains
HISTORICAL_ROOTS_LIMIT.

insertBlock now reads the parent *state*, exactly as on_block does;
parentsPresent_insertBlock therefore takes the #1176 M-4 blocks-states
alignment as a hypothesis to carry presence over to the block map.

insertBlock_slot_gap_bounded and insertBlock_within_horizon extract
the two bounds from a successful insertion - the formal content of
issue #1171's fix.

Hold this PR until upstream #1182 merges; re-verify the mirrored
guards against the merged diff then.

Author: adust09

LeanSpec/Forks/Lstar/Config.lean

@@ -26,4 +26,9 @@ deliberately not a whole slot (`GOSSIP_DISPARITY_INTERVALS`, a `Uint64`
 upstream). -/
 def GOSSIP_DISPARITY_INTERVALS : Nat := 1
 
+/-- SSZ limit on the historical-roots list, doubling as the bound on how
+far a block's slot may run beyond its parent
+(`HISTORICAL_ROOTS_LIMIT`, a `Uint64` upstream). -/
+def HISTORICAL_ROOTS_LIMIT : Nat := 2 ^ 18
+
 end LeanSpec.Forks.Lstar

LeanSpec/Forks/Lstar/Errors.lean

@@ -32,6 +32,11 @@ function and fork-choice attestation validation:
   - `attestationSlotBeforeHead`         ↔ `ATTESTATION_SLOT_BEFORE_HEAD`
   - `attestationTooFarInFuture`         ↔ `ATTESTATION_TOO_FAR_IN_FUTURE`
   - `unknownParentBlock`                ↔ `UNKNOWN_PARENT_BLOCK`
+  - `blockSlotGapTooLarge`              ↔ `BLOCK_SLOT_GAP_TOO_LARGE`
+  - `blockTooFarInFuture`               ↔ `BLOCK_TOO_FAR_IN_FUTURE`
+                                          (both added by the pending
+                                          leanEthereum/leanSpec#1182,
+                                          fixing issue #1171)
 
 The `STError` name is historical — the state-transition function was
 modeled first; the type now carries every modeled rejection reason, like
@@ -84,6 +89,8 @@ inductive STError where
   | attestationSlotBeforeHead (slot head : Slot) : STError
   | attestationTooFarInFuture (slot maxAdmissible : Nat) : STError
   | unknownParentBlock (root : Root) : STError
+  | blockSlotGapTooLarge (slot parentSlot : Slot) : STError
+  | blockTooFarInFuture (slot : Slot) (maxAdmissible : Nat) : STError
   deriving Repr, BEq, Inhabited
 
 /-- Result of a fallible state-transition step. -/

LeanSpec/Storage/Blocks.lean

@@ -1,28 +1,47 @@
 /-
-Block-store chain structure: every stored block's parent is stored.
+Block-store chain structure: every stored block's parent is stored, and
+block acceptance is horizon-bounded.
 
 The catalog sources STOR-1 to a `Database.add_block` parent-existence
 precondition; in current leanSpec no such database method exists — the
 gate lives in fork choice: `on_block`
-(`src/lean_spec/spec/forks/lstar/fork_choice.py`) rejects a block whose
-parent state is not in the store (`UNKNOWN_PARENT_BLOCK`) before
+(`src/lean_spec/spec/forks/lstar/fork_choice.py`) looks up the parent
+*state* and rejects `UNKNOWN_PARENT_BLOCK` when it is absent, before
 `SyncService._persist_block` writes anything, so a block reaches the
 block map only when its parent is already there. The exception is the
 chain anchor: `create_store` seeds the map with a block whose parent is
 outside the tree — the zero hash for a genesis anchor, an absent block
 for a checkpoint-sync anchor.
 
-Modeled here as the guarded insertion `insertBlock` (the parent gate of
-`on_block`, with the upstream `dict` replace-by-key) on the fork-choice
-`Store`, and the invariant `ParentsPresent` it maintains.
+This file also tracks the pending leanEthereum/leanSpec#1182 (head
+`5e1b7b51`, fixing issue #1171): right after the parent lookup,
+`on_block` bounds the block's slot before the empty-slot loop of the
+state transition runs — the slot may run at most
+`HISTORICAL_ROOTS_LIMIT` beyond the parent state
+(`BLOCK_SLOT_GAP_TOO_LARGE`), and at most one slot past the store clock
+(`BLOCK_TOO_FAR_IN_FUTURE`). Re-verify the mirrored guards against the
+merged diff when #1182 lands.
 
-Proves STOR-1 from `docs/lean4-proof-propositions.md`:
+Modeled as the guarded insertion `insertBlock` (the `on_block` gate
+sequence at the point a block enters the block map, with the upstream
+`dict` replace-by-key) on the fork-choice `Store`, and the invariant
+`ParentsPresent` it maintains. The gate reads the *states* map exactly
+as upstream does; carrying its presence over to the *blocks* map is the
+blocks-states alignment invariant (`Store.WellFormed.blocksStatesAligned`,
+issue #1176 M-4), which enters the preservation theorem as a
+hypothesis.
+
+Proves STOR-1 from `docs/lean4-proof-propositions.md` (and the horizon
+bounds of issue #1171):
   - STOR-1: every non-anchor block has its parent in the store —
     anchoring establishes the invariant (`parentsPresent_anchor`),
     guarded insertion preserves it (`parentsPresent_insertBlock`), and
-    on a genesis-anchored store it takes the catalog's form: a stored
-    block's parent is the zero hash or itself stored
+    on a genesis-anchored store it takes the catalog's form
     (`parent_exists_or_genesis`).
+  - An accepted block sits at most `HISTORICAL_ROOTS_LIMIT` beyond its
+    parent state (`insertBlock_slot_gap_bounded`) and at most one slot
+    past the store clock (`insertBlock_within_horizon`) — the formal
+    content of the #1182 fix.
 -/
 
 import LeanSpec.Forks.Lstar.Store.Ancestry
@@ -36,17 +55,29 @@ namespace Store
 
 open LeanSpec.Forks.Lstar.Store
 
-/-- Insert a block under its root, gated on the parent being known —
-the `UNKNOWN_PARENT_BLOCK` rejection of `on_block`, at the point where
-the block enters the store's block map (upstream `dict` assignment,
-replacing any entry with the same root). -/
+/-- Insert a block under its root, gated as `on_block` gates it at the
+point where the block enters the store's block map: the parent *state*
+must be known (`UNKNOWN_PARENT_BLOCK`), the slot may run at most
+`HISTORICAL_ROOTS_LIMIT` beyond the parent (`BLOCK_SLOT_GAP_TOO_LARGE`
+— the empty-slot loop in the transition runs once per slot from the
+parent to the block), and at most one slot past the store clock
+(`BLOCK_TOO_FAR_IN_FUTURE`), per the pending leanEthereum/leanSpec#1182.
+The insertion is the upstream `dict` assignment, replacing any entry
+with the same root. Python's negative slot gap and the truncated `Nat`
+subtraction both pass the gap guard. -/
 def insertBlock (st : LeanSpec.Forks.Lstar.Store) (root : Root)
     (b : Block) : ST.Result LeanSpec.Forks.Lstar.Store :=
-  if (st.getBlock? b.parentRoot).isSome then
-    .ok { st with
-      blocks := (root, b) :: st.blocks.filter (fun p => !(p.1 == root)) }
-  else
-    .error (.unknownParentBlock b.parentRoot)
+  match st.getState? b.parentRoot with
+  | none => .error (.unknownParentBlock b.parentRoot)
+  | some parentState =>
+    if HISTORICAL_ROOTS_LIMIT < b.slot.toNat - parentState.slot.toNat then
+      .error (.blockSlotGapTooLarge b.slot parentState.slot)
+    else if st.time.toNat / INTERVALS_PER_SLOT + 1 < b.slot.toNat then
+      .error (.blockTooFarInFuture b.slot
+        (st.time.toNat / INTERVALS_PER_SLOT + 1))
+    else
+      .ok { st with
+        blocks := (root, b) :: st.blocks.filter (fun p => !(p.1 == root)) }
 
 /-- STOR-1 invariant: every stored block is the chain anchor or has its
 parent stored (the anchor's parent is outside the tree — the zero hash
@@ -113,31 +144,42 @@ private theorem getBlock?_isSome_insert
     exact this st.blocks h
 
 /-- STOR-1, preservation: the parent-gated insertion keeps every stored
-block's parent stored — the new block's parent was required present,
+block's parent stored. The gate reads the states map, as upstream does;
+the blocks-states alignment (`Store.WellFormed.blocksStatesAligned`,
+issue #1176 M-4) carries the parent's presence over to the block map,
 and a replace-by-key insertion never makes a present root absent. -/
 theorem parentsPresent_insertBlock
     (st st' : LeanSpec.Forks.Lstar.Store) (anchorRoot root : Root)
     (b : Block)
+    (halign : ∀ r : Root,
+      (st.getBlock? r).isSome ↔ (st.getState? r).isSome)
     (hpp : ParentsPresent st anchorRoot)
     (h : insertBlock st root b = .ok st') :
     ParentsPresent st' anchorRoot := by
   unfold insertBlock at h
   split at h
-  · next hparent =>
-    injection h with h'
-    subst h'
-    intro p hp
-    cases List.mem_cons.mp hp with
-    | inl hnew =>
-      subst hnew
-      exact .inr (getBlock?_isSome_insert st root b _ hparent)
-    | inr hold =>
-      have hmem := (List.mem_filter.mp hold).1
-      cases hpp p hmem with
-      | inl hanchor => exact .inl hanchor
-      | inr hpresent =>
-        exact .inr (getBlock?_isSome_insert st root b _ hpresent)
   · simp at h
+  · next parentState hparent =>
+    split at h
+    · simp at h
+    · split at h
+      · simp at h
+      · injection h with h'
+        subst h'
+        intro p hp
+        cases List.mem_cons.mp hp with
+        | inl hnew =>
+          subst hnew
+          have hstate : (st.getState? b.parentRoot).isSome := by
+            rw [hparent]; rfl
+          exact .inr (getBlock?_isSome_insert st root b _
+            ((halign b.parentRoot).mpr hstate))
+        | inr hold =>
+          have hmem := (List.mem_filter.mp hold).1
+          cases hpp p hmem with
+          | inl hanchor => exact .inl hanchor
+          | inr hpresent =>
+            exact .inr (getBlock?_isSome_insert st root b _ hpresent)
 
 /-- STOR-1, catalog form: on a genesis-anchored store — the invariant
 plus an anchor whose block carries the zero-hash parent — every stored
@@ -155,5 +197,41 @@ theorem parent_exists_or_genesis (st : LeanSpec.Forks.Lstar.Store)
   | inl hroot => exact .inl (hanchor p hp hroot)
   | inr hpresent => exact .inr hpresent
 
+/-! ## Horizon bounds (issue #1171, pending fix leanEthereum/leanSpec#1182) -/
+
+/-- An accepted block names a stored parent state and sits at most
+`HISTORICAL_ROOTS_LIMIT` beyond it — the empty-slot loop the state
+transition runs from the parent to the block is bounded. -/
+theorem insertBlock_slot_gap_bounded
+    (st st' : LeanSpec.Forks.Lstar.Store) (root : Root) (b : Block)
+    (h : insertBlock st root b = .ok st') :
+    ∃ parentState, st.getState? b.parentRoot = some parentState ∧
+      b.slot.toNat - parentState.slot.toNat ≤ HISTORICAL_ROOTS_LIMIT := by
+  unfold insertBlock at h
+  split at h
+  · simp at h
+  · next parentState hparent =>
+    split at h
+    · simp at h
+    · next hgap =>
+      split at h
+      · simp at h
+      · exact ⟨parentState, hparent, Nat.le_of_not_lt hgap⟩
+
+/-- An accepted block sits at most one slot past the store clock — the
+future-slot horizon issue #1171 asked for. -/
+theorem insertBlock_within_horizon
+    (st st' : LeanSpec.Forks.Lstar.Store) (root : Root) (b : Block)
+    (h : insertBlock st root b = .ok st') :
+    b.slot.toNat ≤ st.time.toNat / INTERVALS_PER_SLOT + 1 := by
+  unfold insertBlock at h
+  split at h
+  · simp at h
+  · split at h
+    · simp at h
+    · split at h
+      · simp at h
+      · next hhorizon => exact Nat.le_of_not_lt hhorizon
+
 end Store
 end LeanSpec.Storage

docs/lean4-proof-propositions.md

@@ -494,7 +494,7 @@ The propositions here guarantee **chain-structure consistency and write atomicit
 - [x] **STOR-1: Every non-genesis Block has its parent in the store**
   - Source: `Database.add_block` (parent-existence precondition; no such database method exists in current leanSpec — the gate is `on_block`'s `UNKNOWN_PARENT_BLOCK` rejection in `src/lean_spec/spec/forks/lstar/fork_choice.py`, which runs before `SyncService._persist_block` writes anything)
   - Note: Each block in the store has a parent block root (`parent_root`); for non-genesis blocks the parent must exist in `store.blocks` (the `block_root → Block` map). The exception generalizes beyond genesis: `create_store` seeds the map with a chain anchor whose parent is outside the tree (zero hash for genesis, an absent block for a checkpoint-sync anchor), so the invariant is stated relative to the anchor root.
-  - Proved at: `LeanSpec/Storage/Blocks.lean` (`Store.parentsPresent_anchor` establishes the invariant at anchoring, `Store.parentsPresent_insertBlock` shows the parent-gated insertion preserves it, and `Store.parent_exists_or_genesis` is the catalog form on a genesis-anchored store)
+  - Proved at: `LeanSpec/Storage/Blocks.lean` (`Store.parentsPresent_anchor` establishes the invariant at anchoring, `Store.parentsPresent_insertBlock` shows the parent-gated insertion preserves it — the gate reads the states map as upstream does, so the #1176 M-4 blocks-states alignment enters as a hypothesis — and `Store.parent_exists_or_genesis` is the catalog form on a genesis-anchored store). `insertBlock` also carries the horizon guards of the pending leanEthereum/leanSpec#1182 (fixing issue #1171): `insertBlock_slot_gap_bounded` and `insertBlock_within_horizon` bound an accepted block's slot against the parent and the store clock.
   - Sample code:
 
     ```lean