krabka_verified/
retention.rs

1//! Retention-prefix selection for the local log and the remote tier.
2//!
3//! Kafka deletes retained-away segments oldest first and stops at the first
4//! segment it keeps, so every selection here is a contiguous prefix. The local
5//! walk and the remote walk combine their predicates differently, because
6//! Kafka does: `UnifiedLog.deleteOldSegments` runs separate passes over the
7//! local log, while `RemoteLogManager`'s `RemoteLogRetentionHandler` checks
8//! every predicate per remote segment. Each walk is proved equal to a
9//! reference fold that states the Kafka rule.
10
11use creusot_std::prelude::*;
12
13/// What the local retention walk knows about one local segment.
14#[krabka_macros::model_type(proof(std::clone::Clone, Copy))]
15pub struct LocalRetentionSegment {
16    /// No pass may delete this segment, and every pass stops at it. The host
17    /// sets it for a segment that holds a record whose delivery time has not
18    /// arrived, or for a tiered segment that the remote tier does not cover
19    /// whole. It plays the part of Kafka's high-watermark bound and its
20    /// `isSegmentEligibleForDeletion` check.
21    pub blocked: bool,
22    /// The segment breaches `retention.ms`, or it lies wholly below the log
23    /// start offset.
24    pub expired: bool,
25    /// The segment's exact size in bytes.
26    pub size: u64,
27}
28
29/// What the remote retention walk knows about one finished remote segment.
30#[krabka_macros::model_type(proof(std::clone::Clone, Copy))]
31pub struct RemoteRetentionSegment {
32    /// A scheduled batch is not due, or its activation cannot be established.
33    /// Every retention axis stops before this segment.
34    pub blocked: bool,
35    /// The segment's whole offset range lies below the log start offset.
36    pub log_start_breached: bool,
37    /// The segment breaches `retention.ms`.
38    pub time_expired: bool,
39    /// The segment's exact size in bytes.
40    pub size: u64,
41}
42
43mod remote_retention_model;
44pub use remote_retention_model::{barrier_cut_expired, local_retention_prefix};
45#[cfg(creusot)]
46pub use remote_retention_model::{
47    local_retention_limit, local_retention_model, remote_retention_model,
48};
49
50mod delete_target;
51pub use delete_target::{remote_retention_prefix, retention_delete_target};
52
53mod coverage;
54pub use coverage::remote_covered_through;
55#[cfg(creusot)]
56pub use coverage::{remote_covers_offset, remote_ranges_valid};
57
58#[cfg(creusot)]
59mod local_bytes;
60#[cfg(creusot)]
61pub use local_bytes::{local_prefix_bytes, local_prefix_bytes_monotone};
62
63#[cfg(creusot)]
64mod remote_bytes;
65#[cfg(creusot)]
66pub use remote_bytes::remote_prefix_charge;
67
68mod remote_floor;
69pub use remote_floor::remote_retention_floor_step;
70
71// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
72#[cfg(creusot)]
73#[cfg_attr(test, mutants::skip)]
74#[logic(open)]
75/// Size retention consumes a row only while positive debt funds its entire charged prefix.
76pub fn remote_charge_funded(debt: Int, charged: Int, next_charge: Int) -> bool {
77    pearlite! { debt > 0 && charged < debt && next_charge <= debt }
78}
79
80#[cfg(test)]
81mod tests;
krabka_verified/retention.rs

krabka_verified/
retention.rs
