feat(lstar): sync model with upstream typed-rejection fixes (leanSpec #1177-#1181) - #42
Merged
Merged
Conversation
Upstream leanEthereum/leanSpec#1178 (issue #1174) made Slot.is_justifiable_after total: a slot before the finalized boundary returns False instead of tripping an assert reachable from untrusted state. Mirror the guard in isJustifiableAfter, discharge it in justifiable_iff via the finalized <= target hypothesis, and prove the settled-slot behavior as justifiable_before_finalized (CONT-2).
Upstream leanEthereum/leanSpec#1178 and #1180 (issues #1173/#1174) turned the process_attestations vote-layout asserts into SpecRejectionError raises with dedicated reasons, and split SpecRejectionError from AssertionError via a new SpecError base. Mirror that here: processAttestations now rejects an empty registry (EMPTY_VALIDATOR_REGISTRY), a flat vote list whose length is not roots x validators (JUSTIFICATION_VOTES_LENGTH_MISMATCH), and a zero-hash tracked root (ZERO_HASH_JUSTIFICATION_ROOT), with the two new STError variants added. noJustifiableBetween carries the same settled-slot guard is_justifiable_after gained. The ST-3/ST-4/ST-6 preservation proofs are extended over the new error paths.
Upstream leanEthereum/leanSpec#1179 (issue #1176) documented that Checkpoint.advance_to selects by slot only and that descent from the finalized block is a separate store invariant. Mirror the note so the Lean model and the Python spec read the same.
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
The formalization in this repo surfaced six issues in leanEthereum/leanSpec (adust09's #1171-#1176). Five fixes are now merged upstream (#1177-#1181, current
main@57d4339). This PR re-syncs the Lean model with the updated Python definitions.Upstream changes mirrored
Slot.is_justifiable_aftertotalized: a slot below the finalized boundary returnsFalseinstead of tripping anassertisJustifiableAftergains the settled-slot guard; CONT-2justifiable_iffnow discharges it fromfinalized ≤ target; new lemmajustifiable_before_finalizedproves the guard behavior.noJustifiableBetweencarries the same guardprocess_attestationsvote-layoutasserts became typed rejectionsprocessAttestationsnow rejects withemptyValidatorRegistry, the newjustificationVotesLengthMismatch, and the newzeroHashJustificationRoot; finalization pruning that drops slot-map-missing roots (already the Lean behavior) is upstream behavior now, so the divergence note is retiredSpecRejectionErrorsplit fromAssertionErrorvia a newSpecErrorbaseExcept STErroralready modeled the type-level separation;Errors.leanrecords that upstream now matchesCheckpoint.advance_todocstring: selection is by slot only, ancestry is a store invariantadvanceTodocstring mirrors the noteST-3 / ST-4 / ST-6 preservation proofs are extended over the new error paths;
lake buildpasses with nosorry.Not applicable to the current Lean tree
first_offset == 0, issue #1175): the variable-size list decoder is not yet formalized (SSZ-1..7 cover primitives only) — nothing to update.BLOCK_SLOT_GAP_TOO_LARGE/BLOCK_TOO_FAR_IN_FUTUREraised infork_choice.on_block— outside the state-transition subsetErrors.leanmirrors, so no Lean change is needed even once it merges.