feat(fc): prove FC-8 stored histories mirror the block map - #63
Merged
Conversation
Discharges the stored half of FC-7's residual hjnew hypothesis: an STF-advanced justified checkpoint always names an imported block at its own slot. The descent half stays as the explicit quorum-level assumption (hjdesc) — a competing fork's state can justify a checkpoint off the finalized subtree unless a 2/3-quorum argument (accountable safety) excludes conflicting supermajorities, which is the catalog's known open frontier, not a history fact. STF level (HistoryAlignment.lean): - transition_hist / transition_hist_size: the post-history is the parent history, then the parent root, then one zero hash per skipped slot, sized to the block's slot. - transition_justified_on_chain: the justified checkpoint stays, anchors at slot 0, or lands on the post-history at its own slot with a non-zero root — extracted from the lies_on_chain filter through applyJustification and the attestation fold. Store level (Store/ChainAlignment.lean): - Store.ChainAligned: stored histories are sized to their state's slot, every non-zero entry names a stored block at exactly that slot, and no stored state's justified slot outruns the store's. - applyBlock_chainAligned: the import writes preserve it (parent entries transfer, the boundary entry is the parent block, the tail is zero hashes). - applyBlock_justified_stored: the discharged hjnew half. - onBlock_invariants (FC-8): on_block preserves WellFormed ∧ Aligned ∧ ChainAligned, composing FC-6/FC-7 machinery with the new layer. Catalog: FC-8 entry added; progress table now 34 proved / 1 axiom.
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
Discharges the stored half of FC-7's residual
hjnewhypothesis: an STF-advanced justified checkpoint always names an imported block at exactly its own slot. What remains is precisely the quorum-level assumption (hjdesc), now isolated and documented as the catalog's open frontier.STF level (
HistoryAlignment.lean)transition_hist/transition_hist_size: the post-history is the parent history, then the parent root, then one zero hash per skipped slot — sized exactly to the block's slot.transition_justified_on_chain: across a successful transition the justified checkpoint stays, anchors at slot 0 (genesis), or lands on the post-history at its own slot with a non-zero root. Extracted from thelies_on_chainfilter throughapplyJustificationand the attestation fold (liesOnChain_targetpins target checkpoints to the history).Store level (
Store/ChainAlignment.lean)Store.ChainAligned: stored histories are sized to their state's slot; every non-zero history entry names a stored block at exactly that slot; no stored state's justified slot outruns the store's.applyBlock_chainAligned: the import writes preserve it — parent entries transfer across the grown map, the boundary entry is the parent block, the tail is zero hashes.applyBlock_justified_stored: the dischargedhjnewhalf (three-way index case analysis over the extended history).onBlock_invariants(FC-8):on_blockpreservesWellFormed ∧ Aligned ∧ ChainAligned, composing the FC-6/FC-7 machinery with the new layer.What deliberately remains
The descent half (
hjdesc: an advanced justified checkpoint descends from the store's finalized checkpoint) is not a history fact: a competing fork's state can justify a checkpoint off the finalized subtree unless a 2/3-quorum argument (accountable safety) excludes conflicting supermajorities. Upstream's own M-1 invariant implicitly rests on the same assumption. Isolating it as a single named hypothesis is the point of this PR — the next milestone is the quorum/accountable-safety layer.Catalog
FC-8 entry added; progress table now 34 proved / 1 axiom / 35 total.
Verification
lake buildsucceeds (39 jobs);#print axioms→ standard axioms only; nosorry.