Module embedding 

Deep embedding of the VmSpace and VmReader/VmWriter API.

VmStore is the abstract state of a caller of these APIs: it holds the MetaRegionOwners plus a registry of every owner object the caller currently has access to.

Op is an ADT enumerating the public exec API. lemma_step is the single proof-mode dispatcher; it requires s.inv() and the per-op precondition op_pre (which says the ids referenced in op resolve to existing entries with the right cross-store relationships). op_pre contains all preconditions necessary to dispatch each operation, which makes it the cornerstone of soundness. See its documentation for analysis.

Module layout

• vm_space: ops on the crate::mm::vm_space::VmSpace type (new, drop).
• cursor: ops on Cursor / CursorMut (open, drop, query, find_next, jump, map, unmap, protect_next).
• io: ops on VmReader / VmWriter (creation, drop, the user-space and kernel-space IO methods).
• trace: explicit-induction theorems over Seq<Op>.

Soundness boundary: _embedded axioms

Each axiom named <exec_function_path>_embedded mirrors the ensures clause of one public exec function. Naming is the only mechanism keeping the axiom in sync with its exec counterpart; reviewers touching either side should grep for the partner.

Modules

cursor

Embedding of Cursor / CursorMut operations: open, drop, navigation (query/find_next/jump), and mutation (map/unmap/protect_next).

frame

Embedding of Frame lifecycle operations: allocate (from_unused), acquire-by-paddr (from_in_use), and drop.

io

Embedding of VmReader / VmWriter operations.

kvirt_store

Kernel-side one-step-soundness store for the kernel virtual area API ([crate::mm::kspace::kvirt_area::KVirtArea]) — the kernel analog of super::VmStore.

list_store

Self-contained one-step-soundness harness for the frame LinkedList (crate::mm::frame::LinkedList) — the embedding’s companion to super::VmStore, specialised to linked-list operations.

segment

Embedding of Segment lifecycle operations: contiguous-range allocate (segment_from_unused_embedded) and drop (lemma_segment_drop_embedded).

trace

Lazy trace generation: run generates a trace on the fly by repeatedly stepping with arbitrary-but-valid Ops.

unique

Embedding of UniqueFrame lifecycle operations: allocate (unique_from_unused_embedded) and drop (unique_drop_embedded).

vm_space

Embedding of VmSpace-level operations: creation and drop.

Structs

CursorEntry

Per-cursor entry in the store.

FrameEntry

Per-Frame entry in the store. Represents one outstanding handle to the slot at paddr — i.e., one unit of refcount in regions.slot_owner(paddr).

SegmentEntry

Per-Segment entry in the store. Represents one outstanding Segment<M> covering the contiguous physical range range.

UniqueEntry

Per-UniqueFrame entry in the store.

VmIoEntry

Per-VmIo entry in the store.

VmStore

Resource store: the abstract state visible to a caller of the VmSpace + VmReader/VmWriter API.

Enums

CursorKind

Whether a cursor is a read-only Cursor or a mutable CursorMut.

Op

Public exec API of ostd::mm::vm_space and ostd::mm::io, lifted to data.

VmIoKind

Whether a VmIoOwner backs a VmReader or a VmWriter.

Functions

fresh_cursor_id

fresh_frame_id

fresh_segment_id

fresh_unique_id

fresh_vm_io_id

fresh_vm_space_id

handle_count

lemma_frame_drop_pre_derivable

lemma_fresh_cursor_id_not_in_dom

lemma_fresh_frame_id_not_in_dom

lemma_fresh_segment_id_not_in_dom

lemma_fresh_unique_id_not_in_dom

lemma_fresh_vm_io_id_not_in_dom

lemma_fresh_vm_space_id_not_in_dom

lemma_handle_count_insert_fresh

lemma_handle_count_remove

lemma_segment_cover_contains

lemma_segment_cover_insert_inside

lemma_segment_cover_insert_outside

lemma_segment_cover_remove_inside

lemma_segment_cover_remove_outside

lemma_segment_cover_shrink_front

lemma_segment_cover_split

lemma_segment_cover_witness

lemma_step

op_pre

segment_cover_count

tracked_cursor_entry_new

tracked_frame_entry_new

tracked_segment_entry_new

tracked_unique_entry_new

tracked_vm_io_entry_new

Type Aliases

CursorId

Logical identifier for a CursorOwner in the store.

FrameId

Logical identifier for a held crate::mm::frame::Frame handle in the store.

SegmentId

Logical identifier for a held crate::mm::frame::Segment handle in the store.

UniqueId

Logical identifier for a held crate::mm::frame::UniqueFrame handle in the store.

VmIoId

Logical identifier for a VmIoOwner in the store.

VmSpaceId

Logical identifier for a VmSpaceOwner in the store.