tla: M3 — MVCC.tla (MVCC-1 + MVCC-4) + mvcc wired into tla-check

[bootjp]

Summary

M3 of the TLA+ safety spec — the MVCC layer encoded as a per-key version chain with a Compact action and a ghost variable that preserves the original Write history so MVCC-4 is checkable.

Follows PR #858 (M2 OCC spec).

What lands

• tla/mvcc/MVCC.tla — Write(k, v) allocates a fresh tsCounter and appends to both versions[k] and the ghost originalVersions[k]; Compact(newMin) advances the retention watermark and (under EnableSafety) retains the largest commit_ts below newMin per key so reads at read_ts ≥ minRetained still see the original value.
• tla/mvcc/MCMVCC.tla — TLC model module with key + value symmetry.
• tla/mvcc/MCMVCC.cfg / MCMVCC_gap.cfg — safe (PASS) + gap (FAIL on MVCC-4).
• scripts/tla-check.sh — TLA_MODULES gains "mvcc"; gap_invariant_for gains the pinned MVCC-4 string.
• tla/README.md — M3 status Not started → Landed; MVCC module description + invariant table.

Invariants

#	Statement	Form
MVCC-1	No two distinct version records on the same key share a commit_ts	INVARIANT
MVCC-4	For every key k and every read_ts ∈ [minRetained, MaxTs], LatestBefore(versions[k], ts) = LatestBefore(originalVersions[k], ts)	INVARIANT
MVCC_TsMonotonic	tsCounter weakly increases across every step	PROPERTY
MVCC_GhostMonotonic	originalVersions[k] only grows; Compact leaves it UNCHANGED	PROPERTY

Deferred to M5

• MVCC-2 (no version below the HLC physical ceiling) is properly an HLC.tla property — the ceiling discipline lives there. M5 will check the cross-spec form once HLC.tla is INSTANCE-d into the composed model.
• MVCC-3 (cross-node read consistency) requires a multi-node model that the single-node M3 spec cannot express.

Verification (local)

$ make tla-check
... TLC: tla/hlc/MCHLC.cfg  (correct design, expected PASS)
... 3594 distinct states found, 0 left on queue
... TLC: tla/hlc/MCHLC_gap.cfg  (...expected FAIL on HLC4...)
OK: MCHLC_gap.cfg failed as designed (Invariant HLC4_NoRegressionAcrossTerms is violated)

... TLC: tla/occ/MCOCC.cfg  (correct design, expected PASS)
... 150 distinct states found, 0 left on queue
... TLC: tla/occ/MCOCC_gap.cfg  (...expected FAIL on OCC1...)
OK: MCOCC_gap.cfg failed as designed (Invariant OCC1_CommitTsAboveStart is violated)

... TLC: tla/mvcc/MCMVCC.cfg  (correct design, expected PASS)
... 79 distinct states found, 0 left on queue
... TLC: tla/mvcc/MCMVCC_gap.cfg  (...expected FAIL on MVCC4...)
OK: MCMVCC_gap.cfg failed as designed (Invariant MVCC4_NoLostCommitOnSnapshotInstall is violated)

tla-check: all model-check outcomes match the design contract.

The MVCC-4 counterexample is short (depth 3): one Write at commit_ts = 1, one Compact(newMin = 2), and the read at read_ts ∈ [2, MaxTs] now sees NotFound where the ghost still shows the Write's value.

Modelling notes

• Compact retention semantics. Under EnableSafety the per-key prune keeps every version with commit_ts ≥ newMin AND the single largest version with commit_ts < newMin (so any later read in [newMin, MaxTs] still sees the same value the original log would have shown). Under the gap toggle, the prune drops every version with commit_ts < newMin, including the latest-before-newMin retention.
• originalVersions as a ghost. Carrying every Write in a parallel set that Compact never touches lets MVCC-4 be a direct equality between the actual store and the canonical "what should be visible" set. It is the simplest faithful encoding of "no commit is lost" for a single-node spec.
• HLC abstraction. tsCounter is a single monotonic counter; M5 will replace it with an INSTANCE of HLC.tla's real 48/16 layout. This keeps M3's state space tight (79 distinct states under the default bounds).
• Symmetry. Keys and values are both symmetric in MVCC.tla because they participate only as indices in the invariants — neither has an ordering. MCMVCC.tla declares both via Permutations.

Self-review (5-lens per CLAUDE.md)

