rootle-kernel 0.13.1

Allocation-free request lifetime decisions extracted to Lean with Charon and Aeneas
Documentation 
1
2
3
4
5
6
7
8
9
10

//! Monotonic request issuance. Exhaustion refuses instead of reusing an epoch.

/// Issue the next generation, or refuse at the end of the identifier space.
pub fn next_generation(current: u64) -> Option<u64> {
    if current == u64::MAX {
        None
    } else {
        Some(current + 1)
    }
}