krabka_verified/
producer.rs

1//! Idempotent-producer sequence arithmetic and deduplication decision.
2
3use creusot_std::prelude::*;
4
5/// The sequence range of one batch a producer's entry retains: Kafka's
6/// `BatchMetadata` `firstSeq` and `lastSeq`.
7#[krabka_macros::model_type]
8pub struct RetainedSequenceRange {
9    pub base_sequence: i32,
10    pub last_sequence: i32,
11}
12
13/// The fields of one producer's tracked entry that the sequence check reads.
14#[krabka_macros::model_type]
15pub struct ProducerEntryFacts {
16    /// The entry's producer epoch.
17    pub epoch: i16,
18    /// The last sequence the entry accepted.
19    pub last_sequence: i32,
20}
21
22/// Result of classifying an idempotent-producer batch.
23#[krabka_macros::model_type]
24pub enum ProducerDecision {
25    Append,
26    /// The batch repeats the retained batch at this index of the slice the
27    /// caller passed.
28    Duplicate {
29        retained: usize,
30    },
31    OutOfOrder,
32    Fenced,
33}
34
35mod sequence_decision;
36pub use sequence_decision::{decrement_sequence, increment_sequence};
37#[cfg(creusot)]
38pub use sequence_decision::{
39    first_retained_duplicate, retained_duplicate_exists, retained_matches, sequence_decision,
40    sequence_modulo_2_31,
41};
42
43mod decision;
44pub use decision::producer_decision;
45
46mod completion;
47pub use completion::producer_completion_window;
48#[cfg(creusot)]
49pub(crate) use completion::{completion_epoch_accepts, completion_window_bounded};
50#[cfg(creusot)]
51pub use completion::{completion_offset, completion_source_selected};
52
53#[cfg(test)]
54mod tests;
krabka_verified/producer.rs

krabka_verified/
producer.rs
