Adding an abstract consensus spec (#6438)

Co-authored-by: Markus Alexander Kuppe <[email protected]>

.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

tla/consensus/MCabs.cfg

@@ -0,0 +1,17 @@
+SPECIFICATION AbsSpec
+
+CONSTANTS
+    NodeOne = n1
+    NodeTwo = n2
+    NodeThree = n3
+    Servers <- MCServers
+    Terms <- MCTerms
+    MaxLogLength <- MCMaxLogLength
+
+INVARIANTS
+    NoConflicts
+    TypeOK
+
+PROPERTIES 
+    AppendOnlyProp
+

tla/consensus/MCabs.tla

@@ -0,0 +1,11 @@
+---- MODULE MCabs ----
+
+EXTENDS abs
+
+CONSTANTS NodeOne, NodeTwo, NodeThree
+
+MCServers == {NodeOne, NodeTwo, NodeThree}
+MCTerms == 2..4
+MCMaxLogLength == 7
+
+====

tla/consensus/MCccfraft.cfg

@@ -68,6 +68,7 @@ PROPERTIES
     MembershipStateTransitionsProp
     PendingBecomesFollowerProp
     NeverCommitEntryPrevTermsProp
+    RefinementToAbsProp
 
 INVARIANTS
     LogInv

tla/consensus/MCccfraft.tla

@@ -126,4 +126,20 @@ DebugNotTooManySigsInv ==
     \A i \in Servers:
         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 <- StartTerm..MaxTermLimit,
+    MaxLogLength <- MaxLogLength,
+    cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
+
+RefinementToAbsProp == MappingToAbs!AbsSpec
+
 ===================================

tla/consensus/abs.tla

@@ -0,0 +1,61 @@
+---- MODULE abs ----
+\* 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, FiniteSetsExt
+
+CONSTANT Servers, Terms, MaxLogLength
+
+\* Commit logs from each node
+\* 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}]
+
+StartTerm == Min(Terms)
+
+InitialLogs == {
+    <<>>,
+    <<StartTerm, StartTerm>>,
+    <<StartTerm, StartTerm, StartTerm, StartTerm>>}
+
+Init ==
+    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)]
+
+\* 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..(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) 
+        \/ ExtendToMax(i)
+
+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])
+
+====