Struct PluginState 

pub struct PluginState { /* private fields */ }

State of a single plugin instance

Corresponds to Lean: @[ext] structure PluginState

INVARIANTS:

• heldCaps contains only capability IDs, not actual capabilities
• Validity of held capabilities is checked at use time via kernel lookup
• Memory bounds are immutable after creation
• Resource usage must not exceed quotas (DoS prevention)

Implementations

impl PluginState

pub fn empty(level: SecurityLevel, mem_size: Size) -> Self

Create empty plugin with given security level and memory size

Corresponds to Lean: def PluginState.empty (level : SecurityLevel) (memSize : Nat) : PluginState

pub fn with_quotas( level: SecurityLevel, mem_size: Size, memory_quota: u64, cap_quota: u64, ipc_queue_limit: u64, ) -> Self

Create plugin with custom quotas

Corresponds to Lean: def PluginState.withQuotas

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

Check if plugin holds a capability by ID

Corresponds to Lean: def PluginState.holds_cap (ps : PluginState) (capId : CapId) : Prop

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

Grant capability ID to plugin (idempotent)

Corresponds to Lean: def PluginState.grant_cap

Returns the new PluginState with the capability ID added.

pub fn grant_cap_mut(&mut self, cap_id: CapId)

Grant capability ID to plugin (mutating version)

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

Remove capability ID from plugin

Corresponds to Lean: def PluginState.revoke_cap

Returns the new PluginState with the capability ID removed.

pub fn revoke_cap_mut(&mut self, cap_id: CapId)

Remove capability ID from plugin (mutating version)

pub fn level(&self) -> SecurityLevel

Get the security level

pub fn memory(&self) -> &LinearMemory

Get a reference to the memory

pub fn held_cap_count(&self) -> usize

Get the number of held capabilities

pub fn local_state(&self) -> PluginLocal

Get the local state

pub fn held_caps(&self) -> Vec<CapId>

Get held capability IDs as a Vec

Note: Returns a cloned Vec. The Vec is maintained in sorted order.

pub fn held_caps_ref(&self) -> &Vec<CapId>

Get a reference to held capability IDs

pub fn memory_bounds(&self) -> Size

Get memory bounds

pub fn can_alloc_memory(&self, size: u64) -> bool

Check if memory allocation would exceed quota

Corresponds to Lean: def PluginState.canAllocMemory Returns false if addition would overflow (DoS prevention)

pub fn can_hold_cap(&self) -> bool

Check if plugin can hold another capability

Corresponds to Lean: def PluginState.canHoldCap

pub fn can_queue_ipc(&self, queue_len: u64) -> bool

Check if adding to IPC queue would exceed limit

Corresponds to Lean: def PluginState.canQueueIpc

pub fn alloc_memory(&mut self, size: u64) -> bool

Record memory allocation (update used counter)

Corresponds to Lean: def PluginState.allocMemory Returns false if quota would be exceeded

pub fn free_memory(&mut self, size: u64)

Record memory deallocation (update used counter)

Corresponds to Lean: def PluginState.freeMemory

pub fn memory_used(&self) -> u64

Get current memory usage

pub fn memory_quota(&self) -> u64

Get memory quota

pub fn cap_quota(&self) -> u64

Get capability quota

pub fn ipc_queue_limit(&self) -> u64

Get IPC queue limit

Trait Implementations

impl Clone for PluginState

fn clone(&self) -> PluginState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PluginState

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

Formats the value using the given formatter.

impl Default for PluginState

fn default() -> Self

Default plugin: Public level (no clearance), empty memory, no caps.

Corresponds to Lean: noncomputable instance : Inhabited PluginState

This is the semantically correct default - uninitialized plugins have no security privileges.

impl PartialEq for PluginState

fn eq(&self, other: &PluginState) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for PluginState

impl StructuralPartialEq for PluginState