ostd::specs::mm

Module embedding

Expand description

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. 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.

§Roadmap — DONE / open work

All five originally-deferred items have landed. Shape B for segments is fully active: Op::SegmentFromUnused / Op::SegmentDrop are in the dispatch, [accounting_inv] has the generalised rc == H + P + cover_count equation, and [structural_inv] carries raw_count == segment_cover_count + segment-covered ⟹ Frame-usage + segment range well-formedness.

Strengthen crate::specs::mm::frame::meta_owners::MetaSlotOwner::inv’s SHARED branch — DONE. The branch (0 < rc <= REF_COUNT_MAX) now carries inner_perms.storage.is_init() and inner_perms.in_list.value() == 0. The rc == 1 ⟹ ... guards on storage/in_list in [crate::mm::frame::Frame::drop_requires] were dropped.
Frame::wf(state) — DONE at both layers.
- Embedding layer: lemma_frame_drop_pre_derivable derives all of frame::drop_pre’s residuals (rc not in sentinels, rc <= REF_COUNT_MAX, storage.is_init, in_list == 0, rc == 1 ⟹ paths empty) plus the rc == 1 ⟹ handle_count == 1 clause from s.inv() + the FrameEntry’s registration + the segment-cover hypothesis. op_pre[FrameDrop] and step_frame_drop shrink to id-existence + segment-cover only.
- Exec layer: crate::mm::frame::Frame::inv_with_regions packages the per-handle cross-object validity (slot/pointer identity + SHARED rc bounds — > 0 ∧ ≠ UNUSED ∧ ≠ UNIQUE ∧ ≤ MAX). Frame::drop_requires is refactored to read self.inv_with_regions(s) ∧ raw_count == 0 ∧ rc == 1 ⟹ paths empty, which keeps the drop-specific bits explicit while consolidating the static “this Frame is valid against this state” conjuncts.
- clone_requires not refactored: would cascade into PageTableConfig::clone_requires_concrete (a trait method with multiple implementors); left explicit to keep the change local.
- Preservation of inv_with_regions (FUTURE). Frame::inv_with_regions’s preservation across drops of other handles at the same slot is currently informal (claimed in the docstring; no machine-checked proof). To prove it, every Frame<M> needs a tracked ghost “reference-count share” certificate that proves “I contribute 1 to my slot’s rc,” combined with an aggregate invariant on MetaSlotOwner saying held_shares == rc.value(). Recommended primitive: [vstd_extra::resource::ghost_resource::tokens::Token] (alias for CountGhost<(), TOTAL>) with TOTAL = REF_COUNT_MAX. The resource framework provides split / combine / agree / bounded pre-proven; the Frame side adds a Tracked<Token<MAX>> field and the MetaSlotOwner side adds a CountGhostResource<(), MAX> aggregate of remaining shares with the linking invariant rc.value() + remaining == MAX. Cursor map / unmap axioms gain share-juggling clauses (paths_in_pt += 1 ↔ split off 1 share). The math is proven by vstd_extra; the integration is a multi-day refactor with cascading effects on every MetaRegionOwners consumer. The embedding’s handle_count already provides the equivalent property at the abstract level, so this is only needed if downstream code outside the embedding’s tracking needs Frame::inv_with_regions preservation proofs.

3a. Op::Map consumes a FrameId — DONE. Op::Map { c, fid, prop } extracts the matching FrameEntry (so H at the mapped slot decrements by 1, paired with the cursor axiom’s paths_in_pt += 1 at the same slot). Combined with the cursor_mut_map_embedded axiom’s per-slot ensures (rc / usage / storage preserved at target, changed-slots ⟹ PT-node ⟹ usage != Frame), [accounting_inv]’s Frame-scoped equation rc == H + P chains.

3b. Op::Query clone modeling — DONE. The cursor_query_embedded axiom now returns Option<Paddr>: Some(paddr) when query resolved a tracked leaf and clone_item bumped rc at that slot; None otherwise (out-of-range / no leaf / MMIO leaf). [step_query] consumes the paddr to register a fresh FrameEntry so H at the cloned slot grows in lockstep with rc, keeping accounting_inv’s rc == H + P chained.

