From d8c21ad9089f2d0f20ae170e7e88e757e0c528d4 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Tue, 13 Aug 2024 15:59:50 +0000
Subject: [PATCH 01/19] adding abs consensus spec

---
 tla/consensus/MCccfraft.cfg |  1 +
 tla/consensus/MCccfraft.tla | 12 ++++++++++
 tla/consensus/abs.cfg       |  6 +++++
 tla/consensus/abs.tla       | 47 +++++++++++++++++++++++++++++++++++++
 4 files changed, 66 insertions(+)
 create mode 100644 tla/consensus/abs.cfg
 create mode 100644 tla/consensus/abs.tla

diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
index 668a34c98727..4d62a74afacc 100644
--- a/tla/consensus/MCccfraft.cfg
+++ b/tla/consensus/MCccfraft.cfg
@@ -68,6 +68,7 @@ PROPERTIES
     MembershipStateTransitionsProp
     PendingBecomesFollowerProp
     NeverCommitEntryPrevTermsProp
+    RefinementToAbsProp
 
 INVARIANTS
     LogInv
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
index 3b19795881eb..7257a4a03831 100644
--- a/tla/consensus/MCccfraft.tla
+++ b/tla/consensus/MCccfraft.tla
@@ -126,4 +126,16 @@ DebugNotTooManySigsInv ==
     \A i \in Servers:
         FoldSeq(LAMBDA e, count: IF e.contentType = TypeSignature THEN count + 1 ELSE count, 0, log[i]) < 8
 
+----
+
+MappingToAbs == 
+  INSTANCE abs WITH
+    Servers <- Servers,
+    Terms <- 1..MaxTermLimit,
+    RequestLimit <- RequestLimit,
+    StartTerm <- StartTerm,
+    CLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
+
+RefinementToAbsProp == MappingToAbs!AbsSpec
+
 ===================================
diff --git a/tla/consensus/abs.cfg b/tla/consensus/abs.cfg
new file mode 100644
index 000000000000..a5651e4799a6
--- /dev/null
+++ b/tla/consensus/abs.cfg
@@ -0,0 +1,6 @@
+SPECIFICATION AbsSpec
+
+CONSTANTS
+    NodeOne = n1
+    NodeTwo = n2
+    NodeThree = n3
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
new file mode 100644
index 000000000000..485904c09069
--- /dev/null
+++ b/tla/consensus/abs.tla
@@ -0,0 +1,47 @@
+---- MODULE abs ----
+\* Abstract specification for a distributed consensus algorithm.
+
+EXTENDS Sequences, SequencesExt, Naturals, FiniteSets
+
+CONSTANT Servers, Terms, RequestLimit, StartTerm
+
+\* Commit logs from each node
+VARIABLE CLogs
+
+\* Max log length
+MaxLogLength == (RequestLimit*2) + Cardinality(Terms)
+
+\* All possible logs
+Logs == [1..MaxLogLength -> Terms]
+
+Init ==
+    CLogs \in [Servers -> {
+        << >>,
+        << StartTerm, StartTerm >>,
+        << StartTerm, StartTerm, StartTerm, StartTerm >>}]
+
+\* A node can copy a ledger suffix from another node.
+Copy(i) ==
+    \E j \in Servers : 
+        /\ Len(CLogs[j]) > Len(CLogs[i])
+        /\ \E l \in 1..(Len(CLogs[j]) - Len(CLogs[i])) : 
+            \E s \in [1..l -> Terms] :
+                CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o s]
+
+\* The node with the longest log can extend its log.
+Extend(i) ==
+    /\ \A j \in Servers : Len(CLogs[j]) \leq Len(CLogs[i])
+    /\ \E l \in 0..(MaxLogLength - Len(CLogs[i])) : 
+        \E s \in [1..l -> Terms] :
+            CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o s]
+
+\* The only possible actions are to append log entries.
+\* There cannot be any conflicting log entries, since log entries are copied if the node is not the longest.
+Next ==
+    \E i \in Servers : 
+        \/ Copy(i) 
+        \/ Extend(i)
+
+AbsSpec == Init /\ [][Next]_CLogs
+
+====
\ No newline at end of file

