Add new invariant, stating that CommittableIndices are all (known) si…

…gnatures
microsoft · Oct 24, 2023 · 76bdc88 · 76bdc88
1 parent 499f170
commit 76bdc88
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git 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
@@ -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