Struct KeyState 

pub struct KeyState { /* private fields */ }

Key state for HMAC key rotation support.

Corresponds to Lean: structure KeyState

Design rationale:

• current: The active key used for sealing new capabilities
• epoch: Monotonically increasing counter identifying the current key
• previous: Optional previous key for validating in-flight capabilities
• previous_epoch: Epoch of the previous key

The grace period (keeping previous key) allows capabilities that were sealed just before rotation to still be verified.

SECURITY INVARIANT: epoch is monotonically increasing (never wraps in practice).

Implementations

impl KeyState

pub fn initial(key: Key) -> Self

Create initial key state with no previous key

Corresponds to Lean: def KeyState.initial

pub fn empty() -> Self

Create empty key state (for default/placeholder purposes)

Corresponds to Lean: def KeyState.empty

pub fn rotate(&mut self, new_key: Key)

Rotate to a new key

Corresponds to Lean: def KeyState.rotate

The current key becomes the previous key for grace period verification. The epoch is incremented.

SECURITY: Only kernel can trigger rotation (not plugins). Uses checked arithmetic – epoch overflow is a critical error.

pub fn rotated(&self, new_key: Key) -> Self

Rotate to a new key (immutable version)

Returns a new KeyState with the rotated key.

pub fn current(&self) -> &Key

Get the current key

pub fn epoch(&self) -> u64

Get the current epoch

pub fn previous(&self) -> Option<&Key>

Get the previous key (if available)

pub fn previous_epoch(&self) -> Option<u64>

Get the previous epoch (if available)

pub fn epoch_valid(&self, cap_epoch: u64) -> bool

Check if epoch is current or within grace period

Corresponds to Lean: def KeyState.epochValid

pub fn verify_seal(&self, payload: &CapPayload, tag: &SealedTag) -> bool

Verify a capability’s seal against the key state

Corresponds to Lean: def KeyState.verify

Strategy:

1. Try current key first
2. Fall back to previous key for in-flight capabilities (grace period)

Returns true if the capability verifies against either key.

pub fn verify_with_epoch( &self, payload: &CapPayload, tag: &SealedTag, cap_epoch: u64, ) -> bool

Combined verification: seal AND epoch valid

Corresponds to Lean: def KeyState.verifyWithEpoch

pub fn clear_previous(&mut self)

Clear the previous key (end grace period)

Call this after sufficient time has passed since rotation to clear the previous key from memory.

Trait Implementations

impl Clone for KeyState

fn clone(&self) -> KeyState

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for KeyState

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for KeyState

fn default() -> Self

Returns the “default value” for a type.