Struct State 

pub struct State { /* private fields */ }

Complete system state

Corresponds to Lean: @[ext] structure State

INVARIANTS:

• All state transitions preserve isolation (non-active plugins unchanged)
• Temporal safety: freed resources stay freed
• Capability validity is checked at use time
• All collections are sorted by key for deterministic iteration
• Single source of truth: logical time lives in kernel.now, not duplicated here

Implementations

impl State

pub fn empty() -> Self

Create a new empty state

pub fn plugin_memory(&self, pid: PluginId) -> Option<&LinearMemory>

Get plugin memory

Corresponds to Lean: def State.plugin_memory

pub fn plugin_level(&self, pid: PluginId) -> Option<SecurityLevel>

Get plugin security level

Corresponds to Lean: def State.plugin_level

pub fn resource_level(&self, rid: ResourceId) -> Option<SecurityLevel>

Get resource security level

Corresponds to Lean: def State.resource_level

pub fn get_cap(&self, cap_id: CapId) -> Option<&Capability>

Get capability from kernel

Corresponds to Lean: def State.get_cap

pub fn cap_is_valid(&self, cap_id: CapId) -> bool

Check if capability is valid in current state

Corresponds to Lean: def State.cap_is_valid

pub fn plugin_holds(&self, pid: PluginId, cap_id: CapId) -> bool

Check if plugin holds capability by ID

Corresponds to Lean: def State.plugin_holds

pub fn apply_alloc(&self, owner: PluginId, _size: Size) -> Self

Allocate resource, update ghost history

Corresponds to Lean: def State.apply_alloc

pub fn apply_alloc_mut(&mut self, owner: PluginId, _size: Size) -> MemAddr

Allocate resource (mutating version)

pub fn apply_free(&self, addr: MemAddr) -> Result<Self, StateError>

Free resource, mark as dead in ghost history

Corresponds to Lean: def State.apply_free

SECURITY: This checks for dangling capabilities before freeing. If any valid capability targets this address, freeing it would create a USE-AFTER-FREE vulnerability.

Errors

Returns StateError::DanglingCapability if a valid capability still targets the address.

pub fn apply_free_mut(&mut self, addr: MemAddr) -> Result<(), StateError>

Free resource (mutating version)

SECURITY: Checks for dangling capabilities before freeing. Requires the resource to be currently allocated (not unallocated or already freed).

Errors

Returns StateError::DanglingCapability if a valid capability still targets the address. Returns StateError::ResourceNotFound if the address was already freed or never allocated.

pub fn apply_revoke(&self, cap_id: CapId) -> Self

Revoke capability (single cap)

Corresponds to Lean: def State.apply_revoke

pub fn apply_cap_revoke(&self, cap_id: CapId) -> Self

Revoke capability transitively

Corresponds to Lean: def State.apply_cap_revoke

pub fn apply_cap_revoke_mut(&mut self, cap_id: CapId) -> Result<(), KernelError>

Revoke capability transitively (mutating version)

Uses the children-index optimized O(k) fast path with BFS traversal and visited set (no iteration cap).

Errors

Returns KernelError::CapNotFound if the capability does not exist.

pub fn apply_cap_delegate( &self, new_cap: Capability, target: PluginId, ) -> Result<Self, KernelError>

Delegate capability: insert new cap into kernel and grant to target

Corresponds to Lean: def State.apply_cap_delegate

Returns error if capability ID already exists (collision).

Errors

Returns KernelError::CapIdCollision if a capability with the same ID already exists.

pub fn apply_cap_delegate_mut( &mut self, new_cap: Capability, target: PluginId, ) -> Result<(), KernelError>

Delegate capability (mutating version)

Errors

Returns KernelError::CapIdCollision if a capability with the same ID already exists.

pub fn preserves_isolation(&self, other: &State, active: PluginId) -> bool

Check if memory isolation is preserved after step

Corresponds to Lean: def State.preserves_isolation

pub fn temporal_safety(&self, other: &State) -> bool

Check temporal safety: freed resources stay freed

Corresponds to Lean: def State.temporal_safety

pub fn time(&self) -> Time

Get the current logical time (delegates to kernel.now – single source of truth)

Corresponds to Lean: def State.time

pub fn tick(&mut self) -> Result<(), StateError>

Advance logical time via the kernel clock (single source of truth).

Uses checked arithmetic so overflow is explicit rather than silent.

Errors

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

pub fn kernel(&self) -> &KernelState

Get a reference to the kernel state

pub fn ghost(&self) -> &MetaState

Get a reference to the ghost state

pub fn get_plugin(&self, pid: PluginId) -> Option<&PluginState>

Get a plugin state

pub fn get_plugin_mut(&mut self, pid: PluginId) -> Option<&mut PluginState>

Get a mutable plugin state

pub fn insert_plugin( &mut self, pid: PluginId, ps: PluginState, ) -> Result<(), StateError>

Insert a plugin (checks for collision)

SECURITY: Returns error if plugin already exists to prevent silent overwrite.

Errors

Returns StateError::PluginExists if a plugin with the given ID is already registered.

pub fn get_actor(&self, aid: ActorId) -> Option<&ActorRuntime>

Get an actor runtime

pub fn get_actor_mut(&mut self, aid: ActorId) -> Option<&mut ActorRuntime>

Get a mutable actor runtime

pub fn insert_actor( &mut self, aid: ActorId, ar: ActorRuntime, ) -> Result<(), StateError>

Insert an actor (checks for collision)

SECURITY: Returns error if actor already exists to prevent silent overwrite.

Errors

Returns StateError::ActorExists if an actor with the given ID is already registered.

pub fn get_resource(&self, rid: ResourceId) -> Option<&ResourceInfo>

Get a resource

pub fn insert_resource( &mut self, rid: ResourceId, ri: ResourceInfo, ) -> Result<(), StateError>

Insert a resource (checks for collision)

SECURITY: Returns error if resource already exists to prevent silent overwrite.

Errors

Returns StateError::ResourceExists if a resource with the given ID is already registered.

pub fn get_workflow(&self, wid: WorkflowId) -> Option<&WorkflowInstance>

Get a workflow

pub fn get_workflow_mut( &mut self, wid: WorkflowId, ) -> Option<&mut WorkflowInstance>

Get a mutable workflow

pub fn insert_workflow( &mut self, wid: WorkflowId, wi: WorkflowInstance, ) -> Result<(), StateError>

Insert a workflow (checks for collision)

SECURITY: Returns error if workflow already exists to prevent silent overwrite.

Errors

Returns StateError::WorkflowExists if a workflow with the given ID is already registered.

pub fn plugin_count(&self) -> usize

Get the number of plugins

pub fn actor_count(&self) -> usize

Get the number of actors

pub fn resource_count(&self) -> usize

Get the number of resources

pub fn workflow_count(&self) -> usize

Get the number of workflows

pub fn plugin_ids(&self) -> Vec<PluginId>

Get all plugin IDs

pub fn resource_ids(&self) -> Vec<ResourceId>

Get all resource IDs

Trait Implementations

impl Clone for State

fn clone(&self) -> State

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for State

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

Formats the value using the given formatter.

impl Default for State

fn default() -> Self

Returns the “default value” for a type.