Skip to main content

krabka_verified/
wal.rs

1//! Diskless WAL admission decisions.
2
3use creusot_std::prelude::*;
4
5/// Result of authorizing and epoch-fencing one diskless WAL Fetch.
6#[krabka_macros::model_type]
7pub enum WalFetchAdmission {
8    Denied,
9    FencedLeaderEpoch,
10    UnknownLeaderEpoch,
11    Serve,
12}
13
14mod batch_equal;
15#[cfg(creusot)]
16pub use batch_equal::wal_batch_layout;
17pub use batch_equal::{
18    exact_wal_batch_range, wal_batch_equal, wal_checkpoint_range_valid, wal_covering_batch_range,
19};
20
21mod select_wal_voters;
22pub use select_wal_voters::{
23    select_wal_voter_index, select_wal_voters, wal_fetch_admission, wal_voter_set_valid,
24};
25
26// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
27#[cfg(creusot)]
28#[cfg_attr(test, mutants::skip)]
29#[logic(open)]
30/// Every selected WAL voter has a distinct node ID and rack ID.
31pub fn placement_identities_distinct(selected: Seq<(u64, u64)>) -> bool {
32    pearlite! { forall<i: Int, j: Int> 0 <= i && i < j && j < selected.len()
33    ==> selected[i].0 != selected[j].0 && selected[i].1 != selected[j].1 }
34}
35
36#[cfg(test)]
37mod tests;