Module vm_space_embedding 

Deep embedding of the VmSpace API.

VmStore is the abstract state of a caller of the crate::mm::vm_space API: it holds the MetaRegionOwners plus a registry of every owner object (VmSpaceOwner, CursorOwner, VmIoOwner) the caller currently has access to.

Op is an ADT enumerating the public exec API of vm_space.rs. step is a single proof-mode dispatcher: step(s, op) requires s.inv() and ensures s.inv(). Because Verus chains pre/post automatically, induction over arbitrary call sequences is implicit: any program of the form step(s, op0); step(s, op1); ...; step(s, opN); typechecks iff s.inv() holds at every intermediate state.

Soundness boundary: _embedded axioms

Each axiom named <exec_function_path>_embedded mirrors the ensures clause of one public exec function in crate::mm::vm_space. For the embedding to be sound, every _embedded axiom must accurately reflect what its exec counterpart guarantees. The naming convention exists so a reviewer touching either side can grep for the partner. When the exec verus_spec for Foo::bar changes, search for foo_bar_embedded in this file and update it.

Internal helpers that don’t mirror an exec function (e.g. axiom_* lemmas about fresh_id) keep the axiom_ prefix to avoid being confused with the soundness-boundary axioms.

Structs

CursorEntry

Per-cursor entry in the store.

VmIoEntry

Per-VmIo entry in the store.

VmStore

Resource store: the abstract state visible to a caller of the VmSpace API.

Enums

CursorKind

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

CursorMethod

Internal: dispatch tag for [cursor_method_step] (cursor-only methods).

CursorMutRegionsMethod

Internal: dispatch tag for cursor methods that also touch MetaRegionOwners. Map is handled via its own [map_step] because its argument shape (UFrame, PageProperty) doesn’t match the others.

Op

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

VmIoKind

Whether a VmIoOwner backs a VmReader or a VmWriter.

Functions

axiom_cursor_entry_new

axiom_fresh_cursor_id_not_in_dom

axiom_fresh_vm_io_id_not_in_dom

axiom_fresh_vm_space_id_not_in_dom

axiom_vm_io_entry_new

cursor_find_next_embedded

cursor_jump_embedded

cursor_mut_map_embedded

cursor_mut_protect_next_embedded

cursor_mut_unmap_embedded

cursor_query_embedded

fresh_cursor_id

fresh_vm_io_id

fresh_vm_space_id

smoke_test

step

vm_space_cursor_embedded

vm_space_cursor_mut_embedded

vm_space_new_embedded

vm_space_reader_embedded

vm_space_writer_embedded

Type Aliases

CursorId

Logical identifier for a CursorOwner in the store.

VmIoId

Logical identifier for a VmIoOwner in the store.

VmSpaceId

Logical identifier for a VmSpaceOwner in the store.