From 8926f9e9dbad631ec341f0cef1d3dd63d6f4c711 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Tue, 13 Aug 2024 16:11:46 +0000
Subject: [PATCH 02/19] patch to copy

---
 tla/consensus/abs.tla | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index 485904c09069..e35054cbcf27 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -6,6 +6,7 @@ EXTENDS Sequences, SequencesExt, Naturals, FiniteSets
 CONSTANT Servers, Terms, RequestLimit, StartTerm
 
 \* Commit logs from each node
+\* Each log is append-only
 VARIABLE CLogs
 
 \* Max log length
@@ -25,8 +26,7 @@ Copy(i) ==
     \E j \in Servers : 
         /\ Len(CLogs[j]) > Len(CLogs[i])
         /\ \E l \in 1..(Len(CLogs[j]) - Len(CLogs[i])) : 
-            \E s \in [1..l -> Terms] :
-                CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o s]
+                CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o SubSeq(CLogs[j], Len(CLogs[i]) + 1, Len(CLogs[i]) + l)]
 
 \* The node with the longest log can extend its log.
 Extend(i) ==
@@ -36,7 +36,8 @@ Extend(i) ==
             CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o s]
 
 \* The only possible actions are to append log entries.
-\* There cannot be any conflicting log entries, since log entries are copied if the node is not the longest.
+\* But construction there cannot be any conflicting log entries
+\* Log entries are copied if the node is not the longest.
 Next ==
     \E i \in Servers : 
         \/ Copy(i) 

From 3a01fa1519dca9d3e5c2877f88213378e92c6afe Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Tue, 13 Aug 2024 16:13:59 +0000
Subject: [PATCH 03/19] typo fix

---
 tla/consensus/abs.tla | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index e35054cbcf27..836cf51530e7 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -36,7 +36,7 @@ Extend(i) ==
             CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o s]
 
 \* The only possible actions are to append log entries.
-\* But construction there cannot be any conflicting log entries
+\* By construction there cannot be any conflicting log entries
 \* Log entries are copied if the node is not the longest.
 Next ==
     \E i \in Servers : 

From ed05e0ed3d35ca2479fb52d1dfb074e21cf52d8a Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Tue, 13 Aug 2024 16:35:36 +0000
Subject: [PATCH 04/19] with some model checking

---
 tla/consensus/MCabs.cfg | 17 +++++++++++++++++
 tla/consensus/MCabs.tla | 12 ++++++++++++
 tla/consensus/abs.cfg   |  6 ------
 tla/consensus/abs.tla   | 15 ++++++++++++---
 4 files changed, 41 insertions(+), 9 deletions(-)
 create mode 100644 tla/consensus/MCabs.cfg
 create mode 100644 tla/consensus/MCabs.tla
 delete mode 100644 tla/consensus/abs.cfg

diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
new file mode 100644
index 000000000000..f3d83460b149
--- /dev/null
+++ b/tla/consensus/MCabs.cfg
@@ -0,0 +1,17 @@
+SPECIFICATION AbsSpec
+
+CONSTANTS
+    NodeOne = n1
+    NodeTwo = n2
+    NodeThree = n3
+    Servers <- MCServers
+    Terms <- MCTerms
+    RequestLimit <- MCRequestLimit
+    StartTerm <- MCStartTerm
+
+INVARIANTS
+    NoConflicts 
+
+PROPERTIES 
+    AppendOnlyProp
+    
\ No newline at end of file
diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
new file mode 100644
index 000000000000..dbbb76fe65d5
--- /dev/null
+++ b/tla/consensus/MCabs.tla
@@ -0,0 +1,12 @@
+---- MODULE MCabs ----
+
+EXTENDS abs
+
+CONSTANTS NodeOne, NodeTwo, NodeThree
+
+MCServers == {NodeOne, NodeTwo, NodeThree}
+MCTerms == 2..5
+MCRequestLimit == 3
+MCStartTerm == 2
+
+====
\ No newline at end of file
diff --git a/tla/consensus/abs.cfg b/tla/consensus/abs.cfg
deleted file mode 100644
index a5651e4799a6..000000000000
--- a/tla/consensus/abs.cfg
+++ /dev/null
@@ -1,6 +0,0 @@
-SPECIFICATION AbsSpec
-
-CONSTANTS
-    NodeOne = n1
-    NodeTwo = n2
-    NodeThree = n3
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index 836cf51530e7..d3071cbef5a4 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -1,7 +1,7 @@
 ---- MODULE abs ----
 \* Abstract specification for a distributed consensus algorithm.
 
-EXTENDS Sequences, SequencesExt, Naturals, FiniteSets
+EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, SequencesExt
 
 CONSTANT Servers, Terms, RequestLimit, StartTerm
 
@@ -12,8 +12,8 @@ VARIABLE CLogs
 \* Max log length
 MaxLogLength == (RequestLimit*2) + Cardinality(Terms)
 
