krabka_verified/stretch/
quorum_survives_any_single_site_loss.rs

1use creusot_std::prelude::*;
2
3/// The sum of the first `limit` elements of `s`.
4// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
5#[cfg(creusot)]
6#[cfg_attr(test, mutants::skip)]
7#[logic]
8#[variant(limit)]
9pub fn sum_prefix(s: Seq<i64>, limit: Int) -> Int {
10    pearlite! {
11        if limit <= 0 {
12            0
13        } else {
14            sum_prefix(s, limit - 1) + s[limit - 1]@
15        }
16    }
17}
18
19/// The sum of every element of `s`. This is the total voter count.
20// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
21#[cfg(creusot)]
22#[cfg_attr(test, mutants::skip)]
23#[logic]
24pub fn sum_all(s: Seq<i64>) -> Int {
25    pearlite! { sum_prefix(s, s.len()) }
26}
27
28/// One step of the `sum_prefix` recursion, as a fact about `limit - 1`.
29// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
30#[cfg(creusot)]
31#[cfg_attr(test, mutants::skip)]
32#[logic]
33#[requires(1 <= limit && limit <= s.len())]
34#[ensures(sum_prefix(s, limit) == sum_prefix(s, limit - 1) + s[limit - 1]@)]
35pub fn lemma_sum_prefix_step(s: Seq<i64>, limit: Int) {}
36
37/// A prefix sum is not negative when no element of that prefix is negative.
38// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
39#[cfg(creusot)]
40#[cfg_attr(test, mutants::skip)]
41#[logic]
42#[requires(0 <= limit && limit <= s.len())]
43#[requires(forall<k: Int> 0 <= k && k < limit ==> s[k]@ >= 0)]
44#[ensures(sum_prefix(s, limit) >= 0)]
45#[variant(limit)]
46pub fn lemma_sum_prefix_nonnegative(s: Seq<i64>, limit: Int) {
47    if limit > 0 {
48        lemma_sum_prefix_nonnegative(s, limit - 1);
49        lemma_sum_prefix_step(s, limit);
50    }
51}
52
53/// Two sites never survive a site loss, whatever the split of the voters.
54///
55/// This is the reason a stretch cluster needs a third site, and it is the
56/// claim [`quorum_survives_any_single_site_loss`]'s documentation makes about
57/// two sites. One of the two sites holds at least half of the voters. The loss
58/// of that site leaves half of the voters or less, and half is not a strict
59/// majority. No other proof calls this lemma; it exists so that the two-site
60/// claim is proved rather than only asserted.
61// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
62#[cfg(creusot)]
63#[cfg_attr(test, mutants::skip)]
64#[requires([email protected]() == 2)]
65#[requires(forall<k: Int> 0 <= k && k < 2 ==> voters_per_site@[k]@ >= 0)]
66#[ensures(exists<k: Int> 0 <= k && k < [email protected]()
67    && 2 * (sum_all(voters_per_site@) - voters_per_site@[k]@) <= sum_all(voters_per_site@))]
68pub fn lemma_two_sites_never_survive(voters_per_site: &[i64]) {
69    #[cfg(creusot)]
70    proof_assert!({
71        lemma_sum_prefix_nonnegative(voters_per_site@, [email protected]());
72        sum_all(voters_per_site@) >= 0
73    });
74    proof_assert!(sum_prefix(voters_per_site@, 1) == voters_per_site@[0]@);
75    proof_assert!(sum_all(voters_per_site@) == voters_per_site@[0]@ + voters_per_site@[1]@);
76    proof_assert!(voters_per_site@[0]@ >= voters_per_site@[1]@
77        ==> 2 * (sum_all(voters_per_site@) - voters_per_site@[0]@) <= sum_all(voters_per_site@));
78    proof_assert!(voters_per_site@[1]@ >= voters_per_site@[0]@
79        ==> 2 * (sum_all(voters_per_site@) - voters_per_site@[1]@) <= sum_all(voters_per_site@));
80}
81
82/// `true` if the surviving `KRaft` voters still form a strict majority after
83/// the loss of any one site.
84///
85/// `voters_per_site[k]` is the count of `KRaft` voters in site `k`. The check
86/// asks for every site `k` whether `2 * (total - voters_per_site[k]) > total`
87/// holds, where `total` is the sum of the slice. A strict majority is what a
88/// `KRaft` quorum needs to elect a leader and to commit a metadata record, so a
89/// cluster that fails this check stops its metadata writes when it loses a
90/// site.
91///
92/// Two sites never pass this check. Any split of the voters over two sites
93/// leaves one site with half of them or more, and the loss of that site leaves
94/// half or less. This is why a third site must hold at least one voter. A
95/// data-bearing witness is the smallest form of that third site: it holds one
96/// voter, so `[1, 1, 1]` passes the check, and it holds a replica as well, so
97/// it also counts toward `min.insync.replicas`.
98///
99/// An empty slice returns `true`. There is no site to lose, so the condition
100/// holds for every site of the empty set.
101///
102/// The preconditions bound the slice at 1024 sites and each site at 1024
103/// voters. The total is then 1048576 at most, and `2 * total` cannot overflow.
104#[requires([email protected]() <= 1024)]
105#[requires(forall<k: Int> 0 <= k && k < [email protected]()
106    ==> 0 <= voters_per_site@[k]@ && voters_per_site@[k]@ <= 1024)]
107#[ensures(result == (forall<k: Int> 0 <= k && k < [email protected]()
108    ==> 2 * (sum_all(voters_per_site@) - voters_per_site@[k]@) > sum_all(voters_per_site@)))]
109#[must_use]
110pub fn quorum_survives_any_single_site_loss(voters_per_site: &[i64]) -> bool {
111    let n = voters_per_site.len();
112
113    let mut total: i64 = 0;
114    let mut i = 0;
115    #[invariant(i@ <= n@)]
116    #[invariant(total@ == sum_prefix(voters_per_site@, i@))]
117    #[invariant(0 <= total@ && total@ <= i@ * 1024)]
118    #[variant(n@ - i@)]
119    while i < n {
120        proof_assert!(sum_prefix(voters_per_site@, i@ + 1)
121            == sum_prefix(voters_per_site@, i@) + voters_per_site@[i@]@);
122        if let Some(&voters) = voters_per_site.get(i) {
123            total += voters;
124        }
125        i += 1;
126    }
127
128    let mut k = 0;
129    let mut survives = true;
130    #[invariant(k@ <= n@)]
131    #[invariant(0 <= total@ && total@ <= 1024 * 1024)]
132    #[invariant(total@ == sum_all(voters_per_site@))]
133    #[invariant(survives == (forall<j: Int> 0 <= j && j < k@
134        ==> 2 * (sum_all(voters_per_site@) - voters_per_site@[j]@) > sum_all(voters_per_site@)))]
135    #[variant(n@ - k@)]
136    while k < n {
137        if let Some(&voters) = voters_per_site.get(k)
138            && 2 * (total - voters) <= total
139        {
140            survives = false;
141        }
142        k += 1;
143    }
144    survives
145}
krabka_verified/stretch/quorum_survives_any_single_site_loss.rs

krabka_verified/stretch/
quorum_survives_any_single_site_loss.rs
