krabka_verified/
consensus.rs

1//! KIP-595 consensus decision kernels, extracted from `krabka-kraft-core` so
2//! Creusot can verify them (the host crate's `Instant`/async surface is
3//! untranslatable).
4//!
5//! The functions carry their Creusot preconditions, postconditions, invariants,
6//! variants, and supporting lemmas directly beside the executable bodies.
7
8use creusot_std::prelude::*;
9
10/// Offset-aware recovery mode resolved for one partition.
11#[krabka_macros::model_type]
12pub enum FailoverRecovery {
13    None,
14    Balanced,
15    Aggressive,
16}
17
18/// Safety action selected after the host classifies live ISR and replicas.
19#[krabka_macros::model_type]
20pub enum FailoverAction {
21    ElectClean,
22    ElectFromElr,
23    /// The partition's single last-known leader comes back as an unclean
24    /// leader (Kafka's `canElectLastKnownLeader`).
25    ElectLastKnown,
26    Recover(FailoverRecovery),
27    ElectUnclean,
28    Unavailable,
29    ShrinkIsr,
30    NoChange,
31}
32
33/// What the live members of the partition's ISR can do once the leader is
34/// gone. Every live ISR member holds every committed record; a witness is a
35/// live member that never leads.
36#[krabka_macros::model_type]
37pub enum LiveIsr {
38    /// No ISR member is live.
39    Empty,
40    /// Every live ISR member is a witness, so none can lead.
41    WitnessesOnly,
42    /// A live ISR member that is not a witness can lead.
43    Electable,
44}
45
46/// The out-of-ISR options, consulted only when no ISR member is live.
47#[krabka_macros::model_type]
48pub struct OutOfIsrFacts {
49    /// A live KIP-966 eligible leader replica can lead.
50    pub has_electable_elr: bool,
51    /// Kafka's `canElectLastKnownLeader`, less the empty-ISR test that
52    /// [`LiveIsr::Empty`] already carries: the target ELR is empty, the
53    /// partition's `lastKnownElr` holds exactly one replica, and that replica
54    /// is live and can lead.
55    pub last_known_leader_electable: bool,
56    /// The topic's resolved offset-aware recovery strategy.
57    pub recovery: FailoverRecovery,
58    /// The KIP-841 out-of-ISR election is both permitted by
59    /// `unclean.leader.election.enable` and has a live replica to elect.
60    pub unclean_election_available: bool,
61}
62
63/// What the host established about one partition before the failover
64/// decision. The kernel does not see replica sets; every field is the host's
65/// classification of them.
66#[krabka_macros::model_type]
67pub struct FailoverFacts {
68    /// The partition's leader is the replica that went away.
69    pub leader_dead: bool,
70    /// The live ISR is smaller than the recorded ISR.
71    pub isr_shrunk: bool,
72    /// What the live ISR members can do.
73    pub live_isr: LiveIsr,
74    /// The options left when no ISR member is live.
75    pub out_of_isr: OutOfIsrFacts,
76}
77
78/// One surviving replica's log as KIP-966 unclean recovery ranks it, from its
79/// `GetReplicaLogInfo` answer.
80#[krabka_macros::model_type]
81pub struct RecoveryCandidate {
82    /// The leader epoch of the last record the replica wrote.
83    pub last_epoch: i32,
84    /// The offset one past the replica's last record.
85    pub log_end_offset: i64,
86    /// The replica's broker id, which breaks a tie deterministically.
87    pub broker_id: u64,
88}
89
90mod failover;
91#[cfg(creusot)]
92pub use failover::{
93    count_ge, count_ge_prefix, hwm_member_at, lemma_explicit_vote_count_equal, ranks_ge,
94};
95pub use failover::{
96    election_has_quorum, failover_action, majority_size, select_best_recovery_replica,
97};
98
99mod log_is_up_to_date;
100pub use log_is_up_to_date::{election_jitter_ms, log_is_up_to_date};
101#[cfg(creusot)]
102pub use log_is_up_to_date::{
103    least_hwm_member_ge_index, lemma_count_ge_prefix_monotone, lemma_count_ge_prefix_nonnegative,
104    lemma_hwm_member_maximal, lemma_hwm_threshold_has_member,
105};
106
107mod watermark;
108#[cfg(any(creusot, test))]
109use watermark::candidate_has_majority;
110pub use watermark::{majority_watermark, recompute_high_watermark};
111
112// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
113#[cfg(creusot)]
114#[cfg_attr(test, mutants::skip)]
115#[logic(open)]
116/// Every concrete supporting report belongs to a different node.
117pub(crate) fn supporting_nodes_distinct(supporters: Seq<(u64, i64)>) -> bool {
118    pearlite! { forall<i: Int, j: Int> 0 <= i && i < j && j < supporters.len() ==> supporters[i].0 != supporters[j].0 }
119}
120
121// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
122#[cfg(creusot)]
123#[cfg_attr(test, mutants::skip)]
124#[logic(open)]
125/// The majority bound includes the leader's own slot.
126pub(crate) fn valid_hwm_majority(majority: Int, members: Int) -> bool {
127    pearlite! { 1 <= majority && majority <= members + 1 }
128}
129
130// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
131#[cfg(creusot)]
132#[cfg_attr(test, mutants::skip)]
133#[logic(open)]
134/// Each reported supporting frontier reaches the limit and names a voter with concrete evidence.
135pub(crate) fn supporting_voter_witnesses(
136    supporters: Seq<(u64, i64)>,
137    voters: Seq<u64>,
138    limit: Int,
139    evidence: creusot_std::logic::Mapping<(Int, Int), bool>,
140) -> bool {
141    pearlite! { forall<i: Int> 0 <= i && i < supporters.len() ==> supporters[i].1@ >= limit
142    && exists<j: Int> 0 <= j && j < voters.len() && supporters[i].0 == voters[j]
143        && evidence.get((i, j)) }
144}
145
146#[cfg(test)]
147mod tests;
krabka_verified/consensus.rs

krabka_verified/
consensus.rs
