Struct LinearMemory 

pub struct LinearMemory { /* private fields */ }

Linear memory region for a plugin (WASM model)

Corresponds to Lean: structure LinearMemory

INVARIANTS:

• All reads from uninitialized addresses return 0
• Writes only modify the specified address
• Bounds are immutable after creation

Uses 4KiB paged storage – only touched pages are allocated.

Implementations

impl LinearMemory

pub fn empty(size: Size) -> Self

Create empty linear memory with given size

Corresponds to Lean: def LinearMemory.empty (size : Nat) : LinearMemory

pub fn addr_in_bounds(&self, addr: MemAddr, len: Size) -> bool

Check if address is within bounds

Corresponds to Lean: def LinearMemory.addr_in_bounds

pub fn read(&self, addr: MemAddr) -> u8

Read byte at address (returns 0 for uninitialized / missing pages)

Corresponds to Lean: def LinearMemory.read (mem : LinearMemory) (addr : MemAddr) : UInt8

Note: Lean uses mem.bytes.getD addr 0 which returns 0 for missing keys.

pub fn write(&self, addr: MemAddr, val: u8) -> Self

Write byte at address

Corresponds to Lean: def LinearMemory.write

Returns the new memory state with the byte written.

pub fn write_mut(&mut self, addr: MemAddr, val: u8)

Write byte at address (mutating version)

This is an optimization for when we own the memory.

pub fn bounds(&self) -> Size

Get the memory bounds

pub fn written_bytes(&self) -> usize

Get the number of allocated bytes (pages * PAGE_SIZE)

pub fn is_empty(&self) -> bool

Check if memory is empty (no pages allocated)

pub fn read_range( &self, addr: MemAddr, len: Size, ) -> Result<Vec<u8>, MemoryError>

Read a range of bytes

Returns Err if the range would exceed bounds.

Errors

Returns MemoryError::OutOfBounds if the address plus length exceeds the memory bounds.

pub fn write_range( &self, addr: MemAddr, data: &[u8], ) -> Result<Self, MemoryError>

Write a range of bytes

Returns the new memory state with all bytes written.

Errors

Returns MemoryError::OutOfBounds if the address plus data length exceeds the memory bounds.

pub fn write_range_mut(&mut self, addr: MemAddr, data: &[u8])

Write a range of bytes (mutating version)

Trait Implementations

impl Clone for LinearMemory

fn clone(&self) -> LinearMemory

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LinearMemory

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

Formats the value using the given formatter.

impl Default for LinearMemory

fn default() -> Self

Default: empty memory with zero bounds

impl PartialEq for LinearMemory

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

impl StructuralPartialEq for LinearMemory