Module io 

Specification and proof content for crate::mm::io.

Holds the tracked owner/view types (VmIoOwner, VmIoMemView), the trust-boundary axioms that bridge native Rust slices to the tracked memory model, and the wf/inv impls relating exec reader/writer handles to their ghost owners.

Structs

VmIoOwner

The owner of a VM I/O operation, which tracks the memory range and the memory view for the operation.

Enums

VmIoMemView

The memory view used for VM I/O operations.

Functions

axiom_kernel_mem_view

axiom_slice_in_kernel