From 7bce884f0d6f053a9fe8cdc6f16b7e9dd43b3195 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 8 Jan 2024 14:45:54 +0000
Subject: [PATCH] removing MatchIndexLowerBoundNextIndexInv

---
 tla/consensus/MCccfraft.cfg             | 1 -
 tla/consensus/MCccfraftWithReconfig.cfg | 1 -
 tla/consensus/SIMccfraft.cfg            | 2 --
 tla/consensus/ccfraft.tla               | 3 +++
 4 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
index c6912cdd79c9..ba40fc88c7be 100644
--- a/tla/consensus/MCccfraft.cfg
+++ b/tla/consensus/MCccfraft.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
index 572632045965..54e38a3af00d 100644
--- a/tla/consensus/MCccfraftWithReconfig.cfg
+++ b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index c778561b2650..4a85864280f4 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -77,8 +77,6 @@ INVARIANTS
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
 
-    MatchIndexLowerBoundNextIndexInv
-
     CommitCommittableIndices
 
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index 54538e91813b..a69382e809f2 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -1247,6 +1247,9 @@ NoLeaderBeforeInitialTerm ==
     \A i \in Servers :
         currentTerm[i] < StartTerm => state[i] # Leader
 
+\* MatchIndexLowerBoundNextIndexInv is not currently an invariant but 
+\* we might wish to add it in the future. This could be achieved by updating 
+\* nextIndex to max of current nextIndex and matchIndex when an AE ACK is received.
 MatchIndexLowerBoundNextIndexInv ==
     \A i,j \in Servers :
         state[i] = Leader =>