krabka_verified/consensus/
log_is_up_to_date.rs

1#[cfg(creusot)]
2use super::{count_ge, count_ge_prefix, hwm_member_at, valid_hwm_majority};
3use creusot_std::prelude::*;
4
5// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
6#[cfg(creusot)]
7#[cfg_attr(test, mutants::skip)]
8#[logic]
9#[requires(0 <= limit && limit <= s.len() + 1)]
10#[requires(low <= high)]
11#[ensures(count_ge_prefix(log_end, s, low, limit, leader_counts)
12    >= count_ge_prefix(log_end, s, high, limit, leader_counts))]
13#[variant(limit)]
14pub fn lemma_count_ge_prefix_monotone(
15    log_end: Int,
16    s: Seq<i64>,
17    low: Int,
18    high: Int,
19    limit: Int,
20    leader_counts: bool,
21) {
22    if limit > 0 {
23        lemma_count_ge_prefix_monotone(log_end, s, low, high, limit - 1, leader_counts);
24    }
25}
26
27// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
28#[cfg(creusot)]
29#[cfg_attr(test, mutants::skip)]
30#[logic]
31#[requires(0 <= limit && limit <= s.len() + 1)]
32#[ensures(count_ge_prefix(log_end, s, v, limit, leader_counts) >= 0)]
33#[variant(limit)]
34pub fn lemma_count_ge_prefix_nonnegative(
35    log_end: Int,
36    s: Seq<i64>,
37    v: Int,
38    limit: Int,
39    leader_counts: bool,
40) {
41    if limit > 0 {
42        lemma_count_ge_prefix_nonnegative(log_end, s, v, limit - 1, leader_counts);
43    }
44}
45
46// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
47#[cfg(creusot)]
48#[cfg_attr(test, mutants::skip)]
49#[logic]
50#[requires(0 < limit && limit <= s.len() + 1)]
51#[requires(count_ge_prefix(log_end, s, v, limit, leader_counts) >= 1)]
52#[ensures(0 <= result && result < limit)]
53#[ensures(hwm_member_at(log_end, s, result) >= v)]
54#[ensures(count_ge_prefix(log_end, s, hwm_member_at(log_end, s, result), limit, leader_counts)
55    >= count_ge_prefix(log_end, s, v, limit, leader_counts))]
56#[variant(limit)]
57pub fn least_hwm_member_ge_index(
58    log_end: Int,
59    s: Seq<i64>,
60    v: Int,
61    limit: Int,
62    leader_counts: bool,
63) -> Int {
64    // Every step below unfolds `count_ge_prefix` once at `limit`, where the
65    // last member always counts because `limit > 1` puts it past the leader.
66    if limit <= 1 {
67        0
68    } else {
69        let last_index = limit - 1;
70        let last_member = hwm_member_at(log_end, s, last_index);
71        let previous_count = count_ge_prefix(log_end, s, v, last_index, leader_counts);
72        if last_member >= v {
73            if previous_count >= 1 {
74                let previous_index =
75                    least_hwm_member_ge_index(log_end, s, v, last_index, leader_counts);
76                let previous_member = hwm_member_at(log_end, s, previous_index);
77                if last_member <= previous_member {
78                    // The last member is the smaller witness. Monotonicity
79                    // carries the earlier witness's count down to it.
80                    lemma_count_ge_prefix_monotone(
81                        log_end,
82                        s,
83                        last_member,
84                        previous_member,
85                        last_index,
86                        leader_counts,
87                    );
88                    last_index
89                } else {
90                    // The earlier witness stays smaller; the last member
91                    // reaches it, so both counts gain exactly one at `limit`.
92                    previous_index
93                }
94            } else {
95                // No earlier member reaches `v`, so `v`'s count at `limit` is
96                // exactly the last member's one, and the last member's own
97                // count is at least that.
98                lemma_count_ge_prefix_nonnegative(log_end, s, v, last_index, leader_counts);
99                lemma_count_ge_prefix_nonnegative(
100                    log_end,
101                    s,
102                    last_member,
103                    last_index,
104                    leader_counts,
105                );
106                last_index
107            }
108        } else {
109            // The last member misses `v`, so the witness is an earlier one.
110            least_hwm_member_ge_index(log_end, s, v, last_index, leader_counts)
111        }
112    }
113}
114
115// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
116#[cfg(creusot)]
117#[cfg_attr(test, mutants::skip)]
118#[requires(valid_hwm_majority(majority@, [email protected]()))]
119#[ensures(forall<v: Int> count_ge(log_end@, s@, v, leader_counts) >= majority@
120    ==> exists<k: Int> hwm_member_witness(log_end@, s@, k, v, majority@, leader_counts))]
121pub fn lemma_hwm_threshold_has_member(
122    log_end: i64,
123    s: &[i64],
124    majority: usize,
125    leader_counts: bool,
126) {
127    proof_assert!(forall<v: Int> count_ge(log_end@, s@, v, leader_counts) >= majority@ ==>
128        exists<k: Int> k == least_hwm_member_ge_index(log_end@, s@, v, [email protected]() + 1, leader_counts)
129            && hwm_member_witness(log_end@, s@, k, v, majority@, leader_counts));
130}
131
132// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
133#[cfg(creusot)]
134#[cfg_attr(test, mutants::skip)]
135#[requires(valid_hwm_majority(majority@, [email protected]()))]
136#[requires(forall<k: Int> 0 <= k && k < [email protected]() + 1
137    && count_ge(log_end@, s@, hwm_member_at(log_end@, s@, k), leader_counts) >= majority@
138    ==> hwm_member_at(log_end@, s@, k) <= best@)]
139#[ensures(forall<v: Int> count_ge(log_end@, s@, v, leader_counts) >= majority@ ==> v <= best@)]
140pub fn lemma_hwm_member_maximal(
141    log_end: i64,
142    s: &[i64],
143    majority: usize,
144    best: i64,
145    leader_counts: bool,
146) {
147    lemma_hwm_threshold_has_member(log_end, s, majority, leader_counts);
148}
149
150/// Deterministic per-`(node, epoch)` election-timeout jitter in `[0, base_ms)`.
151///
152/// This is Raft's randomized backoff, made reproducible for the deterministic
153/// sims: the jitter is a fixed hash of the node ID and the epoch, so the same
154/// run replays the same way. The contract proves only the range, `0` for a
155/// zero base and below `base_ms` otherwise. It does not prove that two nodes,
156/// or two epochs of one node, get different values; the hash usually spreads
157/// them, and the unit tests pin a few spread values, but a collision is
158/// possible and nothing here rules it out.
159#[ensures(base_ms@ == 0 ==> result@ == 0)]
160#[ensures(base_ms@ > 0 ==> result@ < base_ms@)]
161#[must_use]
162pub fn election_jitter_ms(me: u64, epoch: u32, base_ms: u64) -> u64 {
163    if base_ms == 0 {
164        return 0;
165    }
166    // Cheap integer hash of (node id, epoch); avoids any RNG so the sims stay
167    // deterministic.
168    let mix = me.wrapping_mul(0x9E37_79B9_7F4A_7C15)
169        ^ u64::from(epoch).wrapping_mul(0xD1B5_4A32_D192_ED03);
170    mix % base_ms
171}
172
173/// `true` if the candidate's log is at least as up-to-date as ours.
174///
175/// KIP-595: the higher last epoch wins. On a tie, the higher or equal offset
176/// wins.
177#[ensures(result == (cand_epoch@ > my_epoch@
178    || (cand_epoch@ == my_epoch@ && cand_offset@ >= my_end@)))]
179#[must_use]
180pub const fn log_is_up_to_date(
181    my_epoch: u32,
182    my_end: i64,
183    cand_epoch: u32,
184    cand_offset: i64,
185) -> bool {
186    cand_epoch > my_epoch || (cand_epoch == my_epoch && cand_offset >= my_end)
187}
188
189// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
190#[cfg(creusot)]
191#[cfg_attr(test, mutants::skip)]
192#[logic(open)]
193/// This actual high-watermark member reaches the threshold with a majority.
194fn hwm_member_witness(
195    end: Int,
196    offsets: Seq<i64>,
197    index: Int,
198    value: Int,
199    majority: Int,
200    leader_counts: bool,
201) -> bool {
202    pearlite! { 0 <= index && index < offsets.len() + 1 && hwm_member_at(end, offsets, index) >= value
203    && count_ge(end, offsets, hwm_member_at(end, offsets, index), leader_counts) >= majority }
204}
krabka_verified/consensus/log_is_up_to_date.rs

krabka_verified/consensus/
log_is_up_to_date.rs
