Skip to main content

krabka_verified/authz/
controller_session.rs

1use {
2    super::{RequestAuthState, request_auth_admission},
3    creusot_std::prelude::*,
4};
5
6/// Controller connections currently require reconnecting to reauthenticate.
7///
8/// Expiry therefore fails the authentication phase before any API dispatch. A
9/// session expires only strictly after its deadline, as Kafka's
10/// `KafkaChannel.serverAuthenticationSessionExpired` decides, so a request at
11/// exactly `expiry_ms` is still admitted.
12#[ensures(result == match expiry_ms {
13    None => true,
14    Some(at) => now_ms@ <= at@,
15})]
16#[must_use]
17pub fn controller_request_admission(expiry_ms: Option<i64>, api_key: i16, now_ms: i64) -> bool {
18    let state = match expiry_ms {
19        Some(at) if now_ms > at => RequestAuthState::Failed,
20        _ => RequestAuthState::Authenticated,
21    };
22    request_auth_admission(state, api_key)
23}