krabka_verified/
directory.rs

1//! Replica-directory assignment and controller-response decisions.
2
3use creusot_std::prelude::*;
4
5/// Change selected for one reported topic-partition replica.
6#[krabka_macros::model_type]
7pub enum DirectoryAssignmentDecision {
8    Ignore,
9    NoOp,
10    Assign(usize),
11}
12
13/// Select only the reporting broker's exact replica slot, and suppress an
14/// assignment that is already current.
15#[ensures((result == DirectoryAssignmentDecision::Ignore) == (replica_slot == None))]
16#[ensures((result == DirectoryAssignmentDecision::NoOp) ==
17    (replica_slot != None && already_assigned))]
18#[ensures(forall<slot: usize> result == DirectoryAssignmentDecision::Assign(slot) ==
19    (replica_slot == Some(slot) && !already_assigned))]
20#[must_use]
21pub fn directory_assignment_decision(
22    replica_slot: Option<usize>,
23    already_assigned: bool,
24) -> DirectoryAssignmentDecision {
25    match replica_slot {
26        None => DirectoryAssignmentDecision::Ignore,
27        Some(_) if already_assigned => DirectoryAssignmentDecision::NoOp,
28        Some(slot) => DirectoryAssignmentDecision::Assign(slot),
29    }
30}
31
32/// Classification of an assignment report's controller response.
33#[krabka_macros::model_type]
34pub enum DirectoryResponseDecision {
35    ControllerError,
36    StaleController,
37    Accept,
38}
39
40/// Accept success only while the controller identity that answered remains
41/// the current leader. A missing or changed leader makes the response stale.
42#[ensures((result == DirectoryResponseDecision::ControllerError) == !response_ok)]
43#[ensures((result == DirectoryResponseDecision::StaleController) ==
44    (response_ok && current_controller != Some(sent_controller)))]
45#[ensures((result == DirectoryResponseDecision::Accept) ==
46    (response_ok && current_controller == Some(sent_controller)))]
47#[must_use]
48pub fn directory_response_decision(
49    response_ok: bool,
50    sent_controller: u64,
51    current_controller: Option<u64>,
52) -> DirectoryResponseDecision {
53    if !response_ok {
54        DirectoryResponseDecision::ControllerError
55    } else if current_controller != Some(sent_controller) {
56        DirectoryResponseDecision::StaleController
57    } else {
58        DirectoryResponseDecision::Accept
59    }
60}
61
62#[cfg(test)]
63mod tests {
64    use {
65        super::{
66            DirectoryAssignmentDecision, DirectoryResponseDecision, directory_assignment_decision,
67            directory_response_decision,
68        },
69        assert2::check,
70    };
71
72    #[test]
73    fn planning_is_exact_idempotent_and_response_fenced() {
74        use {
75            DirectoryAssignmentDecision::{Assign, Ignore, NoOp},
76            DirectoryResponseDecision::{Accept, ControllerError, StaleController},
77        };
78
79        check!(directory_assignment_decision(None, false) == Ignore);
80        check!(directory_assignment_decision(None, true) == Ignore);
81        check!(directory_assignment_decision(Some(3), true) == NoOp);
82        check!(directory_assignment_decision(Some(3), false) == Assign(3));
83
84        check!(directory_response_decision(false, 7, Some(7)) == ControllerError);
85        check!(directory_response_decision(true, 7, Some(8)) == StaleController);
86        check!(directory_response_decision(true, 7, None) == StaleController);
87        check!(directory_response_decision(true, 7, Some(7)) == Accept);
88    }
89}
krabka_verified/directory.rs

krabka_verified/
directory.rs
