krabka_verified/
list_offsets.rs

1//! End-to-end `ListOffsets` request and visibility decisions.
2
3#[cfg(creusot)]
4use creusot_std::prelude::{DeepModel, logic};
5
6/// The meaning of one `ListOffsets` request timestamp at its wire version.
7#[krabka_macros::model_type]
8pub enum ListOffsetsKind {
9    Unsupported,
10    Earliest,
11    Latest,
12    MaxTimestamp,
13    EarliestLocal,
14    LatestTiered,
15    EarliestPendingUpload,
16    Timestamp,
17}
18
19/// KIP-320 leader-epoch admission for one partition row.
20#[krabka_macros::model_type]
21pub enum ListOffsetsEpochDecision {
22    RejectMalformed,
23    Proceed,
24    Fenced,
25    Unknown,
26}
27
28/// The offsets that select one request's isolation bound.
29#[krabka_macros::model_type]
30pub struct ListOffsetsBoundFacts {
31    pub replica_id: i32,
32    pub isolation_level: i8,
33    pub log_end: i64,
34    pub high_watermark: i64,
35    pub last_stable: i64,
36}
37
38/// A valid last-fetchable offset, or a fail-closed malformed-state result.
39#[krabka_macros::model_type]
40pub enum ListOffsetsBoundDecision {
41    RejectMalformed,
42    Bound { offset: i64 },
43}
44
45/// Local and optional cold-tier candidates for the `EARLIEST` sentinel.
46#[krabka_macros::model_type]
47pub struct ListOffsetsEarliestFacts {
48    pub local: i64,
49    pub has_remote: bool,
50    pub remote: i64,
51    pub has_diskless: bool,
52    pub diskless: i64,
53}
54
55/// One tier-specific candidate before the final visibility clamp.
56#[krabka_macros::model_type]
57pub struct ListOffsetsSelectionFacts {
58    pub kind: ListOffsetsKind,
59    pub candidate_offset: i64,
60    pub candidate_timestamp: i64,
61    pub candidate_epoch: i32,
62    pub last_fetchable: i64,
63}
64
65/// The final visible partition-row value.
66#[krabka_macros::model_type]
67pub enum ListOffsetsSelectionDecision {
68    RejectMalformed,
69    Unknown,
70    Resolved {
71        offset: i64,
72        timestamp: i64,
73        leader_epoch: i32,
74    },
75}
76
77mod selection_model;
78#[cfg(creusot)]
79pub use selection_model::list_offsets_selection_model;
80pub use selection_model::{
81    list_offsets_bound_decision, list_offsets_earliest, list_offsets_epoch_decision,
82    list_offsets_kind,
83};
84
85mod selection_decision;
86pub use selection_decision::list_offsets_selection_decision;
87
88mod timestamp_candidate;
89pub use timestamp_candidate::earliest_timestamp_candidate;
90
91#[cfg(test)]
92mod tests;
krabka_verified/list_offsets.rs

krabka_verified/
list_offsets.rs
