krabka_verified/
barrier.rs

1//! Barrier target, marker-fence, and cut-classification decisions.
2
3#[cfg(creusot)]
4use creusot_std::prelude::{DeepModel, logic};
5
6/// The result of adding one topic's partitions to a frozen target count.
7#[krabka_macros::model_type]
8pub enum BarrierTargetCountDecision {
9    Malformed,
10    Overflow,
11    Expand { next: i64 },
12}
13
14/// Facts that bind a marker append to one installed leadership generation.
15#[krabka_macros::model_type]
16pub struct BarrierMarkerFenceFacts {
17    pub image_present: bool,
18    pub expected_leader: u64,
19    pub expected_epoch: i32,
20    pub image_leader: u64,
21    pub image_epoch: i32,
22    pub current_leader: u64,
23    pub current_epoch: i32,
24}
25
26/// Whether one marker append is admitted by the leader and epoch fence.
27#[krabka_macros::model_type]
28pub enum BarrierMarkerFenceDecision {
29    Malformed,
30    NotLeader,
31    FencedEpoch,
32    Append,
33}
34
35/// Whether one successful marker response may enter the cut.
36#[krabka_macros::model_type]
37pub enum BarrierPlacementDecision {
38    Reject,
39    Accept,
40}
41
42/// The status derived from the exact missing-target set.
43#[krabka_macros::model_type]
44pub enum BarrierCutClassification {
45    Complete,
46    Partial,
47}
48
49mod cut_classification;
50pub use cut_classification::{
51    barrier_cut_classification, barrier_marker_fence_decision, barrier_placement_decision,
52    barrier_target_count_decision,
53};
54
55#[cfg(test)]
56mod tests;
krabka_verified/barrier.rs

krabka_verified/
barrier.rs
