diff --git a/.kiro/specs/raft-sim-conformance/tasks.md b/.kiro/specs/raft-sim-conformance/tasks.md index 6a8544ea..11fb4263 100644 --- a/.kiro/specs/raft-sim-conformance/tasks.md +++ b/.kiro/specs/raft-sim-conformance/tasks.md @@ -20,7 +20,7 @@ ## 1. Harness types and in-memory adapter backing -- [ ] 1.1 Extend the `XCE_TESTING` sim section of `raft.h` with the harness data types +- [x] 1.1 Extend the `XCE_TESTING` sim section of `raft.h` with the harness data types - Add `raft_sim_msg_kind_t`, `raft_sim_msg_t` (vote/AE req+rsp union fields), `raft_sim_log_entry_t {term, value}`, `raft_sim_action_t {kind, actor, msg_index, term, index}`, and the `RAFT_SIM_MAX_LOG/MSGS/STEPS` bounds - Extend `raft_sim_node_t` with `log[]`, `log_len`, `commit_index`, `applied[]`, and a persisted-`(term, votedFor)` shadow for Restart; extend `raft_sim_cluster_t` with `bag[]`+`bag_count`, PRNG state, `seed`, and `trace[]`+`trace_len` - Observable completion: `raft.h` compiles under `XCE_TESTING`; no protocol declaration changed; `sizeof(raft_sim_cluster_t)` grows by the new fixed arrays diff --git a/src/lib/raft/raft.h b/src/lib/raft/raft.h index 36c51a20..7cd0ccf6 100644 --- a/src/lib/raft/raft.h +++ b/src/lib/raft/raft.h @@ -444,6 +444,16 @@ void raft_snapshot(const raft_state_t *s, raft_snapshot_t *snap); /* Upper bound on buffered AppendEntries awaiting delivery (mirrors pending[]). */ #define RAFT_SIM_MAX_AE 64 +/* ---- conformance harness bounds (raft-sim-conformance) ---- + * Capacity of the unified message bag (cluster.bag[], mirrors raft.tla's + * `messages`): in-flight vote/AE requests and responses, the unit on which + * Drop/Duplicate/Reorder operate. Sized generously above RAFT_SIM_MAX_AE so a + * bounded run never overflows the bag (duplicates add members). */ +#define RAFT_SIM_MAX_MSGS 256 +/* Upper bound on recorded scheduler steps (cluster.trace[]) for replayable + * failure traces. One raft_sim_action_t is recorded per step. */ +#define RAFT_SIM_MAX_STEPS 1024 + /* Buffered RPC entry: one pending vote-request to route. * last_log_term/last_log_index capture the CANDIDATE's advertised last-log tuple * at SEND time (mirroring raft_sim_ae_t.leader_term) so the (lastLogTerm, @@ -487,6 +497,76 @@ typedef struct { size_t entry_len; /* valid when n_entries == 1 */ } raft_sim_ae_t; +/* ---- conformance harness data types (raft-sim-conformance) ---- + * + * These mirror raft.tla's `messages` bag and per-node variables for the + * deterministic conformance/verification harness. They are SEPARATE from the + * byte-payload WAL model above (raft_sim_entry_t / raft_sim_ae_t / raft_sim_rpc_t): + * the conformance harness uses a lightweight (term, value) log entry and a single + * unified message type so a randomized, seeded action scheduler can drive N library + * instances purely synchronously and assert the four Raft safety invariants. */ + +/* Unified bag-message kind: a vote/AE request or its matching response. */ +typedef enum { + RAFT_SIM_MSG_VOTE_REQ, + RAFT_SIM_MSG_VOTE_RSP, + RAFT_SIM_MSG_AE_REQ, + RAFT_SIM_MSG_AE_RSP, +} raft_sim_msg_kind_t; + +/* One in-flight RPC in the message bag (mirrors raft.tla `messages`). Carries the + * union of vote/AE request and response fields; only the fields relevant to `kind` + * are meaningful. This is the unit Drop/Duplicate/Reorder operate on; a handler + * reply is pushed back as a *_RSP member so responses are first-class. */ +typedef struct { + raft_sim_msg_kind_t kind; + int src, dst; + uint64_t term; /* RPC term (all kinds) */ + /* AE request */ + uint64_t prev_log_index, prev_log_term, leader_commit; + uint64_t entry_term, entry_value; /* one entry per AE (raft.tla "<=1 entry") */ + int entries_len; /* 0 = heartbeat, 1 = one entry */ + /* responses */ + int granted; /* vote rsp */ + int success; /* AE rsp */ + uint64_t match_index; /* AE rsp */ +} raft_sim_msg_t; + +/* One conformance-harness log entry: term stamp + synthetic monotone client value. + * The 1-based array position is the log index (= WAL LSN); `value` makes State + * Machine Safety divergence observable. Distinct from raft_sim_entry_t (which models + * the byte-payload WAL): this is the (term, value) bag/applied model. */ +typedef struct { + uint64_t term; + uint64_t value; +} raft_sim_log_entry_t; + +/* The Next-action set the scheduler chooses from; each maps to a raft.tla `Next` + * disjunct. Only *enabled* actions are eligible at a given step. */ +typedef enum { + RAFT_SIM_ACT_RESTART, /* Restart: re-init preserving persisted state */ + RAFT_SIM_ACT_TIMEOUT, /* Timeout: become candidate, bump term */ + RAFT_SIM_ACT_REQUEST_VOTE, /* RequestVote: deliver a vote-request */ + RAFT_SIM_ACT_BECOME_LEADER, /* BecomeLeader: deliver quorum-completing vote-rsp */ + RAFT_SIM_ACT_CLIENT_REQUEST, /* ClientRequest: leader appends a client value */ + RAFT_SIM_ACT_APPEND_ENTRIES, /* AppendEntries: leader pushes an AE-request */ + RAFT_SIM_ACT_ADVANCE_COMMIT, /* AdvanceCommitIndex: leader advances commit */ + RAFT_SIM_ACT_RECEIVE, /* Receive: deliver a bag message to its handler */ + RAFT_SIM_ACT_DUPLICATE_MESSAGE, /* DuplicateMessage: re-push a bag member */ + RAFT_SIM_ACT_DROP_MESSAGE, /* DropMessage: discard a bag member */ +} raft_sim_action_kind_t; + +/* One replayable trace unit: the action taken at a scheduler step plus the operands + * needed to reproduce it (actor node, target message index in the bag, and the + * (term, index) the action referenced). Recorded per step into cluster.trace[]. */ +typedef struct { + raft_sim_action_kind_t kind; + int actor; /* node that took the action (-1 if N/A) */ + int msg_index; /* bag index acted on (-1 if N/A) */ + uint64_t term; /* term referenced by the action (0 if N/A) */ + uint64_t index; /* log index referenced by the action (0 if N/A) */ +} raft_sim_action_t; + /* One simulated node */ typedef struct { raft_state_t state; @@ -506,6 +586,19 @@ typedef struct { * commit-advance DRIVER helper is a later task; this is only the callback half. */ uint64_t commit_index; int commit_advanced_count; + /* ---- conformance harness per-node state (raft-sim-conformance) ---- + * applied[k-1] holds the client value applied at committed index k (set by the + * node's on_commit_advanced as commit_index advances). State Machine Safety + * checks that applied[k] agrees across nodes. NOTE: log_count above already + * satisfies the design's `log_len` requirement for the in-memory log length; + * no separate log_len field is added (it would duplicate log_count). */ + uint64_t applied[RAFT_SIM_MAX_LOG]; + /* Persisted-(term, votedFor) shadow surviving a Restart, mirroring raft.tla's + * `Restart` (keeps currentTerm/votedFor/log, resets volatile state). The + * conformance restart action restores from this shadow rather than re-reading + * live volatile state. */ + uint64_t persisted_term; + int persisted_voted_for; /* per-node trace event log for test assertions */ char trace_buf[4096]; int trace_len; @@ -523,6 +616,18 @@ typedef struct { * task 8.2); on_send_append_entries enqueues here. */ raft_sim_ae_t ae_pending[RAFT_SIM_MAX_AE]; int ae_pending_count; + /* ---- conformance harness cluster state (raft-sim-conformance) ---- + * Unified message bag mirroring raft.tla `messages`: vote/AE requests and + * responses, the unit Drop/Duplicate/Reorder operate on. */ + raft_sim_msg_t bag[RAFT_SIM_MAX_MSGS]; + int bag_count; + /* Seeded deterministic PRNG: `seed` is the run's reproducibility key; `prng` + * is the evolving generator state (SplitMix64/xorshift, no libc rand()). */ + uint64_t seed; + uint64_t prng; + /* Replayable per-step action trace for failure dumps. */ + raft_sim_action_t trace[RAFT_SIM_MAX_STEPS]; + int trace_len; } raft_sim_cluster_t; /* diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index 167dd405..17568d34 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -3203,6 +3203,76 @@ static void test_raft_snapshot_returns_current_state(void) #ifdef XCE_TESTING +/* + * test_sim_conformance_types_compile (raft-sim-conformance task 1.1) + * + * Structural / compile-reference test for the conformance harness data types + * added to the XCE_TESTING section of raft.h. This task is non-behavioral: it + * only declares new types and struct fields. The test proves the new types are + * usable (construct a raft_sim_msg_t / raft_sim_log_entry_t / raft_sim_action_t + * and read fields back) and that raft_sim_cluster_t / raft_sim_node_t carry the + * new fixed arrays (sizeof grows to include bag[]/trace[]/applied[]). + */ +static void test_sim_conformance_types_compile(void) +{ + /* Bag message round-trips its fields. */ + raft_sim_msg_t m; + memset(&m, 0, sizeof(m)); + m.kind = RAFT_SIM_MSG_AE_REQ; + m.src = 1; + m.dst = 2; + m.term = 7; + m.entry_term = 7; + m.entry_value = 42; + m.entries_len = 1; + TEST_ASSERT_EQUAL_INT(RAFT_SIM_MSG_AE_REQ, m.kind); + TEST_ASSERT_EQUAL_UINT64(42, m.entry_value); + TEST_ASSERT_EQUAL_INT(1, m.entries_len); + + /* Lightweight (term, value) log entry. */ + raft_sim_log_entry_t e = { .term = 3, .value = 99 }; + TEST_ASSERT_EQUAL_UINT64(3, e.term); + TEST_ASSERT_EQUAL_UINT64(99, e.value); + + /* Replayable action record over the Next-action enum. */ + raft_sim_action_t a; + memset(&a, 0, sizeof(a)); + a.kind = RAFT_SIM_ACT_APPEND_ENTRIES; + a.actor = 0; + a.msg_index = -1; + a.term = 7; + a.index = 5; + TEST_ASSERT_EQUAL_INT(RAFT_SIM_ACT_APPEND_ENTRIES, a.kind); + TEST_ASSERT_EQUAL_UINT64(5, a.index); + + /* New node + cluster fields exist and are addressable. */ + raft_sim_node_t n; + memset(&n, 0, sizeof(n)); + n.applied[0] = 11; + n.persisted_term = 4; + n.persisted_voted_for = 2; + TEST_ASSERT_EQUAL_UINT64(11, n.applied[0]); + TEST_ASSERT_EQUAL_INT(2, n.persisted_voted_for); + + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + c.seed = 0xDEADBEEFULL; + c.prng = c.seed; + c.bag_count = 0; + c.trace_len = 0; + c.bag[0] = m; + c.trace[0] = a; + TEST_ASSERT_EQUAL_UINT64(0xDEADBEEFULL, c.seed); + TEST_ASSERT_EQUAL_INT(RAFT_SIM_MSG_AE_REQ, c.bag[0].kind); + TEST_ASSERT_EQUAL_INT(RAFT_SIM_ACT_APPEND_ENTRIES, c.trace[0].kind); + + /* sizeof grows to include the new fixed arrays (bounds are positive). */ + TEST_ASSERT_TRUE(RAFT_SIM_MAX_MSGS > 0); + TEST_ASSERT_TRUE(RAFT_SIM_MAX_STEPS > 0); + TEST_ASSERT_TRUE(sizeof(c.bag) == sizeof(raft_sim_msg_t) * RAFT_SIM_MAX_MSGS); + TEST_ASSERT_TRUE(sizeof(c.trace) == sizeof(raft_sim_action_t) * RAFT_SIM_MAX_STEPS); +} + /* * test_sim_init_3node * @@ -6933,6 +7003,9 @@ void test_raft(void) /* simulator init (task 4.1) */ #ifdef XCE_TESTING + /* conformance harness data types (raft-sim-conformance task 1.1) */ + RUN_TEST(test_sim_conformance_types_compile); + RUN_TEST(test_sim_init_3node); RUN_TEST(test_sim_trace_buf);