Prove B1 and B3, and make the TLA+ model terminate#3
Merged
Conversation
The raw 3-node model never terminated (msgs grows monotonically): a 12-min run hit 100M+ states and kept going. Two mechanisms fix it: - SYMMETRY Perms == Permutations(Nodes): nodes are interchangeable and every invariant is quantified over all nodes, so permuting them is a sound symmetry for the safety invariants we check. - CONSTRAINT StateConstraint: MaxBallots=1, MaxInflight=6, MaxInhibit=2. One ballot suffices because every invariant here is per-ballot, including the inhibition/approval race. Result: the check completes green — 776,646 distinct states, depth 18, ~1min 48s. The decisive lever was MaxBallots=1, not symmetry alone. The bound has teeth: removing the on_vote fix from the model (the p \notin inhibited[p] guard on RecvVote) makes TLC report NoApproveWhileInhibited violated in ~4s at exactly these bounds, so a passing run is meaningful rather than vacuous. check-tla.sh now terminates green in ~2 min and is a usable gate; docs/tla/README.md, README.md and DEVELOPMENT.md updated to match. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ment Discharges the two remaining Track-B proof targets in EkkHeartbeat.thy, so EkkVerification now machine-checks B1+B2+B3 (green in ~22 s, no sorry, no quick_and_dirty). B1 (ekk_heartbeat_init_verif_ok, total correctness): the lifted init function returns EKK_OK on valid arguments. The 64-iteration neighbor- zeroing loop (six heap writes per iteration) is proved terminating and guard-safe. The postcondition is heap-independent, so the loop invariant carries only the validity facts the per-iteration guards consume; the measure 0x40 - i gives termination. Annotating with whileLoop_add_inv is what keeps wp from unfolding the fixpoint and blowing the stack. is_valid survives the value-heap writes because is_valid_AnonStructN' and heap_AnonStructN'_update are distinct lifted_globals record fields (lifted_globals.simps), leaving only word-arithmetic residues (unat_arith). B3 (health-transition refinement): health_transition_valid_correct proves the C validator computes exactly the abstract valid_health_edge relation, health_step_accepted then shows every abstract health_step transition is accepted, and set_neighbor_health_verif_sets_health proves the setter writes exactly the health field. This re-proves the TLA+ health-machine safety property at the C level. VERIFICATION_PLAN.md: mark phases B1 and B3 DONE with the discharged lemma names, matching the B2 status block. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
What this adds
Follow-up verification work on top of the merged B2 proof (PR #2). Two commits:
a74b014— Make the TLA+ check terminate: symmetry + bounded state constraintThe raw 3-node protocol model never terminated (
msgsgrows monotonically →100M+ states). Added
SYMMETRY Perms == Permutations(Nodes)plus aCONSTRAINT StateConstraint(MaxBallots = 1 — the decisive lever, since everyinvariant is per-ballot — MaxInflight = 6, MaxInhibit = 2). TLC now terminates
green: 776,646 distinct states, depth 18, ~1:48 on the 8 GiB host.
Mutation-tested for teeth: removing the
on_voteinhibition guard makes it failin ~4 s.
8929ba5— Prove B1 and B3 (heartbeat init totality + health refinement)Discharges the two remaining Track-B targets in
EkkHeartbeat.thy:ekk_heartbeat_init_verif_ok(total correctness,⦃ ⦄!): the liftedinit function returns
EKK_OKon valid arguments; the 64-iterationneighbor-zeroing loop (six heap writes/iteration) is proved terminating and
guard-safe. The invariant carries only the per-slot validity the guards
consume; measure
0x40 - igives termination. Annotating withwhileLoop_add_invis what keepswpfrom unfolding the fixpoint.health_transition_valid_correctprovesthe C validator computes exactly the abstract
valid_health_edgerelation;health_step_acceptedshows every abstracthealth_steptransition isaccepted;
set_neighbor_health_verif_sets_healthproves the setter writesexactly the
healthfield. This re-proves the TLA+ health-machine safetyproperty at the C level.
VERIFICATION_PLAN.mdphases B1 and B3 marked DONE with the discharged lemmanames, matching the existing B2 status block.
Verification state
EkkVerificationsession builds green — B1 + B2 + B3 all machine-checked.sorry, noquick_and_dirty(gated byscripts/check-no-sorry.sh).scripts/check-tla.sh).Test / gate status
isabelle build … EkkVerificationscripts/check-no-sorry.shscripts/check-tla.sh(TLC bounded)🤖 Generated with Claude Code