Model Raft leadership nomination edge cases

[Amaury Chamayou (achamayou)]

Align the TLA+ consensus model and C++ tracing with leadership nomination edge cases.

Changes

• Ignore a stale ProposeVoteRequest when its term differs from the recipient current term.
• Add late_nomination, where a node advances to term 3 before receiving a term-2 nomination and remains a candidate.
• Emit step_down_and_nominate_successor tracing only when an explicit nomination selects a successor and sends ProposeVoteRequest.
• Add nominate_without_successor, where a single-node leader remains leader and queues no proposal or nomination trace event.
• Keep these model-dependent scenarios separate from Expand Raft driver scenario coverage #8122 following review feedback.

Validation

• Both tracing-enabled and tracing-disabled raft_driver builds pass.
• All 44 scenarios on this branch plus the eight additional scenarios from Expand Raft driver scenario coverage #8122 execute successfully and pass TLC trace validation.
• late_nomination emits one explicit nomination event; nominate_without_successor emits none.
• Combined with Expand Raft driver scenario coverage #8122, whole-binary coverage moves from 50.89% to 50.95% for lines and 64.52% to 64.78% for branches; focused Raft/driver coverage moves from 79.74% to 79.86% for lines and 68.06% to 68.37% for branches.

[Copilot]

Pull request overview

Updates the Raft TLA+ consensus model so ProposeVoteRequest (leadership nomination) messages are ignored and discarded when their term does not match the recipient’s currentTerm, matching the C++ implementation, and adds a deterministic Raft-driver scenario to exercise this case.

Changes:

• Exclude ProposeVoteRequest from UpdateTerm, preventing term advancement due to nomination messages.
• Update RcvProposeVoteRequest to explicitly discard mismatched-term nominations while leaving node state unchanged.
• Add tests/raft_scenarios/late_nomination to validate that a delayed, stale nomination does not restart candidacy.

Custom instructions used:

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

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
tla/consensus/ccfraft.tla	Aligns the TLA receive/update-term logic with C++ behavior for stale ProposeVoteRequest nominations.
tests/raft_scenarios/late_nomination	Adds a deterministic scenario where a delayed term-2 nomination arrives after the recipient advances to term 3, and must be ignored.

[Copilot]

Pull request overview

Copilot reviewed 4 out of 4 changed files in this pull request and generated no new comments.