From 76bdc88b04bee245a13d9adf8563f0e0c7b77e93 Mon Sep 17 00:00:00 2001
From: Eddy Ashton <edashton@microsoft.com>
Date: Tue, 24 Oct 2023 08:55:54 +0000
Subject: [PATCH] Add new invariant, stating that CommittableIndices are all
 (known) signatures

---
 tla/consensus/SIMccfraft.cfg | 2 ++
 tla/consensus/ccfraft.tla    | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index e91d7f01dbbf..a61bc3a863bd 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -76,6 +76,8 @@ INVARIANTS
 
     CommitCommittableIndices
 
+    CommittableIndicesAreKnownSignaturesInv
+
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index 653aa5fb0bfa..15a1680c48c6 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -1295,6 +1295,12 @@ CommitCommittableIndices ==
     \A i \in Servers :
         committableIndices[i] # {} => commitIndex[i] < Min(committableIndices[i])
 
+CommittableIndicesAreKnownSignaturesInv ==
+    \A i \in Servers :
+        \A j \in committableIndices[i] :
+            /\ j \in DOMAIN(log[i])
+            /\ HasTypeSignature(log[i][j])
+
 ------------------------------------------------------------------------------
 \* Properties