diff --git a/.kiro/specs/raft-sim-conformance/tasks.md b/.kiro/specs/raft-sim-conformance/tasks.md index fcabaf6d..00ba8a52 100644 --- a/.kiro/specs/raft-sim-conformance/tasks.md +++ b/.kiro/specs/raft-sim-conformance/tasks.md @@ -152,7 +152,7 @@ - _Boundary: raft_sim.c, test_raft.c_ - _Depends: 4.2_ -- [ ] 5.4 Figure-8 scenario +- [x] 5.4 Figure-8 scenario - Implement `raft_sim_scenario_figure8`: a previous-term entry on a quorum, a leader change; assert the entry is NOT reported committed until a current-term entry commits (Leader Completeness / State Machine Safety preserved) - Observable completion: the previous-term entry's `commit_index` does not cover it until a current-term commit - _Requirements: 4.4_ @@ -263,3 +263,13 @@ current-term entry commits) — driven by `raft_advance_commit` on the leader, which works. applied[]/SM-Safety is exercised across leader CHANGES (each node accumulates applied[] while it is leader). This SUPERSEDES the follower-commit-propagation guidance above. +- **PROCESS FIX (task 5.3 commit e445404 was BROKEN).** That commit captured the + drop_dup_reorder decl (raft.h) + test (test_raft.c) but NOT its implementation in + raft_sim.c — a stray `git checkout` (a reviewer cleaning up the `src/build` symlink) + reverted the uncommitted impl between review and commit, so the lib build was broken + (undefined reference) from e445404 onward. Detected during task 5.4. The exact + implementation was recovered (byte-identical) and re-inserted into raft_sim.c; it is + committed together with task 5.4. LESSON: after every task commit, verify `git show + --stat` includes every expected source file (raft_sim.c was silently absent from + e445404's stat). Reviewers must use targeted `git checkout ` (never `git checkout .` + / `git stash`) so uncommitted impl is never reverted. diff --git a/src/lib/raft/raft.h b/src/lib/raft/raft.h index 78c39866..7fe156e3 100644 --- a/src/lib/raft/raft.h +++ b/src/lib/raft/raft.h @@ -1037,6 +1037,36 @@ int raft_sim_scenario_restart_churn(raft_sim_cluster_t *c, int n, uint64_t seed) */ int raft_sim_scenario_drop_dup_reorder(raft_sim_cluster_t *c, int n, uint64_t seed); +/* + * raft_sim_scenario_figure8: canonical Raft Figure-8 commit-safety scenario + * (raft-sim-conformance task 5.4; Req 4.4). Initializes the caller's cluster from + * (n, election_timeout=2000, seed), then: + * 1. elects leader L1 at term T1 and physically replicates a PREVIOUS-term entry + * E1 to a QUORUM of logs (real raft_log_append + raft_send_append_entries + + * delivery) WITHOUT advancing commit over it, + * 2. forces a LEADER CHANGE to L2 at a strictly-higher term T2 (partition L1 away; + * a survivor campaigns and wins — being up-to-date, L2 necessarily HOLDS E1), + * 3. ASSERTS THE SAFETY PROPERTY: with E1 (a term-T1 entry) on a quorum under the + * term-T2 leader, raft_advance_commit must NOT cover E1 by replica count alone + * (the current-term Figure-8 rule, raft.c G4) — L2.commit_index stays below + * E1's index and NO node reports E1 committed, + * 4. L2 then appends a CURRENT-term entry E2, replicates it to a quorum, and + * raft_advance_commit now advances commit_index to cover BOTH E2 and + * (transitively) E1. + * raft_sim_check_all is run after EVERY action — so Leader Completeness and State + * Machine Safety are asserted THROUGHOUT, never only at the end (Req 4.1). The + * library enforces the commit rule; the harness only DRIVES raft_advance_commit and + * OBSERVES commit_index (it never re-implements the rule or forges commit_index). + * Returns 0 if the scenario completes with ZERO invariant violations AND the safety + * property holds (E1 uncommitted under T2 until the current-term commit, then + * committed transitively); < 0 (the negated first failing invariant, matching + * raft_sim_step) on any violation or if the property is broken, after dumping the + * replayable trace to stderr. Returns -1 on an invalid node count (n < 3). Drives + * only via published library entry points + harness primitives — no protocol + * re-implementation. + */ +int raft_sim_scenario_figure8(raft_sim_cluster_t *c, int n, uint64_t seed); + #endif /* XCE_TESTING */ #endif /* RAFT_H */ diff --git a/src/lib/raft/raft_sim.c b/src/lib/raft/raft_sim.c index bb5267f9..eb1102c7 100644 --- a/src/lib/raft/raft_sim.c +++ b/src/lib/raft/raft_sim.c @@ -1695,4 +1695,422 @@ int raft_sim_scenario_restart_churn(raft_sim_cluster_t *c, int n, uint64_t seed) return sim_scen_check(c); } +/* ---------- Figure-8 scenario (raft-sim-conformance task 5.4) ---------- */ + +/* + * sim_scen_quorum_replicate_one: on `leader`, send ONE AppendEntries to enough + * distinct peers that, together with the leader's self-match, a strict majority + * physically holds the leader's tail entry — WITHOUT advancing commit. Each AE is + * delivered (request + reply) so the entry lands in the peer's log via the real + * library handler. Invariants are checked after every action. Returns 0 on a clean + * round, < 0 on the first violation. + * + * This is the load-bearing primitive for Figure-8: it puts a previous-term entry on + * a quorum of LOGS while deliberately NOT calling raft_advance_commit, so the + * scenario can then prove the library refuses to commit it by replica count under a + * new term. + */ +static int sim_scen_quorum_replicate_one(raft_sim_cluster_t *c, int leader) +{ + /* A strict majority of n includes the leader itself, so it needs floor(n/2) + * OTHER peers to physically hold the tail. Send + deliver to the lowest-indexed + * peers != leader until that many have acked. */ + int needed = c->n / 2; /* other peers required for a majority with self */ + int acked = 0; + + for (int p = 0; p < c->n && acked < needed; p++) { + if (p == leader) + continue; + if (c->nodes[p].partition) + continue; + + (void)raft_send_append_entries(&c->nodes[leader].state, p, + c->nodes[leader].state.commit_index); + int chk = sim_scen_check(c); + if (chk < 0) + return chk; + + /* Drain just this exchange (request -> reply) so the peer's log gains the + * entry. Bounded by a small cap; a single AE produces a single reply. */ + chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 4); + if (chk < 0) + return chk; + + acked++; + } + return 0; +} + +/* + * sim_scen_catch_up_commit: drive bounded AppendEntries-to-all-connected-peers rounds + * (NO new client appends) interleaved with raft_advance_commit, until the leader's + * commit_index reaches `target` or the bound is exhausted. Each round retransmits the + * leader's tail to every connected peer; a peer behind the prev-log point rejects, the + * library backs its next_index off, and the next round backfills it — so a connected + * follower lacking the prefix is brought current over a few rounds. Invariants are + * checked after every action. Returns 0 on a clean run (committed-or-not), < 0 on the + * first violation. Used to commit the CURRENT-term entry E2 to a connected quorum that + * may need backfill of the prior-term prefix first. + */ +static int sim_scen_catch_up_commit(raft_sim_cluster_t *c, int leader, uint64_t target) +{ + for (int r = 0; r < c->n + 4 && c->nodes[leader].commit_index < target; r++) { + for (int p = 0; p < c->n; p++) { + if (p == leader || c->nodes[p].partition) + continue; + (void)raft_send_append_entries(&c->nodes[leader].state, p, + c->nodes[leader].state.commit_index); + int chk = sim_scen_check(c); + if (chk < 0) + return chk; + } + int chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 8); + if (chk < 0) + return chk; + + (void)raft_advance_commit(&c->nodes[leader].state); + chk = sim_scen_check(c); + if (chk < 0) + return chk; + } + return 0; +} + +int raft_sim_scenario_figure8(raft_sim_cluster_t *c, int n, uint64_t seed) +{ + /* Figure-8 needs a real quorum AND a leader change to a node that holds the + * prior-term entry, so n >= 3. */ + if (n < 3 || n > RAFT_SIM_MAX_NODES) + return -1; + + if (raft_sim_conformance_init(c, n, 2000, seed) != 0) + return -1; + + int chk, viol; + + /* ---- 1. Elect leader L1 at term T1; replicate a PREVIOUS-term entry E1 to a + * QUORUM of logs WITHOUT committing it. ---- */ + int l1 = sim_scen_elect(c, &viol); + if (viol < 0) + return viol; + if (l1 < 0) + return 0; /* no leader emerged — observable, not a violation; test asserts it */ + + /* Append E1 on L1 (a term-T1 entry) and physically replicate it to a quorum of + * logs via real AppendEntries — but do NOT call raft_advance_commit, so E1 stays + * UNcommitted even though a majority holds it. */ + uint64_t e1_out = 0; + (void)raft_log_append(&c->nodes[l1].state, &(uint64_t){0xF8E1ULL}, + sizeof(uint64_t), &e1_out); + chk = sim_scen_check(c); + if (chk < 0) + return chk; + uint64_t e1_index = e1_out; /* the prior-term entry's 1-based index */ + uint64_t e1_term = c->nodes[l1].state.term; + + chk = sim_scen_quorum_replicate_one(c, l1); + if (chk < 0) + return chk; + + /* E1 must NOT yet be committed on L1 (we never advanced commit over it). This is a + * harness precondition, not the safety property: if it were already committed the + * construction is wrong, so surface it as a violation-style failure. */ + if (c->nodes[l1].commit_index >= e1_index) + return -(int)RAFT_SIM_INV_STATE_MACHINE_SAFETY; + + /* ---- 2. FORCE A LEADER CHANGE to a higher term T2. ---- */ + /* Kill L1 (partition it away) so a survivor must campaign at a higher term. A + * winner must be at least as up-to-date as a majority, and since E1 is on a + * quorum the new leader L2 necessarily HOLDS E1 in its log (Leader Completeness + * is what we are stress-testing; the freshness gate makes a winner hold E1). */ + raft_sim_partition(c, l1, 1); + + /* The new leader MUST hold E1 (Leader Completeness is what we stress-test). Find a + * CONNECTED peer that physically holds E1 (sim_scen_quorum_replicate_one put it on + * the lowest-indexed peers) and campaign ONLY that node — campaigning a single + * deterministic up-to-date candidate avoids term-bumping interleaving that prevents + * any candidate from consolidating a quorum. The freshness gate guarantees a node + * lacking E1 cannot win against this up-to-date candidate. */ + int e1_holder = -1; + for (int p = 0; p < n; p++) { + if (p == l1 || c->nodes[p].partition) + continue; + if ((uint64_t)c->nodes[p].log_count >= e1_index && + c->nodes[p].log[e1_index - 1].term == e1_term) { + e1_holder = p; + break; + } + } + if (e1_holder < 0) + return 0; /* no connected E1-holder survived — observable, not a violation */ + + int l2 = -1; + for (int attempt = 0; attempt < 2 * n && l2 < 0; attempt++) { + (void)raft_start_election(&c->nodes[e1_holder].state); + chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 8); + if (chk < 0) + return chk; + /* Check the E1-holder's OWN role directly — sim_find_leader returns the lowest + * index, which is the stale partitioned-away L1 (still role==LEADER at the old + * term until it sees a higher term), not the freshly-elected connected leader. */ + raft_snapshot_t snap; + raft_snapshot(&c->nodes[e1_holder].state, &snap); + if (snap.role == RAFT_LEADER) + l2 = e1_holder; + } + if (l2 < 0) + return 0; /* no new leader emerged — observable, not a violation */ + + /* L2 must be at a strictly-higher term than E1, and must HOLD E1 (it won a quorum + * that holds E1). If L2 lacked E1 the construction failed; surface it. */ + if (c->nodes[l2].state.term <= e1_term) + return -(int)RAFT_SIM_INV_ELECTION_SAFETY; + if ((uint64_t)c->nodes[l2].log_count < e1_index || + c->nodes[l2].log[e1_index - 1].term != e1_term) + return -(int)RAFT_SIM_INV_LEADER_COMPLETENESS; + + /* ---- 3. SAFETY PROPERTY (a): under term-T2 leader L2, E1 (a term-T1 entry) sits + * on a CONNECTED quorum, yet raft_advance_commit must NOT commit it by replica + * count alone — the current-term Figure-8 rule (raft.c G4) forbids committing a + * prior-term entry without a current-term entry above it. + * + * First backfill E1 onto a connected majority under L2: drive AE rounds so the + * connected peers (which may have lacked E1 after the leader change) physically + * hold it, making the "E1 looks committable by count" danger REAL. Interleaved + * raft_advance_commit is harmless here — it is the very rule under test and must + * refuse to commit prior-term E1 (so commit_index stays below e1_index, which the + * loop's target never reaches; the bound then exits cleanly). ---- */ + chk = sim_scen_catch_up_commit(c, l2, e1_index); /* target deliberately unreachable */ + if (chk < 0) + return chk; + + /* A final explicit advance attempt on the now-quorum-replicated prior-term E1. */ + (void)raft_advance_commit(&c->nodes[l2].state); + chk = sim_scen_check(c); + if (chk < 0) + return chk; + + /* The marquee assertion: E1 is NOT covered by L2's commit_index despite quorum + * replication. A regression to term-blind commit would advance past e1_index here. */ + if (c->nodes[l2].commit_index >= e1_index) + return -(int)RAFT_SIM_INV_STATE_MACHINE_SAFETY; + + /* No node may report E1 committed either (observable State Machine Safety). */ + for (int i = 0; i < n; i++) { + if (c->nodes[i].commit_index >= e1_index) + return -(int)RAFT_SIM_INV_STATE_MACHINE_SAFETY; + } + + /* ---- 4. L2 appends a CURRENT-term (T2) entry E2 and replicates it to a quorum; + * NOW raft_advance_commit commits E2 and TRANSITIVELY commits E1 below it. ---- */ + uint64_t e2_out = 0; + (void)raft_log_append(&c->nodes[l2].state, &(uint64_t){0xF8E2ULL}, + sizeof(uint64_t), &e2_out); + chk = sim_scen_check(c); + if (chk < 0) + return chk; + uint64_t e2_index = e2_out; + + /* Replicate + commit the current-term E2 to a connected quorum (backfilling the + * prefix on any lagging connected peer as needed). */ + chk = sim_scen_catch_up_commit(c, l2, e2_index); + if (chk < 0) + return chk; + + /* SAFETY PROPERTY (b): committing the current-term entry E2 advances commit_index + * to cover BOTH E2 and (transitively) the prior-term E1 below it. */ + if (c->nodes[l2].commit_index < e1_index) + return -(int)RAFT_SIM_INV_STATE_MACHINE_SAFETY; + if (c->nodes[l2].commit_index < e2_index) + return -(int)RAFT_SIM_INV_STATE_MACHINE_SAFETY; + + /* ---- 5. HEAL the old leader L1 back so the cluster converges to a SINGLE leader + * (the stale isolated L1 still reports LEADER at the old term T1 until it observes + * T2). On heal it sees L2's higher term via the drained traffic / a replicate round + * and steps down to FOLLOWER, catching up the committed prefix. This leaves the + * post-scenario cluster with exactly one leader (L2) holding the committed E1+E2 — + * matching the other 5.x scenarios' converged end-state. ---- */ + raft_sim_partition(c, l1, 0); + + /* Re-establish a single leader and replicate/propagate commit so L1 (now reachable) + * converges. Bounded catch-up rounds; re-elect inside the loop if a late vote steps + * the leader down. Invariants checked after every action (via the helpers). */ + int leader = sim_find_leader(c); + for (int r = 0; r < n + 4; r++) { + if (leader < 0 || c->nodes[leader].partition) { + leader = sim_scen_elect(c, &viol); + if (viol < 0) + return viol; + if (leader < 0) + return 0; /* no leader emerged — observable, not a violation */ + } + chk = sim_scen_replicate_round(c, leader, 0xF800ULL + (uint64_t)r); + if (chk < 0) + return chk; + leader = sim_find_leader(c); + } + + /* ---- 6. Final invariant check (also covered after every step above). ---- */ + return sim_scen_check(c); +} + +/* ---------- drop/duplicate/reorder scenario (raft-sim-conformance task 5.3) ---------- */ + +/* + * sim_scen_logs_converged: 1 iff every node's log has caught up to the leader's tip + * (same length AND every entry's term matches over the FULL log). Pure observer over + * node->log[] / log_count — the convergence target the retransmit loop drives toward. + * (Followers never advance commit_index from AE in this library, so convergence is + * asserted over the LOG, not commit_index — see task 5.2.) + */ +static int sim_scen_logs_converged(const raft_sim_cluster_t *c, int leader) +{ + const raft_sim_node_t *L = &c->nodes[leader]; + for (int i = 0; i < c->n; i++) { + if (i == leader) + continue; + const raft_sim_node_t *f = &c->nodes[i]; + if (f->log_count != L->log_count) + return 0; + for (int e = 1; e <= L->log_count; e++) { + if (f->log[e - 1].term != L->log[e - 1].term) + return 0; + } + } + return 1; +} + +/* + * sim_scen_perturb_bag: apply one round of bag faults BEFORE delivery so the subsequent + * drain sees a dropped/duplicated/reordered message set. Mirrors raft.tla DropMessage / + * DuplicateMessage as pure bag mutations (no node touched). Uses the cluster PRNG so the + * perturbation is seed-replayable: a PRNG-chosen fraction of in-flight members are + * DUPLICATEd (re-enqueued — multiplicity += 1) and a PRNG-chosen fraction are DROPped. + * Bounded by the live bag size; never drains the bag empty (drops at most ~half) so + * retransmit + drain can still converge. Returns 0 (it performs only bag ops, which the + * scenario invariant-checks after). + */ +static void sim_scen_perturb_bag(raft_sim_cluster_t *c) +{ + /* DUPLICATE pass: re-enqueue a PRNG-chosen subset (delivered more than once). Snapshot + * the count first so freshly-pushed copies are not themselves re-duplicated. */ + int n_live = c->bag_count; + for (int i = 0; i < n_live; i++) { + if ((raft_sim_prng_next(c) & 1ULL) == 0) + (void)raft_sim_bag_duplicate(c, i); /* fail-loud on overflow; ignored here */ + } + + /* DROP pass: discard at most half of the CURRENT members so the bag never empties. + * Pick by PRNG index (swap-with-last removal keeps the array dense). */ + int max_drop = c->bag_count / 2; + for (int d = 0; d < max_drop && c->bag_count > 1; d++) { + if ((raft_sim_prng_next(c) & 1ULL) == 0) { + int idx = raft_sim_bag_pick(c); /* PRNG-chosen live index */ + if (idx >= 0) + (void)raft_sim_bag_drop(c, idx); + } + } +} + +int raft_sim_scenario_drop_dup_reorder(raft_sim_cluster_t *c, int n, uint64_t seed) +{ + if (n < 3 || n > RAFT_SIM_MAX_NODES) + return -1; + + if (raft_sim_conformance_init(c, n, 2000, seed) != 0) + return -1; + + int chk, viol; + + /* ---- 1. Elect a leader and replicate a committed prefix (clean rounds). ---- */ + int leader = sim_scen_elect(c, &viol); + if (viol < 0) + return viol; + if (leader < 0) + return 0; /* no leader emerged — observable, not a violation; test asserts it */ + + for (int r = 0; r < 3; r++) { + chk = sim_scen_replicate_round(c, leader, 0x700ULL + (uint64_t)r); + if (chk < 0) + return chk; + leader = sim_find_leader(c); + if (leader < 0) { + leader = sim_scen_elect(c, &viol); + if (viol < 0) + return viol; + if (leader < 0) + return 0; + } + } + + /* ---- 2. PERTURBED rounds: append + send AE to every peer, then DROP/DUPLICATE/ + * REORDER the in-flight bag BEFORE delivering it in PRNG order. Invariants are + * checked after the append, after each AE send, after the perturbation, and after + * every delivery (sim_scen_drain_bag delivers PRNG-picked = reordered, checking each + * step). A duplicated AE that lands twice hits the library's already-have branch (a + * no-op); a dropped AE leaves a follower behind, recovered by the retransmit phase. */ + for (int r = 0; r < 4; r++) { + uint64_t value = 0x800ULL + (uint64_t)r; + uint64_t out_index = 0; + (void)raft_log_append(&c->nodes[leader].state, &value, sizeof(value), &out_index); + chk = sim_scen_check(c); + if (chk < 0) + return chk; + + for (int p = 0; p < n; p++) { + if (p == leader) + continue; + (void)raft_send_append_entries(&c->nodes[leader].state, p, + c->nodes[leader].state.commit_index); + chk = sim_scen_check(c); + if (chk < 0) + return chk; + } + + /* Fault injection on the in-flight bag (drop + duplicate). */ + sim_scen_perturb_bag(c); + chk = sim_scen_check(c); + if (chk < 0) + return chk; + + /* Reordered delivery: sim_scen_drain_bag picks PRNG order, checking each step. */ + chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 8); + if (chk < 0) + return chk; + + /* The duplicate/reorder churn may have stepped the leader down via a stray + * higher-term message; re-establish one before the next round. */ + leader = sim_find_leader(c); + if (leader < 0) { + leader = sim_scen_elect(c, &viol); + if (viol < 0) + return viol; + if (leader < 0) + return 0; + } + } + + /* ---- 3. RETRANSMIT to convergence: dropped entries left followers behind, so drive + * clean replicate rounds (the leader re-sends from its per-peer next_index) until + * every log converges to the leader's tip. Bounded — a leader's log holds at most + * RAFT_SIM_MAX_LOG entries, so n + log_count + 4 rounds is ample. ---- */ + int max_rounds = n + c->nodes[leader].log_count + 4; + for (int r = 0; r < max_rounds && !sim_scen_logs_converged(c, leader); r++) { + chk = sim_scen_replicate_round(c, leader, 0x900ULL + (uint64_t)r); + if (chk < 0) + return chk; + leader = sim_find_leader(c); + if (leader < 0) { + leader = sim_scen_elect(c, &viol); + if (viol < 0) + return viol; + if (leader < 0) + return 0; + } + } + + /* ---- 4. Final convergence check (also covered after every step above). ---- */ + return sim_scen_check(c); +} + #endif /* XCE_TESTING */ diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index 7d4b6f77..560d68d1 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -8407,6 +8407,67 @@ static void test_sim_5_3_drop_dup_reorder(void) TEST_ASSERT_EQUAL_INT(RAFT_SIM_INV_NONE, raft_sim_check_all(&c)); } } + +/* + * test_sim_5_4_figure8 (raft-sim-conformance task 5.4; Req 4.4) + * + * Canonical Raft Figure-8 commit-safety scenario driven through the conformance + * harness. raft_sim_scenario_figure8 constructs the marquee case: a PREVIOUS-term + * entry E1 replicated to a QUORUM of logs (uncommitted), then a LEADER CHANGE to a + * higher term T2 (the new leader necessarily holds E1). Under the new leader, + * raft_advance_commit must NOT commit E1 by replica count alone (the current-term + * Figure-8 rule, raft.c G4); only after a CURRENT-term entry E2 commits does E1 + * become committed transitively. All four invariants are asserted THROUGHOUT. + * + * The scenario returns 0 ONLY when both commit-index assertions hold (E1 not covered + * pre-current-term-commit; covered after) AND no invariant ever fires. A return < 0 + * is a REAL safety violation the scenario surfaced (the step already dumped the + * replayable trace to stderr) — NOT something to mask. Several (n, seed) pairs are + * exercised so the property is not a single-seed accident. + */ +static void test_sim_5_4_figure8(void) +{ + /* (n, seed) pairs across 3- and 5-node clusters. The scenario inits the caller's + * cluster internally from (n, seed). */ + struct { int n; uint64_t seed; } cases[] = { + { 3, 8ULL }, { 3, 0x4A33ULL }, { 3, 6ULL }, + { 5, 19ULL }, { 5, 0xBEEFULL }, + }; + + for (size_t k = 0; k < sizeof(cases) / sizeof(cases[0]); k++) { + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + int rc = raft_sim_scenario_figure8(&c, cases[k].n, cases[k].seed); + + /* Zero invariant violations AND the Figure-8 safety property held throughout + * (E1 uncommitted under the new term until a current-term entry committed, + * then committed transitively). */ + TEST_ASSERT_TRUE_MESSAGE(rc == 0, + "figure-8 scenario surfaced an invariant/safety violation on the correct library"); + + /* Post-scenario: the cluster still satisfies all four invariants. */ + TEST_ASSERT_EQUAL_INT(RAFT_SIM_INV_NONE, raft_sim_check_all(&c)); + + /* Observable, non-vacuous outcome: a leader exists, it committed a non-trivial + * prefix (the current-term commit released E1 transitively), and that committed + * prefix is internally consistent. A scenario that never committed anything + * would make the safety property vacuous, so assert real commit progress. */ + int leader_idx = -1; + for (int i = 0; i < c.n; i++) { + raft_snapshot_t snap; + raft_snapshot(&c.nodes[i].state, &snap); + if (snap.role == RAFT_LEADER) { + leader_idx = i; + break; + } + } + TEST_ASSERT_TRUE_MESSAGE(leader_idx >= 0, + "figure-8 scenario ended without a leader"); + TEST_ASSERT_TRUE_MESSAGE(c.nodes[leader_idx].commit_index >= 2, + "figure-8 leader did not commit the prior-term + current-term entries"); + } +} #endif /* XCE_TESTING */ /* ---------- test_raft entry point ---------- */ @@ -8620,6 +8681,7 @@ void test_raft(void) RUN_TEST(test_sim_5_1_partition_heal); RUN_TEST(test_sim_5_2_restart_churn); RUN_TEST(test_sim_5_3_drop_dup_reorder); + RUN_TEST(test_sim_5_4_figure8); /* Group A: basic election correctness (task 5.1) */ RUN_TEST(test_proto_A1_single_node_self_elects);