krabka_verified/wal/
select_wal_voters.rs

1use {super::WalFetchAdmission, creusot_std::prelude::*};
2
3// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
4#[cfg(creusot)]
5#[cfg_attr(test, mutants::skip)]
6#[logic(open(crate))]
7pub(crate) fn wal_fetch_authorized(
8    authenticated_node: Option<u64>,
9    claimed_node: u64,
10    local_node: u64,
11    voters: Seq<u64>,
12) -> bool {
13    pearlite! {
14        authenticated_node == Some(claimed_node)
15            && voters.len() > 0
16            && voters[0] == local_node
17            && exists<i: Int> 0 <= i && i < voters.len() && voters[i] == claimed_node
18    }
19}
20
21/// Whether `value` occurs in `values`; used for voter ids and rack ids alike.
22#[ensures(result == (exists<i: Int>
23    0 <= i && i < [email protected]() && values@[i] == value))]
24pub(super) fn contains(values: &[u64], value: u64) -> bool {
25    let mut i = 0;
26    #[cfg_attr(creusot, invariant(i@ <= [email protected]()))]
27    #[cfg_attr(creusot, invariant(forall<k: Int> 0 <= k && k < i@ ==> values@[k] != value))]
28    #[cfg_attr(creusot, variant([email protected]() - i@))]
29    while i < values.len() {
30        if matches!(values.get(i), Some(&candidate) if candidate == value) {
31            return true;
32        }
33        i += 1;
34    }
35    false
36}
37
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(open)]
42/// A `(node, rack)` candidate may not become a WAL voter when its node or its
43/// rack is already used, or when only the local broker is eligible and the
44/// candidate is another broker.
45fn voter_blocked(
46    candidate: (u64, u64),
47    used_nodes: Seq<u64>,
48    used_racks: Seq<u64>,
49    local_node: u64,
50    require_local: bool,
51) -> bool {
52    pearlite! {
53        (exists<j: Int> 0 <= j && j < used_nodes.len() && used_nodes[j] == candidate.0)
54            || (exists<j: Int> 0 <= j && j < used_racks.len() && used_racks[j] == candidate.1)
55            || (require_local && candidate.0 != local_node)
56    }
57}
58
59/// Select the first candidate, in the caller's order, whose node and rack are
60/// both unused. When `require_local` is set, only the local broker is
61/// eligible.
62#[ensures(match result {
63    None => forall<i: Int> 0 <= i && i < [email protected]() ==>
64        voter_blocked(candidates@[i], used_nodes@, used_racks@, local_node, require_local),
65    Some(index) => index@ < [email protected]()
66        && !voter_blocked(candidates@[index@], used_nodes@, used_racks@, local_node, require_local)
67        && forall<i: Int> 0 <= i && i < index@ ==>
68            voter_blocked(candidates@[i], used_nodes@, used_racks@, local_node, require_local),
69})]
70#[must_use]
71pub fn select_wal_voter_index(
72    candidates: &[(u64, u64)],
73    used_nodes: &[u64],
74    used_racks: &[u64],
75    local_node: u64,
76    require_local: bool,
77) -> Option<usize> {
78    let mut i = 0usize;
79    #[invariant(i@ <= [email protected]())]
80    #[invariant(forall<k: Int> 0 <= k && k < i@ ==>
81        voter_blocked(candidates@[k], used_nodes@, used_racks@, local_node, require_local))]
82    #[variant([email protected]() - i@)]
83    while i < candidates.len() {
84        let &candidate = candidates.get(i)?;
85        if !contains(used_nodes, candidate.0)
86            && !contains(used_racks, candidate.1)
87            && (!require_local || candidate.0 == local_node)
88        {
89            return Some(i);
90        }
91        i += 1;
92    }
93    None
94}
95
96/// Admit exactly a complete, nonempty, local-first set of distinct voter IDs.
97/// A repeated ID cannot vote twice through the same durable-offset map entry.
98#[ensures(result == (expected@ > 0 && [email protected]() == expected@
99    && voters@[0] == local_node
100    && crate::sequence::distinct(voters@)))]
101#[must_use]
102pub fn wal_voter_set_valid(voters: &[u64], local_node: u64, expected: usize) -> bool {
103    if expected == 0
104        || voters.len() != expected
105        || !matches!(voters.first(), Some(&first) if first == local_node)
106    {
107        return false;
108    }
109    let mut i = 0usize;
110    #[invariant(i@ <= [email protected]())]
111    #[invariant(forall<j: Int, k: Int> 0 <= j && j < k && k < i@ ==> voters@[j] != voters@[k])]
112    #[variant([email protected]() - i@)]
113    while i < voters.len() {
114        if let (Some(seen), Some(&voter)) = (voters.get(..i), voters.get(i))
115            && contains(seen, voter)
116        {
117            return false;
118        }
119        i += 1;
120    }
121    true
122}
123
124/// Authorize a diskless WAL Fetch and classify its leader epoch.
125///
126/// Authorization deliberately precedes epoch classification, so an
127/// unauthenticated caller learns no placement epoch.
128#[ensures((result == WalFetchAdmission::Denied)
129    == !wal_fetch_authorized(authenticated_node, claimed_node, local_node, voters@))]
130#[ensures((result == WalFetchAdmission::FencedLeaderEpoch)
131    == (wal_fetch_authorized(authenticated_node, claimed_node, local_node, voters@)
132        && request_epoch@ >= 0 && request_epoch@ < leader_epoch@))]
133#[ensures((result == WalFetchAdmission::UnknownLeaderEpoch)
134    == (wal_fetch_authorized(authenticated_node, claimed_node, local_node, voters@)
135        && request_epoch@ >= 0 && request_epoch@ > leader_epoch@))]
136#[ensures((result == WalFetchAdmission::Serve)
137    == (wal_fetch_authorized(authenticated_node, claimed_node, local_node, voters@)
138        && (request_epoch@ < 0 || request_epoch@ == leader_epoch@)))]
139#[must_use]
140pub fn wal_fetch_admission(
141    authenticated_node: Option<u64>,
142    claimed_node: u64,
143    local_node: u64,
144    voters: &[u64],
145    request_epoch: i32,
146    leader_epoch: i32,
147) -> WalFetchAdmission {
148    if authenticated_node != Some(claimed_node)
149        || voters.first() != Some(&local_node)
150        || !contains(voters, claimed_node)
151    {
152        return WalFetchAdmission::Denied;
153    }
154    if request_epoch < 0 || request_epoch == leader_epoch {
155        return WalFetchAdmission::Serve;
156    }
157    if request_epoch < leader_epoch {
158        WalFetchAdmission::FencedLeaderEpoch
159    } else {
160        WalFetchAdmission::UnknownLeaderEpoch
161    }
162}
163
164/// Assemble the existing greedy, local-first placement across distinct nodes
165/// and racks. An incomplete result must be rejected by the quorum installer.
166#[ensures([email protected]() <= requested@)]
167#[ensures(([email protected]() == 0) == (requested@ == 0
168    || forall<i: Int> 0 <= i && i < [email protected]() ==> candidates@[i].0 != local_node))]
169#[ensures([email protected]() > 0 ==> result@[0].0 == local_node)]
170#[ensures(forall<i: Int> 0 <= i && i < [email protected]()
171    ==> exists<j: Int> 0 <= j && j < [email protected]() && result@[i] == candidates@[j])]
172#[ensures(crate::wal::placement_identities_distinct(result@))]
173#[ensures(0 < [email protected]() && [email protected]() < requested@ ==>
174    forall<i: Int> 0 <= i && i < [email protected]() ==>
175        exists<j: Int> 0 <= j && j < [email protected]()
176            && (candidates@[i].0 == result@[j].0 || candidates@[i].1 == result@[j].1))]
177#[must_use]
178pub fn select_wal_voters(
179    candidates: &[(u64, u64)],
180    local_node: u64,
181    requested: usize,
182) -> Vec<(u64, u64)> {
183    let mut selected: Vec<(u64, u64)> = Vec::new();
184    let mut nodes: Vec<u64> = Vec::new();
185    let mut racks: Vec<u64> = Vec::new();
186    #[invariant([email protected]() <= requested@)]
187    #[invariant([email protected]() == [email protected]() && [email protected]() == [email protected]())]
188    #[invariant([email protected]() > 0 ==> selected@[0].0 == local_node)]
189    #[invariant(forall<i: Int> 0 <= i && i < [email protected]()
190        ==> selected@[i].0 == nodes@[i] && selected@[i].1 == racks@[i])]
191    #[invariant(forall<i: Int> 0 <= i && i < [email protected]()
192        ==> exists<j: Int> 0 <= j && j < [email protected]() && selected@[i] == candidates@[j])]
193    #[invariant(crate::wal::placement_identities_distinct(selected@))]
194    #[variant(requested@ - [email protected]())]
195    while selected.len() < requested {
196        let Some(index) = select_wal_voter_index(
197            candidates,
198            &nodes,
199            &racks,
200            local_node,
201            matches!(selected.len(), 0),
202        ) else {
203            return selected;
204        };
205        let Some(&candidate) = candidates.get(index) else {
206            return selected;
207        };
208        selected.push(candidate);
209        nodes.push(candidate.0);
210        racks.push(candidate.1);
211    }
212    selected
213}
krabka_verified/wal/select_wal_voters.rs

krabka_verified/wal/
select_wal_voters.rs
