Context
Proven assets over the attestation fold (LeanSpec/Forks/Lstar/CheckpointForward.lean, LeanSpec/Forks/Lstar/StateTransition.lean):
foldlM_processAttestation_mono / _forward / _jf / _justified — the fold only moves justification state forward.- VAL
no_double_vote / no_double_vote_after — a repeated vote from the same validator has no effect.
What is not yet stated is the algebraic structure these strongly suggest: each processAttestation is a monotone, idempotent update on a join-semilattice of justification bits, so the fold result is invariant under permutation and deduplication of the batch.
Proposal
- Prove commutativity:
processAttestation a ∘ processAttestation b and the swapped composition reach the same state (both land on "bits {a,b} set", and checkpoint promotion depends only on the reached bit-set).
- Prove idempotence as a fold-level statement:
foldl processAttestation s l = foldl processAttestation s (dedup l) (lifting no_double_vote).
- Combine into the batch theorem: the fold result is invariant under any permutation + dedup of the attestation list.
- Feed upstream as spec text: implementations may reorder, deduplicate, and aggregate attestations before applying them — currently only implied, never guaranteed.
Why
Aggregation-first processing is what real clients do with gossip batches; today its correctness against the sequential spec fold is folklore. A permutation-invariance theorem makes the reference fold order-free by construction and rules out a class of cross-client divergence (same attestation set, different arrival order).
Estimated scope
Small–medium — the monotonicity/idempotence lemmas exist; the new work is the pairwise commutation lemma and the standard fold-permutation lifting.
Context
Proven assets over the attestation fold (
LeanSpec/Forks/Lstar/CheckpointForward.lean,LeanSpec/Forks/Lstar/StateTransition.lean):foldlM_processAttestation_mono/_forward/_jf/_justified— the fold only moves justification state forward.no_double_vote/no_double_vote_after— a repeated vote from the same validator has no effect.What is not yet stated is the algebraic structure these strongly suggest: each
processAttestationis a monotone, idempotent update on a join-semilattice of justification bits, so the fold result is invariant under permutation and deduplication of the batch.Proposal
processAttestation a ∘ processAttestation band the swapped composition reach the same state (both land on "bits {a,b} set", and checkpoint promotion depends only on the reached bit-set).foldl processAttestation s l = foldl processAttestation s (dedup l)(liftingno_double_vote).Why
Aggregation-first processing is what real clients do with gossip batches; today its correctness against the sequential spec fold is folklore. A permutation-invariance theorem makes the reference fold order-free by construction and rules out a class of cross-client divergence (same attestation set, different arrival order).
Estimated scope
Small–medium — the monotonicity/idempotence lemmas exist; the new work is the pairwise commutation lemma and the standard fold-permutation lifting.