Verified safety of store pruning below the finalized root (via ST-6 / FC-2)

[adust09]

Context

Proven assets:

• ST-6 finalization_irreversible — the finalized checkpoint never moves backward across any reachable transition.
• FC-2 head_descends_from_justified / computeLmdGhostHead_descends — every head returned by fork choice is a descendant of the justified root.
• ST-4 justified_ge_finalized — the justified checkpoint never sits below the finalized one.

Together these imply that no future fork-choice computation can ever reference a block that is not a descendant of the current finalized root. Upstream leanSpec keeps the full block/state maps forever; production clients prune, but the safety of pruning is re-derived informally by every team.

Note: the incremental-head refinement (#67) is about recomputation cost; this issue is about memory — they compose but are independent.

Proposal

1. Define prune : Store → Store that drops every block/state not satisfying AncestorOrEqual st finalizedRoot r (plus the mirrored history entries, per FC-8 HistoryAlignment).
2. Prove observational equivalence: for any WellFormed reachable store, update_head, on_block acceptance, and checkpoint evolution agree between st and prune st (any divergence would require the head to escape the finalized subtree, contradicting FC-2 + ST-6).
3. Prove prune preserves WellFormed and HistoryAlignment.
4. State the resulting memory bound (live store size ≤ blocks at or above the finalized slot) and feed it upstream as a normative pruning rule, spec-feedback.md format.

Why

Pruning is an optimization every client ships and the spec is silent about; a machine-checked equivalence turns "we believe pruning is safe" into a shared theorem, and gives the spec a statable memory upper bound.

Estimated scope

Medium — needs the prune model and a congruence pass over the FC lemmas (ancestorWalk_congr, checkpointIsAncestor_congr, chainAligned_congr already exist as the pattern to follow).

[adust09]

Fully delivered across #73 and #76 (merged to main at ba72845):

• Store.prune — concrete pruning of everything outside the finalized subtree (LeanSpec/Forks/Lstar/Store/Prune.lean).
• Memory bound — prune_blocks_length_le: live store ≤ blocks at or above the finalized slot.
• Invariant preservation — prune_wellFormed.
• Observational equivalence — updateHead_head_prune (head, hypothesis-free) and updateHead_prune (head ∧ re-derived finalized checkpoint, under finalization monotonicity of stored states) in Store/PruneHead.lean.

The monotonicity hypothesis is the fork-choice face of leanEthereum/leanSpec#1176 M-3 (latest_finalized is reorg-mutable): the proof surfaces M-3 as the precise boundary of pruning safety. Upstream proposal follows separately, citing these theorems.