krabka_verified/delegation_token/
token_is_active.rs

1use {
2    super::{TokenCreateDecision, TokenDeadlines, TokenExpireDecision, TokenRenewDecision},
3    creusot_std::prelude::*,
4};
5
6// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
7#[cfg(creusot)]
8#[cfg_attr(test, mutants::skip)]
9#[logic]
10fn deadline_model(now_ms: i64, duration_ms: Int) -> Int {
11    pearlite! {
12        if now_ms@ + duration_ms > i64::MAX@ { i64::MAX@ } else { now_ms@ + duration_ms }
13    }
14}
15
16// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
17#[cfg(creusot)]
18#[cfg_attr(test, mutants::skip)]
19#[logic]
20fn bounded_period_model(requested_ms: i64, default_ms: i64) -> Int {
21    pearlite! {
22        if requested_ms@ > 0 && requested_ms@ < default_ms@ { requested_ms@ } else { default_ms@ }
23    }
24}
25
26// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
27#[cfg(creusot)]
28#[cfg_attr(test, mutants::skip)]
29#[logic]
30fn min_model(left: Int, right: Int) -> Int {
31    pearlite! {
32        if left < right { left } else { right }
33    }
34}
35
36/// Kafka's `DelegationTokenControlManager.sum`: `now + duration`, saturated
37/// at `i64::MAX` instead of wrapping.
38#[requires(duration_ms@ >= 0)]
39#[ensures(result@ == deadline_model(now_ms, duration_ms@))]
40fn token_deadline(now_ms: i64, duration_ms: i64) -> i64 {
41    now_ms.checked_add(duration_ms).unwrap_or(i64::MAX)
42}
43
44/// A requested period, bounded by the configured one.
45///
46/// Kafka's `createDelegationToken` and `renewDelegationToken` both use the
47/// configured value for a request of 0 or less, and the smaller of the two
48/// for a positive request.
49#[requires(default_ms@ > 0)]
50#[ensures(result@ == bounded_period_model(requested_ms, default_ms))]
51#[ensures(result@ > 0)]
52fn bounded_period(requested_ms: i64, default_ms: i64) -> i64 {
53    if requested_ms > 0 {
54        requested_ms.min(default_ms)
55    } else {
56        default_ms
57    }
58}
59
60/// Derive both stored deadlines of a new token.
61///
62/// Matches `DelegationTokenControlManager.createDelegationToken` in Kafka
63/// trunk: the lifetime is `delegation.token.max.lifetime.ms` (`ceiling_ms`)
64/// for a request of 0 or less and the smaller of the two otherwise, the
65/// maximum timestamp is `now` plus that lifetime, and the first expiry is
66/// `now` plus `delegation.token.expiry.time.ms` (`default_renew_period_ms`),
67/// capped at the maximum timestamp. Both sums saturate at `i64::MAX`. Kafka's
68/// configuration validation rejects a period below 1, so a non-positive host
69/// setting is `Invalid` here.
70#[ensures((result == TokenCreateDecision::Invalid) ==
71    (ceiling_ms@ <= 0 || default_renew_period_ms@ <= 0))]
72#[ensures(match result {
73    TokenCreateDecision::Invalid => true,
74    TokenCreateDecision::Create(deadlines) =>
75        deadlines.max_timestamp_ms@ ==
76            deadline_model(now_ms, bounded_period_model(requested_ms, ceiling_ms))
77            && deadlines.initial_expiry_ms@ == min_model(
78                deadlines.max_timestamp_ms@,
79                deadline_model(now_ms, default_renew_period_ms@),
80            ),
81})]
82// Export arithmetic bounds independently of the private exact-value models.
83#[ensures(match result {
84    TokenCreateDecision::Invalid => true,
85    TokenCreateDecision::Create(d) => now_ms@ <= d.initial_expiry_ms@
86        && d.initial_expiry_ms@ <= d.max_timestamp_ms@
87        && d.max_timestamp_ms@ <= now_ms@ + ceiling_ms@
88        && (requested_ms@ > 0 ==> d.max_timestamp_ms@ <= now_ms@ + requested_ms@)
89        && d.initial_expiry_ms@ <= now_ms@ + default_renew_period_ms@
90        && (d.max_timestamp_ms@ == i64::MAX@ || d.max_timestamp_ms@ == now_ms@ + ceiling_ms@
91            || (requested_ms@ > 0 && d.max_timestamp_ms@ == now_ms@ + requested_ms@))
92        && (d.initial_expiry_ms@ == d.max_timestamp_ms@
93            || d.initial_expiry_ms@ == now_ms@ + default_renew_period_ms@),
94})]
95#[must_use]
96pub fn create_token_deadlines(
97    now_ms: i64,
98    requested_ms: i64,
99    ceiling_ms: i64,
100    default_renew_period_ms: i64,
101) -> TokenCreateDecision {
102    if ceiling_ms <= 0 || default_renew_period_ms <= 0 {
103        return TokenCreateDecision::Invalid;
104    }
105
106    let max_timestamp_ms = token_deadline(now_ms, bounded_period(requested_ms, ceiling_ms));
107    let renew_deadline_ms = token_deadline(now_ms, default_renew_period_ms);
108    TokenCreateDecision::Create(TokenDeadlines {
109        max_timestamp_ms,
110        initial_expiry_ms: renew_deadline_ms.min(max_timestamp_ms),
111    })
112}
113
114/// Derive a renewed expiry.
115///
116/// Matches `DelegationTokenControlManager.renewDelegationToken` in Kafka
117/// trunk: a token whose expiry or maximum timestamp is strictly before `now`
118/// is `Expired`. Otherwise the renew period is the configured
119/// `delegation.token.expiry.time.ms` for a request of 0 or less and the
120/// smaller of the two for a positive request, and the new expiry is `now`
121/// plus that period, capped at the maximum timestamp. The new expiry replaces
122/// the current one even when it is earlier. A non-positive configured period
123/// is `Invalid`.
124#[ensures((result == TokenRenewDecision::Expired) ==
125    (current_expiry_ms@ < now_ms@ || max_timestamp_ms@ < now_ms@))]
126#[ensures((result == TokenRenewDecision::Invalid) == (
127    current_expiry_ms@ >= now_ms@
128        && max_timestamp_ms@ >= now_ms@
129        && default_renew_period_ms@ <= 0
130))]
131#[ensures(match result {
132    TokenRenewDecision::Renew(expiry) =>
133        expiry@ == min_model(
134            max_timestamp_ms@,
135            deadline_model(now_ms, bounded_period_model(requested_ms, default_renew_period_ms)),
136        ),
137    _ => true,
138})]
139// Export the interval independently of the private arithmetic models.
140#[ensures(match result {
141    TokenRenewDecision::Renew(expiry) => now_ms@ <= expiry@ && expiry@ <= max_timestamp_ms@
142        && (now_ms@ < max_timestamp_ms@ ==> now_ms@ < expiry@),
143    _ => true,
144})]
145#[must_use]
146pub fn renew_token_expiry(
147    now_ms: i64,
148    requested_ms: i64,
149    default_renew_period_ms: i64,
150    current_expiry_ms: i64,
151    max_timestamp_ms: i64,
152) -> TokenRenewDecision {
153    if current_expiry_ms < now_ms || max_timestamp_ms < now_ms {
154        return TokenRenewDecision::Expired;
155    }
156    if default_renew_period_ms <= 0 {
157        return TokenRenewDecision::Invalid;
158    }
159
160    let period = bounded_period(requested_ms, default_renew_period_ms);
161    TokenRenewDecision::Renew(token_deadline(now_ms, period).min(max_timestamp_ms))
162}
163
164/// Select deletion or a bounded expiry update.
165///
166/// Matches `DelegationTokenControlManager.expireDelegationToken` in Kafka
167/// trunk: every negative period deletes the token, whatever its deadlines.
168/// Otherwise a token whose expiry or maximum timestamp is strictly before
169/// `now` is `Expired`, and a live token gets `now + period`, saturated at
170/// `i64::MAX` and capped at its maximum timestamp.
171#[ensures((result == TokenExpireDecision::Delete) == (period_ms@ < 0))]
172#[ensures((result == TokenExpireDecision::Expired) ==
173    (period_ms@ >= 0
174        && (current_expiry_ms@ < now_ms@ || max_timestamp_ms@ < now_ms@)))]
175#[ensures(match result {
176    TokenExpireDecision::Update(expiry) =>
177        expiry@ == min_model(max_timestamp_ms@, deadline_model(now_ms, period_ms@)),
178    _ => true,
179})]
180#[must_use]
181pub fn expire_token_deadline(
182    now_ms: i64,
183    period_ms: i64,
184    current_expiry_ms: i64,
185    max_timestamp_ms: i64,
186) -> TokenExpireDecision {
187    if period_ms < 0 {
188        return TokenExpireDecision::Delete;
189    }
190    if current_expiry_ms < now_ms || max_timestamp_ms < now_ms {
191        return TokenExpireDecision::Expired;
192    }
193
194    TokenExpireDecision::Update(token_deadline(now_ms, period_ms).min(max_timestamp_ms))
195}
krabka_verified/delegation_token/token_is_active.rs

krabka_verified/delegation_token/
token_is_active.rs