1. Data loss — exactly the property MVCC-4 captures. Verified by gap-config counterexample.
2. Concurrency — single-node M3 model; multi-node interactions deferred to M5.
3. Performance — make tla-check end-to-end runs in under 5 seconds at default bounds.
4. Data consistency — MVCC-1 (uniqueness) + MVCC-4 (preserved visibility) + two PROPERTY transitions. MVCC-2 / MVCC-3 deferred to M5 with rationale.
5. Test coverage — no Go tests added (spec-only). make tla-check is the new coverage layer.

Test plan

• tla-check CI workflow runs green (watches tla/**)
• tla-spec-ai-review does NOT fire — spec-only PR
• Reviewer cross-checks MVCC-1 / MVCC-4 invariants against §5.3 of the design doc
• Reviewer runs make tla-check and confirms 6 outcomes (HLC / OCC / MVCC safe pass + gap fail)

Out of scope

• MVCC-2 (HLC ceiling discipline) — checked in M5.
• MVCC-3 (multi-node read consistency) — checked in M5.
• M4 (Routes) and M5 (Composed) — separate future PRs.

Summary by CodeRabbit

• New Features

  • Added a formal MVCC model capturing per-key version chains, compaction behavior, and snapshot safety checks.

• Documentation

  • Marked milestone M3 (MVCC) as landed and expanded docs describing model scope, invariants, modes, and expected gap-counterexample behavior.

• Tests

  • Extended verification harness to run MVCC in both safety and gap modes, including an expected counterexample check for the MVCC-4 invariant.

[coderabbitai]

Warning

Review limit reached

@bootjp, we couldn't start this review because you've reached your PR review rate limit.

More reviews will be available in 36 minutes and 5 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 @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

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 configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 2407920f-de8e-4162-b8c8-da668f6a45f0

📥 Commits

Reviewing files that changed from the base of the PR and between 9142eaa and e7a8a0b.

📒 Files selected for processing (6)

• scripts/tla-check.sh
• tla/README.md
• tla/routes/MCRoutes.cfg
• tla/routes/MCRoutes.tla
• tla/routes/MCRoutes_gap.cfg
• tla/routes/Routes.tla

📝 Walkthrough

Walkthrough

Adds a TLA+ MVCC spec with per-key version chains, compaction behavior, safety invariants, model-check harness and safe/gap TLC configs, plus README updates and test-harness integration to run MVCC checks.

Changes

MVCC Formal Specification and Verification

Layer / File(s)	Summary
MVCC specification contracts and initialization tla/mvcc/MVCC.tla (lines 1–75)	Defines module constants (Keys, Vals, MaxTs, MaxOps, EnableSafety), state variables (versions, originalVersions, tsCounter, minRetained, opCount), the NotFound sentinel, LatestBefore helper, and Init initialization.
MVCC transitions and safety properties tla/mvcc/MVCC.tla (lines 85–192)	Implements Write(k,v) and Compact(newMin) with RetainOnCompact; defines Spec, StateConstraint, TypeOK, MVCC1_VisibleVersionUnique, MVCC4_NoLostCommitOnSnapshotInstall, and monotonicity properties (MVCC_TsMonotonic, MVCC_GhostMonotonic).
Model checking harness with symmetry tla/mvcc/MCMVCC.tla	Adds MCMVCC module extending MVCC and TLC, defines KeySymmetry, ValSymmetry, and Symmetry using permutations.
Model checking configurations (safe and gap) tla/mvcc/MCMVCC.cfg, tla/mvcc/MCMVCC_gap.cfg	MCMVCC.cfg runs the MVCC model with EnableSafety=TRUE and bounded params, enabling invariants and temporal checks. MCMVCC_gap.cfg runs EnableSafety=FALSE to expose the expected MVCC4_NoLostCommitOnSnapshotInstall counterexample.
Documentation and test integration tla/README.md, scripts/tla-check.sh	Marks M3 (MVCC) as Landed, documents the MVCC model and invariants (notably MVCC4_NoLostCommitOnSnapshotInstall), and updates scripts/tla-check.sh to include mvcc and recognize the gap-case violation string.

Sequence Diagram

sequenceDiagram
  participant Harness as Test Harness
  participant SafeConfig as MCMVCC.cfg (EnableSafety=TRUE)
  participant GapConfig as MCMVCC_gap.cfg (EnableSafety=FALSE)
  participant MVCC as MVCC Spec

  Harness->>SafeConfig: Run TLC
  SafeConfig->>MVCC: Execute Write/Compact transitions
  MVCC->>SafeConfig: Verify invariants (MVCC4 holds)
  SafeConfig-->>Harness: Success

  Harness->>GapConfig: Run TLC (gap)
  GapConfig->>MVCC: Execute transitions with EnableSafety=FALSE
  MVCC->>GapConfig: MVCC4 counterexample produced
  GapConfig-->>Harness: Failure (MVCC4 violated)
  Harness->>Harness: Grep for MVCC4 violation string to confirm expected failure

Loading

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~45 minutes

Possibly related PRs

• bootjp/elastickv#858: Introduces the module-aware TLA checking framework in scripts/tla-check.sh that this PR extends with the mvcc module.

Poem

🐰 Version chains now formally blessed,
Compaction trims where old commits rest,
Safety flags guard the snapshot line,
TLC finds the gap where commits decline,
A rabbit cheers — MVCC verified in jest!

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly and specifically summarizes the main changes: adding MVCC TLA+ specification (M3) with MVCC-1 and MVCC-4 invariants, and integrating it into the tla-check tooling.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch feat/tla-m3-mvcc-spec

---

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[gemini-code-assist]

Code Review

This pull request implements Milestone 3 (M3) by introducing the TLA+ specification for the MVCC layer (tla/mvcc/MVCC.tla) along with its model-checking instances (MCMVCC.tla, MCMVCC.cfg, and MCMVCC_gap.cfg). It also updates the TLA check script (scripts/tla-check.sh) to include the new mvcc module and its expected gap invariant violation, and documents these additions in tla/README.md. There are no review comments to address, and I have no additional feedback to provide on these changes.

[coderabbitai]

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

tla/README.md (1)

49-51: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Update the “currently HLC and OCC” wording to include MVCC.

This text is now stale since make tla-check includes mvcc; please align the Run section with current harness behavior.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@tla/README.md` around lines 49 - 51, Update the Run section wording to
reflect that make tla-check (scripts/tla-check.sh) now includes MVCC: replace
the phrase "currently HLC and OCC" with "currently HLC, OCC, and MVCC" (or
equivalent) so the README's description of which modules are checked matches the
actual harness behavior.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Outside diff comments:
In `@tla/README.md`:
- Around line 49-51: Update the Run section wording to reflect that make
tla-check (scripts/tla-check.sh) now includes MVCC: replace the phrase
"currently HLC and OCC" with "currently HLC, OCC, and MVCC" (or equivalent) so
the README's description of which modules are checked matches the actual harness
behavior.

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: bafc5492-134a-4fc4-946b-e60bf830072c

📥 Commits

Reviewing files that changed from the base of the PR and between ebce174 and 4d0af12.

📒 Files selected for processing (6)

• scripts/tla-check.sh
• tla/README.md
• tla/mvcc/MCMVCC.cfg
• tla/mvcc/MCMVCC.tla
• tla/mvcc/MCMVCC_gap.cfg
• tla/mvcc/MVCC.tla

[bootjp]

Coderabbit Minor fixed in 9142eaa1 — Run section parenthetical now lists "HLC, OCC, and MVCC". Gemini had no findings. All CI green.

@claude review

[claude]

Claude finished @bootjp's task in 3m 3s —— View job

---

Code Review — M3 MVCC TLA+ Spec

• Gather context
• Read changed files
• Review MVCC.tla spec
• Review model-check configs and MCMVCC.tla
• Review tla-check.sh and README updates
• Post findings

---

Summary

Solid spec. The ghost-variable approach for MVCC-4, the EnableSafety toggle, and the RetainOnCompact retention logic are all correct. One stale-text issue to fix; a few minor observations below.

---

Finding: stale forward-reference in README (minor)

tla/README.md line 84:

The OCC module follows the same pattern under `tla/occ/` with
`MCOCC.cfg` / `MCOCC_gap.cfg`; future M3 / M4 / M5 modules will too.

M3 has now landed, so this should read "future M4 / M5 modules will too." Fix this →

---

Observations (not bugs)

LatestBefore — v.commitTs > 0 guard

tla/mvcc/MVCC.tla:65

LET below == { v \in S : v.commitTs <= ts /\ v.commitTs > 0 } IN

The > 0 guard is technically unreachable via Write (the first write lands at tsCounter + 1 = 1), but it serves as a defensive fence against the NotFound sentinel being accidentally present in S. Good to have; no action needed.

RetainOnCompact — correctness of single-entry retention

tla/mvcc/MVCC.tla:113–118

The retention of only the single latest-before-newMin entry is correct: for any read_ts >= newMin, LatestBefore maximises over commitTs, so any earlier versions below newMin are shadowed by the retained one. The spec correctly encodes the production store's LSM compaction semantics.

One edge worth confirming mentally: when newMin = 1, RetainOnCompact(k, 1) calls LatestBefore(versions[k], 0), which always returns NotFound (the > 0 guard makes the candidate set empty). So aboveOrAt = { v : v.commitTs >= 1 } = all versions, and nothing is dropped. Correct.

MVCC-1 is only asserted on versions, not originalVersions

tla/mvcc/MVCC.tla:158–161

MVCC-1 checks uniqueness in the live store only. Since originalVersions grows monotonically via the same Write path that enforces uniqueness via the monotonic tsCounter, uniqueness also holds for the ghost — but it is not separately asserted. The invariant's purpose is to validate the live store, and the ghost is only needed for MVCC-4, so this scope decision is intentional and reasonable.

MVCC_TsMonotonic says "weakly increases"

tla/mvcc/MVCC.tla:183

MVCC_TsMonotonic == [][tsCounter' >= tsCounter]_vars

Write strictly increases tsCounter; the >= form is still correct because it must tolerate stuttering steps (TLA+ action properties are stuttering-tolerant). "Weakly increases" in the comment is accurate. No issue.

Symmetry union

tla/mvcc/MCMVCC.tla:20–22

Symmetry == KeySymmetry \cup ValSymmetry

Standard independent-sort symmetry reduction. Keys and values participate only as abstract indices (no ordering on either in any invariant), so both sorts are genuinely symmetric. Follows the same pattern as MCOCC. Correct.

---

Design choices that are sound

• Ghost variable for MVCC-4 — carrying originalVersions as a never-compacted parallel set is the canonical TLA+ approach for "no lost commit" properties. Clean, direct, machine-checkable.
• EnableSafety toggle in a single spec — one module, two configs. Avoids duplication and makes the gap evidence a first-class assertion rather than a narrative claim.
• Deferral of MVCC-2 / MVCC-3 — well-reasoned: MVCC-2 is structurally a consequence of the HLC ceiling discipline and belongs in HLC.tla; MVCC-3 requires a multi-node model that the single-node M3 spec cannot express. Both fit M5 naturally.
• State-space bound — 79 distinct states at MaxTs = 4 / MaxOps = 3 / 2 keys / 2 vals is appropriately tight; the gap counterexample at depth 3 confirms the bounds are sufficient to exercise the violation.

---

Verdict: LGTM with the one stale README nit. The spec is correct, the invariants are faithfully stated, and the gap evidence is genuine.

[bootjp]

Round 2 fix in 644a432b. claude bot Round 1 review found one minor stale README forward-reference ("future M3 / M4 / M5" on line 84 after M3 landed). Updated to note that MVCC follows the same pattern under tla/mvcc/ and M4 / M5 will use the same shape.

All other claude observations were marked LGTM (ghost variable, EnableSafety toggle, RetainOnCompact correctness, MVCC-2/MVCC-3 deferral rationale, symmetry).

@claude review

[claude]

Claude finished @bootjp's task in 1m 42s —— View job

---

Code Review — M3 MVCC TLA+ Spec (Round 2)

• Gather context
• Verify Round 2 fix (644a432) — stale README forward-reference
• Full review pass on spec files
• Post findings

---

Round 2 fixes verified

644a432 — stale M3 forward-reference in README (Round 1 finding)

tla/README.md lines 83–85 now read:

The OCC module follows the same pattern under `tla/occ/` with
`MCOCC.cfg` / `MCOCC_gap.cfg`; MVCC follows under `tla/mvcc/` (see
below).  Future M4 / M5 modules will use the same pattern.

Old "future M3 / M4 / M5" is gone; MVCC is correctly noted as already landed, and only M4 / M5 remain as "future". ✓

9142eaa — Run section module list (Coderabbit finding)

tla/README.md lines 49–51 now read:

…currently HLC, OCC, and MVCC; M4 / M5 will be added as they land…

Matches the actual harness. ✓

---

Fresh spec review

No new findings. For completeness, re-confirmed:

RetainOnCompact edge case newMin = 1 — LatestBefore(versions[k], 0) returns NotFound (the commitTs > 0 guard empties the candidate set), so aboveOrAt is the full version set and nothing is pruned. Correct.

MVCC4 range minRetained..MaxTs — Compact requires newMin <= tsCounter and tsCounter <= MaxTs (via StateConstraint), so minRetained is always <= MaxTs. The quantifier range is never vacuously empty in the unsafe direction. ✓

MVCC_GhostMonotonic stuttering — [][\A k : v[k] ⊆ v'[k]]_vars correctly tolerates stuttering steps where originalVersions' = originalVersions. ✓

opCount not consumed by Compact — intentional and sound: the budget bounds Write actions that generate version history; compaction steps are independently bounded by newMin ∈ 1..MaxTs and the monotonicity guard. ✓

---

Verdict: LGTM. Both Round 1 findings are properly addressed, the Coderabbit note was fixed, and the spec itself remains correct. Ready to merge.