krabka_verified/
break_glass_persistence.rs

1//! Break-glass consumption and local-action persistence decisions.
2
3use creusot_std::prelude::*;
4
5/// How the incoming consume relates to the committed proposal image.
6#[krabka_macros::model_type]
7pub enum BreakGlassProposalState {
8    Missing,
9    Stale,
10    ExactPending,
11}
12
13/// Facts checked before a consumed proposal enters the metadata log.
14#[krabka_macros::model_type]
15pub struct BreakGlassConsumptionFacts {
16    pub proposal: BreakGlassProposalState,
17    pub consumed_at_ms: i64,
18    pub uncommitted_tail: bool,
19}
20
21/// Why a consumed proposal may or may not enter the metadata log.
22#[krabka_macros::model_type]
23pub enum BreakGlassConsumptionDecision {
24    Missing,
25    Malformed,
26    Stale,
27    InFlight,
28    Append,
29}
30
31/// Admit only an exact, positive-timestamp mutation of the current pending
32/// proposal, with no uncommitted metadata tail.
33///
34/// Every refusal reports the first failing check, in this order: a missing
35/// proposal, a nonpositive consumption timestamp (`0` is the unconsumed
36/// sentinel), a stale proposal, then an uncommitted tail.
37#[ensures((result == BreakGlassConsumptionDecision::Missing) ==
38    (facts.proposal == BreakGlassProposalState::Missing))]
39#[ensures((result == BreakGlassConsumptionDecision::Malformed) ==
40    (facts.proposal != BreakGlassProposalState::Missing && facts.consumed_at_ms@ <= 0))]
41#[ensures((result == BreakGlassConsumptionDecision::Stale) ==
42    (facts.proposal == BreakGlassProposalState::Stale && facts.consumed_at_ms@ > 0))]
43#[ensures((result == BreakGlassConsumptionDecision::InFlight) == (
44    facts.proposal == BreakGlassProposalState::ExactPending
45        && facts.consumed_at_ms@ > 0
46        && facts.uncommitted_tail
47))]
48#[ensures((result == BreakGlassConsumptionDecision::Append) == (
49    facts.proposal == BreakGlassProposalState::ExactPending
50        && facts.consumed_at_ms@ > 0
51        && !facts.uncommitted_tail
52))]
53#[must_use]
54pub fn break_glass_consumption_decision(
55    facts: BreakGlassConsumptionFacts,
56) -> BreakGlassConsumptionDecision {
57    match facts.proposal {
58        BreakGlassProposalState::Missing => BreakGlassConsumptionDecision::Missing,
59        BreakGlassProposalState::Stale => {
60            if facts.consumed_at_ms <= 0 {
61                BreakGlassConsumptionDecision::Malformed
62            } else {
63                BreakGlassConsumptionDecision::Stale
64            }
65        }
66        BreakGlassProposalState::ExactPending => {
67            if facts.consumed_at_ms <= 0 {
68                BreakGlassConsumptionDecision::Malformed
69            } else if facts.uncommitted_tail {
70                BreakGlassConsumptionDecision::InFlight
71            } else {
72                BreakGlassConsumptionDecision::Append
73            }
74        }
75    }
76}
77
78/// Durable-spend state for an action outside the metadata log.
79#[krabka_macros::model_type]
80pub enum BreakGlassLocalSpendState {
81    Ungated,
82    MissingOrMismatched,
83    Pending,
84    Committed,
85}
86
87/// Facts checked before an action outside the metadata log may start.
88#[krabka_macros::model_type]
89pub struct BreakGlassLocalActionFacts {
90    pub spend: BreakGlassLocalSpendState,
91    pub commit_succeeded: bool,
92}
93
94/// Whether a privileged local action may start.
95#[krabka_macros::model_type]
96pub enum BreakGlassLocalActionDecision {
97    Reject,
98    Apply,
99}
100
101/// Permit an ungated action, a retry whose spend already committed, or an
102/// exactly bound consume whose commit just succeeded. Every other order fails
103/// closed.
104#[ensures((result == BreakGlassLocalActionDecision::Apply) == (
105    facts.spend == BreakGlassLocalSpendState::Ungated
106        || facts.spend == BreakGlassLocalSpendState::Committed
107        || (facts.spend == BreakGlassLocalSpendState::Pending && facts.commit_succeeded)
108))]
109#[must_use]
110pub fn break_glass_local_action_decision(
111    facts: BreakGlassLocalActionFacts,
112) -> BreakGlassLocalActionDecision {
113    match facts.spend {
114        BreakGlassLocalSpendState::Ungated | BreakGlassLocalSpendState::Committed => {
115            BreakGlassLocalActionDecision::Apply
116        }
117        BreakGlassLocalSpendState::Pending if facts.commit_succeeded => {
118            BreakGlassLocalActionDecision::Apply
119        }
120        BreakGlassLocalSpendState::MissingOrMismatched | BreakGlassLocalSpendState::Pending => {
121            BreakGlassLocalActionDecision::Reject
122        }
123    }
124}
125
126#[cfg(test)]
127mod tests {
128    use super::{
129        BreakGlassConsumptionDecision, BreakGlassConsumptionFacts, BreakGlassLocalActionDecision,
130        BreakGlassLocalActionFacts, BreakGlassLocalSpendState, BreakGlassProposalState,
131        break_glass_consumption_decision, break_glass_local_action_decision,
132    };
133
134    fn exact_pending() -> BreakGlassConsumptionFacts {
135        BreakGlassConsumptionFacts {
136            proposal: BreakGlassProposalState::ExactPending,
137            consumed_at_ms: i64::MAX,
138            uncommitted_tail: false,
139        }
140    }
141
142    #[yare::parameterized(
143        missing = {
144            BreakGlassConsumptionFacts { proposal: BreakGlassProposalState::Missing, ..exact_pending() },
145            BreakGlassConsumptionDecision::Missing,
146        },
147        zero_timestamp = {
148            BreakGlassConsumptionFacts { consumed_at_ms: 0, ..exact_pending() },
149            BreakGlassConsumptionDecision::Malformed,
150        },
151        missing_precedes_tail = {
152            BreakGlassConsumptionFacts {
153                proposal: BreakGlassProposalState::Missing,
154                consumed_at_ms: 0,
155                uncommitted_tail: true,
156            },
157            BreakGlassConsumptionDecision::Missing,
158        },
159        negative_timestamp = {
160            BreakGlassConsumptionFacts { consumed_at_ms: -1, uncommitted_tail: true, ..exact_pending() },
161            BreakGlassConsumptionDecision::Malformed,
162        },
163        stale_zero_timestamp = {
164            BreakGlassConsumptionFacts {
165                proposal: BreakGlassProposalState::Stale,
166                consumed_at_ms: 0,
167                ..exact_pending()
168            },
169            BreakGlassConsumptionDecision::Malformed,
170        },
171        stale = {
172            BreakGlassConsumptionFacts { proposal: BreakGlassProposalState::Stale, ..exact_pending() },
173            BreakGlassConsumptionDecision::Stale,
174        },
175        stale_with_tail = {
176            BreakGlassConsumptionFacts {
177                proposal: BreakGlassProposalState::Stale,
178                uncommitted_tail: true,
179                ..exact_pending()
180            },
181            BreakGlassConsumptionDecision::Stale,
182        },
183        in_flight = {
184            BreakGlassConsumptionFacts { uncommitted_tail: true, ..exact_pending() },
185            BreakGlassConsumptionDecision::InFlight,
186        },
187    )]
188    fn consumption_requires_the_exact_current_proposal_and_no_uncommitted_tail(
189        facts: BreakGlassConsumptionFacts,
190        expected: BreakGlassConsumptionDecision,
191    ) {
192        assert2::check!(break_glass_consumption_decision(facts) == expected);
193    }
194
195    #[yare::parameterized(
196        ungated = {
197            BreakGlassLocalActionFacts { spend: BreakGlassLocalSpendState::Ungated, commit_succeeded: false },
198            BreakGlassLocalActionDecision::Apply,
199        },
200        pending_commit = {
201            BreakGlassLocalActionFacts { spend: BreakGlassLocalSpendState::Pending, commit_succeeded: true },
202            BreakGlassLocalActionDecision::Apply,
203        },
204        committed = {
205            BreakGlassLocalActionFacts { spend: BreakGlassLocalSpendState::Committed, commit_succeeded: false },
206            BreakGlassLocalActionDecision::Apply,
207        },
208        pending_uncommitted = {
209            BreakGlassLocalActionFacts { spend: BreakGlassLocalSpendState::Pending, commit_succeeded: false },
210            BreakGlassLocalActionDecision::Reject,
211        },
212        mismatched = {
213            BreakGlassLocalActionFacts {
214                spend: BreakGlassLocalSpendState::MissingOrMismatched,
215                commit_succeeded: true,
216            },
217            BreakGlassLocalActionDecision::Reject,
218        },
219    )]
220    fn local_actions_run_only_after_a_matching_durable_spend(
221        facts: BreakGlassLocalActionFacts,
222        expected: BreakGlassLocalActionDecision,
223    ) {
224        assert2::check!(break_glass_local_action_decision(facts) == expected);
225    }
226}
krabka_verified/break_glass_persistence.rs

krabka_verified/
break_glass_persistence.rs
