krabka_verified/
producer_id.rs

1//! Producer-ID block allocation fencing and exact range construction.
2
3use creusot_std::prelude::*;
4
5#[krabka_macros::model_type]
6pub struct ProducerIdBlockPlan {
7    pub first: i64,
8    pub len: i32,
9    pub next: i64,
10}
11
12#[krabka_macros::model_type]
13pub enum ProducerIdBlockAllocationDecision {
14    BrokerNotRegistered,
15    StaleBrokerEpoch,
16    InvalidFrontier,
17    Exhausted,
18    Allocate(ProducerIdBlockPlan),
19}
20
21/// Fence one broker generation and construct its exact positive contiguous
22/// producer-ID block without signed overflow.
23#[ensures(match result {
24    ProducerIdBlockAllocationDecision::BrokerNotRegistered =>
25        !broker_id_valid || !broker_registered,
26    ProducerIdBlockAllocationDecision::StaleBrokerEpoch =>
27        broker_id_valid && broker_registered
28            && (requested_broker_epoch@ < 0
29                || registered_broker_epoch@ < 0
30                || requested_broker_epoch@ != registered_broker_epoch@),
31    ProducerIdBlockAllocationDecision::InvalidFrontier =>
32        broker_id_valid && broker_registered
33            && requested_broker_epoch@ >= 0
34            && requested_broker_epoch@ == registered_broker_epoch@
35            && (first@ < 0 || block_len@ <= 0),
36    ProducerIdBlockAllocationDecision::Exhausted =>
37        broker_id_valid && broker_registered
38            && requested_broker_epoch@ >= 0
39            && requested_broker_epoch@ == registered_broker_epoch@
40            && first@ >= 0 && block_len@ > 0
41            && first@ + block_len@ > i64::MAX@,
42    ProducerIdBlockAllocationDecision::Allocate(plan) =>
43        broker_id_valid && broker_registered
44            && requested_broker_epoch@ >= 0
45            && requested_broker_epoch@ == registered_broker_epoch@
46            && plan.first@ == first@
47            && plan.len@ == block_len@
48            && plan.next@ == first@ + block_len@
49            && plan.first@ >= 0
50            && plan.len@ > 0
51            && plan.first@ < plan.next@
52            && plan.next@ <= i64::MAX@,
53})]
54#[must_use]
55pub fn producer_id_block_allocation(
56    broker_id_valid: bool,
57    broker_registered: bool,
58    requested_broker_epoch: i64,
59    registered_broker_epoch: i64,
60    first: i64,
61    block_len: i32,
62) -> ProducerIdBlockAllocationDecision {
63    if !broker_id_valid || !broker_registered {
64        return ProducerIdBlockAllocationDecision::BrokerNotRegistered;
65    }
66    if requested_broker_epoch < 0
67        || registered_broker_epoch < 0
68        || requested_broker_epoch != registered_broker_epoch
69    {
70        return ProducerIdBlockAllocationDecision::StaleBrokerEpoch;
71    }
72    if first < 0 || block_len <= 0 {
73        return ProducerIdBlockAllocationDecision::InvalidFrontier;
74    }
75    let Some(next) = first.checked_add(i64::from(block_len)) else {
76        return ProducerIdBlockAllocationDecision::Exhausted;
77    };
78    ProducerIdBlockAllocationDecision::Allocate(ProducerIdBlockPlan {
79        first,
80        len: block_len,
81        next,
82    })
83}
84
85#[cfg(test)]
86mod tests {
87    use {
88        super::{
89            ProducerIdBlockAllocationDecision, ProducerIdBlockPlan, producer_id_block_allocation,
90        },
91        assert2::assert,
92    };
93
94    #[test]
95    fn allocation_fences_broker_and_builds_only_exact_positive_blocks() {
96        use ProducerIdBlockAllocationDecision::{
97            Allocate, BrokerNotRegistered, Exhausted, InvalidFrontier, StaleBrokerEpoch,
98        };
99
100        assert!(producer_id_block_allocation(false, true, 3, 3, 0, 1_000) == BrokerNotRegistered);
101        assert!(producer_id_block_allocation(true, false, 3, 3, 0, 1_000) == BrokerNotRegistered);
102        assert!(producer_id_block_allocation(true, true, -1, 3, 0, 1_000) == StaleBrokerEpoch);
103        assert!(producer_id_block_allocation(true, true, 1, -1, 0, 1_000) == StaleBrokerEpoch);
104        assert!(producer_id_block_allocation(true, true, 2, 3, 0, 1_000) == StaleBrokerEpoch);
105        assert!(
106            producer_id_block_allocation(true, true, 0, 0, 0, 1_000)
107                == Allocate(ProducerIdBlockPlan {
108                    first: 0,
109                    len: 1_000,
110                    next: 1_000,
111                })
112        );
113        assert!(producer_id_block_allocation(true, true, 3, 3, -1, 1_000) == InvalidFrontier);
114        assert!(producer_id_block_allocation(true, true, 3, 3, 0, 0) == InvalidFrontier);
115        assert!(producer_id_block_allocation(true, true, 3, 3, i64::MAX - 999, 1_000) == Exhausted);
116        assert!(
117            producer_id_block_allocation(true, true, 3, 3, i64::MAX - 1_000, 1_000)
118                == Allocate(ProducerIdBlockPlan {
119                    first: i64::MAX - 1_000,
120                    len: 1_000,
121                    next: i64::MAX,
122                })
123        );
124    }
125}
krabka_verified/producer_id.rs

krabka_verified/
producer_id.rs
