krabka_verified/freeze/
mutation_decision.rs

1#[cfg(creusot)]
2use super::logic;
3use {
4    super::{
5        FreezeIdentityState, FreezeMutationDecision, FreezeMutationKind, FreezeScopeDecision,
6        FreezeScopeRank, FreezeSignatureDecision, FreezeSignatureFacts,
7    },
8    creusot_std::prelude::*,
9};
10
11/// Mathematical skew-window predicate, without machine-integer overflow.
12// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
13#[cfg(creusot)]
14#[cfg_attr(test, mutants::skip)]
15#[logic]
16pub fn freeze_timestamp_in_window_model(set_at_ms: i64, now_ms: i64, max_skew_ms: i64) -> bool {
17    pearlite! {
18        max_skew_ms@ >= 0
19            && set_at_ms@ >= now_ms@ - max_skew_ms@
20            && set_at_ms@ <= now_ms@ + max_skew_ms@
21    }
22}
23
24/// Check the symmetric skew window with saturating machine bounds.
25#[ensures(result == freeze_timestamp_in_window_model(set_at_ms, now_ms, max_skew_ms))]
26#[must_use]
27pub const fn freeze_timestamp_in_window(set_at_ms: i64, now_ms: i64, max_skew_ms: i64) -> bool {
28    if max_skew_ms < 0 {
29        return false;
30    }
31    let earliest = now_ms.saturating_sub(max_skew_ms);
32    let latest = now_ms.saturating_add(max_skew_ms);
33    set_at_ms >= earliest && set_at_ms <= latest
34}
35
36// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
37#[cfg(creusot)]
38#[cfg_attr(test, mutants::skip)]
39#[logic(open)]
40fn freeze_signature_preconditions(facts: FreezeSignatureFacts) -> bool {
41    pearlite! { facts.identity == FreezeIdentityState::Bound
42    && freeze_timestamp_in_window_model(
43        facts.set_at_ms,
44        facts.now_ms,
45        facts.max_skew_ms,
46    )
47    && (!facts.replaces || facts.set_at_ms@ > facts.replaced_set_at_ms@) }
48}
49
50/// Apply the six signature rules in their security-sensitive order.
51#[ensures(match result {
52    FreezeSignatureDecision::UnknownKey => facts.identity == FreezeIdentityState::UnknownKey,
53    FreezeSignatureDecision::AuthorIsNotKeyPrincipal => {
54        facts.identity == FreezeIdentityState::WrongKeyPrincipal
55    }
56    FreezeSignatureDecision::AuthorIsNotConnectionPrincipal => {
57        facts.identity == FreezeIdentityState::WrongConnectionPrincipal
58    }
59    FreezeSignatureDecision::TimestampOutsideSkewWindow => {
60        facts.identity == FreezeIdentityState::Bound
61            && !freeze_timestamp_in_window_model(
62                facts.set_at_ms,
63                facts.now_ms,
64                facts.max_skew_ms,
65            )
66    }
67    FreezeSignatureDecision::TimestampNotNewer => {
68        facts.identity == FreezeIdentityState::Bound
69            && freeze_timestamp_in_window_model(
70                facts.set_at_ms,
71                facts.now_ms,
72                facts.max_skew_ms,
73            )
74            && facts.replaces
75            && facts.set_at_ms@ <= facts.replaced_set_at_ms@
76    }
77    FreezeSignatureDecision::SignatureInvalid => {
78        freeze_signature_preconditions(facts)
79            && !facts.signature_valid
80    }
81    FreezeSignatureDecision::Admit => {
82        freeze_signature_preconditions(facts)
83            && facts.signature_valid
84    }
85})]
86#[must_use]
87pub fn freeze_signature_decision(facts: FreezeSignatureFacts) -> FreezeSignatureDecision {
88    match facts.identity {
89        FreezeIdentityState::UnknownKey => FreezeSignatureDecision::UnknownKey,
90        FreezeIdentityState::WrongKeyPrincipal => FreezeSignatureDecision::AuthorIsNotKeyPrincipal,
91        FreezeIdentityState::WrongConnectionPrincipal => {
92            FreezeSignatureDecision::AuthorIsNotConnectionPrincipal
93        }
94        FreezeIdentityState::Bound => {
95            if !freeze_timestamp_in_window(facts.set_at_ms, facts.now_ms, facts.max_skew_ms) {
96                FreezeSignatureDecision::TimestampOutsideSkewWindow
97            } else if facts.replaces && facts.set_at_ms <= facts.replaced_set_at_ms {
98                FreezeSignatureDecision::TimestampNotNewer
99            } else if !facts.signature_valid {
100                FreezeSignatureDecision::SignatureInvalid
101            } else {
102                FreezeSignatureDecision::Admit
103            }
104        }
105    }
106}
107
108/// Make every caller use literal-over-prefix and longest-prefix precedence.
109#[ensures((result == FreezeScopeDecision::Replace) == match (current, candidate) {
110    (_, FreezeScopeRank::NoMatch) | (FreezeScopeRank::Literal, _) => false,
111    (FreezeScopeRank::NoMatch, _) => true,
112    (FreezeScopeRank::Prefix { .. }, FreezeScopeRank::Literal) => true,
113    (
114        FreezeScopeRank::Prefix { length: current_length },
115        FreezeScopeRank::Prefix { length: candidate_length },
116    ) => candidate_length@ > current_length@,
117})]
118#[must_use]
119pub fn freeze_scope_decision(
120    current: FreezeScopeRank,
121    candidate: FreezeScopeRank,
122) -> FreezeScopeDecision {
123    match (current, candidate) {
124        (_, FreezeScopeRank::NoMatch) | (FreezeScopeRank::Literal, _) => FreezeScopeDecision::Keep,
125        (FreezeScopeRank::NoMatch, _)
126        | (FreezeScopeRank::Prefix { .. }, FreezeScopeRank::Literal) => {
127            FreezeScopeDecision::Replace
128        }
129        (
130            FreezeScopeRank::Prefix {
131                length: current_length,
132            },
133            FreezeScopeRank::Prefix {
134                length: candidate_length,
135            },
136        ) => {
137            if candidate_length > current_length {
138                FreezeScopeDecision::Replace
139            } else {
140                FreezeScopeDecision::Keep
141            }
142        }
143    }
144}
145
146krabka_macros::freeze_refusal_rules! {
147    FreezeMutationKind;
148    refuse [Produce, TransactionEnlistment, DeleteRecords, DeleteTopic, ReassignmentAlter, Compaction, Retention];
149    allow [TransactionCompletion, ReassignmentCompletion, OffsetCommit, Replication, BarrierMarker, TieringCopy];
150    runtime {
151/// Classify the complete topic-mutation inventory under a live freeze.
152#[ensures(result == freeze_refusal_model(kind))]
153#[must_use]
154pub const fn freeze_refuses(kind: FreezeMutationKind) -> bool
155    }
156    model {
157/// Logical mirror of [`freeze_refuses`] for the mutation contract.
158// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
159#[cfg(creusot)]
160#[cfg_attr(test, mutants::skip)]
161#[logic]
162fn freeze_refusal_model(kind: FreezeMutationKind) -> bool
163    }
164}
165
166/// Rank authorization ahead of freeze detail, then apply the one refusal
167/// classification shared by every mutation adapter.
168#[ensures((result == FreezeMutationDecision::AuthorizationDenied) == !authorized)]
169#[ensures((result == FreezeMutationDecision::Frozen) == (
170    authorized && frozen && freeze_refusal_model(kind)
171))]
172#[ensures((result == FreezeMutationDecision::Admit) == (
173    authorized && (!frozen || !freeze_refusal_model(kind))
174))]
175#[must_use]
176pub const fn freeze_mutation_decision(
177    authorized: bool,
178    frozen: bool,
179    kind: FreezeMutationKind,
180) -> FreezeMutationDecision {
181    if !authorized {
182        FreezeMutationDecision::AuthorizationDenied
183    } else if frozen && freeze_refuses(kind) {
184        FreezeMutationDecision::Frozen
185    } else {
186        FreezeMutationDecision::Admit
187    }
188}
krabka_verified/freeze/mutation_decision.rs

krabka_verified/freeze/
mutation_decision.rs