-\* All possible logs
-Logs == [1..MaxLogLength -> Terms]
+\* All possible completed logs
+Logs == [1..MaxLogLength -> Terms] 
 
 Init ==
     CLogs \in [Servers -> {
@@ -45,4 +45,13 @@ Next ==
 
 AbsSpec == Init /\ [][Next]_CLogs
 
+
+AppendOnlyProp ==
+    [][\A i \in Servers : IsPrefix(CLogs[i], CLogs'[i])]_CLogs
+
+NoConflicts ==
+    \A i, j \in Servers : 
+        \/ IsPrefix(CLogs[i], CLogs[j]) 
+        \/ IsPrefix(CLogs[j], CLogs[i])
+
 ====
\ No newline at end of file

From 92b50bbce6b9fe29561c9aabd73b9aaf50ec5fd7 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Tue, 13 Aug 2024 16:57:23 +0000
Subject: [PATCH 05/19] forgot bootstrapping in max log length calculation

---
 tla/consensus/abs.tla | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index d3071cbef5a4..cf9cd1cc1bb0 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -10,7 +10,7 @@ CONSTANT Servers, Terms, RequestLimit, StartTerm
 VARIABLE CLogs
 
 \* Max log length
-MaxLogLength == (RequestLimit*2) + Cardinality(Terms)
+MaxLogLength == 4 + (RequestLimit*2) + Cardinality(Terms)
 
 \* All possible completed logs
 Logs == [1..MaxLogLength -> Terms] 

From 1135e8c723a746592dd350ccfec5f93eac267ffa Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Wed, 14 Aug 2024 07:51:36 +0000
Subject: [PATCH 06/19] adding abs to mc ci

---
 .github/workflows/tlaplus.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml
index 6644bc7204f9..bdd3374a4a46 100644
--- a/.github/workflows/tlaplus.yml
+++ b/.github/workflows/tlaplus.yml
@@ -129,6 +129,12 @@ jobs:
           sudo apt install -y default-jre
           python3 ./tla/install_deps.py
 
+      - name: MCabs.cfg
+        run: |
+          set -x
+          cd tla/
+          ./tlc.sh -workers auto consensus/MCabs.tla -dumpTrace tla MCabs.trace.tla -dumpTrace json MCabs.json
+
       - name: MCccfraft.cfg
         run: |
           set -x

From 84d8d7b185dda64f88cd38b44f0ca7d7e08d6758 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Wed, 14 Aug 2024 08:00:40 +0000
Subject: [PATCH 07/19] refactor to make initial logs clearer

---
 tla/consensus/abs.tla | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index cf9cd1cc1bb0..d1b7a6e79674 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -13,13 +13,15 @@ VARIABLE CLogs
 MaxLogLength == 4 + (RequestLimit*2) + Cardinality(Terms)
 
 \* All possible completed logs
-Logs == [1..MaxLogLength -> Terms] 
+Logs == [1..MaxLogLength -> Terms]
 
+InitialLogs == {
+    <<>>,
+    <<StartTerm, StartTerm>>,
+    <<StartTerm, StartTerm, StartTerm, StartTerm>>}
+    
 Init ==
-    CLogs \in [Servers -> {
-        << >>,
-        << StartTerm, StartTerm >>,
-        << StartTerm, StartTerm, StartTerm, StartTerm >>}]
+    CLogs \in [Servers -> InitialLogs]
 
 \* A node can copy a ledger suffix from another node.
 Copy(i) ==

From 50a07e5c2293cde573ef533e8f03e164d56076da Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Wed, 14 Aug 2024 09:40:04 +0000
Subject: [PATCH 08/19] ci fix

---
 tla/consensus/MCabs.cfg     |  5 +++--
 tla/consensus/MCabs.tla     |  4 ++--
 tla/consensus/MCccfraft.tla |  2 +-
 tla/consensus/abs.tla       | 10 ++++------
 4 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
index f3d83460b149..53d91813f073 100644
--- a/tla/consensus/MCabs.cfg
+++ b/tla/consensus/MCabs.cfg
@@ -6,11 +6,12 @@ CONSTANTS
     NodeThree = n3
     Servers <- MCServers
     Terms <- MCTerms
-    RequestLimit <- MCRequestLimit
+    MaxLogLength <- MCMaxLogLength
     StartTerm <- MCStartTerm
 
 INVARIANTS
-    NoConflicts 
+    NoConflicts
+    TypeOK
 
 PROPERTIES 
     AppendOnlyProp
diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
index dbbb76fe65d5..1deeee1fbddc 100644
--- a/tla/consensus/MCabs.tla
+++ b/tla/consensus/MCabs.tla
@@ -5,8 +5,8 @@ EXTENDS abs
 CONSTANTS NodeOne, NodeTwo, NodeThree
 
 MCServers == {NodeOne, NodeTwo, NodeThree}
-MCTerms == 2..5
-MCRequestLimit == 3
+MCTerms == 2..4
+MCMaxLogLength == 5
 MCStartTerm == 2
 
 ====
\ No newline at end of file
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
index 7257a4a03831..d9f046dc5dee 100644
--- a/tla/consensus/MCccfraft.tla
+++ b/tla/consensus/MCccfraft.tla
@@ -132,7 +132,7 @@ MappingToAbs ==
   INSTANCE abs WITH
     Servers <- Servers,
     Terms <- 1..MaxTermLimit,
-    RequestLimit <- RequestLimit,
+    MaxLogLength <- 4 + (RequestLimit*2) + MaxTermLimit,
     StartTerm <- StartTerm,
     CLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
 
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index d1b7a6e79674..d9f6da8acf40 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -3,17 +3,12 @@
 
 EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, SequencesExt
 
-CONSTANT Servers, Terms, RequestLimit, StartTerm
+CONSTANT Servers, Terms, MaxLogLength, StartTerm
 
 \* Commit logs from each node
 \* Each log is append-only
 VARIABLE CLogs
 
-\* Max log length
-MaxLogLength == 4 + (RequestLimit*2) + Cardinality(Terms)
-
-\* All possible completed logs
-Logs == [1..MaxLogLength -> Terms]
 
 InitialLogs == {
     <<>>,
@@ -47,6 +42,9 @@ Next ==
 
 AbsSpec == Init /\ [][Next]_CLogs
 
+TypeOK ==
+    /\ CLogs \in [Servers -> 
+        UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
 
 AppendOnlyProp ==
     [][\A i \in Servers : IsPrefix(CLogs[i], CLogs'[i])]_CLogs

From 35d7d946241d53eb8e4eac1ca116134670d818a7 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Thu, 15 Aug 2024 09:03:40 +0000
Subject: [PATCH 09/19] some documentation

---
 tla/consensus/abs.tla | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index d9f6da8acf40..9a455a46e6a8 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -1,12 +1,13 @@
 ---- MODULE abs ----
 \* Abstract specification for a distributed consensus algorithm.
+\* Assumes that any node can inspect the state of all other nodes. 
 
-EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, SequencesExt
+EXTENDS Sequences, SequencesExt, Naturals, FiniteSets
 
 CONSTANT Servers, Terms, MaxLogLength, StartTerm
 
 \* Commit logs from each node
-\* Each log is append-only
+\* Each log is append-only and the logs will never diverge.
 VARIABLE CLogs
 
 
@@ -18,7 +19,7 @@ InitialLogs == {
 Init ==
     CLogs \in [Servers -> InitialLogs]
 
-\* A node can copy a ledger suffix from another node.
+\* A node i can copy a ledger suffix from another node j.
 Copy(i) ==
     \E j \in Servers : 
         /\ Len(CLogs[j]) > Len(CLogs[i])

From 1d131f6eeb43042f48cada238fe7474957f843ac Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 2 Sep 2024 14:00:46 +0000
Subject: [PATCH 10/19] atomically inspect

---
 tla/consensus/abs.tla | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index 9a455a46e6a8..5a077925bb0b 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -1,6 +1,6 @@
 ---- MODULE abs ----
 \* Abstract specification for a distributed consensus algorithm.
-\* Assumes that any node can inspect the state of all other nodes. 
+\* Assumes that any node can atomically inspect the state of all other nodes. 
 
 EXTENDS Sequences, SequencesExt, Naturals, FiniteSets
 

From 6dbe828f7d63f4c274c7e240221c71bcb7280672 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 2 Sep 2024 14:04:24 +0000
Subject: [PATCH 11/19] moving typeOk

---
 tla/consensus/abs.tla | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index 5a077925bb0b..732739144dd3 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -10,6 +10,9 @@ CONSTANT Servers, Terms, MaxLogLength, StartTerm
 \* Each log is append-only and the logs will never diverge.
 VARIABLE CLogs
 
+TypeOK ==
+    /\ CLogs \in [Servers -> 
+        UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
 
 InitialLogs == {
     <<>>,
@@ -43,10 +46,6 @@ Next ==
 
 AbsSpec == Init /\ [][Next]_CLogs
 
-TypeOK ==
-    /\ CLogs \in [Servers -> 
-        UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
-
 AppendOnlyProp ==
     [][\A i \in Servers : IsPrefix(CLogs[i], CLogs'[i])]_CLogs
 

From a696ad56bd58ed0ff910323b8cd9700c7ddfb819 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 2 Sep 2024 14:05:32 +0000
Subject: [PATCH 12/19] if the node's log is not the longest

---
 tla/consensus/abs.tla | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index 732739144dd3..1fed7fbfd627 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -38,7 +38,7 @@ Extend(i) ==
 
 \* The only possible actions are to append log entries.
 \* By construction there cannot be any conflicting log entries
-\* Log entries are copied if the node is not the longest.
+\* Log entries are copied if the node's log is not the longest.
 Next ==
     \E i \in Servers : 
         \/ Copy(i) 

From e9c2fe0af9440f926dee393d34049b5439caf156 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 2 Sep 2024 14:17:26 +0000
Subject: [PATCH 13/19] CLog @'s

---
 tla/consensus/abs.tla | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index 1fed7fbfd627..f4715bcc0ef5 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -27,14 +27,14 @@ Copy(i) ==
     \E j \in Servers : 
         /\ Len(CLogs[j]) > Len(CLogs[i])
         /\ \E l \in 1..(Len(CLogs[j]) - Len(CLogs[i])) : 
-                CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o SubSeq(CLogs[j], Len(CLogs[i]) + 1, Len(CLogs[i]) + l)]
+                CLogs' = [CLogs EXCEPT ![i] = @ \o SubSeq(CLogs[j], Len(@) + 1, Len(@) + l)]
 
 \* The node with the longest log can extend its log.
 Extend(i) ==
     /\ \A j \in Servers : Len(CLogs[j]) \leq Len(CLogs[i])
     /\ \E l \in 0..(MaxLogLength - Len(CLogs[i])) : 
         \E s \in [1..l -> Terms] :
-            CLogs' = [CLogs EXCEPT ![i] = CLogs[i] \o s]
+            CLogs' = [CLogs EXCEPT ![i] = @ \o s]
 
 \* The only possible actions are to append log entries.
 \* By construction there cannot be any conflicting log entries

From cf707d278e8e523152ebcaf52b6c39f188d95f7c Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 2 Sep 2024 14:42:35 +0000
Subject: [PATCH 14/19] comment on +4

---
 tla/consensus/MCccfraft.tla | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
index d9f046dc5dee..152cba01eab8 100644
--- a/tla/consensus/MCccfraft.tla
+++ b/tla/consensus/MCccfraft.tla
@@ -127,12 +127,17 @@ DebugNotTooManySigsInv ==
         FoldSeq(LAMBDA e, count: IF e.contentType = TypeSignature THEN count + 1 ELSE count, 0, log[i]) < 8
 
 ----
+\* Refinement
+
+\* The inital log is up to 4 entries long + one log entry per request/reconfiguration + one signature per request/reconfiguration or new view (no consecutive sigs except across views)
+MaxLogLength == 
+    4 + ((RequestLimit + Len(Configurations)) * 2) + MaxTermLimit
 
 MappingToAbs == 
   INSTANCE abs WITH
     Servers <- Servers,
     Terms <- 1..MaxTermLimit,
-    MaxLogLength <- 4 + (RequestLimit*2) + MaxTermLimit,
+    MaxLogLength <- MaxLogLength,
     StartTerm <- StartTerm,
     CLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
 

From 4f7f5a926793fdf54adf6fe26215fcbd1888c481 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 2 Sep 2024 15:00:02 +0000
Subject: [PATCH 15/19] upping MC state space

---
 tla/consensus/MCabs.tla | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
index 1deeee1fbddc..7b4d530af23a 100644
--- a/tla/consensus/MCabs.tla
+++ b/tla/consensus/MCabs.tla
@@ -6,7 +6,7 @@ CONSTANTS NodeOne, NodeTwo, NodeThree
 
 MCServers == {NodeOne, NodeTwo, NodeThree}
 MCTerms == 2..4
-MCMaxLogLength == 5
+MCMaxLogLength == 7
 MCStartTerm == 2
 
 ====
\ No newline at end of file

From 6af582086e03354ac40754b2a0a292ecb0090fe0 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 2 Sep 2024 15:16:07 +0000
Subject: [PATCH 16/19] removing StartTerm

---
 tla/consensus/MCabs.cfg     | 1 -
 tla/consensus/MCabs.tla     | 1 -
 tla/consensus/MCccfraft.tla | 3 +--
 tla/consensus/abs.tla       | 6 ++++--
 4 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
index 53d91813f073..3a104fd2d151 100644
--- a/tla/consensus/MCabs.cfg
+++ b/tla/consensus/MCabs.cfg
@@ -7,7 +7,6 @@ CONSTANTS
     Servers <- MCServers
     Terms <- MCTerms
     MaxLogLength <- MCMaxLogLength
-    StartTerm <- MCStartTerm
 
 INVARIANTS
     NoConflicts
diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
index 7b4d530af23a..02abc41ebd58 100644
--- a/tla/consensus/MCabs.tla
+++ b/tla/consensus/MCabs.tla
@@ -7,6 +7,5 @@ CONSTANTS NodeOne, NodeTwo, NodeThree
 MCServers == {NodeOne, NodeTwo, NodeThree}
 MCTerms == 2..4
 MCMaxLogLength == 7
-MCStartTerm == 2
 
 ====
\ No newline at end of file
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
index 152cba01eab8..37a9b20d8b58 100644
--- a/tla/consensus/MCccfraft.tla
+++ b/tla/consensus/MCccfraft.tla
@@ -136,9 +136,8 @@ MaxLogLength ==
 MappingToAbs == 
   INSTANCE abs WITH
     Servers <- Servers,
-    Terms <- 1..MaxTermLimit,
+    Terms <- StartTerm..MaxTermLimit,
     MaxLogLength <- MaxLogLength,
-    StartTerm <- StartTerm,
     CLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
 
 RefinementToAbsProp == MappingToAbs!AbsSpec
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index f4715bcc0ef5..fcd06ed7555a 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -2,9 +2,9 @@
 \* Abstract specification for a distributed consensus algorithm.
 \* Assumes that any node can atomically inspect the state of all other nodes. 
 
-EXTENDS Sequences, SequencesExt, Naturals, FiniteSets
+EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, FiniteSetsExt
 
-CONSTANT Servers, Terms, MaxLogLength, StartTerm
+CONSTANT Servers, Terms, MaxLogLength
 
 \* Commit logs from each node
 \* Each log is append-only and the logs will never diverge.
@@ -14,6 +14,8 @@ TypeOK ==
     /\ CLogs \in [Servers -> 
         UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
 
+StartTerm == Min(Terms)
+
 InitialLogs == {
     <<>>,
     <<StartTerm, StartTerm>>,

From 2ab3dfec0eb1a1be140e845624a60f9c5d992707 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 9 Sep 2024 10:39:52 +0000
Subject: [PATCH 17/19] lowercase variable name

---
 tla/consensus/MCccfraft.tla |  2 +-
 tla/consensus/abs.tla       | 24 ++++++++++++------------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
index 37a9b20d8b58..b314b05e6bf8 100644
--- a/tla/consensus/MCccfraft.tla
+++ b/tla/consensus/MCccfraft.tla
@@ -138,7 +138,7 @@ MappingToAbs ==
     Servers <- Servers,
     Terms <- StartTerm..MaxTermLimit,
     MaxLogLength <- MaxLogLength,
-    CLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
+    cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
 
 RefinementToAbsProp == MappingToAbs!AbsSpec
 
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index fcd06ed7555a..4a8cb9f0f4b2 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -8,10 +8,10 @@ CONSTANT Servers, Terms, MaxLogLength
 
 \* Commit logs from each node
 \* Each log is append-only and the logs will never diverge.
-VARIABLE CLogs
+VARIABLE cLogs
 
 TypeOK ==
-    /\ CLogs \in [Servers -> 
+    /\ cLogs \in [Servers -> 
         UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
 
 StartTerm == Min(Terms)
@@ -22,21 +22,21 @@ InitialLogs == {
     <<StartTerm, StartTerm, StartTerm, StartTerm>>}
     
 Init ==
-    CLogs \in [Servers -> InitialLogs]
+    cLogs \in [Servers -> InitialLogs]
 
 \* A node i can copy a ledger suffix from another node j.
 Copy(i) ==
     \E j \in Servers : 
-        /\ Len(CLogs[j]) > Len(CLogs[i])
-        /\ \E l \in 1..(Len(CLogs[j]) - Len(CLogs[i])) : 
-                CLogs' = [CLogs EXCEPT ![i] = @ \o SubSeq(CLogs[j], Len(@) + 1, Len(@) + l)]
+        /\ Len(cLogs[j]) > Len(cLogs[i])
+        /\ \E l \in 1..(Len(cLogs[j]) - Len(cLogs[i])) : 
+                cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]
 
 \* The node with the longest log can extend its log.
 Extend(i) ==
-    /\ \A j \in Servers : Len(CLogs[j]) \leq Len(CLogs[i])
-    /\ \E l \in 0..(MaxLogLength - Len(CLogs[i])) : 
+    /\ \A j \in Servers : Len(cLogs[j]) \leq Len(cLogs[i])
+    /\ \E l \in 0..(MaxLogLength - Len(cLogs[i])) : 
         \E s \in [1..l -> Terms] :
-            CLogs' = [CLogs EXCEPT ![i] = @ \o s]
+            cLogs' = [cLogs EXCEPT ![i] = @ \o s]
 
 \* The only possible actions are to append log entries.
 \* By construction there cannot be any conflicting log entries
@@ -49,11 +49,11 @@ Next ==
 AbsSpec == Init /\ [][Next]_CLogs
 
 AppendOnlyProp ==
-    [][\A i \in Servers : IsPrefix(CLogs[i], CLogs'[i])]_CLogs
+    [][\A i \in Servers : IsPrefix(cLogs[i], cLogs'[i])]_CLogs
 
 NoConflicts ==
     \A i, j \in Servers : 
-        \/ IsPrefix(CLogs[i], CLogs[j]) 
-        \/ IsPrefix(CLogs[j], CLogs[i])
+        \/ IsPrefix(cLogs[i], cLogs[j]) 
+        \/ IsPrefix(cLogs[j], cLogs[i])
 
 ====
\ No newline at end of file

From 8931e18313570a194edaf7a648d434f8556f283b Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 9 Sep 2024 10:47:22 +0000
Subject: [PATCH 18/19] conceptual state contraint for extend action

---
 tla/consensus/abs.tla | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index 4a8cb9f0f4b2..b1b652ca1761 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -31,20 +31,22 @@ Copy(i) ==
         /\ \E l \in 1..(Len(cLogs[j]) - Len(cLogs[i])) : 
                 cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]
 
-\* The node with the longest log can extend its log.
-Extend(i) ==
+\* A node i with the longest log can extend its log upto length k.
+Extend(i, k) ==
     /\ \A j \in Servers : Len(cLogs[j]) \leq Len(cLogs[i])
-    /\ \E l \in 0..(MaxLogLength - Len(cLogs[i])) : 
+    /\ \E l \in 0..(k - Len(cLogs[i])) : 
         \E s \in [1..l -> Terms] :
             cLogs' = [cLogs EXCEPT ![i] = @ \o s]
 
+ExtendToMax(i) == Extend(i, MaxLogLength)
+
 \* The only possible actions are to append log entries.
 \* By construction there cannot be any conflicting log entries
 \* Log entries are copied if the node's log is not the longest.
 Next ==
     \E i \in Servers : 
         \/ Copy(i) 
-        \/ Extend(i)
+        \/ ExtendToMax(i)
 
 AbsSpec == Init /\ [][Next]_CLogs
 

From d94cc79089cd17cea8a021ff0bbdbac69f5d9c25 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 9 Sep 2024 10:49:54 +0000
Subject: [PATCH 19/19] find replace fail

---
 tla/consensus/abs.tla | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index b1b652ca1761..b0855392f03d 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -48,10 +48,10 @@ Next ==
         \/ Copy(i) 
         \/ ExtendToMax(i)
 
-AbsSpec == Init /\ [][Next]_CLogs
+AbsSpec == Init /\ [][Next]_cLogs
 
 AppendOnlyProp ==
-    [][\A i \in Servers : IsPrefix(cLogs[i], cLogs'[i])]_CLogs
+    [][\A i \in Servers : IsPrefix(cLogs[i], cLogs'[i])]_cLogs
 
 NoConflicts ==
     \A i, j \in Servers :