feat(fc): define store pruning and prove the finalized-slot memory bound (#73)

* feat(fc): define store pruning and prove the finalized-slot memory bound

Deliver the memory-bound half of #71: a concrete Store.prune dropping
every block/state outside the finalized subtree, with

- mem_prune_blocks_iff: a block survives iff the finalized checkpoint
  is its ancestor,
- prune_block_slot_ge / prune_blocks_length_le: every retained block
  sits at or above the finalized slot, bounding the live store by the
  finalized-slot horizon (the statable memory bound for upstream),
- prune_blocks_sublist: pruning only drops entries.

The observational-equivalence half needs a new prune-congruence lemma
family (existing congruence lemmas require blocks equality, which
pruning breaks) and is split into follow-up work.

* feat(fc): prove pruning preserves the store invariants

Deliver the invariant half of #71 on top of the memory bound:

- getBlock?_prune_iff / getState?_prune_iff: lookups on the pruned
  store return the original entry exactly when pruning keeps it
  (via an association-list find?/filter characterization under key
  uniqueness).
- ancestorWalk_sound: walk success exhibits the relational ancestry
  plus the ancestor block at the checkpoint slot (converse of
  ancestorWalk_complete).
- keepBlock_of_ancestorOrEqual: every finalized-subtree block
  survives pruning.
- properAncestor_prune: finalized-rooted ancestry derivations
  transfer to the pruned store (each visited node is kept).
- prune_wellFormed: pruning preserves WellFormed. The justified
  anchor survives with its finalized ancestry: the justified root
  lies on the finalized subtree (M-1), the transferred relation is
  re-run by walk completeness inside the pruned store via an
  auxiliary store whose justified checkpoint is the finalized one
  (breaking the WellFormed circularity), and congruence maps the
  result back.

Author: adust09

LeanSpec.lean

@@ -19,6 +19,7 @@ import LeanSpec.Forks.Lstar.Store.Ancestry
 import LeanSpec.Forks.Lstar.Store.BlockProduction
 import LeanSpec.Forks.Lstar.Store.ChainAlignment
 import LeanSpec.Forks.Lstar.Store.OnBlock
+import LeanSpec.Forks.Lstar.Store.Prune
 import LeanSpec.Forks.Lstar.Store.Store
 import LeanSpec.Networking.Config
 import LeanSpec.Networking.ReqResp