krabka_verified/
break_glass.rs

1//! Break-glass proposal admission and deterministic selection.
2
3use creusot_std::prelude::*;
4
5/// First fail-closed reason that prevents a proposal from being spent.
6#[krabka_macros::model_type]
7pub enum BreakGlassAdmission {
8    Withdrawn,
9    Consumed,
10    Expired,
11    NotEnoughApprovals,
12    Unsigned,
13    Usable,
14}
15
16/// Whether the configured policy requires signed approvals for the action.
17#[krabka_macros::model_type]
18pub enum BreakGlassSignaturePolicy {
19    Optional,
20    Required,
21}
22
23/// Whether the proposal carries at least one approval and every approval
24/// carries a key id and a signature.
25#[krabka_macros::model_type]
26pub enum BreakGlassApprovalSigning {
27    AllSigned,
28    NotAllSigned,
29}
30
31/// The independent lifecycle and approval facts of one covering proposal.
32#[krabka_macros::model_type]
33pub struct BreakGlassProposalFacts {
34    pub withdrawn: bool,
35    pub consumed: bool,
36    pub expired: bool,
37    /// Distinct approving principals.
38    pub held_approvals: usize,
39    pub required_approvals: usize,
40    pub signature_policy: BreakGlassSignaturePolicy,
41    pub signing: BreakGlassApprovalSigning,
42}
43
44/// Apply the break-glass lifecycle and approval checks in reporting order:
45/// each variant holds exactly when its check fails and every earlier one
46/// passes.
47#[ensures((result == BreakGlassAdmission::Withdrawn) == facts.withdrawn)]
48#[ensures((result == BreakGlassAdmission::Consumed) == (!facts.withdrawn && facts.consumed))]
49#[ensures((result == BreakGlassAdmission::Expired) ==
50    (!facts.withdrawn && !facts.consumed && facts.expired))]
51#[ensures((result == BreakGlassAdmission::NotEnoughApprovals) ==
52    (!facts.withdrawn && !facts.consumed && !facts.expired
53        && facts.held_approvals@ < facts.required_approvals@))]
54#[ensures((result == BreakGlassAdmission::Unsigned) ==
55    (!facts.withdrawn && !facts.consumed && !facts.expired
56        && facts.held_approvals@ >= facts.required_approvals@
57        && facts.signature_policy == BreakGlassSignaturePolicy::Required
58        && facts.signing == BreakGlassApprovalSigning::NotAllSigned))]
59#[ensures((result == BreakGlassAdmission::Usable) ==
60    (!facts.withdrawn && !facts.consumed && !facts.expired
61        && facts.held_approvals@ >= facts.required_approvals@
62        && (facts.signature_policy == BreakGlassSignaturePolicy::Optional
63            || facts.signing == BreakGlassApprovalSigning::AllSigned)))]
64#[must_use]
65pub fn break_glass_admission(facts: BreakGlassProposalFacts) -> BreakGlassAdmission {
66    if facts.withdrawn {
67        BreakGlassAdmission::Withdrawn
68    } else if facts.consumed {
69        BreakGlassAdmission::Consumed
70    } else if facts.expired {
71        BreakGlassAdmission::Expired
72    } else if facts.held_approvals < facts.required_approvals {
73        BreakGlassAdmission::NotEnoughApprovals
74    } else if matches!(
75        (facts.signature_policy, facts.signing),
76        (
77            BreakGlassSignaturePolicy::Required,
78            BreakGlassApprovalSigning::NotAllSigned
79        )
80    ) {
81        BreakGlassAdmission::Unsigned
82    } else {
83        BreakGlassAdmission::Usable
84    }
85}
86
87/// Lexicographic `<=` on `(expiry, UUID high bits, UUID low bits)` keys.
88// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
89#[cfg(creusot)]
90#[cfg_attr(test, mutants::skip)]
91#[logic]
92pub fn lex_le(a: (i64, u64, u64), b: (i64, u64, u64)) -> bool {
93    pearlite! {
94        a.0@ < b.0@
95            || (a.0@ == b.0@ && (a.1@ < b.1@ || (a.1@ == b.1@ && a.2@ <= b.2@)))
96    }
97}
98
99/// `best` is the first index of a lexicographically minimal key among the
100/// first `len` keys: no key is smaller, and every earlier key is strictly
101/// greater.
102// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
103#[cfg(creusot)]
104#[cfg_attr(test, mutants::skip)]
105#[logic]
106pub fn is_min_by(keys: Seq<(i64, u64, u64)>, best: Int, len: Int) -> bool {
107    pearlite! {
108        0 <= best && best < len && len <= keys.len()
109            && (forall<j: Int> 0 <= j && j < len ==> lex_le(keys[best], keys[j]))
110            && (forall<j: Int> 0 <= j && j < best ==> !lex_le(keys[j], keys[best]))
111    }
112}
113
114/// Select the earliest `(expiry, UUID high bits, UUID low bits)` key; on an
115/// exact duplicate key, the first index wins.
116#[ensures(match result {
117    None => [email protected]() == 0,
118    Some(index) => is_min_by(candidates@, index@, [email protected]()),
119})]
120#[must_use]
121pub fn select_break_glass_candidate(candidates: &[(i64, u64, u64)]) -> Option<usize> {
122    let mut best: Option<usize> = None;
123    let mut cursor = 0usize;
124    #[invariant(cursor@ <= [email protected]())]
125    #[invariant(match best {
126        None => cursor@ == 0,
127        Some(b) => is_min_by(candidates@, b@, cursor@),
128    })]
129    #[variant([email protected]() - cursor@)]
130    while cursor < candidates.len() {
131        let Some(&candidate) = candidates.get(cursor) else {
132            break;
133        };
134        let Some(b) = best else {
135            best = Some(cursor);
136            cursor += 1;
137            continue;
138        };
139        best = match candidates.get(b) {
140            None => Some(cursor),
141            Some(&current) => {
142                if candidate.0 < current.0
143                    || (candidate.0 == current.0 && candidate.1 < current.1)
144                    || (candidate.0 == current.0
145                        && candidate.1 == current.1
146                        && candidate.2 < current.2)
147                {
148                    Some(cursor)
149                } else {
150                    Some(b)
151                }
152            }
153        };
154        cursor += 1;
155    }
156    best
157}
158
159#[cfg(test)]
160mod tests {
161    use super::*;
162
163    fn base_facts() -> BreakGlassProposalFacts {
164        BreakGlassProposalFacts {
165            withdrawn: false,
166            consumed: false,
167            expired: false,
168            held_approvals: 2,
169            required_approvals: 2,
170            signature_policy: BreakGlassSignaturePolicy::Required,
171            signing: BreakGlassApprovalSigning::AllSigned,
172        }
173    }
174
175    fn all_failing() -> BreakGlassProposalFacts {
176        BreakGlassProposalFacts {
177            withdrawn: true,
178            consumed: true,
179            expired: true,
180            held_approvals: 0,
181            signing: BreakGlassApprovalSigning::NotAllSigned,
182            ..base_facts()
183        }
184    }
185
186    #[yare::parameterized(
187        withdrawn = { all_failing(), BreakGlassAdmission::Withdrawn },
188        consumed = {
189            BreakGlassProposalFacts { withdrawn: false, ..all_failing() },
190            BreakGlassAdmission::Consumed,
191        },
192        expired = {
193            BreakGlassProposalFacts { withdrawn: false, consumed: false, ..all_failing() },
194            BreakGlassAdmission::Expired,
195        },
196        insufficient_approvals = {
197            BreakGlassProposalFacts { held_approvals: 1, ..base_facts() },
198            BreakGlassAdmission::NotEnoughApprovals,
199        },
200        unsigned = {
201            BreakGlassProposalFacts { signing: BreakGlassApprovalSigning::NotAllSigned, ..base_facts() },
202            BreakGlassAdmission::Unsigned,
203        },
204        optional_unsigned = {
205            BreakGlassProposalFacts {
206                signature_policy: BreakGlassSignaturePolicy::Optional,
207                signing: BreakGlassApprovalSigning::NotAllSigned,
208                ..base_facts()
209            },
210            BreakGlassAdmission::Usable,
211        },
212        admitted = { base_facts(), BreakGlassAdmission::Usable },
213        extra_approvals = {
214            BreakGlassProposalFacts { held_approvals: 3, ..base_facts() },
215            BreakGlassAdmission::Usable,
216        },
217    )]
218    fn break_glass_checks_are_ordered_and_fail_closed(
219        facts: BreakGlassProposalFacts,
220        expected: BreakGlassAdmission,
221    ) {
222        assert2::assert!(break_glass_admission(facts) == expected);
223    }
224
225    #[yare::parameterized(
226        empty = { &[][..], None },
227        earliest_expiry = { &[(20, 0, 0), (10, 9, 9)][..], Some(1) },
228        uuid_high = { &[(10, 4, 9), (10, 3, 99)][..], Some(1) },
229        uuid_low = { &[(10, 3, 9), (10, 3, 8)][..], Some(1) },
230        earlier_expiry = { &[(10, 3, 9), (20, 2, 8)][..], Some(0) },
231        expiry_tie = { &[(10, 3, 9), (20, 3, 2)][..], Some(0) },
232        earlier_uuid = { &[(10, 3, 9), (10, 4, 2)][..], Some(0) },
233        duplicate_keeps_first = { &[(10, 3, 8), (10, 3, 8)][..], Some(0) },
234        duplicate_after_lesser = { &[(30, 0, 0), (10, 3, 8), (10, 3, 8)][..], Some(1) },
235    )]
236    fn proposal_selection_uses_expiry_then_uuid_then_first_index(
237        candidates: &[(i64, u64, u64)],
238        expected: Option<usize>,
239    ) {
240        assert2::assert!(select_break_glass_candidate(candidates) == expected);
241    }
242}
krabka_verified/break_glass.rs

krabka_verified/
break_glass.rs
