tla: M5 — Composed.tla (Composed-1 + Composed-3) wired into tla-check#865
Conversation
Per §8.1 of docs/design/2026_05_28_partial_tla_safety_spec.md (M5 deliverable): the cross-module safety properties — the two seam invariants that no single-module spec (M1..M4) can express. What lands: - tla/composed/Composed.tla — Recreates the minimal cross-module state needed for Composed-1 (catalog history routes[v], txn observed catalog version txnObservedVer[t], committing group txnCommitGroup[t]) and Composed-3 (monotonic tsCounter advancing on every Commit). Does NOT INSTANCE M1..M4 — that would explode the state space well past the <10 min target from §8.1; the M5 projection preserves the invariants the full product would assert. - tla/composed/MCComposed.tla — TLC model with key + group + txn symmetry. - tla/composed/MCComposed.cfg — safe config (PASS). - tla/composed/MCComposed_gap.cfg — gap config (FAIL on Composed1_CommitToOwningGroup). Invariants encoded: - Composed-1 every committed write key was owned by the committing group at the txn's observed catalog version. Load-bearing cross- module invariant — ties OCC's commit decision to the Routes catalog snapshot the txn read at BeginTxn. - Composed-2 vacuously TRUE in this abstraction because the implementation's SplitRange is same-group only (CLAUDE.md). ProposeRouteChange in M5 explicitly DOES allow cross-group moves so Composed-1 has teeth; Composed-2's cross-group migration clause is a forward-looking guard rail. - Composed-3 distinct commit_ts across committed txns. Holds by construction (monotonic tsCounter advancing on every Commit); PROPERTY Composed3_TsAction strengthens this to "every Commit raises the clock". - Composed_CatalogMonotonic (PROPERTY) catalogVersion weakly increases on every step. - Composed_TsMonotonic (PROPERTY) tsCounter weakly increases. Tooling: - scripts/tla-check.sh: TLA_MODULES gains "composed"; gap_invariant_for + mc_basename gain the corresponding cases. - tla/README.md: M5 status Not started -> Landed; Composed module description + invariant table + MCComposed subsection. Verified locally with `make tla-check`: - HLC safe (3,594) + gap (HLC-4 ce at depth 5). - OCC safe (150) + gap (OCC-1 ce at depth 5). - MVCC safe (79) + gap (MVCC-4 ce at depth 3). - Routes safe (29) + gap (Routes-4 ce at depth 3). - Composed safe (1,684 distinct states) + gap (Composed-1 ce at depth 4: BeginTxn(t), WriteIntent(t, k1), ProposeRouteChange(k1, g2), Commit(t, g2) where routes[0][k1] = g1 # g2). End-to-end runtime well under M5's <10 min target. This is the cap on the spec-only roadmap. Remaining work: - M6 (liveness, OPTIONAL): OCC-L1 + Routes-L1 under fairness. Can follow as a separate PR. - M1 Go follow-up: HLC-4 (iii) ceiling fence — change HLC.Next() to fail-closed when wallNow >= physicalCeiling. Separate code PR with caller audit of every Next() site.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
Warning Review limit reached
More reviews will be available in 20 minutes and 10 seconds. Learn how PR review limits work. Your organization has run out of usage credits. Purchase more in the billing tab. ⌛ How to resolve this issue?After more reviews become available, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans include higher PR review limits than trial, open-source, and free plans. In all cases, reviews become available again over time. During sustained high-volume PR review activity, CodeRabbit may temporarily slow when the next review becomes available. Please see our Fair Usage Limits Policy for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (8)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request implements the M5 milestone by introducing the composed TLA+ specification (Composed.tla) and its corresponding model-checking configurations to verify cross-module safety properties, specifically Composed-1 (committing to the owning group) and Composed-3 (strict serializability bound). It also integrates the new module into the tla-check.sh test harness and updates the documentation. The feedback points out a critical issue in MCComposed.tla where the Symmetry set is defined as a union of permutation sets, which is mathematically incorrect for TLC's symmetry reduction and can lead to unsound model checking. A code suggestion is provided to correctly define the symmetry group as a direct product of the symmetric groups.
| KeySymmetry == Permutations(Keys) | ||
| GroupSymmetry == Permutations(Groups) | ||
| TxnSymmetry == Permutations(TxnIds) | ||
| Symmetry == KeySymmetry \cup GroupSymmetry \cup TxnSymmetry |
There was a problem hiding this comment.
Defining Symmetry as the union of permutation sets (KeySymmetry \cup GroupSymmetry \cup TxnSymmetry) is mathematically incorrect and can lead to unsoundness in TLC model checking. TLC's symmetry reduction algorithm assumes that the set of permutations specified in SYMMETRY forms a group under function composition. The union of symmetric groups on disjoint sets is not closed under composition (e.g., a permutation that permutes both keys and groups is not in the union), so it is not a group. This violates TLC's assumptions and can cause TLC to miss states or behave unpredictably. To fix this, define the symmetry group as the direct product of the symmetric groups using the function union operator @@ from the TLC module.
Symmetry == { kSym @@ gSym @@ tSym : kSym \in KeySymmetry, gSym \in GroupSymmetry, tSym \in TxnSymmetry }
…i HIGH on PR #865) Replaces `KeySymmetry \cup … \cup TxnSymmetry` (and the two analogous two-set constructions in MCMVCC / MCOCC) with the direct product of the per-domain permutation groups, built via the TLC `@@` (function union) operator. Gemini's HIGH-priority review on PR #865 flagged this in MCComposed: TLC's `SYMMETRY` option requires the supplied set to be a *group* of permutations, closed under composition. The set-theoretic union of the disjoint per-domain permutation groups is NOT closed under composition — a permutation that touches both Keys and Groups (for example) is not in the union — so TLC's symmetry-reduction algorithm can silently elide states and report a falsely-clean run. The same construction was duplicated in: * tla/composed/MCComposed.tla (the gemini-flagged file) * tla/mvcc/MCMVCC.tla (KeySymmetry \cup ValSymmetry) * tla/occ/MCOCC.tla (TxnSymmetry \cup KeySymmetry) All three are fixed in one commit so the symmetry contract is consistent across the spec suite. The single-domain modules (MCHLC, MCRoutes) already supplied a single `Permutations(S)` directly, which is already a group, so they are unchanged. The construction `{ kSym @@ … : kSym \in KeySymmetry, … }` works because the per-domain constants are *disjoint* model values (Keys, Vals, Groups, TxnIds, etc.), so `@@` over them is plain function union — every element of the resulting set is a bijection on the disjoint union of the constant sets, and the family is closed under function composition (the product of independent permutations on disjoint domains). Verification: `make tla-check` post-fix — HLC safe pass + HLC-4 gap fail OCC safe pass + OCC-1 gap fail MVCC safe pass + MVCC-4 gap fail Routes safe pass + Routes-4 gap fail Composed safe pass (68 distinct states, depth 4) + Composed-1 gap fail All ten outcomes match the design contract. No spec semantics or invariant statements change — only the symmetry hint expressed to TLC.
|
Gemini HIGH addressed in f8d97b3:
@claude review |
|
Claude finished @bootjp's task in 3m 36s —— View job Code Review — M5 Composed.tla + Symmetry Fix (f8d97b3)
Symmetry fix (f8d97b3) — Correct ✅The Gemini HIGH was correctly addressed. The fix in all three \* OLD (wrong): union of per-domain permutation sets — not closed under composition
Symmetry == KeySymmetry \cup GroupSymmetry \cup TxnSymmetry
\* NEW (correct): direct product via @@ — closed under composition
Symmetry == { kSym @@ gSym @@ tSym :
kSym \in KeySymmetry,
gSym \in GroupSymmetry,
tSym \in TxnSymmetry }Why the fix is sound:
One edge case to confirm is already correct: the sentinel
|
1 participant
Summary
M5 of the TLA+ safety spec — the cross-module safety properties, capping the spec-only roadmap (M1..M5).
M1..M4 each modelled a single subsystem in isolation. M5 captures the seams between them — the two safety properties that no single-module spec can express.
What lands
tla/composed/Composed.tla— recreates the minimal cross-module state needed for Composed-1 (catalog historyroutes[v], txn observed catalog versiontxnObservedVer[t], committing grouptxnCommitGroup[t]) and Composed-3 (monotonictsCounteradvancing on every Commit). Does NOTINSTANCEM1..M4 — that would explode the state space well past M5's<10 min at default boundstarget from §8.1.tla/composed/MCComposed.tla— TLC model with key + group + txn symmetry.tla/composed/MCComposed.cfg/MCComposed_gap.cfg— safe (PASS) + gap (FAIL on Composed-1).scripts/tla-check.sh—TLA_MODULESgains"composed";gap_invariant_for+mc_basenamegain the corresponding cases.tla/README.md— M5 statusNot started→Landed; Composed module description + invariant table.Invariants
SplitRangeis same-group only per CLAUDE.mdcommit_tsComposed_CatalogMonotoniccatalogVersionweakly increases on every stepComposed_TsMonotonictsCounterweakly increases on every stepComposed3_TsActiontsCounterWhy no
INSTANCE?Each M1..M4 module tightly bounds its own state for tractable TLC. Bringing all four
INSTANCEs into one product spec would multiply the state spaces — even a 100x growth lands well past M5's<10 min at default boundstarget. M5 instead recreates the minimal cross-module state needed to express the two seam invariants. The integration claim is that this projection preserves the invariants the full product would assert; reviewers can sanity-check each Composed action against the corresponding M1..M4 action (e.g.,ProposeRouteChangemirrorsRoutes.tla,BeginTxn+CommitmirrorOCC.tlawith a cross-module observed-catalog-version pin).Verification (local)
The Composed-1 counterexample is the canonical 4-step regression:
BeginTxn(t)—txnobservescatalogVersion = 0, whereroutes[0][k1] = g1.WriteIntent(t, k1).ProposeRouteChange(k1, g2)—catalogVersion → 1,routes[1][k1] = g2.Commit(t, g2)(gap mode) — committing group isg2, butroutes[0][k1] = g1 ≠ g2. Composed-1 fails.Self-review (5-lens per CLAUDE.md)
make tla-checkend-to-end runs in ~10 s on a dev laptop, well under the 10-min target.make tla-checkis the coverage layer.Roadmap status (post-merge)
Test plan
tla-checkCI runs green (watchestla/**)tla-spec-ai-reviewdoes NOT fire — spec-only PRmake tla-checkand confirms 10 outcomes (5 safe pass + 5 gap fail)INSTANCE-free projection claim — each Composed action mirrors the corresponding M1..M4 actionOut of scope
SplitRangein the real implementation (currently same-group only)