Fix committed RW real-time response indexing

[Amaury Chamayou (achamayou)]

CommittedRwOrderedRealTimeInv compares three history events:

• i is a committed read-write response that occurred first.
• j is a later committed read-write request.
• k is the committed read-write response matching j.

k was incorrectly selected from RoTxResponseCommittedEventIndexes. Because request transaction values are unique, a read-only response cannot match the committed read-write request j, so history[k].tx = history[j].tx could not hold and the implication was vacuously true. In the no-read model, the read-only response set is empty. Ranging k over RwTxResponseCommittedEventIndexes selects the intended matching response and makes the real-time ordering check effective.

TLC checks passed with no errors:

• python3 ./tlc.py mc consistency/MCMultiNode.tla
• python3 ./tlc.py mc consistency/MCMultiNodeReads.tla

This defect was noticed while examining #8134. This PR is intentionally independent and contains none of #8134 invariant-relaxation work, including no change to CommittedRwOrderedSerializableInv.

[Copilot]

Pull request overview

This PR fixes a TLA+ specification defect in CommittedRwOrderedRealTimeInv where the “matching response” event index k was incorrectly ranged over committed read-only responses, making the invariant vacuously true (notably in the no-read model where that set is empty). By ranging k over committed read-write responses instead, the real-time ordering check becomes effective and aligns with the invariant’s intent.

Changes:

• Update CommittedRwOrderedRealTimeInv to select k from RwTxResponseCommittedEventIndexes rather than RoTxResponseCommittedEventIndexes.
• Restores meaningful real-time ordering checking for committed RW transactions in models with no RO responses.

Custom instructions used:

• .github/copilot-instructions.md
• .github/instructions/reviewing.instructions.md

---

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

[Heidi Howard (heidihoward)]

Yes, this was a typo. It was missed by TLC as L234 meant this invariants conditions were never satisfied so it was triviality true