krabka_verified/oauth/
completion.rs

1#[cfg(creusot)]
2use crate::jwks::jwks_cache_facts_admissible_at;
3use {
4    crate::jwks::{JwksCacheDecision, JwksCacheFacts, jwks_cache_admission},
5    creusot_std::prelude::*,
6};
7
8/// Bind validation completion to a forward clock observation and, when
9/// supplied, the still-current and fresh JWKS generation.
10///
11/// The supplied cache timestamp is a start observation; freshness is always
12/// recomputed at finish.
13#[ensures(result == (started_ms@ >= 0 && completed_ms@ >= started_ms@ && match cache {
14    None => true,
15    Some(facts) => jwks_cache_facts_admissible_at(facts, completed_ms),
16}))]
17#[must_use]
18pub fn oauth_validation_admission(
19    started_ms: i64,
20    completed_ms: i64,
21    cache: Option<JwksCacheFacts>,
22) -> bool {
23    if started_ms < 0 || completed_ms < started_ms {
24        return false;
25    }
26    let Some(mut facts) = cache else {
27        return true;
28    };
29    facts.now_ms = completed_ms;
30    matches!(jwks_cache_admission(facts), JwksCacheDecision::Admit)
31}
krabka_verified/oauth/completion.rs

krabka_verified/oauth/
completion.rs
