Function failover_action 

pub fn failover_action(facts: FailoverFacts) -> FailoverAction

Select the failover action class by a fixed precedence ladder.

What the contract proves is the ladder, and only the ladder. For a dead leader it picks, in order: a clean election when a live ISR member can lead; otherwise, and only when no ISR member is live, an election from the eligible leader replicas; otherwise the last known leader; otherwise the configured offset-aware recovery; otherwise the KIP-841 election when it is available; otherwise the partition stays unavailable. A live ISR of witnesses only stops the ladder at unavailable. For a live leader it only shrinks the ISR or leaves it alone. Each outcome is pinned to exactly one combination of FailoverFacts.

Why each rung is safe is not part of the proof. It rests on the host’s classification and on Kafka’s semantics: an ISR member holds every committed record; a KIP-966 eligible leader replica left the ISR while the partition still held min.insync.replicas members, so it holds every committed record too, and neither the unclean.leader.election.enable toggle nor unclean.recovery.strategy gates it. Its rung is reachable only once the live ISR is empty, the same guard Apache Kafka’s PartitionChangeBuilder.isValidNewLeader puts on its targetElr disjunct. The last known leader is the one replica that led when the partition lost its leader, but it may have lost an unflushed tail, so electing it is an unclean election that Kafka takes without either toggle: its rung sits directly under the ELR one, exactly where electAnyLeader and electPreferredLeader put canElectLastKnownLeader, ahead of the KIP-841 branch.

unclean_election_available joins the KIP-841 toggle and the existence of a replica that can serve, because the ladder never separates them: an election that is allowed with nobody to elect and one that has a candidate and no permission are the same unavailable partition.