Enum HostFunction 

pub enum HostFunction {
    CapCall,
    CapSend,
    KernelAlloc,
    MemFree,
    CapRevoke,
    Declassify,
    ThreadCreate,
    ThreadConfigure,
    ThreadResume,
    ThreadSuspend,
    ThreadDestroy,
}

All host functions that cross the trust boundary (EROS-style 6 operations)

Corresponds to Lean: inductive HostFunctionId

EROS consolidation (13 -> 6):

• CapInvoke -> CapCall (synchronous capability invocation)
• CapDelegate, CapAccept -> User-space protocol over CapSend
• IpcSend -> CapSend (async message send)
• IpcReceive -> Removed (mailbox read via CapCall)
• MemAlloc, ResourceCreate, ResourceAccess -> KernelAlloc
• MemFree -> MemFree (keep separate for safety)
• CapRevoke -> CapRevoke (kernel operation)
• WorkflowStart, WorkflowStep -> Removed (user-space library)
• Declassify -> Declassify (IFC operation)

Variants

CapCall

Synchronous capability invocation (replaces cap_invoke)

Corresponds to Lean: | cap_call

CapSend

Async message send (replaces ipc_send; delegation is user-space protocol)

Corresponds to Lean: | cap_send

KernelAlloc

Kernel resource allocation (replaces mem_alloc, resource_create)

Corresponds to Lean: | kernel_alloc

MemFree

Memory deallocation (keep separate for safety)

Corresponds to Lean: | mem_free

CapRevoke

Capability revocation

Corresponds to Lean: | cap_revoke

Declassify

Controlled information declassification (IFC operation)

Corresponds to Lean: | declassify

ThreadCreate

Create new thread (requires ThreadControl capability)

Corresponds to Lean: | thread_create

ThreadConfigure

Configure thread bindings (requires ThreadControl capability)

Corresponds to Lean: | thread_configure

ThreadResume

Resume suspended thread (requires ThreadControl capability)

Corresponds to Lean: | thread_resume

ThreadSuspend

Suspend running thread (requires ThreadControl capability)

Corresponds to Lean: | thread_suspend

ThreadDestroy

Terminate thread (requires ThreadControl capability)

Corresponds to Lean: | thread_destroy

Implementations

impl HostFunction

pub const CAP_INVOKE: HostFunction = HostFunction::CapCall

👎Deprecated:

Use HostFunction::CapCall instead (EROS consolidation)

Legacy alias: CapInvoke -> CapCall

pub const IPC_SEND: HostFunction = HostFunction::CapSend

👎Deprecated:

Use HostFunction::CapSend instead (EROS consolidation)

Legacy alias: IpcSend -> CapSend

pub const MEM_ALLOC: HostFunction = HostFunction::KernelAlloc

👎Deprecated:

Use HostFunction::KernelAlloc instead (EROS consolidation)

Legacy alias: MemAlloc -> KernelAlloc

impl HostFunction

pub fn is_effectful(&self) -> bool

Check if this host function is effectful

All host functions cross the trust boundary, so all are effectful.

Corresponds to Lean: def is_effectful_host_call

pub fn is_declassify(&self) -> bool

Check if this is a declassify operation

Corresponds to Lean: def is_declassify

pub fn is_cap_operation(&self) -> bool

Check if this is a capability operation (may modify kernel.revocation)

Corresponds to Lean: def is_cap_operation

pub fn is_mem_operation(&self) -> bool

Check if this is a memory operation (modifies ghost state)

Corresponds to Lean: def is_mem_operation

pub fn execute( &self, state: &State, hc: &HostCall, result: &HostResult, ) -> Result<State, StepError>

Execute the host function

Corresponds to Lean: def KernelExecHost

Errors

Returns StepError::PluginNotFound if the caller plugin does not exist. Returns StepError::HostCallPreconditionFailed if function-specific preconditions are not met. Returns StepError::ActorNotFound if a destination actor does not exist (CapSend). Returns StepError::QuotaExceeded if the allocation would exceed the plugin’s memory quota (KernelAlloc). Returns StepError::AddressAlreadyFreed if the address is already freed (MemFree). Returns StepError::CapabilityTargetsAddress if a valid capability targets the address (MemFree). Returns StepError::CapabilityNotFound if the capability does not exist (CapRevoke).

pub fn execute_mut( &self, state: &mut State, hc: &HostCall, result: &HostResult, ) -> Result<(), StepError>

Execute the host function (mutating version).

Same validation as execute but modifies &mut State in place.

pub fn is_thread_operation(&self) -> bool

Check if this is a thread operation (requires ThreadControl capability)

Corresponds to Lean: thread_create/configure/resume/suspend/destroy

Trait Implementations

impl Clone for HostFunction

fn clone(&self) -> HostFunction

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for HostFunction

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

Formats the value using the given formatter.

impl Hash for HostFunction

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for HostFunction

fn eq(&self, other: &HostFunction) -> 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 Copy for HostFunction

impl Eq for HostFunction

impl StructuralPartialEq for HostFunction