Repair TLA+ ordered serialisability invariant

[Amaury Chamayou (achamayou)]

Summary

• Repair CommittedRwOrderedSerializableInv: the old equality treated adjacency after filtering for explicitly observed committed statuses as ledger adjacency, but the minimal seven-event trace contains an intervening write with no response or status event.
• Require each later committed read-write response in TxID order to strictly extend the earlier observation as a proper prefix and to end with its own write.
• Add the single-node HistoryLimit = 7 positive CI regression. It reaches the minimal trace and would fail with the old equality.
• Keep CommittedRwOrderedSpecLinearizableInv enabled in the normal MCMultiNode and MCMultiNodeReads configurations.

Validation

• cd tla && ./tlc.py --workers 1 --config consistency/MCSingleNodeOrderedSerializable.cfg mc consistency/MCSingleNode.tla: no errors; 88,557 generated states, 63,449 distinct states, depth 15.
• Focused Prettier, whitespace, and ASCII checks passed for the changed YAML and TLA files.
• The previously completed multi-node HistoryLimit = 7 run also passed with 21,586,197 distinct states.

[Heidi Howard (heidihoward)]

Yes, this invariant is too strong. It should be relaxed instead of removed

[Amaury Chamayou (achamayou)]

Heidi Howard (@heidihoward) updated the PR to be a fix instead

[Copilot]

Pull request overview

This PR fixes the TLA+ invariant CommittedRwOrderedSerializableInv so it correctly handles traces where committed RW responses (filtered by explicitly observed committed statuses) are not adjacent in the underlying ledger history due to intervening writes without corresponding response/status events. It also adds a dedicated single-node TLC CI regression run that reaches the minimal seven-event trace and would have failed under the previous invariant definition.

Changes:

• Update CommittedRwOrderedSerializableInv to require that each later committed RW response’s observed sequence strictly extends the earlier one as a proper prefix and ends with its own write.
• Add a new TLC config (HistoryLimit = 7) to model-check only the repaired invariant on the single-node spec.
• Extend CI verification to run TLC with --workers 1 and the new config to cover the previously failing minimal trace.

Custom instructions used:

• None (no additional repository instruction files were loaded from .github/copilot-instructions.md or .github/instructions/ during this review).

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
tla/consistency/MCSingleNodeOrderedSerializable.cfg	New TLC config to specifically check CommittedRwOrderedSerializableInv under HistoryLimit = 7.
tla/consistency/ExternalHistoryInvars.tla	Repairs CommittedRwOrderedSerializableInv to use strict prefix-extension semantics and ensure each later observation ends with its own write.
.github/workflows/ci-verification.yml	Adds a CI TLC run using the new config (single worker) to regress the minimal seven-event trace.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.