krabka_verified/stretch.rs
1//! Durability arithmetic for a stretch cluster.
2//!
3//! A stretch cluster holds one Kafka cluster in more than one site. The claim
4//! that such a cluster keeps the data and stays available through the loss of
5//! one whole site rests on three numbers: the replica count that survives a
6//! site loss, the `min.insync.replicas` value that stays satisfiable after that
7//! loss, and the split of the `KRaft` voters over the sites. This module states
8//! those three numbers as kernels, and Creusot proves the contracts.
9//!
10//! The replica numbers are stated against a model of the placement,
11//! `round_robin_load`: replica `r` of a partition lands on site `r % sites`.
12//! The contracts say what each site then holds and what the loss of each site
13//! leaves, and the proof derives the `ceil(rf / sites)` arithmetic from that
14//! model. That the broker's placer actually places replicas this way is not
15//! proved here; it is the host's responsibility.
16//!
17//! The preconditions bound the inputs at 1024. A replication factor, a site
18//! count, and a voter count are all small in a real deployment. The bounds only
19//! keep the arithmetic away from `i64` overflow, and a stated bound is honest
20//! about what the proof covers.
21
22#[cfg(creusot)]
23use creusot_std::prelude::*;
24
25mod quorum_survives_any_single_site_loss;
26pub use quorum_survives_any_single_site_loss::quorum_survives_any_single_site_loss;
27#[cfg(creusot)]
28pub use quorum_survives_any_single_site_loss::{
29 lemma_sum_prefix_step, lemma_two_sites_never_survive, sum_all, sum_prefix,
30};
31
32mod min_insync_is_site_loss_safe;
33#[cfg(creusot)]
34pub use min_insync_is_site_loss_safe::{
35 lemma_div_exact, lemma_div_monotone, lemma_round_robin_load, lemma_round_robin_step,
36 lemma_site_load_at_most_first, round_robin_load,
37};
38pub use min_insync_is_site_loss_safe::{min_insync_is_site_loss_safe, site_loss_survivors};
39
40#[cfg(test)]
41mod tests;