From 63a9740c855de5f1d2f18af533d2f8dc7f351f7c Mon Sep 17 00:00:00 2001 From: Rongsong Shen Date: Wed, 24 Jun 2026 12:44:18 +0000 Subject: [PATCH] feat(raft-sim-conformance): Leader Completeness invariant checker (task 3.3) --- .kiro/specs/raft-sim-conformance/tasks.md | 2 +- src/lib/raft/raft.h | 23 +++++++ src/lib/raft/raft_sim.c | 43 +++++++++++++ src/lib/testsuite/test_raft.c | 76 +++++++++++++++++++++++ 4 files changed, 143 insertions(+), 1 deletion(-) diff --git a/.kiro/specs/raft-sim-conformance/tasks.md b/.kiro/specs/raft-sim-conformance/tasks.md index 607f758a..f1c04aec 100644 --- a/.kiro/specs/raft-sim-conformance/tasks.md +++ b/.kiro/specs/raft-sim-conformance/tasks.md @@ -71,7 +71,7 @@ - _Boundary: raft_sim.c, test_raft.c_ - _Depends: 1.1_ -- [ ] 3.3 RED+GREEN: Leader Completeness checker (P) +- [x] 3.3 RED+GREEN: Leader Completeness checker (P) - Test: a committed `(index, term)` absent from a higher-term leader's log fails; present passes - Implement `raft_sim_check_leader_completeness` using `commit_index` + per-node logs, tracking the highest-term leader to date - Observable completion: both directions assert correctly diff --git a/src/lib/raft/raft.h b/src/lib/raft/raft.h index 98373571..f940cda8 100644 --- a/src/lib/raft/raft.h +++ b/src/lib/raft/raft.h @@ -790,6 +790,29 @@ int raft_sim_check_log_matching(const raft_sim_cluster_t *c); */ int raft_sim_check_election_safety(const raft_sim_cluster_t *c); +/* + * raft_sim_check_leader_completeness: assert the Raft Leader Completeness property + * over the cluster's observable per-node state (Req 3.3, 3.6). + * + * Leader Completeness: if an entry is committed in term t, then that entry is + * present (same index, same term) in the logs of all leaders of terms > t. + * + * Computed purely from observable state (Req 3.6): the committed set is every + * index k in 1..node->commit_index for each node (carrying that node's + * log[k-1].term — the per-node mirror filled by on_commit_advanced); the current + * leaders are the nodes with role == RAFT_LEADER (read via raft_snapshot). For + * each leader L at term T_L and each committed entry (k, t) with t < T_L, L's log + * MUST contain index k at term t; otherwise the property is violated. Presence is + * keyed on (index, term) — Log Matching covers payload identity. + * + * Returns 1 if Leader Completeness holds across the whole cluster, 0 if any + * higher-term leader is missing (or carries a different term for) a lower-term + * committed entry. Pure read-only over c (no I/O, no Unity assertions) so the lib + * stays test-framework-agnostic; the caller asserts on the returned value (same + * convention as raft_sim_check_log_matching). + */ +int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c); + /* * raft_sim_advance_commit: drive raft_advance_commit on node_idx (task 6.1). * diff --git a/src/lib/raft/raft_sim.c b/src/lib/raft/raft_sim.c index 7d4c3fc5..38056976 100644 --- a/src/lib/raft/raft_sim.c +++ b/src/lib/raft/raft_sim.c @@ -839,6 +839,49 @@ int raft_sim_check_election_safety(const raft_sim_cluster_t *c) return 1; /* holds */ } +int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c) +{ + /* Leader Completeness: an entry committed in term t must be present (same + * index, same term) in the log of every leader of a strictly-higher term. + * + * Pure per-snapshot observer (Req 3.6): the committed set is every index k in + * 1..commit_index over ALL nodes (carrying that node's log[k-1].term); the + * current leaders are the role==RAFT_LEADER nodes. For each leader L at term + * T_L and each committed (k, t) with t < T_L, L's log must hold index k at + * term t — else the property is violated. (index, term) presence suffices; + * Log Matching covers payload identity. */ + for (int L = 0; L < c->n; L++) { + raft_snapshot_t sl; + raft_snapshot(&c->nodes[L].state, &sl); + if (sl.role != RAFT_LEADER) + continue; + + const raft_sim_node_t *leader = &c->nodes[L]; + + /* Scan every node's committed prefix for entries committed under a term + * strictly lower than this leader's term. */ + for (int d = 0; d < c->n; d++) { + const raft_sim_node_t *src = &c->nodes[d]; + int committed = (int)src->commit_index; + if (committed > src->log_count) + committed = src->log_count; + + for (int k = 1; k <= committed; k++) { + uint64_t t = src->log[k - 1].term; + if (t >= sl.term) + continue; /* only lower-term committed entries bind */ + + /* Leader L must contain index k at term t. */ + if (k > leader->log_count) + return 0; /* leader missing the committed index */ + if (leader->log[k - 1].term != t) + return 0; /* leader has a different term at index k */ + } + } + } + return 1; /* holds */ +} + int raft_sim_restart_node(raft_sim_cluster_t *c, int node_idx) { if (node_idx < 0 || node_idx >= c->n) diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index 1d6016cd..c7197e90 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -3750,6 +3750,80 @@ static void test_sim_check_election_safety_pass_on_single_leader(void) TEST_ASSERT_EQUAL_INT(1, raft_sim_check_election_safety(&c)); } +/* + * test_sim_check_leader_completeness_fail_on_missing_committed (task 3.3) + * + * Leader Completeness: an entry committed in term t must be present (same index, + * same term) in the log of every leader of a higher term. Hand-build a cluster + * where node B has committed (index=2, term=3) but the current higher-term leader + * (node A, LEADER at term 5) is MISSING that index ⇒ the checker must FAIL (0). + * (Hand-set role/term/log/commit_index directly — this is a checker unit test over + * a hand-built cluster, not a protocol run.) + */ +static void test_sim_check_leader_completeness_fail_on_missing_committed(void) +{ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000)); + + /* Node B (idx 1): committed prefix 1..2, with entry 2 carrying term 3. */ + c.nodes[1].log[0].term = 1; + c.nodes[1].log[1].term = 3; + c.nodes[1].log_count = 2; + c.nodes[1].commit_index = 2; /* (index=2, term=3) is committed */ + + /* Node A (idx 0): current LEADER at the HIGHER term 5, but its log is SHORT + * (only index 1) ⇒ it is MISSING the committed index 2 ⇒ violation. */ + c.nodes[0].state.role = RAFT_LEADER; + c.nodes[0].state.term = 5; + c.nodes[0].log[0].term = 1; + c.nodes[0].log_count = 1; + + c.nodes[2].state.role = RAFT_FOLLOWER; + c.nodes[2].state.term = 5; + + TEST_ASSERT_EQUAL_INT(0, raft_sim_check_leader_completeness(&c)); +} + +/* + * test_sim_check_leader_completeness_pass_when_present (task 3.3) + * + * Leader Completeness holds when every higher-term leader's log contains every + * lower-term committed entry at the same (index, term). Two scenarios pass: + * (a) the committed (index=2, term=3) entry IS present in higher-term leader A; + * (b) a clean cluster with no current leaders trivially holds. + */ +static void test_sim_check_leader_completeness_pass_when_present(void) +{ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000)); + + /* Node B (idx 1): committed prefix 1..2, entry 2 carries term 3. */ + c.nodes[1].log[0].term = 1; + c.nodes[1].log[1].term = 3; + c.nodes[1].log_count = 2; + c.nodes[1].commit_index = 2; + + /* (a) Node A (idx 0): LEADER at higher term 5 and DOES contain index 2 at + * term 3 (and index 1) ⇒ Leader Completeness holds. */ + c.nodes[0].state.role = RAFT_LEADER; + c.nodes[0].state.term = 5; + c.nodes[0].log[0].term = 1; + c.nodes[0].log[1].term = 3; + c.nodes[0].log_count = 2; + + c.nodes[2].state.role = RAFT_FOLLOWER; + c.nodes[2].state.term = 5; + TEST_ASSERT_EQUAL_INT(1, raft_sim_check_leader_completeness(&c)); + + /* (b) no current leaders at all ⇒ trivially holds (nothing to bind). */ + c.nodes[0].state.role = RAFT_FOLLOWER; + TEST_ASSERT_EQUAL_INT(1, raft_sim_check_leader_completeness(&c)); +} + /* ---------- Group: Simulator invariant tests (tasks 9.1-9.4) ---------- * * These are observation-based invariant tests. They drive the COMPLETE @@ -7485,6 +7559,8 @@ void test_raft(void) RUN_TEST(test_sim_3_2_log_matching_shared_idx_term_requires_identical_prefix); RUN_TEST(test_sim_check_election_safety_fail_on_two_leaders); RUN_TEST(test_sim_check_election_safety_pass_on_single_leader); + RUN_TEST(test_sim_check_leader_completeness_fail_on_missing_committed); + RUN_TEST(test_sim_check_leader_completeness_pass_when_present); RUN_TEST(test_sim_9_1_replication_and_partition_catch_up); RUN_TEST(test_sim_9_2_divergent_suffix_truncation); RUN_TEST(test_sim_9_3_drop_dup_reorder_convergence);