feat(fc): prove pruning preserves the fork-choice head and finalized checkpoint - #76

Merged

adust09 merged 7 commits into

mainfrom

feat/fc-prune-head-equiv

Jul 30, 2026

Commits on Jul 30, 2026

feat(fc): define store pruning and prove the finalized-slot memory bound
adust09
committed
b01fda3
feat(fc): prove incremental weight maintenance agrees with the naive tally
adust09
committed
2f85856
feat(fc): prove pruning preserves the store invariants
adust09
committed
57dd6c0
merge: bring incremental-weights lemmas into prune-equiv base
adust09
committed
8dfe08a
feat(fc): prove pruning never changes the fork-choice head
adust09
committed
5865935
feat(fc): prove pruning preserves the re-derived finalized checkpoint
adust09
committed
92f5b7b
merge: resolve LeanSpec.lean import conflict after #73/#74/#75 squash-merges
adust09
committed
aa947c1