Correct etcd log freshness and add commit liveness

README.md

@@ -35,11 +35,11 @@ We currently focus on a few hard problems (due to token shortage).
 | [Cahill’s serializable snapshot isolation](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/CahillSSI/CahillSerializability.tla) | Protocol | 1  | 1 |
 | [Ivy TLB](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/ivy_examples_tlb/ivy_examples_tlb.tla) | System | 1  | 2 |
 | [OpenAddressing](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/OpenAddressing/OpenAddressing.tla) | System | 1 | 5 |
-| [etcd Raft](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla) | System | 1 | 8 |
+| [etcd Raft](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla) | System | 1 | 9 |
 | [HashiCorp Raft](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/HashicorpRaft/HashicorpRaft.tla) | System | 1 | 6 |
 | [ZooKeeper implementation](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/ZooKeeper_LowLevel/ZkV3_7_0.tla) | System | 1 | 9 |
 | [MongoDB distributed transactions](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/MongoDB/MultiShardTxnSnapshot.tla) | System | 1 | 1 |
-| **Total** |  | 9 | 56 |
+| **Total** |  | 9 | 57 |
 
 For more problems, check out [the full problem set](https://github.com/specula-org/TLAPS-Bench/tree/main/benchmark/proof-from-scratch-module).
 

benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla

@@ -43,4 +43,11 @@ THEOREM QuorumLog == Spec => []QuorumLogInv
 \* BEGIN AGENT PROOF etcd_raft/etcd_raft_QuorumLog.tla
 PROOF OMITTED
 \* END AGENT PROOF etcd_raft/etcd_raft_QuorumLog.tla
+
+THEOREM CommitLiveness ==
+    \A l \in InitServer : \A Q \in Quorum(InitServer) : \A n \in Nat \ {0} :
+        LiveSpec(l, Q, n) => CommitProgress(l, n)
+\* BEGIN AGENT PROOF etcd_raft/etcd_raft_CommitLiveness.tla
+PROOF OMITTED
+\* END AGENT PROOF etcd_raft/etcd_raft_CommitLiveness.tla
 ====

benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla

@@ -38,11 +38,13 @@ QuorumLogInv ==
             IsPrefix(Committed(i), log[j])
 
 MoreUpToDateCorrectInv ==
-    \A i, j \in Server :
-       (\/ LastTerm(log[i]) > LastTerm(log[j])
-        \/ /\ LastTerm(log[i]) = LastTerm(log[j])
-           /\ Len(log[i]) >= Len(log[j])) =>
-       IsPrefix(Committed(j), log[i])
+    \A i \in Server :
+       (\E Q \in Quorum(GetConfig(i)) :
+           \A j \in Q :
+               \/ LastTerm(log[i]) > LastTerm(log[j])
+               \/ /\ LastTerm(log[i]) = LastTerm(log[j])
+                  /\ Len(log[i]) >= Len(log[j])) =>
+       \A j \in Server : IsPrefix(Committed(j), log[i])
 
 LeaderCompletenessInv ==
     \A c \in commitHistory, e \in electionHistory :
@@ -52,5 +54,70 @@ CommittedIsDurableInv ==
     \A i \in Server :
         state[i] = Leader => commitIndex[i] <= durableState[i].log
 
+StableReplicationNext(l, Q) ==
+    /\ RecordEvents
+    /\ currentTerm'[l] = currentTerm[l]
+    /\ state'[l] = Leader
+    /\ \/ ReplicationNext
+       \/ \E i \in Server \ Q : Restart(i)
+       \/ \E i \in Server \ {l} : StepDownToFollower(i)
+       \/ \E m \in DOMAIN messages :
+           /\ messages[m] = 1
+           /\ \/ DuplicateMessage(m)
+              \/ /\ ~(m.msource \in Q /\ m.mdest \in Q)
+                 /\ DropMessage(m)
+
+StableReplication(l, Q) ==
+    /\ l \in Q
+    /\ <>[] (state[l] = Leader /\ \A j \in Q : currentTerm[j] <= currentTerm[l])
+    /\ <>[][StableReplicationNext(l, Q)]_vars
+
+SendThrough(l, j, n) ==
+    /\ n \in 1..Len(log[l])
+    /\ matchIndex[l][j] < n
+    /\ AppendEntries(l, j, <<matchIndex[l][j] + 1, n + 1>>)
+    /\ RecordEvents
+
+ReceiveThrough(l, j, n) ==
+    /\ \E m \in DOMAIN messages :
+        /\ m.mtype = AppendEntriesRequest
+        /\ m.msource = l /\ m.mdest = j
+        /\ m.mterm = currentTerm[l]
+        /\ m.msubtype = "app"
+        /\ m.mprevLogIndex < n
+        /\ m.mprevLogIndex + Len(m.mentries) >= n
+        /\ Receive(m)
+    /\ RecordEvents
+
+ReceiveAckThrough(l, j, n) ==
+    /\ \E m \in DOMAIN messages :
+        /\ m.mtype = AppendEntriesResponse
+        /\ m.msource = j /\ m.mdest = l
+        /\ m.mterm = currentTerm[l]
+        /\ m.msuccess /\ m.mmatchIndex >= n
+        /\ Receive(m)
+    /\ RecordEvents
+
+ReplicationFairness(l, Q, n) ==
+    /\ \A j \in Q : WF_vars(Ready(j) /\ RecordEvents)
+    /\ WF_vars(matchIndex[l][l] < n /\ AppendEntriesToSelf(l) /\ RecordEvents)
+    /\ WF_vars(AdvanceCommitIndex(l) /\ RecordEvents)
+    /\ \A j \in Q : SF_vars(ReceiveAckThrough(l, j, n))
+    /\ \A j \in Q \ {l} :
+        /\ WF_vars(SendThrough(l, j, n))
+        /\ SF_vars(ReceiveThrough(l, j, n))
+
+LiveSpec(l, Q, n) ==
+    /\ Spec
+    /\ StableReplication(l, Q)
+    /\ ReplicationFairness(l, Q, n)
+
+CurrentTermEntry(l, n) ==
+    /\ state[l] = Leader
+    /\ n \in 1..Len(log[l])
+    /\ log[l][n].term = currentTerm[l]
+
+CommitProgress(l, n) == <>[] (CurrentTermEntry(l, n) ~> commitIndex[l] >= n)
+
 ===============================================================================
 

benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla

@@ -482,7 +482,7 @@ DropMessage(m) ==
     /\ Discard(m)
     /\ UNCHANGED <<pendingMessages, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
 
-NextAsync == 
+ReplicationNext ==
     \/ \E i,j \in Server : RequestVote(i, j)
     \/ \E i \in Server : BecomeLeader(i)
     \/ \E i \in Server: ClientRequest(i, 0)
@@ -492,8 +492,11 @@ NextAsync ==
     \/ \E i,j \in Server : Heartbeat(i, j)
     \/ \E i,j \in Server : \E index \in 1..commitIndex[i] : SendSnapshot(i, j, index)
     \/ \E m \in DOMAIN messages : Receive(m)
-    \/ \E i \in Server : Timeout(i)
     \/ \E i \in Server : Ready(i)
+
+NextAsync ==
+    \/ ReplicationNext
+    \/ \E i \in Server : Timeout(i)
     \/ \E i \in Server : StepDownToFollower(i)
 
 NextCrash == \E i \in Server : Restart(i)

benchmark/proof-from-scratch-module/manifest.json

@@ -1,6 +1,6 @@
 {
   "format_version": 1,
-  "corpus_sha256": "58395353d2eb2d0d6ee4e0fc6c657a7d0cc508f91e1ef7a0e07bd3675f2cca7d",
+  "corpus_sha256": "78e9956d3fe3aab33c76b3fa0c83ea74c7b685b9a2347fc025d2d82c93dbfa3d",
   "complete": true,
   "module_tasks": [
     {
@@ -997,7 +997,7 @@
       "spec": {
         "format_version": 1,
         "task_id": "etcd_raft/etcd_raft.tla",
-        "source_sha256": "e6aa5a22b17d9556f7cb97a659cdae152d2b9b038d56739068697d8cd3aa3d3f",
+        "source_sha256": "8c0822bfc40a2af2a0578f2943fb9c448904b59ab27a1e3d812b282ca7004caa",
         "proof_units": [
           {
             "task_id": "etcd_raft/etcd_raft_LogInv.tla",
@@ -1030,6 +1030,10 @@
           {
             "task_id": "etcd_raft/etcd_raft_QuorumLog.tla",
             "statement_sha256": "042668e54a03ee5119ed166a69f8bfca8fcd98fab0f634430dd53ecff973db9d"
+          },
+          {
+            "task_id": "etcd_raft/etcd_raft_CommitLiveness.tla",
+            "statement_sha256": "180e0fe63faa15175f80a0e07b90e16f4aadf9c6074261699bceb4f21e801dce"
           }
         ]
       },

benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla

@@ -482,7 +482,7 @@ DropMessage(m) ==
     /\ Discard(m)
     /\ UNCHANGED <<pendingMessages, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
 
-NextAsync == 
+ReplicationNext ==
     \/ \E i,j \in Server : RequestVote(i, j)
     \/ \E i \in Server : BecomeLeader(i)
     \/ \E i \in Server: ClientRequest(i, 0)
@@ -492,8 +492,11 @@ NextAsync ==
     \/ \E i,j \in Server : Heartbeat(i, j)
     \/ \E i,j \in Server : \E index \in 1..commitIndex[i] : SendSnapshot(i, j, index)
     \/ \E m \in DOMAIN messages : Receive(m)
-    \/ \E i \in Server : Timeout(i)
     \/ \E i \in Server : Ready(i)
+
+NextAsync ==
+    \/ ReplicationNext
+    \/ \E i \in Server : Timeout(i)
     \/ \E i \in Server : StepDownToFollower(i)
 
 NextCrash == \E i \in Server : Restart(i)

benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLiveness.tla

@@ -0,0 +1,12 @@
+---- MODULE etcd_raft_CommitLiveness ----
+EXTENDS etcd_raft_CommitLivenessDefs
+
+\* BEGIN AGENT HELPERS
+\* END AGENT HELPERS
+THEOREM CommitLiveness ==
+    \A l \in InitServer : \A Q \in Quorum(InitServer) : \A n \in Nat \ {0} :
+        LiveSpec(l, Q, n) => CommitProgress(l, n)
+\* BEGIN AGENT PROOF
+PROOF OBVIOUS
+\* END AGENT PROOF
+====