Model former candidate double voting in Raft

[achamayou]

Summary

• add a deterministic five-node Raft scenario reproducing a former candidate voting twice in one term
• retain a committable suffix on the elected leader so the former candidate rejects its first heartbeat, steps down, and grants a delayed competing vote request
• align ReturnToFollowerState with CCF by clearing votedFor when a candidate steps down within the same term

The scenario provides concrete trace coverage for the implementation behavior. Trace validation now accepts that behavior, while the bounded consensus model checks establish whether it violates election safety, log safety, leader completeness, or related durability properties.

Validation

• focused Raft scenario passes
• focused consensus trace validation passes
• run-long-verification enabled for the reconfiguration model checks

Closes #5891

[Copilot]

Pull request overview

This PR updates the TLA+ CCF Raft specification and test scenarios to explicitly model and reproduce the “former candidate can vote twice in one term” behavior described in #5891, so that trace validation and bounded model checks can cover the observed implementation behavior.

Changes:

• Update the TLA+ ReturnToFollowerState transition to clear votedFor when a candidate steps down within the same term (matching current CCF behavior).
• Add a deterministic 5-node raft_driver scenario reproducing the double-vote-in-one-term sequence from #5891.

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	Adjusts the TLA+ step-down transition to clear votedFor even when stepping down within the same term.
tests/raft_scenarios/former_candidate_double_vote	Adds a deterministic scenario script to reproduce the former-candidate double vote behavior for trace/model coverage.

[eddyashton]

Scenario looks like it does what it claims to do.

I'd appreciate a nod from @cjen1-msft or @heidihoward that they're also happy with the TLA+ change.

I'll reiterate the choice this PR makes - align the TLA+ spec with the implementation behaviour (become_aware_of_new_term resets voted_for, so a node may vote for multiple distinct candidates within a term). That behaviour sounds a tad fishy, but I don't believe it can lead to dual primaries within a term. With more time, I'd love to explore more variations of this branch (many serial re-votes, around reconfigurations) to confirm, but I think we have to punt to the existing verification for now.

[achamayou]

@eddyashton thanks for the re-iteration, that's also my understanding. I've only run the long verification, if we think we ought to extend the model checking in a particular direction to firm this up, I'm open to suggestions.

+1 for reviews from @cjen1-msft and @heidihoward.

[cjen1-msft]

Going through this now. I think this is fine as the nodes which voted for the leader are never downgraded back to follower again and so no other node can be elected? But I'm validating this currently.

[cjen1-msft]

See #8094 for a violation. We aren't picking this up in the CI model checking in this PR as:

• we need 5 nodes for this.
• Simulation would require different weights (1/1000 -> 1/50?)

[eddyashton]

Closing this PR, preferring #8094. That adds a similar (fewer nodes, but +PreVote, does that sum to "simpler?") scenario, that shows a violation is possible. Don't want to align the spec with bad behaviour, as this PR proposes. Should consider salvaging this scenario as further coverage, or finally tackle improving simulation coverage by seeding from scenarios.