krabka_verified/
recovery.rs

1//! Controller recovery replay-bound decisions.
2
3use creusot_std::prelude::*;
4
5/// Whether controller recovery replays one metadata record.
6#[krabka_macros::model_type]
7pub enum ReplayRecordDecision {
8    /// Apply the record, which sits at this absolute offset.
9    Apply(i64),
10    /// Skip the record.
11    Skip,
12}
13
14/// Whether a replay loop advances its cursor, and to where.
15#[krabka_macros::model_type]
16pub enum ReplayCursorDecision {
17    /// Continue replay from this exclusive next offset.
18    Advance(i64),
19    /// End replay.
20    Stop,
21}
22
23/// The keyed barrier-state record that recovery is folding.
24#[krabka_macros::model_type]
25pub enum BarrierRecoveryRecordKind {
26    Group,
27    InjectionStart,
28    Cut,
29}
30
31/// The only state mutation one ordered barrier record may perform.
32#[krabka_macros::model_type]
33pub enum BarrierRecoveryFoldAction {
34    DefineGroup,
35    RemoveGroup,
36    SetPending,
37    KeepPending,
38    ClearPending,
39    UpsertCut { retire_pending: bool },
40    RemoveCut,
41}
42
43/// Whether recovery may close an interrupted barrier injection.
44#[krabka_macros::model_type]
45pub enum BarrierRecoveryFinalizeDecision {
46    NoPending,
47    MalformedPending,
48    UnknownCoordinator,
49    FencedCoordinator,
50    FinalizePartial,
51}
52
53mod replay_cursor_decision;
54#[cfg(creusot)]
55pub use replay_cursor_decision::replay_record_admitted;
56pub use replay_cursor_decision::{
57    barrier_recovery_finalize_decision, barrier_recovery_fold_action, replay_cursor_decision,
58    replay_record_decision,
59};
60
61mod should_capture_first_downgrade;
62pub use should_capture_first_downgrade::{
63    replay_batch_cursor_decision, should_capture_first_downgrade,
64};
65
66#[cfg(test)]
67mod tests;
krabka_verified/recovery.rs

krabka_verified/
recovery.rs
