From c89aa8f43cceb2bb1973961648c70c44e88f9297 Mon Sep 17 00:00:00 2001
From: Rain <rain@oxide.computer>
Date: Mon, 26 Oct 2026 16:19:47 -0700
Subject: [PATCH] [trust-quorum] tla: let the coordinator receive its own
 commit

---
 trust-quorum/tla/check.sh         | 2 +-
 trust-quorum/tla/trust_quorum.tla | 7 ++-----
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/trust-quorum/tla/check.sh b/trust-quorum/tla/check.sh
index 1f74d0ba5e7..36fd3c62bbf 100755
--- a/trust-quorum/tla/check.sh
+++ b/trust-quorum/tla/check.sh
@@ -71,7 +71,7 @@ WORKERS="${TLC_WORKERS:-auto}"
 # cfg  module  expected-exit-status
 EXPECTED=(
     "trust_quorum.cfg          trust_quorum  0"
-    "trust_quorum_nocrash.cfg  trust_quorum  13"
+    "trust_quorum_nocrash.cfg  trust_quorum  0"
 )
 
 selected=("$@")
diff --git a/trust-quorum/tla/trust_quorum.tla b/trust-quorum/tla/trust_quorum.tla
index 739aabcc355..2aa15830e9a 100644
--- a/trust-quorum/tla/trust_quorum.tla
+++ b/trust-quorum/tla/trust_quorum.tla
@@ -413,11 +413,6 @@ CommittedNodesHaveShares ==
 (* Temporal properties *)
 AllNodesUnlock == <>[](\A id \in nexus.config.members: nodeOp[id] # "Unlock")
 
-\* This is currently expected to FAIL under trust_quorum_nocrash.cfg, because
-\* RecvCommit never fires for the coordinator (it stays in CoordinatePrepare),
-\* so NexusRecvCommitAck never reaches Idle and epoch 2 never starts.
-\* trust_quorum.cfg only gets there because n1 is in CRASHSET and commits after
-\* restarting.
 ReconfigurationStarts == <>(nexus.config.epoch = 2)
 
 -----------------------------------------------------------------------------
@@ -898,6 +893,8 @@ RecvCommit(id) ==
     /\ m # NONE
     /\ \/ nodeOp[id] = "Idle"
        \/ nodeOp[id] = "Uncommitted"
+       \* The coordinator commits its own config like any other member.
+       \/ nodeOp[id] = "CoordinatePrepare"
     /\ Assert(nodes[id].has_share,
               <<"Commits should only be sent to nodes that have prepared", id>>)
     /\ nodeOp' = [nodeOp EXCEPT ![id] = "Idle"]