Struct MetaState 

pub struct MetaState { /* private fields */ }

Ghost state for verification (not runtime)

Corresponds to Lean: structure MetaState

This tracks resource lifecycle for proofs about temporal safety. At runtime, only the freed_set is used for double-free prevention.

Implementations

impl MetaState

pub fn empty() -> Self

Create empty meta state

Corresponds to Lean: def MetaState.empty : MetaState

pub fn is_live(&self, addr: MemAddr) -> bool

Check if resource is live (allocated and not freed)

Corresponds to Lean: def MetaState.is_live (ms : MetaState) (addr : MemAddr) : Prop

pub fn alloc(&self, addr: MemAddr, owner: PluginId) -> Self

Mark resource as allocated

Corresponds to Lean: def MetaState.alloc

Returns the new MetaState with the resource marked as allocated.

pub fn free(&self, addr: MemAddr) -> Self

Mark resource as freed

Corresponds to Lean: def MetaState.free

Data Refinement Note (from Lean): The resources field is NOT updated. Only freed_set is used for double-free prevention.

pub fn alloc_mut(&mut self, addr: MemAddr, owner: PluginId)

Mark resource as allocated (mutating version)

pub fn free_mut(&mut self, addr: MemAddr) -> Result<(), MemoryError>

Mark resource as freed (mutating version)

Requires the resource to be currently allocated. Updates the resource status to Freed and adds the address to the freed set.

Errors

Returns MemoryError::DoubleFree if the address has already been freed. Returns MemoryError::NotAllocated if the address was never allocated.

pub fn allocated_count(&self) -> usize

Get the number of allocated resources

pub fn freed_count(&self) -> usize

Get the number of freed resources

pub fn resource_count(&self) -> usize

Get the number of resources in the map

pub fn is_freed(&self, addr: MemAddr) -> bool

Check if an address has been freed

pub fn get_status(&self, addr: MemAddr) -> Option<&ResourceStatus>

Get the status of a resource

Trait Implementations

impl Clone for MetaState

fn clone(&self) -> MetaState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for MetaState

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

Formats the value using the given formatter.

impl Default for MetaState

fn default() -> Self

Returns the “default value” for a type.

impl PartialEq for MetaState

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

impl StructuralPartialEq for MetaState