krabka_verified/
compaction.rs

1//! KIP-534 log-compaction decision core.
2//!
3//! This core comes out of `krabka-log`, so that Creusot can verify it. The host
4//! crate re-exports these functions, and the stateright model in
5//! `krabka-log/src/compact_model.rs` drives these exact functions.
6
7use creusot_std::prelude::*;
8
9/// Per-record facts the retain decision needs.
10#[krabka_macros::model_type]
11pub struct RecordMeta {
12    /// Whether the record has a key.
13    pub has_key: bool,
14    /// Whether the record has a non-null value.
15    pub has_value: bool,
16}
17
18/// Per-batch facts the retain decision needs.
19#[krabka_macros::model_type]
20pub struct BatchMeta {
21    /// Whether the batch is a transactional control batch.
22    pub is_control: bool,
23    /// Producer id for transactional batches. It is negative for
24    /// non-transactional batches.
25    pub producer_id: i64,
26    /// The batch's existing delete horizon, which is `base_timestamp` when bit
27    /// 6 is set. It is `None` if the batch has never been stamped.
28    pub existing_horizon: Option<i64>,
29}
30
31/// Whether the cleaner read data of a control marker's own transaction in this
32/// pass. This is Kafka's per-transaction rule (`CleanedTransactionMetadata`),
33/// not a per-producer one.
34#[krabka_macros::model_type]
35pub enum TxnDataState {
36    /// `producer_id < 0`: not a transactional producer.
37    NotTransactional,
38    /// The pass read at least one batch of this marker's transaction, so the
39    /// marker stays.
40    DataSurvives,
41    /// The pass read no batch of this marker's transaction, so the marker may
42    /// age out through the delete horizon.
43    DataFullyGone,
44}
45
46/// What to do with a record during the rewrite pass.
47#[krabka_macros::model_type]
48pub enum RetainDecision {
49    /// Keep the record as-is.
50    Keep,
51    /// Keep the record, but stamp its batch with this delete horizon:
52    /// `base_timestamp = horizon`, with bit 6 set.
53    SetHorizon(i64),
54    /// Drop the record.
55    Delete,
56}
57
58/// Whether a compaction batch-stream decode is complete, made progress, or
59/// encountered corrupt input.
60#[krabka_macros::model_type]
61pub enum CompactionDecodeStep {
62    /// The input is exhausted. This is the only successful completion state.
63    Done,
64    /// One batch decoded and consumed at least one byte.
65    Continue,
66    /// Nonempty input did not decode with strict progress.
67    Corrupt,
68}
69
70mod retain_decision;
71#[cfg(creusot)]
72pub use retain_decision::compute_horizon_model;
73pub use retain_decision::{compaction_decode_step, compute_horizon, retain_decision};
74
75#[cfg(test)]
76mod tests;
krabka_verified/compaction.rs

krabka_verified/
compaction.rs
