Store pruning below the finalized root is provably safe — propose a normative pruning rule and memory bound

[adust09]

TL;DR

The spec's fork-choice Store keeps blocks/states forever (store.py#L53-L60). Every production client will prune, and each team currently has to re-derive the safety of doing so informally. We have machine-checked that safety in Lean 4 and propose stating it normatively.

How this was found: continuing the formalization at NyxFoundation/formal-leanSpec (same effort as #1176/#1171). All theorems below type-check under lake build at ba72845; model: Store/Prune.lean, Store/PruneHead.lean.

What is proved

Define prune(store): drop every block/state whose root is not a descendant-or-equal of latest_finalized (decided by the spec's own _checkpoint_is_ancestor walk). Then, for any store satisfying the #1176/#1179 invariants:

1. Memory bound (prune_blocks_length_le): the live store never exceeds the blocks at or above the finalized slot — the currently-unbounded maps get a statable upper bound.
2. Invariant preservation (prune_wellFormed): key uniqueness, block/state alignment (M-4), parent-slot order, and the justified checkpoint's presence and finalized ancestry (M-1) all survive pruning.
3. Head equivalence (updateHead_head_prune, hypothesis-free): update_head selects the same head before and after pruning — vote tally, child enumeration, and the fix(fork-choice): make the equal-slot equivocation tie deterministic #1181 content-derived tie-break all read only the finalized subtree.
4. Finalized-checkpoint equivalence (updateHead_prune): the re-derived latest_finalized also agrees, under one condition — no stored post-state finalizes below the store's finalized checkpoint.

The M-3 connection

Condition 4 is exactly #1176 M-3 in fork-choice form: latest_finalized is documented reorg-mutable, so a head state may finalize below the pruning horizon, and the proof shows this is the precise boundary of pruning safety (the descendToSlot walks genuinely diverge there; with monotonicity both landings miss the exact-slot check and agree). consensus-specs avoids this by making update_checkpoints advance-only.

Suggested spec change

1. Add normative text: a node MAY drop any block/state that is not a descendant-or-equal of latest_finalized; a conforming node's update_head output is unchanged by doing so. Cite the memory bound as the resulting storage guarantee.
2. Either make store finalization monotone (the M-3 resolution, matching consensus-specs) or scope the pruning rule to finalization-monotone stores — the theorems support both phrasings.