Enum KernelOp 

pub enum KernelOp {
    RouteOne {
        dst: ActorId,
    },
    WorkflowTick {
        wid: WorkflowId,
    },
    TimeTick,
    UnblockSend {
        dst: ActorId,
    },
    ThreadSwitch {
        from: ThreadId,
        to: ThreadId,
    },
}

Kernel-internal operations (no external trigger)

Corresponds to Lean: inductive KernelOp

Variants

RouteOne

Deliver one message to actor

Corresponds to Lean: | route_one (dst : ActorId)

Fields

dst: ActorId

Destination actor to receive the message

WorkflowTick

Advance workflow

Corresponds to Lean: | workflow_tick (w : WorkflowId)

Fields

wid: WorkflowId

Workflow to advance

TimeTick

Increment global time

Corresponds to Lean: | time_tick

UnblockSend

Unblock actor waiting to send

Corresponds to Lean: | unblock_send (dst : ActorId)

Fields

dst: ActorId

Destination actor to unblock

ThreadSwitch

Context switch between threads

Corresponds to Lean: | thread_switch (from_ to_ : ThreadId)

Fields

from: ThreadId

Thread to switch from

to: ThreadId

Thread to switch to

Implementations

impl KernelOp

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

Execute the kernel operation

Corresponds to Lean: def KernelExecInternal

Each operation modifies only its designated state component:

• route_one: moves message from pending to mailbox
• time_tick: increments global time
• workflow_tick: advances workflow state
• unblock_send: clears blockedOn for actor

Errors

Returns StepError::ActorNotFound if the destination actor does not exist (RouteOne, UnblockSend). Returns StepError::KernelOpFailed if the actor has no pending messages or its mailbox is full (RouteOne). Returns StepError::KernelOpFailed if the workflow is not found or is not running (WorkflowTick).

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

Execute the kernel operation (mutating version).

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

Trait Implementations

impl Clone for KernelOp

fn clone(&self) -> KernelOp

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for KernelOp

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

Formats the value using the given formatter.

impl PartialEq for KernelOp

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

impl StructuralPartialEq for KernelOp