formal(P2): make CeremonyStore actually TLC-checkable + model-check it green#240
Merged
Conversation
…t green Roadmap 1b's gate is "TLA+/TLC model checked first" before the Rust store refines it. That gate had never actually run: `Next` quantified `\E e \in Nat`, and TLC cannot enumerate the infinite `Nat` -- it aborts at the initial state with "non-enumerable quantifier bound Nat". So `THEOREM Spec => []Inv` was asserted, never machine-checked. Fix: bound the head-read to `0..len`. `Append` only fires on `expected = len`, so every `e > len` is a disabled transition -- restricting to `0..len` keeps the transition relation faithful (a stale read `e < len` is the benign CAS loser) AND finite. Add `StateBound == len =< 4` and a committed `CeremonyStore.cfg` (RecordIds = 3 model values). TLC result: Model checking completed, NO error found. 2615 states generated, 547 distinct. `Inv` (TypeOK /\ SpineFunctional /\ NoRollback) holds; the temporal `CheckpointMono` and `LenMono` hold. The P2 store invariants (PO-2/2a/2c, OB-15/16) are now genuinely verified, and the model is the refinement target for the Phase-1b pure Rust state machine. formal/README updated to mark the store TLC-checked with the run command. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
hartsock
force-pushed
the
formal/p2-store-tlc-checked
branch
from
July 17, 2026 03:48
c39db60 to
441ed51
Compare
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.
The P2 store gate had never actually run
Roadmap 1b requires the P2 store to be TLC model-checked first, before the pure Rust state machine refines it. That gate had never run:
Nextquantified\E e \in Nat, and TLC cannot enumerate the infiniteNat— it aborts at the initial state (non-enumerable quantifier bound Nat). SoTHEOREM Spec => []Invwas asserted but never machine-verified.Fix
Bound the head-read to
0..len.Appendfires only onexpected = len, so everye > lenis a disabled transition — restricting to0..lenkeeps the transition relation faithful (a stale reade < lenis the benign CAS loser) and finite. AddStateBound == len =< 4and a committedCeremonyStore.cfg(RecordIds= 3 model values).Result (TLC)
Model checking completed. No error has been found.— 2615 states generated, 547 distinct.Inv=TypeOK ∧ SpineFunctional ∧ NoRollbackholds (PO-2/2a/2c, OB-15/16).CheckpointMonoandLenMonohold.The store model is now the genuinely-verified refinement target for the Phase-1b pure Rust state machine.
Test plan
java -cp tla2tools.jar tlc2.TLC -config CeremonyStore.cfg CeremonyStore.tla→ no error.Risk
Low — additive to
formal/tla+ one README row; no Rust, no CI/build config touched.