feat(fc): prove pruning preserves the fork-choice head and finalized checkpoint - #76
Merged
Conversation
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.
…tally Deliver the weight-delta layer of #67: the algebraic core that makes proto-array-style incremental head computation a refinement of the naive spec walk. - Weights.Equiv: extensional equality of weight maps, with get_bump characterizing bump as pointwise +1. - creditChain_get_add / accumulateAncestorWeights_append: the vote tally is pointwise additive, so per-vote weight deltas are well-defined. - accumulateAncestorWeights_perm: the tally is order-free — an incremental maintainer may apply vote updates in any order. - ghostWalk_congr_weights / computeLmdGhostHead_incremental: the GHOST descent (children, threshold, comparison, tie-break) reads weights only through get, so any maintained map extensionally equal to the full tally selects exactly the spec head. creditChain is made public (was private) so the lemmas can reason about each step, mirroring the ghostWalk precedent. The best-child/best-descendant cache layer of proto-array sits on top and is follow-up; its correctness reduces to the walk over the same weight function proved here.
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.
Deliver the head half of #71's observational equivalence: updateHead_head_prune — for any WellFormed store, (updateHead (prune st)).head = (updateHead st).head. Proof structure: - Subtree closure: ancestors of kept blocks at or above the finalized slot are kept (keepBlock_of_chain, via ancestor comparability); no ancestor of an off-subtree block is kept (keepBlock_off_chain). - Vote weights agree on the subtree (KeptAgree): an on-subtree vote credits an identical chain in both stores (creditChain_prune_keptAgree); an off-subtree vote credits only off-subtree blocks in the full store (creditChain_get_off) and nothing in the pruned store. - The GHOST walk reads only the subtree: children of kept blocks are the same list in both stores (childrenOf_prune, filter absorption), and all weight comparisons happen at kept roots (ghostWalk_prune). - Fuel stability: both walks are driven by blocks.length + 1, which shrinks under pruning; the walks visit only kept blocks at strictly monotone slots, so any fuel above the subtree size gives the same result (creditChain_fuel_stable, ghostWalk_fuel_stable, with keptBelow/keptAbove as decreasing measures). The finalized-checkpoint half of update_head (descendToSlot re-derivation) is follow-up: it interacts with the reorg-mutable latest_finalized (leanEthereum/leanSpec#1176 M-3), since a head state may finalize below the pruning horizon. Branch merges feat/fc-incremental-weights for Weights.get_bump.
Complete #71's observational equivalence of update_head: updateHead_prune — for any WellFormed store whose stored states never finalize below the store's finalized checkpoint, pruning changes neither the selected head nor the re-derived finalized checkpoint. - finalizeAt / descendToSlot_stop: the checkpoint derivation as a function of the walk landing. - descend_finalize_prune: the re-derivation walks may genuinely diverge — when the head chain jumps past the target slot into pruned territory, the full store descends one block further than the pruned store — but both landings then miss the exact-slot check, so the derived checkpoint agrees (the interesting case of the equivalence). - updateHead_latestFinalized_eq: definitional reduction of the latestFinalized field to finalizeAt over the walk. The monotonicity hypothesis is the fork-choice face of leanEthereum/leanSpec#1176 M-3 (latest_finalized is reorg-mutable): it is exactly the condition a pruning client must ensure, mirroring consensus-specs' monotone update_checkpoints. The proof surfaces M-3 as the precise boundary of pruning safety.
adust09
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Completes #71's observational equivalence of
update_head, stacked on #73 and depending on #74 (branch mergesfeat/fc-incremental-weights; diff shrinks toPruneHead.leanonce those land).Main theorems (
LeanSpec/Forks/Lstar/Store/PruneHead.lean):Pruning below the finalized root changes neither the selected head (hypothesis-free) nor the re-derived finalized checkpoint (under finalization monotonicity of stored states).
Head half
KeptAgree): on-subtree votes credit identical chains; off-subtree votes credit nothing kept in either store.keptBelow/keptAbovemeasures).Finalized-checkpoint half (second commit)
descend_finalize_prune— the interesting case: thedescendToSlotwalks may genuinely diverge (when the head chain jumps past the target slot into pruned territory, the full store descends one block further), but both landings then miss the exact-slot check, so the derived checkpoint agrees.hmonohypothesis is the fork-choice face of Fork-choice store invariants maintained only by convention (4 unstated invariants) leanEthereum/leanSpec#1176 M-3 (latest_finalizedis reorg-mutable): it is exactly the condition a pruning client must ensure, mirroring consensus-specs' monotoneupdate_checkpoints. The proof surfaces M-3 as the precise boundary of pruning safety — direct evidence for the upstream monotonicity proposal.All theorems sorry-free;
lake buildpasses with zero warnings.Refs #71