Expand Raft driver scenario coverage

[Copilot]

The Raft scenario suite left realistic election, retirement, delayed-message, batching, and driver-diagnostic paths uncovered. This change adds eight deterministic scenarios.

Scenarios

Scenario	Behavior covered
leadership_race	CheckQuorum step-down, leaderless operations, and replacement election
delayed_vote_requests	Competing elections and delayed same-term vote traffic
retirement_rollback	Rollback of an uncommitted node retirement
retired_node_delayed_responses	Vote and append responses arriving after peer removal
large_entry_batching	AppendEntries batch recalculation and proactive sends
message_type_summaries	Compact diagnostics for replication, election, and nomination messages
replicate_on_latest_leader	replicate,latest selection of the highest-term leader
swap_single_node	Atomic replacement of one backup through the singular driver command

Coverage impact

• Whole binary lines: 49.11% -> 50.89% (+118)
• Whole binary branches: 61.76% -> 64.52% (+42)
• Focused Raft/driver lines: 76.48% -> 79.74%
• Focused Raft/driver branches: 65.02% -> 68.06%

Remaining gaps

• Remaining uncovered paths are grouped into unexposed APIs, malformed inputs, defensive states, nondeterministic ordering, trace-model limitations, deprecated or failure-only commands, and instrumentation artifacts.
• Signed-retirement rollback still requires a trace-model extension before a deterministic scenario can cover it.

The stale leadership-nomination scenario and its required TLA+ model change are split into #8126 for independent review.

[Amaury Chamayou (achamayou)]

Copilot please drop the writeup from the PR, it's great to have but only in PR description, not checked in. Also please drop the checked-in ndjson. And please find the relevant location in the C++ where messages with a newer term are ignored if it's a ProposeVoteRequest, and point to it in comment in the spec where you added this condition.

[Copilot]

Copilot please drop the writeup from the PR, it's great to have but only in PR description, not checked in. Also please drop the checked-in ndjson. And please find the relevant location in the C++ wh...

Addressed in f358e92: removed the checked-in coverage writeup and NDJSON trace, and added a commit-pinned link from the TLA+ condition to recv_propose_request_vote() in raft.h.

[Amaury Chamayou (achamayou)]

Copilot make sure the description is up to date.

[Copilot]

Copilot make sure the description is up to date.

Updated the PR description for current head f358e92: it now lists all nine scenarios, scopes the measured coverage to the first eight, and reflects the TLA+ stale-proposal change and remaining signed-retirement gap.

[Copilot]

Pull request overview

This PR expands the Raft driver scenario suite with additional deterministic scenarios to cover previously unexercised election/reconfiguration/diagnostic paths, and updates the TLA+ consensus model to match the C++ behavior when receiving stale-term ProposeVoteRequest messages.

Changes:

• Update the TLA+ model so ProposeVoteRequest is ignored (discarded) unless its term matches the recipient’s current term.
• Add nine new raft-driver scenarios covering leadership races, delayed vote traffic, retirement rollback, delayed responses after retirement/cleanup, batching behavior, compact message diagnostics, latest-leader targeting, single-node swaps, and stale nomination handling.

Custom instructions used:

• .github/copilot-instructions.md
• .github/instructions/reviewing.instructions.md

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tla/consensus/ccfraft.tla	Aligns model behavior for stale-term ProposeVoteRequest handling with the C++ implementation.
tests/raft_scenarios/leadership_race	Adds a deterministic scenario for quorum-loss step-down and replacement election behavior.
tests/raft_scenarios/delayed_vote_requests	Covers delayed same-term vote traffic and ignoring stale responses across election rounds.
tests/raft_scenarios/retirement_rollback	Exercises rollback of an uncommitted retirement/reconfiguration via a later-term election.
tests/raft_scenarios/retired_node_delayed_responses	Verifies delayed responses from a retired/cleaned-up node are ignored appropriately.
tests/raft_scenarios/large_entry_batching	Stresses AppendEntries batching recalculation and proactive sends when entry sizes cross thresholds.
tests/raft_scenarios/message_type_summaries	Adds coverage for compact diagnostic labelling of queued message types.
tests/raft_scenarios/replicate_on_latest_leader	Validates replicate,latest targets the highest-term leader when multiple primaries exist.
tests/raft_scenarios/swap_single_node	Adds a scenario for atomic single-node replacement and convergence.
tests/raft_scenarios/late_candidate	Ensures stale-term nominations/proposals do not restart or alter candidacy.