Struct KernelState 

pub struct KernelState { /* private fields */ }

Complete kernel state (TCB)

Corresponds to Lean: structure KernelState

Implementations

impl KernelState

pub fn initial(key: Key, policy: PolicyState) -> Self

Create initial kernel state

Corresponds to Lean: def KernelState.initial (key : Key) (pol : PolicyState) : KernelState

pub fn tick(&self) -> Result<Self, KernelError>

Advance kernel time (immutable, checked)

Corresponds to Lean: def KernelState.tick (ks : KernelState) : KernelState

Errors

Returns KernelError::CounterOverflow if the time counter would exceed u64::MAX.

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

Rotate HMAC key (kernel-only operation)

Corresponds to Lean: def KernelState.rotateKey

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

SECURITY: This operation should only be callable by privileged kernel code.

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

Rotate HMAC key (immutable version)

pub fn key_epoch(&self) -> u64

Get the current key epoch

pub fn key_state(&self) -> &KeyState

Get a reference to the key state

pub fn verify_cap_seal(&self, cap: &Capability) -> bool

Verify capability seal using key state (supports rotation)

Corresponds to Lean: def KernelState.verify_cap_seal

pub fn alloc_cap_id(&mut self) -> Result<CapId, KernelError>

Allocate a fresh capability ID

Corresponds to Lean: def KernelState.alloc_cap_id

INVARIANT: The returned ID is guaranteed fresh (not in use).

Errors

Returns KernelError::CapIdExhausted if the capability ID counter would overflow.

pub fn next_cap_id(&self) -> CapId

Get the next capability ID (without allocating)

pub fn tick_checked(&mut self) -> Result<(), KernelError>

Advance kernel time (mutating, checked)

Errors

Returns KernelError::CounterOverflow if the time counter would exceed u64::MAX.

pub fn cap_not_revoked(&self, cap: &Capability) -> bool

Check if capability is not revoked

Corresponds to Lean: def KernelState.cap_not_revoked

pub fn now(&self) -> Time

Get the current time

pub fn revocation(&self) -> &RevocationState

Get a reference to the revocation state

pub fn policy(&self) -> &PolicyState

Get a reference to the policy state

Trait Implementations

impl Clone for KernelState

fn clone(&self) -> KernelState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for KernelState

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

Formats the value using the given formatter.

impl Default for KernelState

fn default() -> Self

Default kernel state: empty key, deny-all policy, no capabilities, time=0, next_cap_id=0