Struct PluginInternal 

pub struct PluginInternal {
    pub reads: Vec<(MemAddr, Size)>,
    pub writes: Vec<(MemAddr, Size)>,
    pub consume_mailbox: bool,
}

Plugin internal computation descriptor

Corresponds to Lean: structure PluginInternal

Describes what a plugin’s internal WASM computation does:

• Memory regions read
• Memory regions written
• Whether to consume from mailbox

Fields

reads: Vec<(MemAddr, Size)>

Memory regions read

Corresponds to Lean: reads : List (MemAddr x Size)

writes: Vec<(MemAddr, Size)>

Memory regions written

Corresponds to Lean: writes : List (MemAddr x Size)

consume_mailbox: bool

Whether to consume from mailbox

Corresponds to Lean: consume_mailbox : Bool

Implementations

impl PluginInternal

pub fn new( reads: Vec<(MemAddr, Size)>, writes: Vec<(MemAddr, Size)>, consume_mailbox: bool, ) -> Self

Create a new plugin internal computation descriptor

pub fn compute() -> Self

Create a computation that just computes (no I/O)

pub fn with_reads(reads: Vec<(MemAddr, Size)>) -> Self

Create a computation that reads memory

pub fn with_writes(writes: Vec<(MemAddr, Size)>) -> Self

Create a computation that writes memory

pub fn check_preconditions( &self, state: &State, pid: PluginId, ) -> Result<(), StepError>

Check preconditions for plugin internal execution

Corresponds to Lean: def plugin_internal_pre

Preconditions:

1. Plugin is not blocked on another actor
2. Read regions are in bounds
3. Write regions are in bounds
4. If consuming mailbox, mailbox must not be empty

Errors

Returns StepError::PluginNotFound if the plugin does not exist. Returns StepError::PluginPreconditionFailed if the plugin’s actor is blocked. Returns StepError::PluginPreconditionFailed if a read region is out of bounds. Returns StepError::PluginPreconditionFailed if a write region is out of bounds. Returns StepError::PluginPreconditionFailed if consuming mailbox but the mailbox is empty.

Trait Implementations

impl Clone for PluginInternal

fn clone(&self) -> PluginInternal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PluginInternal

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

Formats the value using the given formatter.

impl Default for PluginInternal

fn default() -> PluginInternal

Returns the “default value” for a type.