Document lack of request payload validation in ctv (#6187)

microsoft · May 17, 2024 · b3d0eff · b3d0eff
1 parent cf8aadd
commit b3d0eff
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -175,7 +175,7 @@ IsClientRequest ==
     /\ IsEvent("replicate")
     /\ ClientRequest(logline.msg.state.node_id)
     /\ ~logline.msg.globally_committable
-    /\ logline.cmd_prefix # "cleanup_nodes"
+    /\ logline.cmd_prefix # "cleanup_nodes" 
     /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id)
     /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
     /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -128,8 +128,7 @@ Network == INSTANCE Network
 \* Helper function for checking the type safety of log entries
 EntryTypeOK(entry) ==
     /\ entry.term \in Nat \ {0}
-    /\ \/ /\ entry.contentType = TypeEntry
-          /\ entry.request \in Nat \ {0}
+    /\ \/ entry.contentType = TypeEntry
        \/ entry.contentType = TypeSignature
        \/ /\ entry.contentType = TypeReconfiguration
           /\ entry.configuration \subseteq Servers
@@ -739,14 +738,16 @@ BecomeLeader(i) ==
         IF @ = RetirementOrdered THEN Active ELSE @]
     /\ UNCHANGED <<messageVars, currentTerm, votedFor, isNewFollower, candidateVars, commitIndex, hasJoined, retirementCompleted>>
 
-\* Leader i receives a client request to add 42 to the log.
+\* Leader i receives a client request to add to the log. The consensus spec is agnostic to request payloads,
+\* and does not model or differentiate them. See the consistency spec (tla/consistency/*) for a specification
+\* from a client's perspective with differentiated payloads.
 ClientRequest(i) ==
     \* Only leaders receive client requests (and therefore they have not yet completed retirement)
     /\ leadershipState[i] = Leader
     \* See raft.h::can_replicate_unsafe()
     /\ membershipState[i] # RetiredCommitted
     \* Add new request to leader's log
-    /\ log' = [log EXCEPT ![i] = Append(@, [term  |-> currentTerm[i], request |-> 42, contentType |-> TypeEntry]) ]
+    /\ log' = [log EXCEPT ![i] = Append(@, [term  |-> currentTerm[i], contentType |-> TypeEntry]) ]
     /\ UNCHANGED <<reconfigurationVars, messageVars, serverVars, candidateVars, leaderVars, commitIndex>>
 
 \* CCF: Signed commits