lei.chen/myxce
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(ha-prevote): Raft safety-invariant property tests + RN-1 consistency argument (task 6.1)

Browse source 
Four property-style raft tests proving the PreVote API preserves the safety
invariants: term/voted_for/role never change and on_persist never fires across
mixed begin/request/reply sequences (WON and LOST); a WON round creates no leader
(stays FOLLOWER); and the real-vote higher-term-adopt + step-down + quorum-elect
path is unchanged (bug-339/340 intact). Records the TLA+/checklist consistency
argument (RN-1) in test_raft.c and research.md, citing the tests as evidence.
Raft suite 123/0/0; zero production change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Rongsong Shen 2026-06-16 07:18:06 +00:00
parent 22fa753fa6
commit e6b234a6a4
3 changed files with 557 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

253
.kiro/specs/ha-prevote/research.md Normal file
View file

@ -0,0 +1,253 @@
# Gap Analysis: ha-prevote
_Generated by `/kiro-validate-gap`. Informational — presents options and research items, not final design decisions._
## Analysis Summary
- **The fix must be sender-side.** The disruptive step-down occurs in `raft_on_vote_request` Step 2 (raft.c:125-134) — term adoption + leader demotion — which runs **before** the `on_vote_eligible` gate (Step 5). No receiver gate today can save a healthy leader from a *fresh, higher-term* `RequestVote`, because the term is already adopted before any stickiness check. PreVote prevents the term inflation at the source.
- **Most receiver-side gating already exists.** `raft_cb_vote_eligible` (ha.c:217-245) already implements PRIMARY-deny, fresh-heartbeat-on-standby deny (leader stickiness), and catch-up deny; the dispatcher already enforces the freshness floor via `ha_vote_self_freshness`. PreVote evaluation can largely **reuse these gates** but must run with **zero state mutation**.
- **The new machinery is the candidate-side PreVote round** plus a wire message and a way to tally PreVote replies without touching `term`/`voted_for`.
- **Recommended shape: Hybrid (Option C).** New PreVote state in the raft library + new wire message/opcode, reusing the existing `ha_elect_ctx_t` collection, dispatcher freshness gate, and `raft_cb_vote_eligible` semantics.
- **Effort: M (3–7 days). Risk: Medium** — touches the safety-critical election path and the TLA+-referenced invariants, but integrates with well-factored, test-covered seams.
---
## 1. Current State Investigation
### Election path (raft library — `src/lib/raft/raft.c`, `raft.h`)
- **State** (`raft_state_t`, raft.h:23-38): `term`, `role` (`RAFT_FOLLOWER|CANDIDATE|LEADER`), `voted_for`, `voted_for_term`, `votes_granted`, `replies_received`, `election_decided`, `election_timeout_ms`, `my_priority`. **No pre-vote fields.**
- **Callbacks** (`raft_callbacks_t`, raft.h:66-96): `on_send_vote_request(ctx, peer_idx, term)`, `on_vote_eligible(ctx, from_idx, term)`, `on_become_leader`, `on_become_follower`, `on_persist(ctx, term, voted_for)`, `on_schedule_timeout`, `on_cancel_timeout`, `on_start_election_after_delay`, `on_trace`.
- **`raft_start_election`** (raft.c:61-108): increments `term`, sets self-vote, **persists**, then sends `on_send_vote_request` to each peer, schedules timeout. Single-node short-circuit promotes immediately.
- **`raft_on_vote_request`** (raft.c:110-191): 6-step flow — (1) stale-term deny; (2) **term upgrade → adopt term, clear vote, step down, fire `on_become_follower` if was LEADER** (the disruptive path); (3) LEADER role deny; (4) one-vote-per-term; (5) `on_vote_eligible` policy gate; (6) persist-then-grant.
- **`raft_on_vote_reply`** (raft.c:193-252): term-upgrade demotion; quorum = `(n_peers/2)+1`; all-replied-no-quorum fallback.
- **Triggers**: `raft_on_leader_lost` → `on_start_election_after_delay` (priority jitter); `raft_check_and_start_election` (raft.c:282-294) skips if already voted for another, else `raft_start_election`.
### Controller adapter (`src/controller/cluster.c`, `ha.c`, `ha.h`)
- **Dispatch** (`cluster.c` `OPCode_requestVote`, lines 359-408): parses `request_vote_req_t`, computes freshness floor via `ha_vote_self_freshness` (max of local and learned-committed tag/LSN), applies `freshness_ok`, maps candidate name → index, then calls `raft_on_vote_request`.
- **Candidate send** (`ha.c` `on_vote_connected`, lines 2579-2610): builds `request_vote_req_t` (term, candidate_id, config_tag, last_log_lsn), sends via `xce_request` (or `xce_vote_request_hook` under `XCE_TESTING`).
- **Collection** (`ha_elect_ctx_t`, ha.h:75-116): flexible-array `votes[]`, `votes_granted` (init 1 = self), `n_replied`, `max_resp_tag/lsn` (yield gate), `done` semaphore. `handle_request_vote_reply` (ha.c:2473-2528) tallies and calls `ha_elect_evaluate_and_signal`. Quorum = `(n_peers+1+1)/2`.
- **Voter gate** (`raft_cb_vote_eligible`, ha.c:217-245): PRIMARY → deny; STANDBY + `ha_heartbeat_is_fresh` → deny; in catch-up → deny; else eligible (freshness already enforced by dispatcher).
- **Leader stickiness primitive** (`ha_heartbeat_is_fresh`, ha.c:2013-2022): `(now - last_activity) < heartbeat_timeout_ms`. `ha_on_heartbeat_received` updates `last_activity`.
- **Election initiation** (`ha_start_election_async`, ha.c:3341-3410): allocates `ha_elect_ctx_t`, sets self-vote, stores `ha->elect_ctx`, delegates to `raft_start_election`.
- **Election triggers**: `ha_on_primary_ctrl_fd_rdhup` (ha.c:3486) on connection loss; `liveness_poll_fn` (ha.c:3684-3722) on heartbeat timeout.
### Wire schema (`src/schema/controller.capnp`)
```capnp
struct RequestVoteRequest { # lines 796-801
term @0; candidateId @1; configTag @2; lastLogLsn @3;
}
struct RequestVoteReply { # lines 803-808
term @0; voteGranted @1; peerConfigTag @2; peerLastLogLsn @3;
}
```
`OPCode` is an enum (lines 10-49); `requestVote @32` (line 43). **No PreVote opcode.**
### Test seams
- `xce_vote_request_hook` (ha.c:2560) intercepts the candidate send without live iomgr/SSL.
- `src/lib/testsuite/test_raft.c` — raft library unit tests with mock callbacks (TLA+ invariants).
- `src/controller/testsuite/`: `test_ha_election.c`, `test_ha_vote_gate.c`, `test_ha_start_election_async.c`, `test_ha_vote_send.c`, `test_ha_liveness.c`, `test_ha_role_lifecycle.c`, `test_ha_failover.c`.
### Relevant constants (`ha.h:121-129`)
`HEARTBEAT_INTERVAL_MS=3000`, `HEARTBEAT_TIMEOUT_MS=10000`, `ELECTION_TIMEOUT_MS=5000`, `ELECTION_JITTER_MAX_MS=200`, `ELECTION_PRIORITY_STEP_MS=500`.
---
## 2. Requirement-to-Asset Map
| Req | Capability needed | Existing asset | Gap |
|-----|-------------------|----------------|-----|
| **1** PreVote precedes term increment | A pre-election round that runs before `raft_start_election`; no persist/term change | `raft_start_election` (raft.c:61), `ha_start_election_async` (ha.c:3341) as the call site to gate | **Missing**: PreVote state + entry point; must interpose between trigger and `raft_start_election` |
| **1.2/1.3** No persistent mutation during PreVote | — | `on_persist` is only called by `raft_start_election`/`raft_on_vote_request` | **Constraint**: PreVote path must never call `on_persist` or mutate `term`/`voted_for` |
| **2** Voter eligibility reuses real-vote gate | Freshness + log-completeness check | Dispatcher freshness (`ha_vote_self_freshness`, cluster.c:389) + `raft_cb_vote_eligible` (ha.c:217) | **Constraint/Reuse**: run the same gate; must NOT record a vote |
| **2.3/2.4** No vote recorded; can still grant real vote later | — | one-vote-per-term lives in `raft_on_vote_request` Step 4 | **Constraint**: PreVote evaluation must bypass Steps 2/4/6 side effects |
| **3** Leader stickiness | Deny PreVote while leader believed alive; PRIMARY denies | `ha_heartbeat_is_fresh` (ha.c:2013), PRIMARY-deny in `raft_cb_vote_eligible` | **Reuse**: already present; just invoke from the PreVote receiver path |
| **3.1** Stickiness window semantics | "would not itself start an election" | Today: `heartbeat_timeout_ms` (10s) for freshness vs. `election_timeout_ms` (5s) probe | **Unknown (Research)**: which window defines stickiness — see RN-2 |
| **4** Frozen-then-resumed is non-disruptive | Candidate gets no PreVote majority → no term bump → re-attach | `ha_on_heartbeat_received` re-attach path | **Missing**: end-to-end behavior emerges from Req 1+3; needs integration test |
| **5** Legitimate changes still proceed | True death / partition heal still elect | `raft_on_vote_reply` term-upgrade demotion; existing failover (bug-339), rejoin (bug-340) | **Constraint**: do not regress; real-vote path unchanged after PreVote success |
| **6** Safety invariants | Election Safety, term monotonicity, Leader Completeness | `raft/raft.tla`, `test_raft.c`, controller verification checklist | **Constraint**: PreVote must be modeled/argued against TLA+; add invariant tests |
| **7.1** Transport compatibility | PreVote over existing election transport | capnp `OPCode`, `xce_request`, `peer_ctrl_msg_handler` | **Missing**: new opcode/flag + reply + dispatch case |
| **7.2/7.3** Observability | Log PreVote denials / abandoned campaigns | `on_trace` callback, `tlog` | **Missing**: trace/log points on PreVote deny + campaign abandonment |
Gap tags: **Missing** = no asset; **Constraint** = existing behavior bounds the design; **Reuse** = asset directly applicable; **Unknown** = research item.
---
## 3. Implementation Approach Options
### Option A — Extend the existing RequestVote path with an `isPreVote` flag
Add `isPreVote @4 :Bool = false` to `RequestVoteRequest` (and a matching flag/struct for the reply). Reuse the same dispatch case, same `on_vote_connected` send, and branch inside `raft_on_vote_request` / `raft_cb_vote_eligible` on the flag to skip all state mutation.
- ✅ Smallest wire change; backward-compatible capnp default; one RPC path.
- ✅ Reuses send/collect/gate machinery almost verbatim.
- ❌ Risks branching the safety-critical `raft_on_vote_request` with "if pre_vote skip steps 2/4/6" — easy to get a side-effect leak wrong.
- ❌ Overloads one function with two semantics (real vs. hypothetical).
### Option B — New PreVote opcode + dedicated PreVote functions
Add `preVoteRequest`/`preVoteReply` opcodes and `PreVoteRequest`/`PreVoteReply` structs; add `raft_start_pre_vote`, `raft_on_pre_vote_request`, `raft_on_pre_vote_reply`, and `raft_cb_pre_vote_eligible`; a parallel (or shared) `ha_elect_ctx_t` pre-vote tally.
- ✅ Clean separation; the pure (no-side-effect) PreVote functions are trivially auditable against the safety invariants.
- ✅ Real-vote path stays byte-for-byte unchanged (zero regression risk to bug-339/340).
- ❌ More new files/symbols and a second dispatch/collection path.
- ❌ Some duplication of freshness/eligibility logic unless carefully shared.
### Option C — Hybrid (recommended)
New PreVote **wire message + raft state-machine functions** (Option B's clarity for the safety-critical core), but **reuse** the controller-side assets: the dispatcher freshness computation, `raft_cb_vote_eligible` semantics (called read-only), the `ha_elect_ctx_t` collection (add a `pre_votes_granted` counter or a `phase` field rather than a whole second struct), and `xce_vote_request_hook` for tests.
- ✅ Keeps the pure PreVote decision isolated and auditable while avoiding duplicate collection/gate code.
- ✅ Real-vote path untouched; PreVote success simply calls the existing `raft_start_election`.
- ✅ Maps onto existing test seams (extend `test_ha_vote_gate.c`, add PreVote cases to `test_raft.c`).
- ❌ Requires a deliberate decision on shared-vs-separate eligibility helper to avoid drift.
---
## 4. Effort & Risk
| Dimension | Rating | Justification |
|-----------|--------|---------------|
| **Effort** | **M (3–7 days)** | New wire message + raft PreVote functions + candidate round + tests; but heavy reuse of existing gates, collection, and transport. |
| **Risk** | **Medium** | Touches the election safety core and TLA+-referenced invariants; mitigated by well-factored callback seams, existing gate logic to reuse, and strong test coverage. Highest-risk subtlety: ensuring the PreVote path has **zero** persistent side effects. |
---
## 5. Recommendations for Design Phase
**Preferred approach:** Option C (Hybrid).
**Key decisions to finalize in design:**
1. **Wire representation** — separate `preVoteRequest`/`preVoteReply` opcodes (recommended for auditability) vs. `isPreVote` flag on the existing struct. Either is capnp-compatible; the opcode keeps the real-vote path provably untouched.
2. **Eligibility sharing** — factor the freshness + `raft_cb_vote_eligible` checks into a read-only helper callable from both the real-vote and PreVote receiver paths, so the two cannot drift.
3. **Collection reuse** — extend `ha_elect_ctx_t` with a PreVote phase/counter rather than a second struct.
4. **PreVote success → real election** — on PreVote majority, call the **unchanged** `raft_start_election`; confirm the candidate re-checks leader-stickiness was still absent at the moment of starting the real round.
5. **Defense-in-depth question** — decide whether to *also* add leader-stickiness gating to the real `raft_on_vote_request` term-upgrade path (Raft "reject RequestVote within min election timeout"), since PreVote alone leaves Step 2 able to step down a leader if a stray higher-term real RequestVote ever arrives.
**Research Needed (carry to design):**
- **RN-1**: Model/argue the PreVote phase against `raft/raft.tla` and the controller verification checklist; confirm Election Safety + term monotonicity hold with the new path. (Req 6)
- **RN-2**: ✅ **RESOLVED — reuse `heartbeat_timeout_ms` via `ha_heartbeat_is_fresh()`.** See "Resolved Decisions → RN-2" below for the full comparison. (Req 3.1)
- **RN-3**: Confirm whether the PRIMARY should deny PreVotes via the existing `raft_cb_vote_eligible` PRIMARY-deny (Req 3.3) and that this composes with CheckQuorum-style behavior already present.
- **RN-4**: Decide PreVote round timeout/abandonment behavior and its interaction with the existing election jitter/priority and `election_timeout_ms` bounds (Req 5.4) — ensure no added unbounded delay.
**Explicitly out of scope:** Backward/rolling-upgrade compatibility with peers that predate PreVote. The product is **pre-release**, so all controllers in a cluster deploy from the same build — there is no mixed-version (old-binary ↔ new-binary) cluster to support. The wire change (new opcode or struct field) may be made without a negotiation/fallback path. Req 7.1's "without disrupting real RequestVote/RequestVoteReply exchanges" refers to PreVote coexisting with the *concurrent same-version* real-vote path, not to inter-version compatibility.
---
## 6. Resolved Decisions
### RN-2 — Leader-stickiness window → reuse `heartbeat_timeout_ms` (Opt 1)
**Decision:** The voter's leader-stickiness predicate is the existing `ha_heartbeat_is_fresh()` (`now − last_activity < heartbeat_timeout_ms`, currently 10s), gated on `role == CTRL_STANDBY`. PreVote introduces **no new timing concept**.
**The governing invariant.** Stickiness is a single voter-side predicate: *"do I still believe a leader is alive?"* It must be **pinned to the failure-detection window** — the period during which the voter would not itself start an election. If the two diverge:
- **stickiness < failure-detection** → a gap opens where the voter grants a PreVote while still believing its leader is alive and not yet failing over → **reopens the disruption hole**.
- **stickiness > failure-detection** → a voter that has already decided the leader is dead (and is campaigning) still denies others' PreVotes → mutual denial → **PreVote majorities can't form → liveness stall**.
So the window must equal whichever constant is XCE's *failure detector*.
**Naming trap.** Textbook Raft overloads one "election timeout" for two roles; XCE separates them, so the dissertation's "reject votes within the minimum election timeout" maps to `HEARTBEAT_TIMEOUT_MS`, **not** `ELECTION_TIMEOUT_MS`:
| Raft concept | XCE constant | Value | Role in XCE |
|---|---|---|---|
| election timeout *as leader-failure detector* | `HEARTBEAT_TIMEOUT_MS` | 10000 | Follower decides primary is dead → triggers failover (`liveness_poll_fn` / RDHUP) |
| election timeout *as vote-collection deadline* | `ELECTION_TIMEOUT_MS` | 5000 | Candidate waits this long for vote replies before giving up |
| heartbeat interval | `HEARTBEAT_INTERVAL_MS` | 3000 | Primary re-sends heartbeat every 3s |
**Option comparison.**
| | Opt 1: `heartbeat_timeout_ms` (10s) | Opt 2: `election_timeout_ms` (5s) | Opt 3: new `prevote_stickiness_ms` | Opt 4: `heartbeat_interval_ms` (3s) |
|---|---|---|---|---|
| Matches XCE failure-detector | ✅ exactly | ❌ wrong constant (vote-collection deadline) | ⚠️ only if set == 10s | ❌ far shorter |
| Consistent w/ existing real-vote gate (`raft_cb_vote_eligible`) | ✅ same predicate reused | ❌ real-vote 10s vs PreVote 5s drift | ⚠️ drift unless tuned | ❌ drift |
| Disruption gap (grant while leader alive) | ✅ none | ❌ [5s,10s] gap on flaky/asymmetric link | ⚠️ gap if < 10s | ❌ [3s,10s] gap |
| Tolerance to transient heartbeat loss | ✅ ~3 missed heartbeats | ⚠️ ~1 missed heartbeat | ⚠️ depends | ❌ 0 missed |
| Liveness-stall risk | ✅ none | ✅ none | ⚠️ stall if > 10s | ✅ none |
| Speeds up legitimate failover | n/a (matches today) | ❌ no real benefit¹ | ⚠️ only by also lowering failover timeout | ❌ no |
| New config surface | none | none | +1 tunable | none |
¹ Under symmetric silent death nobody campaigns until the 10s failure-detection fires, so a shorter stickiness window has no candidate to grant to in [5s,10s] — zero speedup. A real crash closes sockets → RDHUP → standbys leave `CTRL_STANDBY` and campaign immediately, independent of the window. The shorter window's only observable effect is the disruption gap on a flaky link (a healthy primary missing ~2 of 3 heartbeats to one voter would get a PreVote granted against it at ~6s).
**Why Opt 1.** It is the single value where the stickiness window, the failure-detection trigger (`liveness_poll_fn`), and the existing real-vote stickiness gate (`raft_cb_vote_eligible`) all key off **one predicate** (`ha_heartbeat_is_fresh`). Gating on `role == CTRL_STANDBY` also handles connection loss for free: RDHUP moves the node out of `CTRL_STANDBY`, so a genuinely disconnected voter stops being sticky immediately instead of waiting the full 10s. This is exactly what Req 3.1's observable phrasing ("received leader traffic recently enough that it would not itself start an election") already describes. If failover latency is later reduced by lowering `HEARTBEAT_TIMEOUT_MS`, stickiness follows automatically — which is itself the argument against Opt 3's separable constant.
**Requirement impact:** Req 3.1 can be tightened in design (Boundary Commitment) to name `ha_heartbeat_is_fresh` / `heartbeat_timeout_ms` as the binding, while keeping the requirement text observable.
---
## 7. Design Synthesis Outcomes (design phase)
Applied the generalization / build-vs-adopt / simplification lenses before writing `design.md`.
### Generalization — share interfaces, not implementations
PreVote and real-vote are two variations of "solicit a vote decision." Two seams are shared rather than duplicated:
- **Voter eligibility** — `raft_cb_vote_eligible` already encodes exactly the PreVote gates (PRIMARY-deny + fresh-heartbeat stickiness + catch-up-deny). The PreVote receiver reuses it verbatim via the existing `on_vote_eligible` callback; the only PreVote-specific rule is "decide without adopting the term."
- **Candidate tally** — `ha_elect_ctx_t` is reused with a `phase` discriminator (`HA_ELECT_PREVOTE` / `HA_ELECT_REAL`) instead of a second collection struct. Same quorum formula `(n_peers + 2) / 2`, same `votes[]` idempotency.
The raft state-machine *functions* stay distinct (`raft_on_pre_vote_*` vs `raft_on_vote_*`) so the pure, no-side-effect PreVote path is independently auditable against the TLA+ model.
### Build vs. Adopt — adopt
- **Algorithm**: Raft dissertation §9.6 PreVote (standard, well-specified). Not invented.
- **Infrastructure**: capnp election transport, iomgr/delaymgr, `ha_elect_ctx_t`, `ha_heartbeat_is_fresh`, `ha_vote_self_freshness`, `xce_vote_request_hook`. No new libraries.
### Simplification decisions
- **Wire**: new `preVoteRequest`/`preVoteReply` **opcodes that reuse the existing `RequestVoteRequest`/`RequestVoteReply` structs and union arms** — no new capnp structs, and the real-vote handler stays byte-for-byte unchanged (zero regression risk to bug-339/340). Chosen over an `isPreVote` flag on the existing struct (which would branch the safety-critical real-vote handler).
- **Defer defense-in-depth** (the RN-4-adjacent / open "real-vote stickiness guard"): PreVote guarantees a candidate only sends a real RequestVote *after* a majority's stickiness has lapsed, so in a same-version cluster no stickiness-violating real RequestVote can arise. Adding the guard would touch the real-vote term-adoption path for no in-scope benefit. **Deferred**, documented in `design.md` → Architecture → Deferred decisions. (Resolves the open defense-in-depth question; RN-4 reduces to "bound the PreVote round with `election_timeout_ms` and re-arm liveness on loss," which the design specifies.)
- **No new role state**: the candidate stays `CTRL_STANDBY` during the PreVote round (tracked by `ctx.phase`), so a lost PreVote needs no rollback. The destructive `truncate-WAL + CTRL_ELECTING` step is **moved** from the failover trigger to PreVote success — the key change that makes a transient freeze a true no-op (Req 4).
### Remaining open research item
- **RN-1**: TLA+ / verification-checklist argument that Election Safety + term monotonicity hold with the PreVote path (the real-vote path is unchanged, so this is largely an argument that the pure PreVote functions mutate nothing). Carried into implementation as `test_raft.c` invariant assertions. RN-3 (PRIMARY-deny composition) is resolved by reusing `raft_cb_vote_eligible`.
---
## RN-1 resolved (task 6.1)
**Decision/outcome:** The PreVote phase is consistent with the repository's
`raft/raft.tla` reference and the controller verification checklist —
Election Safety (≤1 leader per term), Leader Completeness, term monotonicity,
and a monotonic commit index all continue to hold with PreVote enabled.
**Argument (purity ⇒ no new transitions).**
1. **The PreVote functions are pure w.r.t. persistent Raft state.** Across an
arbitrary sequence of `raft_begin_pre_vote` / `raft_on_pre_vote_request` /
`raft_on_pre_vote_reply` calls — mixed grant+deny, duplicate replies,
out-of-range peers, and both WON and LOST terminal outcomes — none of them
ever writes `s->term`, `s->voted_for`, `s->voted_for_term`, or `s->role`,
and none invokes `on_persist`. Mechanical evidence:
`test_invariant_prevote_sequence_pure_no_persist` and
`test_invariant_prevote_lost_sequence_pure_no_persist` in
`src/lib/testsuite/test_raft.c`.
2. **Term monotonicity is preserved.** Because the PreVote path writes no term,
the only writers of `s->term` remain the UNCHANGED `raft_start_election`
(the real, gated term bump) and `raft_on_vote_request` Step 2 (adopt a
strictly higher term). PreVote can only *gate* whether a real election
later runs; it never advances a term itself, and it never decreases one.
3. **Election Safety is preserved.** Because the PreVote path creates no leader
(no `on_become_leader`, no `role := RAFT_LEADER`), it adds no new way to
satisfy the antecedent of Election Safety. A PreVote round reaching
`RAFT_PRE_VOTE_WON` returns a *status* only; the node stays `RAFT_FOLLOWER`
until the separate, unchanged `raft_start_election` / `raft_on_vote_reply`
path runs. Evidence: `test_invariant_prevote_won_grants_no_leadership`.
4. **The bug-339/bug-340 failover path is unchanged.** The legitimate
higher-term-adopt + leader-step-down behavior lives entirely in
`raft_on_vote_request` / `raft_on_vote_reply`, which this feature does not
touch. PreVote sits strictly before that path and (by 1) leaves its inputs
untouched. Evidence: `test_invariant_real_vote_higher_term_adopt_unchanged`
demonstrates the real-vote path still adopts a higher term, fires
`on_become_follower` to step a leader down, and elects at quorum via
`on_become_leader` — even after a full PreVote round has run on the node.
**Conclusion.** PreVote introduces no transition that writes a term or creates
a leader; every term-writing / leadership-creating transition in the model is
byte-for-byte the pre-PreVote transition. The set of reachable
`(term, leader)` configurations is therefore unchanged, so the `raft/raft.tla`
invariants (Election Safety, Leader Completeness, term monotonicity, monotonic
commit index) and the controller verification checklist continue to hold. The
four `test_invariant_*` tests are the mechanical evidence for premises (1)–(4),
and the existing failover/rejoin regression suites remain green with PreVote
enabled (controller suite 563 pass / 0 fail after task 4.2). Requirements
covered: 5.2, 5.3, 6.1, 6.2, 6.3, 6.4.

2
.kiro/specs/ha-prevote/tasks.md
View file

@ -85,7 +85,7 @@
- _Depends: 4.1, 4.2, 5.1_
- [ ] 6. Validation: safety invariants and regression guard
- [ ] 6.1 Assert Raft safety invariants hold with PreVote
- [x] 6.1 Assert Raft safety invariants hold with PreVote
- Add raft-library invariant assertions that the PreVote functions mutate no persistent state (Election Safety and term monotonicity preserved), and record the TLA+/verification-checklist consistency argument (the real-vote path is unchanged, so the higher-term-adopt failover and the bug-339/bug-340 fixes are preserved).
- Observable: invariant tests pass and the existing failover/rejoin regression tests remain green with PreVote enabled.
- _Requirements: 5.2, 5.3, 6.1, 6.2, 6.3, 6.4_