krabka_verified/
jwks.rs

1//! JWKS cache freshness and on-demand refresh decisions.
2
3mod publication;
4use creusot_std::prelude::ensures;
5#[cfg(creusot)]
6use creusot_std::prelude::{DeepModel, logic};
7pub use publication::jwks_publication_generations;
8
9/// Whether a validator may use one observed JWKS cache generation.
10#[krabka_macros::model_type]
11pub enum JwksCacheDecision {
12    Reject,
13    Admit,
14}
15
16/// Values read around one key validation.
17#[krabka_macros::model_type]
18pub struct JwksCacheFacts {
19    pub generation_before: u64,
20    pub generation_after: u64,
21    pub last_successful_fetch_ms: i64,
22    pub now_ms: i64,
23    pub expiry_enabled: bool,
24    pub expiry_ms: i64,
25}
26
27// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
28#[cfg(creusot)]
29#[cfg_attr(test, mutants::skip)]
30#[logic(open(crate))]
31pub fn jwks_cache_facts_admissible_at(facts: JwksCacheFacts, now_ms: i64) -> bool {
32    pearlite! {
33        facts.generation_before@ % 2 == 0
34            && facts.generation_before@ == facts.generation_after@
35            && (!facts.expiry_enabled || (
36                facts.expiry_ms@ >= 0
37                    && facts.last_successful_fetch_ms@ > 0
38                    && now_ms@ >= facts.last_successful_fetch_ms@
39                    && now_ms@ - facts.last_successful_fetch_ms@ <= facts.expiry_ms@
40            ))
41    }
42}
43
44/// Admit only a stable, fully published cache generation that is not stale.
45#[ensures((result == JwksCacheDecision::Admit) == jwks_cache_facts_admissible_at(facts, facts.now_ms))]
46#[must_use]
47pub fn jwks_cache_admission(facts: JwksCacheFacts) -> JwksCacheDecision {
48    if !facts.generation_before.is_multiple_of(2)
49        || facts.generation_before != facts.generation_after
50    {
51        return JwksCacheDecision::Reject;
52    }
53    if !facts.expiry_enabled {
54        return JwksCacheDecision::Admit;
55    }
56    if facts.expiry_ms < 0
57        || facts.last_successful_fetch_ms <= 0
58        || facts.now_ms < facts.last_successful_fetch_ms
59    {
60        return JwksCacheDecision::Reject;
61    }
62    if facts.now_ms - facts.last_successful_fetch_ms > facts.expiry_ms {
63        JwksCacheDecision::Reject
64    } else {
65        JwksCacheDecision::Admit
66    }
67}
68
69/// Whether an on-demand signal may start a fetch.
70#[krabka_macros::model_type]
71pub enum JwksOnDemandDecision {
72    RateLimited,
73    Refresh { next_refresh_ms: i64 },
74}
75
76/// Whether an on-demand refresh may start at `now_ms`: the clock and pause are
77/// nonnegative, the clock has not stepped back behind the last refresh, and
78/// either no refresh has happened yet (`last_refresh_ms <= 0`) or at least
79/// `min_pause_ms` has elapsed since it.
80// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
81#[cfg(creusot)]
82#[cfg_attr(test, mutants::skip)]
83#[logic]
84pub fn jwks_on_demand_refresh_allowed(
85    now_ms: i64,
86    last_refresh_ms: i64,
87    min_pause_ms: i64,
88) -> bool {
89    pearlite! {
90        now_ms@ >= 0
91            && min_pause_ms@ >= 0
92            && now_ms@ >= last_refresh_ms@
93            && (last_refresh_ms@ <= 0 || now_ms@ - last_refresh_ms@ >= min_pause_ms@)
94    }
95}
96
97/// Keep the limiter monotonic and fail closed across wall-clock rollback:
98/// refresh exactly when `jwks_on_demand_refresh_allowed` holds, stamping
99/// `now_ms` as the new last-refresh time.
100#[ensures(match result {
101    JwksOnDemandDecision::RateLimited => !jwks_on_demand_refresh_allowed(
102        now_ms,
103        last_refresh_ms,
104        min_pause_ms,
105    ),
106    JwksOnDemandDecision::Refresh { next_refresh_ms } => next_refresh_ms == now_ms
107        && jwks_on_demand_refresh_allowed(now_ms, last_refresh_ms, min_pause_ms),
108})]
109#[must_use]
110pub fn jwks_on_demand_refresh_decision(
111    now_ms: i64,
112    last_refresh_ms: i64,
113    min_pause_ms: i64,
114) -> JwksOnDemandDecision {
115    if now_ms < 0 || min_pause_ms < 0 || now_ms < last_refresh_ms {
116        return JwksOnDemandDecision::RateLimited;
117    }
118    if last_refresh_ms > 0 && now_ms - last_refresh_ms < min_pause_ms {
119        return JwksOnDemandDecision::RateLimited;
120    }
121    JwksOnDemandDecision::Refresh {
122        next_refresh_ms: now_ms,
123    }
124}
125
126#[cfg(test)]
127mod tests {
128    use super::{
129        JwksCacheDecision, JwksCacheFacts, JwksOnDemandDecision, jwks_cache_admission,
130        jwks_on_demand_refresh_decision,
131    };
132
133    fn fresh_cache_facts() -> JwksCacheFacts {
134        JwksCacheFacts {
135            generation_before: 2,
136            generation_after: 2,
137            last_successful_fetch_ms: 100,
138            now_ms: 200,
139            expiry_enabled: true,
140            expiry_ms: 100,
141        }
142    }
143
144    #[yare::parameterized(
145        fresh = { "a fresh stable generation", fresh_cache_facts(), JwksCacheDecision::Admit },
146        expiry_disabled = {
147            "a stable generation with expiry disabled",
148            JwksCacheFacts { expiry_enabled: false, ..fresh_cache_facts() },
149            JwksCacheDecision::Admit
150        },
151        exact_expiry_boundary = {
152            "a fetch at the zero-expiry boundary",
153            JwksCacheFacts { now_ms: 100, last_successful_fetch_ms: 100, expiry_ms: 0, ..fresh_cache_facts() },
154            JwksCacheDecision::Admit
155        },
156        changed_before_generation = {
157            "a generation changed before reading the cache",
158            JwksCacheFacts { generation_before: 1, ..fresh_cache_facts() },
159            JwksCacheDecision::Reject
160        },
161        changed_after_generation = {
162            "a generation changed while reading the cache",
163            JwksCacheFacts { generation_after: 4, ..fresh_cache_facts() },
164            JwksCacheDecision::Reject
165        },
166        never_fetched = {
167            "a cache with no successful fetch",
168            JwksCacheFacts { last_successful_fetch_ms: 0, ..fresh_cache_facts() },
169            JwksCacheDecision::Reject
170        },
171        zero_fetch_and_clock = {
172            "a cache whose fetch and current times are both zero",
173            JwksCacheFacts { now_ms: 0, last_successful_fetch_ms: 0, ..fresh_cache_facts() },
174            JwksCacheDecision::Reject
175        },
176        clock_before_fetch = {
177            "a clock before the successful fetch",
178            JwksCacheFacts { now_ms: 99, ..fresh_cache_facts() },
179            JwksCacheDecision::Reject
180        },
181        expired = {
182            "an expired cache",
183            JwksCacheFacts { now_ms: 201, ..fresh_cache_facts() },
184            JwksCacheDecision::Reject
185        },
186        negative_expiry = {
187            "a negative expiry",
188            JwksCacheFacts { expiry_ms: -1, ..fresh_cache_facts() },
189            JwksCacheDecision::Reject
190        },
191    )]
192    fn cache_requires_one_fresh_stable_generation(
193        case: &str,
194        facts: JwksCacheFacts,
195        expected: JwksCacheDecision,
196    ) {
197        assert2::check!(jwks_cache_admission(facts) == expected, "{case}");
198    }
199
200    #[yare::parameterized(
201        unrefreshed_zero = { 0, 0, 0, JwksOnDemandDecision::Refresh { next_refresh_ms: 0 } },
202        unrefreshed_pause = { 5, 0, 10, JwksOnDemandDecision::Refresh { next_refresh_ms: 5 } },
203        first_refresh = { 100, 0, 10, JwksOnDemandDecision::Refresh { next_refresh_ms: 100 } },
204        unrefreshed_max = {
205            i64::MAX,
206            0,
207            i64::MAX,
208            JwksOnDemandDecision::Refresh { next_refresh_ms: i64::MAX },
209        },
210        pause_boundary = { 110, 100, 10, JwksOnDemandDecision::Refresh { next_refresh_ms: 110 } },
211        before_pause_boundary = { 109, 100, 10, JwksOnDemandDecision::RateLimited },
212        negative_clock = { -1, 0, 10, JwksOnDemandDecision::RateLimited },
213        negative_pause = { 100, 0, -1, JwksOnDemandDecision::RateLimited },
214        backwards_clock = { 99, 100, 0, JwksOnDemandDecision::RateLimited },
215        elapsed_subtraction_overflow = { i64::MAX, 1, i64::MAX, JwksOnDemandDecision::RateLimited },
216    )]
217    fn on_demand_limit_is_monotonic_and_overflow_safe(
218        now_ms: i64,
219        last_refresh_ms: i64,
220        min_pause_ms: i64,
221        expected: JwksOnDemandDecision,
222    ) {
223        assert2::check!(
224            jwks_on_demand_refresh_decision(now_ms, last_refresh_ms, min_pause_ms) == expected
225        );
226    }
227}
krabka_verified/jwks.rs

krabka_verified/
jwks.rs
