krabka_verified/
scram.rs

1//! SCRAM credential alteration planning decisions.
2
3use creusot_std::prelude::*;
4
5/// Credential operation represented by one KIP-554 request row.
6#[krabka_macros::model_type]
7pub enum ScramAlterationKind {
8    Delete,
9    Upsert,
10}
11
12/// State left by an earlier row for the same user.
13#[krabka_macros::model_type]
14pub enum ScramPriorState {
15    Unseen,
16    Accepted,
17    Rejected,
18}
19
20/// Scalar facts projected from one request row and the current metadata image.
21#[krabka_macros::model_type]
22pub struct ScramAlterationFacts {
23    pub kind: ScramAlterationKind,
24    pub prior: ScramPriorState,
25    pub authorized: bool,
26    pub name_empty: bool,
27    pub mechanism: i8,
28    pub iterations: i32,
29    pub min_iterations: i32,
30    pub max_iterations: i32,
31    pub deletion_target_exists: bool,
32}
33
34/// The first applicable Kafka error, or the mechanism of one accepted row.
35#[krabka_macros::model_type]
36pub enum ScramAlterationDecision {
37    KeepPriorError,
38    Duplicate,
39    Unauthorized,
40    EmptyName,
41    UnsupportedMechanism,
42    TooFewIterations,
43    TooManyIterations,
44    MissingCredential,
45    AcceptSha256,
46    AcceptSha512,
47}
48
49// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
50#[cfg(creusot)]
51#[cfg_attr(test, mutants::skip)]
52#[logic(open)]
53fn alteration_mechanism_admitted(facts: ScramAlterationFacts) -> bool {
54    pearlite! { alteration_name_admitted(facts)
55    && (facts.mechanism@ == 1 || facts.mechanism@ == 2) }
56}
57
58// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
59#[cfg(creusot)]
60#[cfg_attr(test, mutants::skip)]
61#[logic(open)]
62pub fn alteration_name_admitted(facts: ScramAlterationFacts) -> bool {
63    pearlite! { facts.prior == ScramPriorState::Unseen
64    && facts.authorized
65    && !facts.name_empty }
66}
67
68/// Apply KIP-554 validation and conflict rules in their response precedence.
69///
70/// A prior failure is sticky. A prior accepted row becomes a duplicate and
71/// cancels that pending success. Only the two `Accept` variants authorize the
72/// adapter to create one metadata record.
73#[ensures(match result {
74    ScramAlterationDecision::KeepPriorError => facts.prior == ScramPriorState::Rejected,
75    ScramAlterationDecision::Duplicate => facts.prior == ScramPriorState::Accepted,
76    ScramAlterationDecision::Unauthorized => {
77        facts.prior == ScramPriorState::Unseen && !facts.authorized
78    }
79    ScramAlterationDecision::EmptyName => {
80        facts.prior == ScramPriorState::Unseen && facts.authorized && facts.name_empty
81    }
82    ScramAlterationDecision::UnsupportedMechanism => {
83        alteration_name_admitted(facts)
84            && facts.mechanism@ != 1
85            && facts.mechanism@ != 2
86    }
87    ScramAlterationDecision::TooFewIterations => {
88        alteration_mechanism_admitted(facts)
89            && facts.kind == ScramAlterationKind::Upsert
90            && facts.iterations@ < facts.min_iterations@
91    }
92    ScramAlterationDecision::TooManyIterations => {
93        alteration_mechanism_admitted(facts)
94            && facts.kind == ScramAlterationKind::Upsert
95            && facts.iterations@ >= facts.min_iterations@
96            && facts.iterations@ > facts.max_iterations@
97    }
98    ScramAlterationDecision::MissingCredential => {
99        alteration_mechanism_admitted(facts)
100            && facts.kind == ScramAlterationKind::Delete
101            && !facts.deletion_target_exists
102    }
103    ScramAlterationDecision::AcceptSha256 | ScramAlterationDecision::AcceptSha512 => {
104        alteration_mechanism_admitted(facts)
105            && match facts.kind {
106                ScramAlterationKind::Delete => facts.deletion_target_exists,
107                ScramAlterationKind::Upsert => {
108                    facts.iterations@ >= facts.min_iterations@
109                        && facts.iterations@ <= facts.max_iterations@
110                }
111            }
112    }
113})]
114#[ensures(result == ScramAlterationDecision::AcceptSha256 ==> facts.mechanism@ == 1)]
115#[ensures(result == ScramAlterationDecision::AcceptSha512 ==> facts.mechanism@ == 2)]
116#[must_use]
117pub fn scram_alteration_decision(facts: ScramAlterationFacts) -> ScramAlterationDecision {
118    match facts.prior {
119        ScramPriorState::Rejected => return ScramAlterationDecision::KeepPriorError,
120        ScramPriorState::Accepted => return ScramAlterationDecision::Duplicate,
121        ScramPriorState::Unseen => {}
122    }
123
124    if !facts.authorized {
125        return ScramAlterationDecision::Unauthorized;
126    }
127    if facts.name_empty {
128        return ScramAlterationDecision::EmptyName;
129    }
130    if facts.mechanism != 1 && facts.mechanism != 2 {
131        return ScramAlterationDecision::UnsupportedMechanism;
132    }
133
134    match facts.kind {
135        ScramAlterationKind::Delete if !facts.deletion_target_exists => {
136            ScramAlterationDecision::MissingCredential
137        }
138        ScramAlterationKind::Upsert if facts.iterations < facts.min_iterations => {
139            ScramAlterationDecision::TooFewIterations
140        }
141        ScramAlterationKind::Upsert if facts.iterations > facts.max_iterations => {
142            ScramAlterationDecision::TooManyIterations
143        }
144        ScramAlterationKind::Delete | ScramAlterationKind::Upsert => {
145            if facts.mechanism == 1 {
146                ScramAlterationDecision::AcceptSha256
147            } else {
148                ScramAlterationDecision::AcceptSha512
149            }
150        }
151    }
152}
153
154#[cfg(test)]
155mod tests {
156    use super::{
157        ScramAlterationDecision, ScramAlterationFacts, ScramAlterationKind, ScramPriorState,
158        scram_alteration_decision,
159    };
160
161    fn valid_upsert() -> ScramAlterationFacts {
162        ScramAlterationFacts {
163            kind: ScramAlterationKind::Upsert,
164            prior: ScramPriorState::Unseen,
165            authorized: true,
166            name_empty: false,
167            mechanism: 1,
168            iterations: 4096,
169            min_iterations: 4096,
170            max_iterations: 16384,
171            deletion_target_exists: false,
172        }
173    }
174
175    #[test]
176    fn errors_follow_kafka_precedence() {
177        let mut facts = valid_upsert();
178        facts.prior = ScramPriorState::Rejected;
179        facts.authorized = false;
180        facts.name_empty = true;
181        facts.mechanism = 0;
182        facts.iterations = i32::MIN;
183        assert2::check!(
184            scram_alteration_decision(facts) == ScramAlterationDecision::KeepPriorError
185        );
186
187        facts.prior = ScramPriorState::Accepted;
188        assert2::check!(scram_alteration_decision(facts) == ScramAlterationDecision::Duplicate);
189
190        facts.prior = ScramPriorState::Unseen;
191        assert2::check!(scram_alteration_decision(facts) == ScramAlterationDecision::Unauthorized);
192
193        facts.authorized = true;
194        assert2::check!(scram_alteration_decision(facts) == ScramAlterationDecision::EmptyName);
195
196        facts.name_empty = false;
197        assert2::check!(
198            scram_alteration_decision(facts) == ScramAlterationDecision::UnsupportedMechanism
199        );
200
201        facts.mechanism = 1;
202        assert2::check!(
203            scram_alteration_decision(facts) == ScramAlterationDecision::TooFewIterations
204        );
205
206        facts.iterations = i32::MAX;
207        assert2::check!(
208            scram_alteration_decision(facts) == ScramAlterationDecision::TooManyIterations
209        );
210    }
211
212    #[test]
213    fn accepts_only_supported_complete_rows() {
214        let facts = valid_upsert();
215        assert2::check!(scram_alteration_decision(facts) == ScramAlterationDecision::AcceptSha256);
216
217        let sha512 = ScramAlterationFacts {
218            mechanism: 2,
219            iterations: 16384,
220            ..facts
221        };
222        assert2::check!(scram_alteration_decision(sha512) == ScramAlterationDecision::AcceptSha512);
223
224        let missing = ScramAlterationFacts {
225            kind: ScramAlterationKind::Delete,
226            deletion_target_exists: false,
227            ..facts
228        };
229        assert2::check!(
230            scram_alteration_decision(missing) == ScramAlterationDecision::MissingCredential
231        );
232
233        let deletion = ScramAlterationFacts {
234            deletion_target_exists: true,
235            ..missing
236        };
237        assert2::check!(
238            scram_alteration_decision(deletion) == ScramAlterationDecision::AcceptSha256
239        );
240        // A deletion carries no iteration count, so neither bound applies.
241        let sha512_deletion = ScramAlterationFacts {
242            mechanism: 2,
243            iterations: 0,
244            ..deletion
245        };
246        assert2::check!(
247            scram_alteration_decision(sha512_deletion) == ScramAlterationDecision::AcceptSha512
248        );
249    }
250}
krabka_verified/scram.rs

krabka_verified/
scram.rs
