feat(raft-sim-conformance): stale-rejoin scenario, bug-851 G5 term adoption via AE (task 5.5)

src/lib/raft/raft.h

@@ -1067,6 +1067,33 @@ int raft_sim_scenario_drop_dup_reorder(raft_sim_cluster_t *c, int n, uint64_t se
  */
 int raft_sim_scenario_figure8(raft_sim_cluster_t *c, int n, uint64_t seed);
 
+/*
+ * raft_sim_scenario_stale_rejoin: bug-851 G5 stale-rejoin scenario (raft-sim-
+ * conformance task 5.5; Req 4.5). Initializes the caller's cluster from
+ * (n, election_timeout=2000, seed), then:
+ *   1. elects a leader and replicates a committed prefix,
+ *   2. PARTITIONS one node N_stale away and, while it is isolated, advances the
+ *      connected majority's TERM via a fresh election so the surviving (connected)
+ *      leader is at a STRICTLY-HIGHER term than N_stale (which keeps its old/stale
+ *      term; it may also campaign while isolated but can never win — no quorum),
+ *   3. HEALS the partition and drives one AppendEntries/heartbeat from the higher-term
+ *      leader to N_stale, DELIVERED through the bag,
+ *   4. ASSERTS (R4.5): N_stale ADOPTS the higher term via the AE path — after delivery
+ *      N_stale's term == the leader's term (the library's raft_on_append_entries_request
+ *      UpdateTerm stepped it down to FOLLOWER at the leader's term) and N_stale is a
+ *      FOLLOWER, having NOT re-elected at a reused term. The adoption is NON-VACUOUS:
+ *      N_stale's term was confirmed STRICTLY LOWER than the leader's BEFORE the rejoin
+ *      AE. Election Safety holds THROUGHOUT (raft_sim_check_all after every action).
+ * The term adoption comes from the LIBRARY (driven via bag deliver) — the harness never
+ * sets N_stale's term directly. Returns 0 if the scenario completes with ZERO invariant
+ * violations AND the adoption property holds; < 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_stale_rejoin(raft_sim_cluster_t *c, int n, uint64_t seed);
+
 #endif /* XCE_TESTING */
 
 #endif /* RAFT_H */

src/lib/raft/raft_sim.c

@@ -2113,4 +2113,234 @@ int raft_sim_scenario_drop_dup_reorder(raft_sim_cluster_t *c, int n, uint64_t se
     return sim_scen_check(c);
 }
 
+/* ---------- stale-rejoin scenario (raft-sim-conformance task 5.5; bug-851 G5) ---------- */
+
+/*
+ * sim_scen_elect_connected: campaign one CONNECTED node at a time (raft_start_election),
+ * draining the bag after each, until a CONNECTED node holds role==RAFT_LEADER or the
+ * bounded attempts are exhausted. Differs from sim_scen_elect in two ways the stale-
+ * rejoin needs: (1) it skips partitioned candidates, and (2) it returns the index of a
+ * CONNECTED leader (a stale, partitioned-away node that still reports LEADER at an old
+ * term is NOT accepted — sim_find_leader would return that lowest-index stale leader).
+ * On an invariant violation *viol holds the negated invariant and the return is -1;
+ * otherwise *viol is 0 and the return is the connected-leader index (>= 0) or -1.
+ */
+static int sim_scen_elect_connected(raft_sim_cluster_t *c, int *viol)
+{
+    *viol = 0;
+    for (int attempt = 0; attempt < 4 * c->n; attempt++) {
+        int cand = attempt % c->n;
+        if (c->nodes[cand].partition)
+            continue; /* never campaign an isolated node */
+
+        (void)raft_start_election(&c->nodes[cand].state);
+        int chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 8);
+        if (chk < 0) {
+            *viol = chk;
+            return -1;
+        }
+
+        /* Accept only a CONNECTED leader — check candidate roles directly rather than
+         * sim_find_leader (which returns the lowest index, possibly a stale isolated
+         * leader still at an old term). */
+        for (int p = 0; p < c->n; p++) {
+            if (c->nodes[p].partition)
+                continue;
+            raft_snapshot_t snap;
+            raft_snapshot(&c->nodes[p].state, &snap);
+            if (snap.role == RAFT_LEADER)
+                return p;
+        }
+    }
+    return -1; /* no connected leader emerged */
+}
+
+int raft_sim_scenario_stale_rejoin(raft_sim_cluster_t *c, int n, uint64_t seed)
+{
+    /* A surviving connected majority while one node is isolated needs 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 a leader and replicate a committed prefix (fully connected). ---- */
+    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, 0xA00ULL + (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. Pick N_stale = a node != leader; ISOLATE it. While isolated it keeps its
+     * (now stale) term. The connected majority will advance its term below. ---- */
+    int n_stale = (leader == 0) ? 1 : 0; /* any node other than the current leader */
+    raft_sim_partition(c, n_stale, 1);
+    chk = sim_scen_check(c);
+    if (chk < 0)
+        return chk;
+
+    /* The isolated node times out and campaigns — it can bump its OWN term but can NEVER
+     * win (no quorum reachable). Drive a couple of its campaigns so the run exercises the
+     * realistic "stale node spins elections in isolation" path; its messages park in the
+     * bag (partitioned endpoint) and never grant it leadership. */
+    for (int e = 0; e < 2; e++) {
+        (void)raft_start_election(&c->nodes[n_stale].state);
+        chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 4);
+        if (chk < 0)
+            return chk;
+    }
+
+    /* ---- 3. Advance the CONNECTED majority's TERM via fresh elections until a connected
+     * leader sits at a STRICTLY-HIGHER term than N_stale. The connected leader from phase
+     * 1 may have stepped down (or N_stale's isolated campaigns left stale parked traffic);
+     * re-establish a connected leader, then keep campaigning connected nodes until the
+     * connected leader's term exceeds N_stale's term. Bounded. ---- */
+    int conn_leader = sim_scen_elect_connected(c, &viol);
+    if (viol < 0)
+        return viol;
+    if (conn_leader < 0)
+        return 0; /* connected majority could not elect — observable, not a violation */
+
+    for (int bump = 0; bump < 4 * n &&
+                       c->nodes[conn_leader].state.term <= c->nodes[n_stale].state.term;
+         bump++) {
+        /* Force another term bump on the connected side: campaign a different connected
+         * node (a higher term steps the current connected leader down, and the survivors
+         * re-elect at a strictly-higher term). */
+        conn_leader = sim_scen_elect_connected(c, &viol);
+        if (viol < 0)
+            return viol;
+        if (conn_leader < 0)
+            return 0;
+
+        if (c->nodes[conn_leader].state.term > c->nodes[n_stale].state.term)
+            break;
+
+        /* Not yet higher — bump the connected leader's term explicitly by campaigning a
+         * connected follower (its prevote/term bump raises the connected epoch). */
+        for (int p = 0; p < n; p++) {
+            if (p == conn_leader || c->nodes[p].partition)
+                continue;
+            (void)raft_start_election(&c->nodes[p].state);
+            chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 8);
+            if (chk < 0)
+                return chk;
+            break;
+        }
+        conn_leader = sim_scen_elect_connected(c, &viol);
+        if (viol < 0)
+            return viol;
+        if (conn_leader < 0)
+            return 0;
+    }
+
+    /* The connected leader MUST now outrank N_stale; otherwise the construction failed to
+     * create the term gap (observable, not a violation). */
+    if (c->nodes[conn_leader].state.term <= c->nodes[n_stale].state.term)
+        return 0;
+
+    /* Replicate a current-term entry on the connected leader so its log tip carries the
+     * higher term, then drain — this gives the rejoin AE real content to carry. */
+    chk = sim_scen_replicate_round(c, conn_leader, 0xA50ULL);
+    if (chk < 0)
+        return chk;
+    /* sim_scen_replicate_round can step the leader down via a late vote; re-establish a
+     * connected leader still outranking N_stale. */
+    {
+        raft_snapshot_t lsnap;
+        raft_snapshot(&c->nodes[conn_leader].state, &lsnap);
+        if (lsnap.role != RAFT_LEADER) {
+            conn_leader = sim_scen_elect_connected(c, &viol);
+            if (viol < 0)
+                return viol;
+            if (conn_leader < 0)
+                return 0;
+        }
+    }
+    if (c->nodes[conn_leader].state.term <= c->nodes[n_stale].state.term)
+        return 0;
+
+    /* ---- 4. NON-VACUITY: capture the leader's term and N_stale's term BEFORE the rejoin
+     * AE. The adoption assertion is real only if N_stale is STRICTLY behind here. ---- */
+    uint64_t leader_term_pre = c->nodes[conn_leader].state.term;
+    uint64_t stale_term_pre  = c->nodes[n_stale].state.term;
+    if (stale_term_pre >= leader_term_pre)
+        return 0; /* no term gap — construction failed; not a safety violation */
+
+    /* ---- 5. HEAL the partition and drive ONE AppendEntries from the higher-term leader
+     * to N_stale, then DELIVER it through the bag. The library's
+     * raft_on_append_entries_request UpdateTerm path adopts the leader's higher term and
+     * steps N_stale down to FOLLOWER — the term is NOT set by the harness. ---- */
+    raft_sim_partition(c, n_stale, 0);
+    chk = sim_scen_check(c);
+    if (chk < 0)
+        return chk;
+
+    (void)raft_send_append_entries(&c->nodes[conn_leader].state, n_stale,
+                                   c->nodes[conn_leader].state.commit_index);
+    chk = sim_scen_check(c);
+    if (chk < 0)
+        return chk;
+
+    /* Deliver the just-sent AE (and its reply) to N_stale via the bag. Each delivery is
+     * invariant-checked so an Election-Safety violation surfaces the moment it appears. */
+    chk = sim_scen_drain_bag(c, RAFT_SIM_MAX_MSGS * 8);
+    if (chk < 0)
+        return chk;
+
+    /* ---- 6. ADOPTION ASSERTIONS (R4.5), all observable via raft_snapshot:
+     *   (a) N_stale adopted the leader's higher term via the AE path,
+     *   (b) N_stale is a FOLLOWER (it did NOT re-elect at a reused term). ---- */
+    raft_snapshot_t stale_snap;
+    raft_snapshot(&c->nodes[n_stale].state, &stale_snap);
+
+    /* (a) Term adopted from the AE path: N_stale's term advanced to AT LEAST the leader's
+     * pre-rejoin term (UpdateTerm adopts the higher term). It was strictly lower before
+     * (asserted at phase 4), so this is a genuine library-driven adoption, not a no-op. */
+    if (stale_snap.term < leader_term_pre)
+        return -(int)RAFT_SIM_INV_ELECTION_SAFETY;
+
+    /* (b) N_stale stepped to FOLLOWER on adopting the higher term — it did not become a
+     * leader at a reused/duplicate term. */
+    if (stale_snap.role == RAFT_LEADER)
+        return -(int)RAFT_SIM_INV_ELECTION_SAFETY;
+
+    /* ---- 7. Let the cluster converge to a single leader and re-replicate so N_stale
+     * catches up the committed prefix. Bounded; invariants checked after every action via
+     * the helpers (Election Safety asserted THROUGHOUT). ---- */
+    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;
+        }
+        chk = sim_scen_replicate_round(c, leader, 0xA80ULL + (uint64_t)r);
+        if (chk < 0)
+            return chk;
+        leader = sim_find_leader(c);
+    }
+
+    /* ---- 8. Final invariant check (also covered after every step above). ---- */
+    return sim_scen_check(c);
+}
+
 #endif /* XCE_TESTING */