Module consensus 

KIP-595 consensus decision kernels, extracted from krabka-kraft-core so Creusot can verify them (the host crate’s Instant/async surface is untranslatable).

The functions carry their Creusot preconditions, postconditions, invariants, variants, and supporting lemmas directly beside the executable bodies.

Structs

FailoverFacts

What the host established about one partition before the failover decision. The kernel does not see replica sets; every field is the host’s classification of them.

OutOfIsrFacts

The out-of-ISR options, consulted only when no ISR member is live.

RecoveryCandidate

One surviving replica’s log as KIP-966 unclean recovery ranks it, from its GetReplicaLogInfo answer.

Enums

FailoverAction

Safety action selected after the host classifies live ISR and replicas.

FailoverRecovery

Offset-aware recovery mode resolved for one partition.

LiveIsr

What the live members of the partition’s ISR can do once the leader is gone. Every live ISR member holds every committed record; a witness is a live member that never leads.

Functions

election_has_quorum

Whether the unique grants from current voters reach a majority.

election_jitter_ms

Deterministic per-(node, epoch) election-timeout jitter in [0, base_ms).

failover_action

Select the failover action class by a fixed precedence ladder.

log_is_up_to_date

true if the candidate’s log is at least as up-to-date as ours.

majority_size

Majority size for a voter set: floor(n / 2) + 1.

majority_watermark

The watermark a majority has acknowledged, never below current.

recompute_high_watermark

The HWM as the majority-th largest match offset across the leader’s own log end, when leader_counts, and every follower’s acknowledged fetch offset.

select_best_recovery_replica

Select the replica with highest (last leader epoch, log end offset) and lowest broker ID as the deterministic tie-breaker.