krabka_verified/storage/
remote_partition_delete_transition.rs

1use {
2    super::{RemoteCacheAction, RemotePartitionDeleteLifecycle, RemoteSegmentLifecycle},
3    creusot_std::prelude::*,
4};
5
6/// The forward edges of Kafka's segment lifecycle:
7/// `COPY_SEGMENT_STARTED -> COPY_SEGMENT_FINISHED | DELETE_SEGMENT_STARTED`,
8/// `COPY_SEGMENT_FINISHED -> DELETE_SEGMENT_STARTED`, and
9/// `DELETE_SEGMENT_STARTED -> DELETE_SEGMENT_FINISHED`.
10// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
11#[cfg(creusot)]
12#[cfg_attr(test, mutants::skip)]
13#[logic]
14fn segment_forward_edge(from: RemoteSegmentLifecycle, to: RemoteSegmentLifecycle) -> bool {
15    match (from, to) {
16        (RemoteSegmentLifecycle::CopyStarted, RemoteSegmentLifecycle::CopyFinished)
17        | (RemoteSegmentLifecycle::CopyStarted, RemoteSegmentLifecycle::DeleteStarted)
18        | (RemoteSegmentLifecycle::CopyFinished, RemoteSegmentLifecycle::DeleteStarted)
19        | (RemoteSegmentLifecycle::DeleteStarted, RemoteSegmentLifecycle::DeleteFinished) => true,
20        _ => false,
21    }
22}
23
24/// Kafka's `RemoteLogSegmentState.isValidTransition` for a known source state:
25/// a forward lifecycle edge, or a self transition, which Kafka admits so
26/// retries and failover stay idempotent.
27///
28/// A segment with no source state is the host's add path, which admits only
29/// `CopyStarted`.
30#[ensures(result == (from == to || segment_forward_edge(from, to)))]
31#[must_use]
32pub const fn remote_segment_transition(
33    from: RemoteSegmentLifecycle,
34    to: RemoteSegmentLifecycle,
35) -> bool {
36    matches!(
37        (from, to),
38        (
39            RemoteSegmentLifecycle::CopyStarted,
40            RemoteSegmentLifecycle::CopyStarted
41                | RemoteSegmentLifecycle::CopyFinished
42                | RemoteSegmentLifecycle::DeleteStarted
43        ) | (
44            RemoteSegmentLifecycle::CopyFinished,
45            RemoteSegmentLifecycle::CopyFinished | RemoteSegmentLifecycle::DeleteStarted
46        ) | (
47            RemoteSegmentLifecycle::DeleteStarted,
48            RemoteSegmentLifecycle::DeleteStarted | RemoteSegmentLifecycle::DeleteFinished
49        ) | (
50            RemoteSegmentLifecycle::DeleteFinished,
51            RemoteSegmentLifecycle::DeleteFinished
52        )
53    )
54}
55
56/// Classify one remote-segment cache update against the cached state, `None`
57/// when the cache holds no such segment.
58///
59/// A forward lifecycle edge stores its target: readable at `CopyFinished`,
60/// hidden at `DeleteStarted`, removed at `DeleteFinished`. An update for a
61/// missing segment is an idempotent tombstone when it is `DeleteFinished` and
62/// rejected otherwise, so an update can never resurrect a segment.
63///
64/// Kafka's `RemoteLogMetadataCache` admits every self transition. This cache
65/// is stricter: a self transition is a no-op only for an exact retry (the host
66/// compares timestamp, broker and custom metadata) and is rejected as a
67/// conflict otherwise.
68#[ensures(result == match current {
69    None => if target == RemoteSegmentLifecycle::DeleteFinished {
70        RemoteCacheAction::Noop
71    } else {
72        RemoteCacheAction::Reject
73    },
74    Some(current) => if current == target {
75        if exact_retry { RemoteCacheAction::Noop } else { RemoteCacheAction::Reject }
76    } else if segment_forward_edge(current, target) {
77        match target {
78            RemoteSegmentLifecycle::CopyFinished => RemoteCacheAction::StoreFinished,
79            RemoteSegmentLifecycle::DeleteFinished => RemoteCacheAction::Remove,
80            _ => RemoteCacheAction::StoreHidden,
81        }
82    } else {
83        RemoteCacheAction::Reject
84    },
85})]
86#[must_use]
87pub const fn remote_cache_action(
88    current: Option<RemoteSegmentLifecycle>,
89    target: RemoteSegmentLifecycle,
90    exact_retry: bool,
91) -> RemoteCacheAction {
92    match (current, target) {
93        (None, RemoteSegmentLifecycle::DeleteFinished) => RemoteCacheAction::Noop,
94        (Some(RemoteSegmentLifecycle::CopyStarted), RemoteSegmentLifecycle::CopyStarted)
95        | (Some(RemoteSegmentLifecycle::CopyFinished), RemoteSegmentLifecycle::CopyFinished)
96        | (Some(RemoteSegmentLifecycle::DeleteStarted), RemoteSegmentLifecycle::DeleteStarted)
97        | (Some(RemoteSegmentLifecycle::DeleteFinished), RemoteSegmentLifecycle::DeleteFinished) => {
98            if exact_retry {
99                RemoteCacheAction::Noop
100            } else {
101                RemoteCacheAction::Reject
102            }
103        }
104        (Some(RemoteSegmentLifecycle::CopyStarted), RemoteSegmentLifecycle::CopyFinished) => {
105            RemoteCacheAction::StoreFinished
106        }
107        (
108            Some(RemoteSegmentLifecycle::CopyStarted | RemoteSegmentLifecycle::CopyFinished),
109            RemoteSegmentLifecycle::DeleteStarted,
110        ) => RemoteCacheAction::StoreHidden,
111        (Some(RemoteSegmentLifecycle::DeleteStarted), RemoteSegmentLifecycle::DeleteFinished) => {
112            RemoteCacheAction::Remove
113        }
114        _ => RemoteCacheAction::Reject,
115    }
116}
117
118/// The forward edges of Kafka's partition-delete lifecycle:
119/// `DELETE_PARTITION_MARKED -> DELETE_PARTITION_STARTED -> DELETE_PARTITION_FINISHED`.
120// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
121#[cfg(creusot)]
122#[cfg_attr(test, mutants::skip)]
123#[logic]
124fn partition_delete_forward_edge(
125    from: RemotePartitionDeleteLifecycle,
126    to: RemotePartitionDeleteLifecycle,
127) -> bool {
128    match (from, to) {
129        (RemotePartitionDeleteLifecycle::Marked, RemotePartitionDeleteLifecycle::Started)
130        | (RemotePartitionDeleteLifecycle::Started, RemotePartitionDeleteLifecycle::Finished) => {
131            true
132        }
133        _ => false,
134    }
135}
136
137/// Kafka's `RemotePartitionDeleteState.isValidTransition`: with no prior
138/// state only `DELETE_PARTITION_MARKED` is admitted; otherwise a forward edge
139/// or an idempotent self transition.
140#[ensures(result == match from {
141    None => to == RemotePartitionDeleteLifecycle::Marked,
142    Some(from) => from == to || partition_delete_forward_edge(from, to),
143})]
144#[must_use]
145pub const fn remote_partition_delete_transition(
146    from: Option<RemotePartitionDeleteLifecycle>,
147    to: RemotePartitionDeleteLifecycle,
148) -> bool {
149    matches!(
150        (from, to),
151        (None, RemotePartitionDeleteLifecycle::Marked)
152            | (
153                Some(RemotePartitionDeleteLifecycle::Marked),
154                RemotePartitionDeleteLifecycle::Marked | RemotePartitionDeleteLifecycle::Started
155            )
156            | (
157                Some(RemotePartitionDeleteLifecycle::Started),
158                RemotePartitionDeleteLifecycle::Started | RemotePartitionDeleteLifecycle::Finished
159            )
160            | (
161                Some(RemotePartitionDeleteLifecycle::Finished),
162                RemotePartitionDeleteLifecycle::Finished
163            )
164    )
165}
krabka_verified/storage/remote_partition_delete_transition.rs

krabka_verified/storage/
remote_partition_delete_transition.rs