Strengthen cursor_mut_unmap_embedded — DONE. The axiom now mirrors exec: universal preservation of raw_count/in_list/usage/self_addr/vtable_ptr; storage preserved at slots ending non-UNUSED; rc doesn’t bump to UNIQUE; at Frame slots the “non-mapping count” rc - paths.len is invariant with both monotonically non- increasing, and post rc != 0 (Frame teardown collapses rc==0 to REF_COUNT_UNUSED atomically); MMIO slots are untouched (preserving the MetaSlotOwner::inv MMIO exception that allows non-empty paths_in_pt at UNUSED). [step_unmap] discharges accounting via case-splits on Frame / non-Frame / MMIO.
Shape-B segments — base + split landed; the rest is documented with status per op.
- from_unused / drop — DONE. Allocate a segment over a contiguous range of UNUSED frames, and release the segment’s forgotten references with per-frame teardown.
- split — DONE. Partition the segment at a page-aligned offset; regions is unchanged because per-paddr cover_count is invariant under the partition. lemma_segment_cover_split proves the per-paddr invariance.
- clone — NOT modeled, pending exec fix. Today exec Segment::clone bumps rc but not raw_count and doesn’t produce a new SegmentOwner, so the clone is un-droppable from verified code. Planned fix (separate session): generalise Frame::from_raw to raw_count >= 1 + decrement; weaken SegmentOwner::relate_regions to raw_count >= 1; replace RCClone for Segment with an inherent clone that returns (Self, Tracked<SegmentOwner<M>>) and per-frame from_in_use + ManuallyDrop::new. Once it ships, the embedding adds Op::SegmentClone { sid } that inserts a fresh SegmentEntry mirroring sid’s range.
- next — DONE. The conversion bridge between segment-held forgotten references and user-held Frame<M> handles. Per-paddr at the popped slot: raw_count -= 1, cover_count -= 1, H += 1, rc unchanged. The accounting equation rc == H + P + cover_count chains in lockstep because H and cover decrement/increment together; structural raw_count == cover_count chains via lemma_segment_cover_shrink_front.
- slice — NOT modeled, deferred for the same reason as clone (and probably HARDER, despite initial appearances). Both APIs produce an un-droppable handle (no SegmentOwner returned) and don’t bump raw_count. A faithful fix requires generalising Frame::from_raw’s precondition from raw_count <= 1 to raw_count >= 1 (with decrement-not- zero body) so that sliced/cloned segments — which produce multiple forgotten refs at the same slot — can each be drop-reclaimed. An attempted exec fix in this session revealed unanticipated cascade: borrow / borrow_paddr bridge through lemma_from_raw_manuallydrop_general which assumes the single-forgotten-ref case, and the PT-node child_perms_embedding invariant carries raw_count <= 1 without supplying a >= 1 companion. Tightening one half breaks the other. Properly resolving this requires either: (a) per-handle ghost certificates (the FrameCert route documented in the Item 2 future-work note above), or (b) splitting from_raw into two variants — one for the single-forgotten case (existing) and one for multi-forgotten (new) — and threading the discriminator through SegmentOwner so drop can pick the right one. Either path is half-day to multi-day work. slice and clone should be tackled together when that engineering effort is funded; the embedding side is ready to receive a cover_count + 1 / raw_count + 1 Op as soon as the exec ships the API.
- into_raw / from_raw — pub(crate) only in exec, so the embedding can ignore them.

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.
segment: Embedding of Segment lifecycle operations: contiguous-range allocate (segment_from_unused_embedded) and drop (segment_drop_embedded).
trace: Lazy trace generation: run generates a trace on the fly by repeatedly stepping with arbitrary-but-valid Ops.
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_owners[frame_to_index(paddr)].
SegmentEntry: Per-Segment entry in the store. Represents one outstanding Segment<M> covering the contiguous physical range range.
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§

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.
VmIoId: Logical identifier for a VmIoOwner in the store.
VmSpaceId: Logical identifier for a VmSpaceOwner in the store.