Skip to main content

krabka_verified/
delegation_token.rs

1//! KIP-48 delegation-token deadline decisions.
2
3use creusot_std::prelude::*;
4
5/// Delegation-token API whose admission policy is being evaluated.
6#[krabka_macros::model_type]
7pub enum TokenApi {
8    Create,
9    Renew,
10    Expire,
11    Describe,
12}
13
14/// Whether a connection may invoke a delegation-token API.
15#[krabka_macros::model_type]
16pub enum TokenApiAdmission {
17    Reject,
18    Allow,
19}
20
21/// Credential source selected for the first SCRAM round.
22#[krabka_macros::model_type]
23pub enum ScramCredentialSource {
24    Regular,
25    DelegationToken,
26    Unknown,
27}
28
29/// Absolute deadlines stored on a freshly created delegation token.
30#[krabka_macros::model_type]
31pub struct TokenDeadlines {
32    pub max_timestamp_ms: i64,
33    pub initial_expiry_ms: i64,
34}
35
36/// Whether the host configuration admits a create and, if so, its deadlines.
37#[krabka_macros::model_type]
38pub enum TokenCreateDecision {
39    Invalid,
40    Create(TokenDeadlines),
41}
42
43/// Whether a token can be renewed and, if so, its next expiry.
44#[krabka_macros::model_type]
45pub enum TokenRenewDecision {
46    Invalid,
47    Expired,
48    Renew(i64),
49}
50
51/// Mutation selected by `ExpireDelegationToken`.
52#[krabka_macros::model_type]
53pub enum TokenExpireDecision {
54    Expired,
55    Delete,
56    Update(i64),
57}
58
59/// Delegation-token mutation whose committed-state precondition is checked.
60#[krabka_macros::model_type]
61pub enum TokenMutationKind {
62    Renew,
63    Expire,
64    Delete,
65}
66
67/// Relationship between the committed token and a guarded mutation.
68#[krabka_macros::model_type]
69pub enum TokenMutationState {
70    Missing,
71    Expected,
72    Applied,
73    Stale,
74}
75
76/// Controller action for a generation-bound delegation-token mutation.
77#[krabka_macros::model_type]
78pub enum TokenMutationDecision {
79    Append,
80    Retry,
81    Reject,
82}
83
84/// Scalar facts projected by the controller before it mutates token state.
85#[krabka_macros::model_type]
86pub struct TokenMutationFacts {
87    pub kind: TokenMutationKind,
88    pub state: TokenMutationState,
89    pub now_ms: i64,
90    pub expected_expiry_ms: i64,
91    pub incoming_expiry_ms: i64,
92    pub max_timestamp_ms: i64,
93    pub uncommitted_tail: bool,
94}
95
96mod token_mutation_decision;
97pub use token_mutation_decision::{
98    scram_credential_source, token_api_admission, token_describe_visible, token_mutation_decision,
99};
100
101mod token_is_active;
102pub use token_is_active::{create_token_deadlines, expire_token_deadline, renew_token_expiry};
103
104#[cfg(test)]
105mod tests;