feat(st): prove ST-7 checkpoint replacement is strictly forward - #60
Merged
Conversation
Upstream leanEthereum/leanSpec#1185 (closes #1184) now rejects a manifest whose attestation and proposal public keys coincide, at load time and without touching secret bytes. The model's addChecked previously compared PRF seeds as a placeholder for the invited fix; re-align it with the merged shape: - addChecked now compares public keys, with the Arklib-side derivation entering as the publicKeyOf parameter (the repo's crypto-as-parameter pattern). - addChecked_wellFormed holds for every derivation: distinct public keys imply distinct secret keys by congruence alone. - addChecked_seed_distinct keeps the OTS-reuse core of #1184: for seed-fingerprinting derivations an accepted entry's keys have distinct master seeds. - Registry.lean and catalog docstrings drop the stale 'upstream does not enforce' caveat: WellFormed is established by construction since #1185.
ST-3/ST-6 bound only the checkpoint slots, so they still admitted a transition that swaps latest_justified / latest_finalized to a different root at the same slot. ST-7 closes that gap at the STF level: across a successful transition each checkpoint is either unchanged as a whole value (root included) or replaced by one at a strictly higher slot, mirroring Checkpoint.advance_to's strict comparison and the finalized < source.slot finalization guard. - New LeanSpec/Forks/Lstar/CheckpointForward.lean with the per-phase chain applyJustification_forward -> processAttestation_forward -> foldlM -> processAttestations_forward, plus processBlockHeader_checkpoints_of_ne_zero (past genesis anchoring the header stage leaves both checkpoints untouched) and the top-level checkpoint_forward. - Genesis anchoring (the first block filling in its parent root at slot 0) is the one designed same-slot replacement; it is excluded by the latestBlockHeader.slot != 0 hypothesis and documented in the catalog entry. - Root ancestry across branches stays a store invariant per upstream leanSpec#1182's Checkpoint.advance_to / Store.latest_finalized notes; it is future FC work, not an STF property. - Catalog: ST-7 entry added, progress table now 31 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
Stacked on #59 (merge that first; this PR retargets to
mainautomatically when its branch is deleted).ST-3/ST-6 bound only the checkpoint slots, so they still admitted a transition that swaps
latest_justified/latest_finalizedto a different root at the same slot. This PR adds ST-7 to the catalog and proves it: across a successful transition, each checkpoint is either unchanged as a whole value (root included) or replaced by one at a strictly higher slot — mirroringCheckpoint.advance_to's strict comparison and thefinalized < source.slotfinalization guard.Changes
LeanSpec/Forks/Lstar/CheckpointForward.lean: the per-phase lemma chainapplyJustification_forward→processAttestation_forward→foldlM_processAttestation_forward→processAttestations_forward, plusprocessBlockHeader_checkpoints_of_ne_zeroand the top-levelState.checkpoint_forward(composition via theforward_transhelper).latestBlockHeader.slot ≠ 0hypothesis, verified necessary: the same proof fails without it.Checkpoint.advance_tothat "selection is by slot only" and onStore.latest_finalizedthat ancestry is a separate store invariant — that is the next FC-side work item, not an STF property.Verification
lake buildsucceeds (36 jobs);#print axioms State.checkpoint_forward→[propext, Quot.sound]only; nosorry.