//! Per-slot generation counters shared by the kernel's object tables.

use types::generation::Generation;

#[cfg(test)]
#[path = "generations_tests.rs"]
mod tests;

/// Bumped on every destroy or revoke so older capabilities stop matching; a slot whose counter runs out is retired.
pub struct SlotGenerations<const N: usize> {
    gens: [Option<Generation>; N],
}

impl<const N: usize> SlotGenerations<N> {
    pub const fn new() -> Self {
        Self {
            gens: [Some(Generation::initial()); N],
        }
    }

    /// Current generation of `idx`, `None` if retired or out of range.
    pub fn current(&self, idx: usize) -> Option<Generation> {
        *self.gens.get(idx)?
    }

    pub fn is_usable(&self, idx: usize) -> bool {
        self.current(idx).is_some()
    }

    /// Invalidates every capability minted for the current generation.
    pub fn advance(&mut self, idx: usize) {
        if let Some(g) = self.gens.get_mut(idx) {
            *g = g.and_then(|g| g.next());
        }
    }
}

impl<const N: usize> Default for SlotGenerations<N> {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(kani)]
mod proofs {
    use super::SlotGenerations;
    use types::generation::Generation;

    /// However many times a slot is advanced, a generation observed earlier
    /// never comes back, so a capability minted for it stays dead.
    #[kani::proof]
    #[kani::unwind(5)]
    fn an_observed_generation_never_returns() {
        let mut g: SlotGenerations<1> = SlotGenerations::new();
        g.gens[0] = if kani::any() {
            Some(Generation::from_raw(kani::any()))
        } else {
            None
        };
        let observed = g.current(0);
        let steps: u8 = kani::any();
        kani::assume(steps >= 1 && steps <= 4);
        for _ in 0..steps {
            g.advance(0);
            if let (Some(old), Some(now)) = (observed, g.current(0)) {
                assert!(!old.is_valid_against(&now));
            }
        }
    }

    /// A retired slot is never usable again.
    #[kani::proof]
    #[kani::unwind(5)]
    fn retired_slots_stay_retired() {
        let mut g: SlotGenerations<1> = SlotGenerations::new();
        g.gens[0] = None;
        let steps: u8 = kani::any();
        kani::assume(steps <= 4);
        for _ in 0..steps {
            g.advance(0);
        }
        assert!(!g.is_usable(0));
    }
}