Module virt_mem_newer 

Virtual-memory specification model used by VmSpace proofs.

This module defines:

• VirtPtr, a specification-level virtual pointer over a bounded virtual range;
• FrameContents, a physical-frame content model with alignment and range invariants;
• MemView, a projection of virtual-to-physical mappings and frame contents that supports translation, read/write reasoning, borrowing, splitting, and joining.

The model is intentionally verification-oriented (Verus specs/proofs) and is used by crate::mm::vm_space to state and prove reader/writer permission isolation as well as correctness of low-level virtual memory operations that are used by them.

Structs

FrameContents

Byte contents of one physical frame range tracked in a MemView.

GlobalMemView

A GlobalMemView is a more abstract view of memory that elides most of the details. The API specifications of higher-level objects like VmSpaceOwner use this view.

MemView

A local virtual-memory view used in proofs.

VirtPtr

Specification-level virtual pointer with an associated half-open range.