krabka_verified/
diskless.rs

1//! Pure local-trim decision for the diskless WAL flusher.
2
3use creusot_std::prelude::*;
4
5/// Whether and where to advance one diskless partition's local log start.
6#[krabka_macros::model_type]
7pub struct DisklessTrimDecision {
8    pub should_trim: bool,
9    pub target: i64,
10}
11
12/// One decoded-batch step in a diskless cold-read run.
13#[krabka_macros::model_type]
14pub enum DisklessBatchStep {
15    Invalid,
16    Skip(usize),
17    Start(usize),
18    Continue(usize),
19    Stop,
20}
21
22/// One diskless partition's retention configuration and floor, read at `now_ms`.
23#[krabka_macros::model_type(proof(std::clone::Clone, Copy))]
24pub struct DisklessRetentionPolicy {
25    /// `retention.ms`, or `None` for Kafka's unlimited sentinel.
26    pub retention_ms: Option<i64>,
27    /// `retention.bytes`, or `None` for Kafka's unlimited sentinel.
28    pub retention_bytes: Option<u64>,
29    /// The `DeleteRecords` floor.
30    pub log_start_offset: i64,
31    pub now_ms: i64,
32}
33
34mod logical_range;
35pub use logical_range::{
36    diskless_logical_range, diskless_object_reclaimable, diskless_retention_prefix,
37};
38#[cfg(creusot)]
39pub use logical_range::{expirable, indexed_bytes, size_debt_before};
40
41mod trim_decision;
42pub use trim_decision::{diskless_batch_step, diskless_span_extension, diskless_trim_decision};
43
44#[cfg(test)]
45mod tests;
krabka_verified/diskless.rs

krabka_verified/
diskless.rs
