feat(kuilt-raft): structured trace emission for TLC-compatible state-transition logging

[keddie]

🤖 This comment was generated by Claude on behalf of @keddie.

Part of epic #108.

Prior art (don't invent — adopt)

The etcd community has settled both the event vocabulary and the trace format:

• Spec: Use Vanlightly's standard-raft Raft.tla as the TLA+ base (cleaner than etcd's spec which has etcd-specific extensions like joint consensus and Ready/Advance primitives that kuilt-raft doesn't have).
• Vocabulary: Adopt the etcd action names directly — Timeout, RequestVote, BecomeLeader, BecomeFollowerOfTerm, ClientRequest, AppendEntries, Heartbeat, AdvanceCommitIndex, Restart.
• Format: ndjson, one record per state transition, from SEFM 2024 paper (arXiv:2404.16075):

  {"clock": 42, "event": "BecomeLeader", "event_args": ["node1"],
   "currentTerm": [{"op": "Update", "path": ["node1"], "args": [3]}],
   "state": [{"op": "Update", "path": ["node1"], "args": ["Leader"]}]}

  Variables emit deltas (only what changed), not full snapshots.
• TLC validation: Write a TraceSpec.tla using Kuppe's IsEvent("A") pattern (TLA+ Conf 2024 talk) — replaces Init with "matches trace record 0" and each action A with A ∧ IsEvent("A"). Gate with -Ptlc.trace.validation=true like the mdns multicast tests.
• Reference implementation: etcd trace validation PR #204 (Go, not merged due to rebase drift but design is accepted — read the diff).

What to build

1. RaftTraceEvent sealed interface (in commonMain) — use the etcd vocabulary:

sealed interface RaftTraceEvent {
    val clock: Long  // logical clock / message counter
    data class Timeout(override val clock: Long, val node: NodeId) : RaftTraceEvent
    data class RequestVote(override val clock: Long, val from: NodeId, val to: NodeId, val term: Long) : RaftTraceEvent
    data class BecomeLeader(override val clock: Long, val node: NodeId, val term: Long) : RaftTraceEvent
    data class BecomeFollowerOfTerm(override val clock: Long, val node: NodeId, val term: Long, val reason: String) : RaftTraceEvent
    data class ClientRequest(override val clock: Long, val node: NodeId, val index: Long) : RaftTraceEvent
    data class AppendEntries(override val clock: Long, val from: NodeId, val to: NodeId, val prevLogIndex: Long, val entryCount: Int) : RaftTraceEvent
    data class Heartbeat(override val clock: Long, val from: NodeId, val to: NodeId) : RaftTraceEvent
    data class AdvanceCommitIndex(override val clock: Long, val node: NodeId, val commitIndex: Long) : RaftTraceEvent
    data class Restart(override val clock: Long, val node: NodeId) : RaftTraceEvent
}

2. trace: Flow<RaftTraceEvent> on RaftNode interface — hot SharedFlow, replay=0.

3. RaftTraceRecorder utility (in commonMain) — collects events from N nodes into a single ndjson trace file:

class RaftTraceRecorder(private val nodes: Map<NodeId, RaftNode>, private val scope: CoroutineScope) {
    fun startRecording(): Job
    fun snapshot(): List<RaftTraceEvent>  // ordered by clock
    suspend fun writeNdjson(sink: (String) -> Unit)  // one JSON line per event
}

4. Tests in TraceTest.kt:

• initialElection_trace_emits_BecomeLeader — verify exactly one BecomeLeader per term
• proposal_trace_ClientRequest_before_AdvanceCommitIndex — verify ordering invariant
• stepDown_trace_emits_BecomeFollowerOfTerm — verify on higher-term observation
• reElection_trace_noDoubleLeader_sameTermOrdering — no two BecomeLeader events with the same term

5. TLC validation gate (jvmTest only, -Ptlc.trace.validation=true):

• RaftTlcTraceTest collects a trace from a 3-node sim, writes ndjson, runs TLC with TraceSpec.tla against Vanlightly's spec, asserts exit code 0.

Acceptance criteria

• RaftTraceEvent in commonMain; trace: Flow<RaftTraceEvent> on RaftNode
• RaftTraceRecorder can serialize to ndjson matching the SEFM 2024 schema
• 4 TraceTest assertions pass
• TLC gate exists (even if gated behind -P flag; passing CI is the target)

References

• SEFM 2024 paper (arXiv:2404.16075)
• etcd trace validation PR #204 (Go reference)
• Vanlightly standard-raft Raft.tla
• Kuppe TLA+ Conf 2024 talk