krabka_verified/
freeze.rs

1//! Topic-freeze signature, scope, and replacement decisions.
2
3#[cfg(creusot)]
4use creusot_std::prelude::{DeepModel, logic};
5
6/// How far a signed record passed through the principal-binding rules.
7#[krabka_macros::model_type]
8pub enum FreezeIdentityState {
9    UnknownKey,
10    WrongKeyPrincipal,
11    WrongConnectionPrincipal,
12    Bound,
13}
14
15/// Facts used by the ordered six-rule signature admission.
16#[krabka_macros::model_type]
17pub struct FreezeSignatureFacts {
18    pub identity: FreezeIdentityState,
19    pub set_at_ms: i64,
20    pub now_ms: i64,
21    pub max_skew_ms: i64,
22    pub replaces: bool,
23    pub replaced_set_at_ms: i64,
24    pub signature_valid: bool,
25}
26
27/// The first failed rule, or admission after all six pass.
28#[krabka_macros::model_type]
29pub enum FreezeSignatureDecision {
30    UnknownKey,
31    AuthorIsNotKeyPrincipal,
32    AuthorIsNotConnectionPrincipal,
33    TimestampOutsideSkewWindow,
34    TimestampNotNewer,
35    SignatureInvalid,
36    Admit,
37}
38
39/// The precedence of one scope that matches a topic.
40#[krabka_macros::model_type]
41pub enum FreezeScopeRank {
42    NoMatch,
43    Prefix { length: u64 },
44    Literal,
45}
46
47/// Whether a matching scope replaces the current resolver candidate.
48#[krabka_macros::model_type]
49pub enum FreezeScopeDecision {
50    Keep,
51    Replace,
52}
53
54/// Every operation whose interaction with a topic freeze is deliberate.
55///
56/// Keeping the allowed operations in the same closed enum as the refused
57/// ones makes additions visible to the proof and to its exhaustive tests.
58#[krabka_macros::model_type]
59pub enum FreezeMutationKind {
60    Produce,
61    TransactionEnlistment,
62    DeleteRecords,
63    DeleteTopic,
64    ReassignmentAlter,
65    ReassignmentCompletion,
66    Compaction,
67    Retention,
68    TransactionCompletion,
69    OffsetCommit,
70    Replication,
71    BarrierMarker,
72    TieringCopy,
73}
74
75/// The single externally observable result of authorization plus freeze
76/// admission.
77#[krabka_macros::model_type]
78pub enum FreezeMutationDecision {
79    AuthorizationDenied,
80    Frozen,
81    Admit,
82}
83
84/// The committed entry at the exact incoming scope key.
85#[krabka_macros::model_type]
86pub enum FreezeStoredState {
87    Missing,
88    Present { set_at_ms: i64 },
89}
90
91/// Facts checked before a freeze mutation enters the metadata log.
92#[krabka_macros::model_type]
93pub struct FreezeReplacementFacts {
94    pub stored: FreezeStoredState,
95    pub incoming_frozen: bool,
96    pub incoming_set_at_ms: i64,
97    pub uncommitted_tail: bool,
98}
99
100/// Why a freeze mutation may or may not enter the metadata log.
101#[krabka_macros::model_type]
102pub enum FreezeReplacementDecision {
103    Missing,
104    Stale,
105    InFlight,
106    Append,
107}
108
109mod mutation_decision;
110#[cfg(creusot)]
111pub use mutation_decision::freeze_timestamp_in_window_model;
112pub use mutation_decision::{
113    freeze_mutation_decision, freeze_refuses, freeze_scope_decision, freeze_signature_decision,
114    freeze_timestamp_in_window,
115};
116
117mod replacement_decision;
118pub use replacement_decision::freeze_replacement_decision;
119
120#[cfg(test)]
121mod tests;
krabka_verified/freeze.rs

krabka_verified/
freeze.rs
