Skip to main content

krabka_verified/jwks/
publication.rs

1//! Publication generations for the host's exclusive JWKS writer.
2
3use creusot_std::prelude::ensures;
4
5/// Enter an odd write phase and commit the next even generation, or preserve
6/// the prior cache. Never wrap: an old reader generation cannot recur.
7#[ensures((result == None) == (generation@ % 2 != 0 || generation@ > u64::MAX@ - 2))]
8#[ensures(match result {
9    None => true,
10    Some((writing, committed)) => writing@ == generation@ + 1
11        && committed@ == generation@ + 2
12        && generation@ % 2 == 0 && writing@ % 2 == 1 && committed@ % 2 == 0,
13})]
14#[must_use]
15pub fn jwks_publication_generations(generation: u64) -> Option<(u64, u64)> {
16    if !generation.is_multiple_of(2) || generation > u64::MAX - 2 {
17        None
18    } else {
19        Some((generation + 1, generation + 2))
20    }
21}