Module io 

Embedding of VmReader / VmWriter operations.

Per-op steps operate on tracked owners directly — no store lookups, no preconditions on store membership, no if-guards. The store-side extract / insert and id-management lives in super::VmStore’s methods and the super::step dispatcher.

Methods modeled (per the visibility audit against upstream /home/sean/vostd/ostd/src/mm/io.rs):

• VmReader: read_val<T>, collect, limit, skip.
• VmWriter: write_val<T>, fill_zeros, limit, skip.
• VmReader: from_kernel_space, read.
• VmWriter: from_kernel_space, write.
• Pure-read methods (remain, has_remain, cursor on reader; avail, has_avail, cursor on writer): grouped under super::Op::ReaderQuery and super::Op::WriterQuery — handled directly by the dispatcher (no per-op step needed).

Mirroring exec preconditions

After the most recent exec spec changes, only Infallible read / write carry tracked owner params. The Fallible variants (read_val, collect, write_val) and Infallible read_val / write_val are handle-only — exec requires reduces to self.inv() (handle MODEL GAP). Their embedding ops are consequently no-ops on VmStore.

For Infallible read / write, the exec requires:

• owner.inv() — expressible.
• owner.has_write_view(), owner.read_view_initialized() — discharged via VmIoEntry::inv from activated && Writer/Reader.

Model gaps

• Exec VmReader / VmWriter handle: exec requires includes self.inv() and self.wf(owner) over the runtime handle. We don’t model the handle, so these conjuncts are MODEL GAPS.
• remain_spec / avail_spec-bound preconditions: skip requires nbytes <= self.remain_spec(). Handle-derived, inexpressible without the handle.
• from_kernel_space: exec ensures read_view_initialized() / has_write_view() only under a kernel-VA range guard (KERNEL_BASE_VADDR <= ptr.vaddr && ptr.vaddr+len <= KERNEL_END_VADDR). We assume that branch (i.e., the axioms commit to read_view_initialized() / has_write_view() unconditionally) — formally a slight strengthening pending kernel-VA modeling.

Enums

VmIoMethod

Dispatch tag for [vm_io_method_step] (single-owner mutator methods).

Functions

vm_reader_from_kernel_space_embedded

vm_reader_limit_embedded

vm_reader_read_embedded

vm_reader_skip_embedded

vm_space_reader_embedded

vm_space_writer_embedded

vm_writer_fill_zeros_embedded

vm_writer_from_kernel_space_embedded

vm_writer_limit_embedded

vm_writer_skip_embedded

vm_writer_write_embedded