krabka_verified/
storage.rs

1//! Storage-transition admission decisions.
2
3use creusot_std::prelude::*;
4
5/// Segment-prefix and active-segment selection for a tail truncation.
6#[krabka_macros::model_type]
7pub struct LocalTruncationPlan {
8    pub retained_sealed: usize,
9    pub keep_active: bool,
10}
11
12/// KIP-405 `RemoteLogSegmentState`, shared by every remote-segment kernel so
13/// the host maps its state onto one type.
14#[cfg_attr(creusot, derive(std::clone::Clone, Copy, DeepModel))]
15#[cfg_attr(
16    not(creusot),
17    derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)
18)]
19pub enum RemoteSegmentLifecycle {
20    CopyStarted,
21    CopyFinished,
22    DeleteStarted,
23    DeleteFinished,
24}
25
26/// KIP-405 `RemotePartitionDeleteState`.
27#[krabka_macros::model_type]
28pub enum RemotePartitionDeleteLifecycle {
29    Marked,
30    Started,
31    Finished,
32}
33
34/// Mutation of the primary remote-metadata cache and its derived epoch index.
35#[krabka_macros::model_type]
36pub enum RemoteCacheAction {
37    /// Reject a stale, conflicting, or resurrection attempt.
38    Reject,
39    /// Preserve state for an exact retry or an already-absent tombstone.
40    Noop,
41    /// Store the new readable state and index it in the derived epoch index.
42    StoreFinished,
43    /// Store a non-readable state and drop it from the derived epoch index.
44    StoreHidden,
45    /// Remove primary state, and with it any epoch-index entries.
46    Remove,
47}
48
49mod future_log_swap_admission;
50pub use future_log_swap_admission::{
51    future_log_swap_admission, local_append_coordinates, local_truncation_plan,
52    truncation_batch_retained, truncation_frontier, truncation_relative_offset,
53};
54
55mod remote_partition_delete_transition;
56pub use remote_partition_delete_transition::{
57    remote_cache_action, remote_partition_delete_transition, remote_segment_transition,
58};
59
60#[cfg(test)]
61mod tests;
krabka_verified/storage.rs

krabka_verified/
storage.rs
