krabka_verified/
raft.rs

1//! Pure `KRaft` offset-frontier and half-open-window kernels.
2
3#[cfg(creusot)]
4use creusot_std::prelude::*;
5
6/// The only response-derived mutation an admitted `KRaft` Fetch may perform.
7#[krabka_macros::model_type]
8pub enum FetchResponseMutation {
9    /// The response belongs to another leader, role, or epoch, or carries an
10    /// error; apply nothing.
11    Reject,
12    /// Attach to the advertised leader and refetch from it. The responder's
13    /// identity plays no part: the host reaches the leader through the
14    /// leader's own `NodeEndpoints` entry or its voter-set listener.
15    Discover,
16    Snapshot,
17    Truncate,
18    Append,
19    HighWatermark,
20}
21
22/// The receiving node's live fence for one Fetch response.
23#[krabka_macros::model_type]
24pub struct FetchFence {
25    /// The node is an observer with no known leader.
26    pub discovering: bool,
27    /// The leader the live role fetches from.
28    pub role_leader: Option<u64>,
29    /// The leader in the durable quorum state.
30    pub current_leader: Option<u64>,
31    pub current_epoch: u32,
32}
33
34/// Who answered a Fetch, and which leader, epoch and error the answer names.
35#[krabka_macros::model_type]
36pub struct FetchResponseFacts {
37    /// The node the request was sent to.
38    pub from: u64,
39    /// The response's `CurrentLeader.LeaderId`, `None` for Kafka's -1.
40    pub leader: Option<u64>,
41    /// The response's `CurrentLeader.LeaderEpoch`.
42    pub epoch: u32,
43    /// The partition's `ErrorCode` is `NONE`. A Kafka `KRaft` replica answers
44    /// `NONE` only as the leader of its epoch; any other replica answers
45    /// `validateLeaderOnlyRequest`'s error with the leader it knows.
46    pub error_none: bool,
47}
48
49/// Which mutations the response body carries.
50#[krabka_macros::model_type]
51pub struct FetchContent {
52    pub has_snapshot: bool,
53    pub has_divergence: bool,
54    pub has_records: bool,
55}
56
57mod metadata_record_offset_deltas;
58pub use metadata_record_offset_deltas::{
59    advance_high_watermark, control_history_frontier, fetch_response_mutation, frontier_reaches,
60    in_half_open_window, metadata_record_offset_deltas,
61};
62#[cfg(creusot)]
63pub use metadata_record_offset_deltas::{discovery_applies, leader_fence_holds};
64
65#[cfg(test)]
66mod tests;
krabka_verified/raft.rs

krabka_verified/
raft.rs
