ostd/specs/mm/

virt_mem.rs

//! 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.
//!
//! [`VmSpace`]: crate::mm::vm_space::VmSpace
use vstd::pervasive::arbitrary;
use vstd::prelude::*;

use vstd::layout;
use vstd::raw_ptr;
use vstd::set;
use vstd::set_lib;

use core::marker::PhantomData;
use core::ops::Range;

use crate::Pod;
use crate::mm::{Paddr, Vaddr, io::PodOnce};
use crate::prelude::Inv;
use crate::specs::arch::mm::MAX_PADDR;
use crate::specs::mm::page_table::Mapping;
use ostd_pod::{decode_pod, lemma_decode_pod_inverse, pod_bytes};

verus! {

/// Specification-level virtual pointer with an associated half-open range.
///
/// [`VirtPtr`] models a C-like pointer used by verification code:
/// - `vaddr` is the current cursor position;
/// - `range` is the allocation-like bounds `[start, end)`.
///
/// Most operations require `is_valid()` (i.e., the current pointer is within
/// range and not one-past-end), while offset operations additionally require
/// the computed address to stay inside the same range.
pub struct VirtPtr {
    /// Current virtual address represented by this pointer value.
    pub vaddr: Vaddr,
    /// Logical bounds of the pointer's valid object/range.
    pub range: Ghost<Range<Vaddr>>,
}

/// Byte contents of one physical frame range tracked in a [`MemView`].
///
/// This is the physical-memory side of the model: each frame base `Paddr` maps
/// to a [`FrameContents`] value whose metadata (`size`, `range`) constrains how
/// `contents` can be interpreted.
pub ghost struct FrameContents {
    /// Per-byte initialization/value state for this frame.
    pub contents: Seq<raw_ptr::MemContents<u8>>,
    /// Frame size in bytes.
    pub size: usize,
    /// Physical range covered by this frame, modeled as `[start, end)`.
    pub range: Range<Paddr>,
}

impl Inv for FrameContents {
    /// Well-formedness invariant for [`FrameContents`].
    ///
    /// # Invariant
    /// - `contents.len() == size`.
    /// - `size == range.end - range.start`.
    /// - `range.start` and `range.end` are aligned to `size`.
    /// - `range` is ordered and remains below [`MAX_PADDR`].
    open spec fn inv(self) -> bool {
        &&& self.contents.len() == self.size@
        &&& self.size@ == self.range.end - self.range.start
        &&& self.range.start % self.size == 0
        &&& self.range.end % self.size == 0
        &&& self.range.start <= self.range.end < MAX_PADDR
    }
}

/// A local virtual-memory view used in proofs.
///
/// A [`MemView`] pairs:
/// - [`Self::mappings`]: a set of [`Mapping`] entries used by [`Self::addr_transl`];
/// - [`Self::memory`]: frame bytes keyed by physical frame base (`Paddr`) via [`FrameContents`].
///
/// In practice this view is obtained from [`GlobalMemView`] using
/// [`GlobalMemView::take_view`], then consumed by APIs such as [`VirtPtr::read`],
/// [`VirtPtr::write`], and higher-level ownership proofs in
/// [`VmSpaceOwner`].
///
/// [`VmSpaceOwner`]: crate::mm::vm_space::vm_space_specs::VmSpaceOwner
pub tracked struct MemView {
    /// Virtual-to-physical mapping set used for address translation.
    pub mappings: Set<Mapping>,
    /// Physical frame contents for mapped pages referenced by [`Self::mappings`].
    pub memory: Map<Paddr, FrameContents>,
}

impl MemView {
    /// Translates a virtual address to `(frame_base_pa, frame_offset)`.
    ///
    /// Returns [`Option::None`] if no mapping in [`Self::mappings`] covers `va`.
    pub open spec fn addr_transl(self, va: usize) -> Option<(usize, usize)> {
        let mappings = self.mappings.filter(|m: Mapping| m.va_range.start <= va < m.va_range.end);
        if 0 < mappings.len() {
            let m = mappings.choose();  // In a well-formed PT there will only be one, but if malformed this is non-deterministic!
            let off = va - m.va_range.start;
            Some((m.pa_range.start, off as usize))
        } else {
            None
        }
    }

    /// Specification read through virtual translation.
    ///
    /// Equivalent to resolving via [`Self::addr_transl`] and reading from [`Self::memory`].
    pub open spec fn read(self, va: usize) -> raw_ptr::MemContents<u8> {
        let (pa, off) = self.addr_transl(va)->0;
        self.memory[pa].contents[off as int]
    }

    /// Specification write through virtual translation.
    ///
    /// Returns a new [`MemView`] with one byte updated, preserving all mappings.
    pub open spec fn write(self, va: usize, x: u8) -> Self {
        let (pa, off) = self.addr_transl(va)->0;
        MemView {
            memory: self.memory.insert(
                pa,
                FrameContents {
                    contents: self.memory[pa].contents.update(
                        off as int,
                        raw_ptr::MemContents::Init(x),
                    ),
                    ..self.memory[pa]
                },
            ),
            ..self
        }
    }

    /// Spec for writing `bytes.len()` bytes starting at `va`.
    ///
    /// `bytes[0]` is written to `va`, `bytes[1]` to `va + 1`, etc.
    pub open spec fn write_bytes(self, va: usize, bytes: Seq<u8>) -> Self
        decreases bytes.len(),
    {
        if bytes.len() == 0 {
            self
        } else {
            self.write(va, bytes[0]).write_bytes((va + 1) as usize, bytes.drop_first())
        }
    }

    /// Spec for reading `len` bytes starting at `va`.
    ///
    /// The byte at `va + i` is `self.read(va + i).value()`. Callers should only
    /// rely on the result when every byte in the range is initialized; otherwise
    /// the returned sequence contains arbitrary values where memory is `Uninit`.
    pub open spec fn read_bytes(self, va: usize, len: usize) -> Seq<u8>
        decreases len,
    {
        if len == 0 {
            Seq::empty()
        } else {
            seq![self.read(va).value()].add(self.read_bytes((va + 1) as usize, (len - 1) as usize))
        }
    }

    /// Lemma: [`Self::write_bytes`] preserves [`Self::mappings`].
    pub proof fn lemma_write_bytes_mappings(self, va: usize, bytes: Seq<u8>)
        ensures
            self.write_bytes(va, bytes).mappings == self.mappings,
        decreases bytes.len(),
    {
        if bytes.len() > 0 {
            self.write(va, bytes[0]).lemma_write_bytes_mappings(
                (va + 1) as usize,
                bytes.drop_first(),
            );
        }
    }

    /// Lemma: [`Self::write_bytes`] preserves [`Self::addr_transl`] at every address.
    pub proof fn lemma_write_bytes_addr_transl(self, va: usize, bytes: Seq<u8>, query: usize)
        ensures
            self.write_bytes(va, bytes).addr_transl(query) == self.addr_transl(query),
        decreases bytes.len(),
    {
        if bytes.len() > 0 {
            self.write(va, bytes[0]).lemma_write_bytes_addr_transl(
                (va + 1) as usize,
                bytes.drop_first(),
                query,
            );
        }
    }

    /// Lemma: [`Self::write_bytes`] only grows [`Self::memory`]'s domain.
    pub proof fn lemma_write_bytes_memory_dom_grows(self, va: usize, bytes: Seq<u8>)
        ensures
            self.memory.dom().subset_of(self.write_bytes(va, bytes).memory.dom()),
        decreases bytes.len(),
    {
        if bytes.len() > 0 {
            self.write(va, bytes[0]).lemma_write_bytes_memory_dom_grows(
                (va + 1) as usize,
                bytes.drop_first(),
            );
        }
    }

    /// Whether two virtual addresses denote equal byte contents in this view.
    pub open spec fn eq_at(self, va1: usize, va2: usize) -> bool {
        let (pa1, off1) = self.addr_transl(va1)->0;
        let (pa2, off2) = self.addr_transl(va2)->0;
        self.memory[pa1].contents[off1 as int] == self.memory[pa2].contents[off2 as int]
    }

    /// Whether `va` is translated and mapped to frame base `pa`.
    pub open spec fn is_mapped(self, va: usize, pa: usize) -> bool {
        self.addr_transl(va) is Some && self.addr_transl(va)->Some_0.0 == pa
    }

    /// Specification for borrowing a sub-view covering `[vaddr, vaddr + len)`.
    ///
    /// The result keeps overlapping mappings and restricts memory to physical
    /// frames reachable from that virtual range.
    pub open spec fn borrow_at(&self, vaddr: usize, len: usize) -> MemView {
        let range_end = vaddr + len;

        let valid_pas = Set::new(
            |pa: usize|
                exists|va: usize| vaddr <= va < range_end && #[trigger] self.is_mapped(va, pa),
        );

        MemView {
            mappings: self.mappings.filter(
                |m: Mapping| m.va_range.start < range_end && m.va_range.end > vaddr,
            ),
            memory: self.memory.restrict(valid_pas),
        }
    }

    /// Whether mappings in this view are pairwise VA-disjoint.
    pub open spec fn mappings_are_disjoint(self) -> bool {
        forall|m1: Mapping, m2: Mapping|
            #![trigger self.mappings.contains(m1), self.mappings.contains(m2)]
            self.mappings.contains(m1) && self.mappings.contains(m2) && m1 != m2 ==> {
                m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start
            }
    }

    /// Specification for splitting this view at `split_end = vaddr + len`.
    ///
    /// Returns `(left, right)` where:
    /// - `left` covers `[vaddr, split_end)`, i.e. all mappings overlapping that range.
    /// - `right` covers addresses `>= split_end`.
    pub open spec fn split(self, vaddr: usize, len: usize) -> (MemView, MemView) {
        let split_end = vaddr + len;

        // The left part.
        let left_mappings = self.mappings.filter(
            |m: Mapping| m.va_range.start < split_end && m.va_range.end > vaddr,
        );
        let right_mappings = self.mappings.filter(|m: Mapping| m.va_range.end > split_end);

        let left_pas = Set::new(
            |pa: usize| exists|va: usize| vaddr <= va < split_end && self.is_mapped(va, pa),
        );
        let right_pas = Set::new(
            |pa: usize| exists|va: usize| va >= split_end && self.is_mapped(va, pa),
        );

        (
            MemView { mappings: left_mappings, memory: self.memory.restrict(left_pas) },
            MemView { mappings: right_mappings, memory: self.memory.restrict(right_pas) },
        )
    }

    /// Tracked wrapper of [`Self::borrow_at`].
    ///
    /// # Verified Properties
    ///
    /// ## Postconditions
    /// - `r == self.borrow_at(vaddr, len)`.
    #[verifier::external_body]
    pub proof fn tracked_borrow_at(tracked &self, vaddr: usize, len: usize) -> (tracked r: MemView)
        ensures
            r == self.borrow_at(vaddr, len),
    {
        unimplemented!()
    }

    /// Tracked wrapper of [`Self::split`].
    ///
    /// # Verified Properties
    ///
    /// ## Postconditions
    /// - `r == self.split(vaddr, len)`.
    #[verifier::external_body]
    pub proof fn tracked_split(tracked self, vaddr: usize, len: usize) -> (tracked r: (Self, Self))
        ensures
            r == self.split(vaddr, len),
    {
        unimplemented!()
    }

    /// Lemma: [`Self::split`] preserves translation semantics on each side.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `original.split(vaddr, len) == (left, right)`.
    ///
    /// ## Postconditions
    /// - `right.memory.dom().subset_of(original.memory.dom())`.
    /// - For any `va` in `[vaddr, vaddr + len)`,
    ///   `original.addr_transl(va) == left.addr_transl(va)`.
    /// - For any `va >= vaddr + len`,
    ///   `original.addr_transl(va) == right.addr_transl(va)`.
    pub proof fn lemma_split_preserves_transl(
        original: MemView,
        vaddr: usize,
        len: usize,
        left: MemView,
        right: MemView,
    )
        requires
            original.split(vaddr, len) == (left, right),
        ensures
            right.memory.dom().subset_of(original.memory.dom()),
            forall|va: usize|
                vaddr <= va < vaddr + len ==> {
                    #[trigger] original.addr_transl(va) == left.addr_transl(va)
                },
            forall|va: usize|
                va >= vaddr + len ==> {
                    #[trigger] original.addr_transl(va) == right.addr_transl(va)
                },
    {
        assert(right.memory.dom().subset_of(original.memory.dom()));

        assert forall|va: usize| vaddr <= va < vaddr + len implies original.addr_transl(va)
            == left.addr_transl(va) by {
            assert(left.mappings =~= original.mappings.filter(
                |m: Mapping| m.va_range.start < vaddr + len && m.va_range.end > vaddr,
            ));
            let o_mappings = original.mappings.filter(
                |m: Mapping| m.va_range.start <= va < m.va_range.end,
            );
            let l_mappings = left.mappings.filter(
                |m: Mapping| m.va_range.start <= va < m.va_range.end,
            );

            assert(l_mappings <= o_mappings);
            assert forall|m: Mapping| #[trigger] o_mappings.contains(m) implies l_mappings.contains(
                m,
            ) by {
                assert(left.mappings.contains(m));
            };
            assert(o_mappings <= l_mappings);
            assert(o_mappings == l_mappings);
        }

        assert forall|va: usize| va >= vaddr + len implies original.addr_transl(va)
            == right.addr_transl(va) by {
            let split_end = vaddr + len;

            let o_mappings = original.mappings.filter(
                |m: Mapping| m.va_range.start <= va < m.va_range.end,
            );
            let r_mappings = right.mappings.filter(
                |m: Mapping| m.va_range.start <= va < m.va_range.end,
            );

            assert forall|m: Mapping| o_mappings.contains(m) implies r_mappings.contains(m) by {
                assert(right.mappings.contains(m));
                assert(r_mappings.contains(m));
            }

            assert(o_mappings == r_mappings);
        }
    }

    /// Specification for merging two views.
    ///
    /// Mappings are unioned, and memory conflicts are resolved by
    /// [`vstd::map::Map::union_prefer_right`] with `other` taking precedence.
    pub open spec fn join(self, other: MemView) -> MemView {
        MemView {
            mappings: self.mappings.union(other.mappings),
            memory: self.memory.union_prefer_right(other.memory),
        }
    }

    /// Tracked wrapper of [`Self::join`].
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `old(self).mappings.disjoint(other.mappings)`.
    ///
    /// ## Postconditions
    /// - `*self == old(self).join(other)`.
    #[verifier::external_body]
    pub proof fn tracked_join(tracked &mut self, tracked other: Self)
        requires
            old(self).mappings.disjoint(other.mappings),
        ensures
            *final(self) == old(self).join(other),
    {
        unimplemented!()
    }

    /// Lemma: splitting and then joining reconstructs the original view.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `this.split(vaddr, len) == (lhs, rhs)`.
    /// - Every mapping in `this` starts at or after `vaddr`.
    /// - Every physical frame tracked by `this.memory` is reachable from some
    ///   virtual address at or after `vaddr`.
    ///
    /// ## Postconditions
    /// - `lhs.join(rhs)` has the same mappings and memory contents as `this`.
    pub proof fn lemma_split_join_identity(
        this: MemView,
        lhs: MemView,
        rhs: MemView,
        vaddr: usize,
        len: usize,
    )
        requires
            this.split(vaddr, len) == (lhs, rhs),
            forall|m: Mapping| #[trigger]
                this.mappings.contains(m) ==> vaddr <= m.va_range.start < m.va_range.end,
            forall|pa: Paddr| #[trigger]
                this.memory.contains_key(pa) ==> exists|va: usize|
                    vaddr <= va && #[trigger] this.is_mapped(va, pa),
        ensures
            this.mappings == lhs.join(rhs).mappings,
            this.memory == lhs.join(rhs).memory,
    {
    }

    /// Lemma: byte-level reads agree on the right half of a split.
    ///
    /// For any `va >= vaddr + len` whose translated frame is present in
    /// `original.memory`, the stored frame contents at `va` match the
    /// original view. This is the byte-level analogue of
    /// [`Self::lemma_split_preserves_transl`] and supports propagating
    /// the read view across [`VmIoOwner::advance`] calls (used by loops
    /// over `read_once`).
    pub proof fn lemma_split_preserves_read(
        original: MemView,
        vaddr: usize,
        len: usize,
        left: MemView,
        right: MemView,
    )
        requires
            original.split(vaddr, len) == (left, right),
        ensures
            forall|va: usize|
                #![trigger original.read(va)]
                va >= vaddr + len && original.addr_transl(va) is Some
                    && original.memory.contains_key(original.addr_transl(va).unwrap().0)
                    ==> original.read(va) == right.read(va),
    {
        Self::lemma_split_preserves_transl(original, vaddr, len, left, right);
        let split_end = vaddr + len;
        let right_pas = Set::new(
            |pa: usize| exists|va: usize| va >= split_end && original.is_mapped(va, pa),
        );
        assert(right.memory =~= original.memory.restrict(right_pas));
        assert forall|va: usize|
            va >= split_end && original.addr_transl(va) is Some && original.memory.contains_key(
                original.addr_transl(va).unwrap().0,
            ) implies #[trigger] original.read(va) == right.read(va) by {
            assert(original.addr_transl(va) == right.addr_transl(va));
            let pa = original.addr_transl(va).unwrap().0;
            assert(original.is_mapped(va, pa));
            assert(right_pas.contains(pa));
            assert(right.memory[pa] == original.memory[pa]);
        }
    }

    /// Lemma: pointwise [`Self::read`] equality implies [`Self::read_bytes`] equality.
    pub proof fn lemma_read_bytes_eq_pointwise(a: MemView, b: MemView, va: usize, n: usize)
        requires
            forall|i: usize| va <= i < va + n ==> a.read(i) == b.read(i),
            va + n <= usize::MAX,
        ensures
            a.read_bytes(va, n) == b.read_bytes(va, n),
        decreases n,
    {
        if n == 0 {
            return;
        }
        assert(a.read(va) == b.read(va));
        Self::lemma_read_bytes_eq_pointwise(a, b, (va + 1) as usize, (n - 1) as usize);
    }
}

impl Inv for VirtPtr {
    open spec fn inv(self) -> bool {
        &&& self.range@.start <= self.vaddr <= self.range@.end
        &&& self.range@.end >= self.range@.start
    }
}

impl Clone for VirtPtr {
    fn clone(&self) -> (res: Self)
        ensures
            res == self,
    {
        Self { vaddr: self.vaddr, range: Ghost(self.range@) }
    }
}

impl Copy for VirtPtr {

}

impl VirtPtr {
    /// Creates a pointer at `vaddr` with logical range `[vaddr, vaddr + len)`.
    #[vstd::contrib::auto_spec]
    pub fn new(vaddr: Vaddr, len: usize) -> Self {
        Self { vaddr, range: Ghost(Range { start: vaddr, end: (vaddr + len) as usize }) }
    }

    /// Whether the pointer has consistent bounds.
    pub open spec fn is_defined(self) -> bool {
        self.range@.start <= self.vaddr <= self.range@.end
    }

    /// Whether dereferencing the current pointer position is allowed.
    ///
    /// This excludes the one-past-end position (`vaddr == range.end`).
    pub open spec fn is_valid(self) -> bool {
        &&& self.is_defined()
        &&& self.vaddr < self.range@.end
    }

    /// Reads one byte from `self.vaddr` in the provided memory view.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `mem.addr_transl(self.vaddr) is Some`.
    /// - Target byte is initialized:
    ///   `mem.memory[mem.addr_transl(self.vaddr).unwrap().0].contents[mem.addr_transl(self.vaddr).unwrap().1 as int] is Init`.
    /// - `self.is_valid()`.
    ///
    /// ## Postconditions
    /// - Returns `mem.read(self.vaddr).value()`.
    #[verifier::external_body]
    pub fn read(self, Tracked(mem): Tracked<&MemView>) -> u8
        requires
            mem.addr_transl(self.vaddr) is Some,
            mem.memory[mem.addr_transl(self.vaddr).unwrap().0].contents[mem.addr_transl(
                self.vaddr,
            ).unwrap().1 as int] is Init,
            self.is_valid(),
        returns
            mem.read(self.vaddr).value(),
    {
        unimplemented!()
    }

    /// Writes one byte to `self.vaddr` in the provided memory view.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `old(mem).addr_transl(self.vaddr) is Some`.
    /// - `self.is_valid()`.
    ///
    /// ## Postconditions
    /// - `*mem == old(mem).write(self.vaddr, x)`.
    #[verifier::external_body]
    pub fn write(self, Tracked(mem): Tracked<&mut MemView>, x: u8)
        requires
            old(mem).addr_transl(self.vaddr) is Some,
            self.is_valid(),
        ensures
            *final(mem) == old(mem).write(self.vaddr, x),
    {
        unimplemented!()
    }

    /// Reads a [`PodOnce`] value using one volatile memory load from a verified memory view.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `self.inv()`.
    /// - The readable range `[self.vaddr, self.vaddr + size_of::<T>())` must fit in `self.range@`.
    /// - `self.vaddr` must satisfy the alignment requirement of `T`.
    /// - Every byte in that range must translate in `mem` and be initialized.
    ///
    /// ## Safety
    /// - This function is trusted because the underlying volatile typed read relies on raw-pointer
    ///   operations that Verus does not yet model directly.
    #[verifier::external_body]
    pub fn read_volatile<T: PodOnce>(self, Tracked(mem): Tracked<&MemView>) -> (val: T)
        requires
            self.inv(),
            core::mem::size_of::<T>() <= self.range@.end - self.vaddr,
            self.vaddr % core::mem::align_of::<T>() == 0,
            forall|i: usize|
                #![trigger mem.addr_transl(i)]
                self.vaddr <= i < self.vaddr + core::mem::size_of::<T>() ==> {
                    &&& mem.addr_transl(i) is Some
                    &&& mem.memory.contains_key(mem.addr_transl(i).unwrap().0)
                    &&& mem.memory[mem.addr_transl(i).unwrap().0].contents[mem.addr_transl(
                        i,
                    ).unwrap().1 as int] is Init
                },
        ensures
            pod_bytes(val) == mem.read_bytes(self.vaddr, core::mem::size_of::<T>()),
    {
        let pnt = self.vaddr as *const T;
        unsafe { pnt.read_volatile() }
    }

    /// Writes a [`Pod`] value of size `size_of::<T>()` bytes using a volatile memory store
    /// to a verified memory view.
    ///
    /// For `T: PodOnce` the underlying store is non-tearing (single instruction). For
    /// arbitrary `T: Pod` the store may tear across multiple instructions but completes
    /// before this function returns.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `self.inv()`.
    /// - The writable range `[self.vaddr, self.vaddr + size_of::<T>())` must fit in `self.range@`.
    /// - `self.vaddr` must satisfy the alignment requirement of `T`.
    /// - Every byte in that range must translate in `mem`.
    ///
    /// ## Postconditions
    /// - The final memory equals `old(mem).write_bytes(self.vaddr, pod_bytes(val))`.
    /// - `mem.mappings` is unchanged (derivable from `write_bytes`, but stated
    ///   directly for caller convenience).
    /// - `mem.memory.dom()` can only grow (same).
    /// - `addr_transl` is preserved for every virtual address (same).
    ///
    /// ## Safety
    /// - This function is trusted because the underlying volatile typed write relies on raw-pointer
    ///   operations that Verus does not yet model directly.
    #[verifier::external_body]
    pub fn write_volatile<T: Pod>(self, Tracked(mem): Tracked<&mut MemView>, val: T)
        requires
            self.inv(),
            core::mem::size_of::<T>() <= self.range@.end - self.vaddr,
            self.vaddr % core::mem::align_of::<T>() == 0,
            forall|i: usize|
                #![trigger old(mem).addr_transl(i)]
                self.vaddr <= i < self.vaddr + core::mem::size_of::<T>() ==> {
                    &&& old(mem).addr_transl(i) is Some
                },
        ensures
            *final(mem) == old(mem).write_bytes(self.vaddr, pod_bytes(val)),
            final(mem).mappings == old(mem).mappings,
            old(mem).memory.dom().subset_of(final(mem).memory.dom()),
            forall|va: usize|
                #![trigger final(mem).addr_transl(va)]
                old(mem).addr_transl(va) == final(mem).addr_transl(va),
    {
        let pnt = self.vaddr as *mut T;
        unsafe { pnt.write_volatile(val) }
    }

    pub open spec fn add_spec(self, n: usize) -> Self {
        VirtPtr { vaddr: (self.vaddr + n) as usize, range: self.range }
    }

    /// Advances the pointer by `n` bytes.
    ///
    /// This operation only updates the cursor; it does not perform memory access.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `0 <= old(self).vaddr + n < usize::MAX`.
    ///
    /// ## Postconditions
    /// - `*self == old(self).add_spec(n)`.
    pub fn add(&mut self, n: usize)
        requires
    // Option 1: strict C standard compliance
    // old(self).range@.start <= self.vaddr + n <= old(self).range@.end,
    // Option 2: just make sure it doesn't overflow

            0 <= old(self).vaddr + n < usize::MAX,
        ensures
            *final(self) == old(self).add_spec(
                n,
            ),
    // If we take option 1, we can also ensure:
    // self.is_defined()

    {
        self.vaddr = self.vaddr + n
    }

    pub open spec fn sub_spec(self, n: usize) -> Self {
        VirtPtr { vaddr: (self.vaddr - n) as usize, range: self.range }
    }

    /// Returns a new pointer whose address is `self.vaddr` rewound by `n` bytes.
    ///
    /// Mirrors the shape of [`<*const T>::sub`] / [`<*mut T>::sub`] in the raw-pointer
    /// API: takes `self` by value and returns the new pointer.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `n <= self.vaddr` (no underflow).
    ///
    /// ## Postconditions
    /// - `res == self.sub_spec(n)`.
    pub fn sub(self, n: usize) -> (res: Self)
        requires
            n <= self.vaddr,
        returns
            self.sub_spec(n),
    {
        VirtPtr { vaddr: self.vaddr - n, range: self.range }
    }

    pub open spec fn wrapping_add_spec(self, n: usize) -> Self {
        VirtPtr { vaddr: self.vaddr.wrapping_add(n), range: self.range }
    }

    /// Returns a new pointer whose address is `self.vaddr` advanced by `n`
    /// bytes using wrapping arithmetic.
    pub fn wrapping_add(self, n: usize) -> (res: Self)
        returns
            self.wrapping_add_spec(n),
    {
        VirtPtr { vaddr: self.vaddr.wrapping_add(n), range: self.range }
    }

    /// Reinterprets `self.vaddr` as a typed raw pointer to `T`.
    ///
    /// This is purely a type cast; no memory access is performed and no
    /// alignment is checked. The returned pointer carries no provenance — it
    /// is suitable for runtime checks (e.g., `is_aligned`) and for unsafe
    /// volatile reads/writes whose preconditions are independently verified.
    #[verifier::external_body]
    pub fn cast<T>(self) -> (res: *mut T)
        ensures
            res as usize == self.vaddr,
    {
        self.vaddr as *mut T
    }

    pub open spec fn read_offset_spec(self, mem: MemView, n: usize) -> u8 {
        mem.read((self.vaddr + n) as usize).value()
    }

    /// Reads from `self.vaddr + n` without mutating `self`.
    ///
    /// Implemented by creating a temporary pointer and calling [`Self::read`].
    /// When `self.vaddr == self.range.start`, this behaves like array indexing.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `self.vaddr + n < usize::MAX`.
    /// - `self.range@.start <= self.vaddr + n < self.range@.end`.
    /// - `mem.addr_transl((self.vaddr + n) as usize) is Some`.
    /// - Target byte at offset is initialized.
    ///
    /// ## Postconditions
    /// - Returns `self.read_offset_spec(*mem, n)`.
    pub fn read_offset(&self, Tracked(mem): Tracked<&MemView>, n: usize) -> u8
        requires
            self.vaddr + n < usize::MAX,
            self.range@.start <= self.vaddr + n < self.range@.end,
            mem.addr_transl((self.vaddr + n) as usize) is Some,
            mem.memory[mem.addr_transl(
                (self.vaddr + n) as usize,
            ).unwrap().0].contents[mem.addr_transl(
                (self.vaddr + n) as usize,
            ).unwrap().1 as int] is Init,
        returns
            self.read_offset_spec(*mem, n),
    {
        let mut tmp = self.clone();
        tmp.add(n);
        tmp.read(Tracked(mem))
    }

    pub open spec fn write_offset_spec(self, mem: MemView, n: usize, x: u8) -> MemView {
        mem.write((self.vaddr + n) as usize, x)
    }

    /// Writes to `self.vaddr + n` without mutating `self`.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `self.inv()`.
    /// - `self.range@.start <= self.vaddr + n < self.range@.end`.
    /// - `old(mem).addr_transl((self.vaddr + n) as usize) is Some`.
    pub fn write_offset(&self, Tracked(mem): Tracked<&mut MemView>, n: usize, x: u8)
        requires
            self.inv(),
            self.vaddr + n < usize::MAX,
            self.range@.start <= self.vaddr + n < self.range@.end,
            old(mem).addr_transl((self.vaddr + n) as usize) is Some,
        ensures
            *final(mem) == self.write_offset_spec(*old(mem), n, x),
    {
        let mut tmp = self.clone();
        tmp.add(n);
        tmp.write(Tracked(mem), x)
    }

    pub open spec fn copy_offset_spec(
        src: Self,
        dst: Self,
        mem_src: MemView,
        mem_dst: MemView,
        n: usize,
    ) -> MemView {
        let x = src.read_offset_spec(mem_src, n);
        dst.write_offset_spec(mem_dst, n, x)
    }

    /// Copies one byte from `src + n` to `dst + n`.
    ///
    /// Source and destination are reasoned about via distinct memory views.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `src.inv()` and `dst.inv()`.
    /// - Source offset and destination offset are both in-range.
    /// - Source offset is mapped and initialized in `mem_src`.
    /// - Destination offset is mapped in `old(mem_dst)`.
    ///
    /// ## Postconditions
    /// - `*mem_dst == Self::copy_offset_spec(*src, *dst, *mem_src, *old(mem_dst), n)`.
    /// - `mem_dst.mappings == old(mem_dst).mappings`.
    /// - `mem_dst.memory.dom() == old(mem_dst).memory.dom()`.
    pub fn copy_offset(
        src: &Self,
        dst: &Self,
        Tracked(mem_src): Tracked<&MemView>,
        Tracked(mem_dst): Tracked<&mut MemView>,
        n: usize,
    )
        requires
            src.inv(),
            dst.inv(),
            src.vaddr + n < usize::MAX,
            dst.vaddr + n < usize::MAX,
            src.range@.start <= src.vaddr + n < src.range@.end,
            mem_src.addr_transl((src.vaddr + n) as usize) is Some,
            mem_src.memory.contains_key(mem_src.addr_transl((src.vaddr + n) as usize).unwrap().0),
            mem_src.memory[mem_src.addr_transl(
                (src.vaddr + n) as usize,
            ).unwrap().0].contents[mem_src.addr_transl(
                (src.vaddr + n) as usize,
            ).unwrap().1 as int] is Init,
            dst.range@.start <= dst.vaddr + n < dst.range@.end,
            old(mem_dst).addr_transl((dst.vaddr + n) as usize) is Some,
        ensures
            *final(mem_dst) == Self::copy_offset_spec(*src, *dst, *mem_src, *old(mem_dst), n),
            final(mem_dst).mappings == old(mem_dst).mappings,
            old(mem_dst).memory.dom().subset_of(final(mem_dst).memory.dom()),
    {
        let x = src.read_offset(Tracked(mem_src), n);
        dst.write_offset(Tracked(mem_dst), n, x)
    }

    pub open spec fn memcpy_spec(
        src: Self,
        dst: Self,
        mem_src: MemView,
        mem_dst: MemView,
        n: usize,
    ) -> MemView
        decreases n,
    {
        if n == 0 {
            mem_dst
        } else {
            let mem_dst_1 = Self::copy_offset_spec(src, dst, mem_src, mem_dst, (n - 1) as usize);

            Self::memcpy_spec(src, dst, mem_src, mem_dst_1, (n - 1) as usize)
        }
    }

    /// Copies `n` bytes from `src` to `dst` in the given memory view.
    ///
    /// `mem_src` and `mem_dst` are independent tracked memory views — the verifier
    /// enforces this by virtue of the `&MemView` / `&mut MemView` ownership pattern,
    /// so no vaddr-level non-overlap precondition is needed. (`mem_src` is never
    /// mutated during the copy; each byte is read from its original state.)
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `src.inv()` and `dst.inv()`.
    /// - Source slice `[src.vaddr, src.vaddr + n)` is in-range and initialized in `mem_src`.
    /// - Destination slice `[dst.vaddr, dst.vaddr + n)` is in-range and mapped in `old(mem_dst)`.
    ///
    /// ## Postconditions
    /// - `*mem_dst == Self::memcpy_spec(*src, *dst, *mem_src, *old(mem_dst), n)`.
    /// - `mem_dst.mappings == old(mem_dst).mappings`.
    /// - `mem_dst.memory.dom() == old(mem_dst).memory.dom()`.
    /// - Destination slice remains mapped in `mem_dst`.
    pub fn copy_nonoverlapping(
        src: &Self,
        dst: &Self,
        Tracked(mem_src): Tracked<&MemView>,
        Tracked(mem_dst): Tracked<&mut MemView>,
        n: usize,
    )
        requires
            src.inv(),
            dst.inv(),
            src.range@.start <= src.vaddr,
            src.vaddr + n <= src.range@.end,
            forall|i: usize|
                #![trigger mem_src.addr_transl(i)]
                src.vaddr <= i < src.vaddr + n ==> {
                    &&& mem_src.addr_transl(i) is Some
                    &&& mem_src.memory.contains_key(mem_src.addr_transl(i).unwrap().0)
                    &&& mem_src.memory[mem_src.addr_transl(
                        i,
                    ).unwrap().0].contents[mem_src.addr_transl(i).unwrap().1 as int] is Init
                },
            dst.range@.start <= dst.vaddr,
            dst.vaddr + n <= dst.range@.end,
            forall|i: usize|
                dst.vaddr <= i < dst.vaddr + n ==> {
                    &&& old(mem_dst).addr_transl(i) is Some
                },
        ensures
            *final(mem_dst) == Self::memcpy_spec(*src, *dst, *mem_src, *old(mem_dst), n),
            final(mem_dst).mappings == old(mem_dst).mappings,
            // dom() can only grow (writes may insert new pa keys).
            old(mem_dst).memory.dom().subset_of(final(mem_dst).memory.dom()),
            forall|i: usize|
                #![trigger final(mem_dst).addr_transl(i)]
                dst.vaddr <= i < dst.vaddr + n ==> {
                    &&& final(mem_dst).addr_transl(i) is Some
                },
        decreases n,
    {
        if n == 0 {
            return;
        } else {
            let ghost mem0 = *mem_dst;

            Self::copy_offset(src, dst, Tracked(mem_src), Tracked(mem_dst), n - 1);

            proof {
                assert(forall|i: usize|
                    dst.vaddr <= i < dst.vaddr + n - 1 ==> mem_dst.addr_transl(i)
                        == #[trigger] mem0.addr_transl(i));
                assert forall|i: usize|
                    dst.vaddr <= i < dst.vaddr + n - 1 implies mem_dst.addr_transl(i) is Some by {
                    assert(mem_dst.addr_transl(i) == mem0.addr_transl(i));
                }
            }

            Self::copy_nonoverlapping(src, dst, Tracked(mem_src), Tracked(mem_dst), n - 1);
        }
    }

    /// Builds a valid [`VirtPtr`] from a concrete virtual-address range.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `len <= usize::MAX - vaddr`.
    ///
    /// ## Postconditions
    /// - `r.range@.start == vaddr`.
    /// - `r.range@.end == (vaddr + len) as usize`.
    /// - When `len > 0`, the result is valid for dereferencing.
    pub fn from_vaddr(vaddr: usize, len: usize) -> (r: Self)
        requires
            len <= usize::MAX - vaddr,
        ensures
            r.inv(),
            r.vaddr == vaddr,
            r.range@.start == vaddr,
            r.range@.end == (vaddr + len) as usize,
            len > 0 ==> r.is_valid(),
    {
        Self { vaddr, range: Ghost(Range { start: vaddr, end: (vaddr + len) as usize }) }
    }

    /// Executable helper to split the [`VirtPtr`] into two contiguous ranges.
    ///
    /// This updates ghost ranges to match a split operation over the same region.
    ///
    /// # Verified Properties
    ///
    /// ## Preconditions
    /// - `self.is_valid()`.
    /// - `0 <= n <= self.range@.end - self.range@.start`.
    /// - `self.vaddr == self.range@.start`.
    ///
    /// ## Postconditions
    /// - Left pointer covers `[self.range@.start, self.range@.start + n)`.
    /// - Right pointer covers `[self.range@.start + n, self.range@.end)`.
    #[verus_spec(r =>
        requires
            self.is_valid(),
            0 <= n <= self.range@.end - self.range@.start,
            self.vaddr == self.range@.start,
        ensures
            r.0.range@.start == self.range@.start,
            r.0.range@.end == self.range@.start + n,
            r.0.vaddr == self.range@.start,
            r.1.range@.start == self.range@.start + n,
            r.1.range@.end == self.range@.end,
            r.1.vaddr == self.range@.start + n,
    )]
    pub fn split(self, n: usize) -> (Self, Self) {
        let left = VirtPtr {
            vaddr: self.vaddr,
            range: Ghost(Range { start: self.vaddr, end: (self.vaddr + n) as usize }),
        };

        let right = VirtPtr {
            vaddr: self.vaddr + n,
            range: Ghost(Range { start: (self.vaddr + n) as usize, end: self.range@.end }),
        };

        (left, right)
    }

    pub fn addr(&self) -> Vaddr
        returns
            self.vaddr,
    {
        self.vaddr
    }
}

/// A [`GlobalMemView`] is a more abstract view of memory that elides most of the details. The API specifications
/// of higher-level objects like [`VmSpaceOwner`](crate::specs::mm::vm_space::VmSpaceOwner) use this view.
pub tracked struct GlobalMemView {
    pub pt_mappings: Set<Mapping>,
    pub tlb_mappings: Set<Mapping>,
    pub unmapped_pas: Set<Paddr>,
    pub memory: Map<Paddr, FrameContents>,
}

impl Inv for GlobalMemView {
    open spec fn inv(self) -> bool {
        &&& forall|m: Mapping|
            #![auto]
            self.tlb_mappings.contains(m) ==> {
                &&& m.inv()
                &&& forall|pa: Paddr|
                    m.pa_range.start <= pa < m.pa_range.end ==> {
                        &&& self.memory.dom().contains(pa)
                    }
                &&& self.memory.contains_key(m.pa_range.start)
                &&& self.memory[m.pa_range.start].size == m.page_size
                &&& self.memory[m.pa_range.start].inv()
            }
        &&& forall|m: Mapping|
            forall|n: Mapping|
                #![auto]
                self.tlb_mappings.contains(m) ==> self.tlb_mappings.contains(n) ==> m != n
                    ==> #[trigger] m.va_range.end <= n.va_range.start || n.va_range.end
                    <= m.va_range.start
        &&& self.tlb_mappings.finite()
        &&& self.pt_mappings.finite()
        &&& self.memory.dom().finite()
        &&& self.all_pas_accounted_for()
        &&& self.pas_uniquely_mapped()
        &&& self.unmapped_correct()
    }
}

impl GlobalMemView {
    pub open spec fn addr_transl(self, va: usize) -> Option<(usize, usize)> {
        let mappings = self.tlb_mappings.filter(
            |m: Mapping| m.va_range.start <= va < m.va_range.end,
        );
        if 0 < mappings.len() {
            let m = mappings.choose();  // In a well-formed TLB there will only be one, but if malformed this is non-deterministic!
            let off = va - m.va_range.start;
            Some((m.pa_range.start, off as usize))
        } else {
            None
        }
    }

    pub open spec fn is_mapped(self, pa: usize) -> bool {
        exists|m: Mapping| self.tlb_mappings.contains(m) && m.pa_range.start <= pa < m.pa_range.end
    }

    pub open spec fn all_pas_accounted_for(self) -> bool {
        forall|pa: Paddr|
            0 <= pa < MAX_PADDR ==> #[trigger] self.is_mapped(pa)
                || #[trigger] self.unmapped_pas.contains(pa)
    }

    pub open spec fn pas_uniquely_mapped(self) -> bool {
        forall|m1: Mapping, m2: Mapping|
            #![trigger self.tlb_mappings.contains(m1), self.tlb_mappings.contains(m2)]
            self.tlb_mappings.contains(m1) && self.tlb_mappings.contains(m2) && m1 != m2
                ==> m1.pa_range.end <= m2.pa_range.start || m2.pa_range.end <= m1.pa_range.start
    }

    pub open spec fn unmapped_correct(self) -> bool {
        forall|pa: Paddr| #![auto] self.is_mapped(pa) <==> !self.unmapped_pas.contains(pa)
    }

    pub open spec fn take_view(self, vaddr: usize, len: usize) -> (Self, MemView) {
        let range_end = vaddr + len;

        let leave_mappings: Set<Mapping> = self.tlb_mappings.filter(
            |m: Mapping| m.va_range.end <= vaddr || m.va_range.start > range_end,
        );

        let take_mappings = self.tlb_mappings.filter(
            |m: Mapping| m.va_range.start < range_end && m.va_range.end > vaddr,
        );

        let leave_pas = Set::new(
            |pa: usize|
                exists|m: Mapping|
                    leave_mappings.contains(m) && m.pa_range.start <= pa < m.pa_range.end,
        );
        let take_pas = Set::new(
            |pa: usize|
                exists|m: Mapping|
                    take_mappings.contains(m) && m.pa_range.start <= pa < m.pa_range.end,
        );

        (
            GlobalMemView {
                tlb_mappings: leave_mappings,
                memory: self.memory.restrict(leave_pas),
                ..self
            },
            MemView { mappings: take_mappings, memory: self.memory.restrict(take_pas) },
        )
    }

    pub axiom fn tracked_take_view(tracked &mut self, vaddr: usize, len: usize) -> (tracked view:
        MemView)
        ensures
            *final(self) == old(self).take_view(vaddr, len).0,
            view == old(self).take_view(vaddr, len).1,
    ;

    pub open spec fn return_view(self, view: MemView) -> Self {
        GlobalMemView {
            tlb_mappings: self.tlb_mappings.union(view.mappings),
            memory: self.memory.union_prefer_right(view.memory),
            ..self
        }
    }

    pub axiom fn tracked_return_view(&mut self, view: MemView)
        ensures
            *final(self) == old(self).return_view(view),
    ;

    pub open spec fn tlb_flush_vaddr(self, vaddr: Vaddr) -> Self {
        let tlb_mappings = self.tlb_mappings.filter(
            |m: Mapping| m.va_range.end <= vaddr || vaddr < m.va_range.start,
        );
        GlobalMemView { tlb_mappings, ..self }
    }

    pub axiom fn tracked_tlb_flush_vaddr(&mut self, vaddr: Vaddr)
        requires
            old(self).inv(),
        ensures
            *final(self) == old(self).tlb_flush_vaddr(vaddr),
            final(self).inv(),
    ;

    pub open spec fn tlb_soft_fault(self, vaddr: Vaddr) -> Self {
        let mapping = self.pt_mappings.filter(
            |m: Mapping| m.va_range.start <= vaddr < m.va_range.end,
        ).choose();
        GlobalMemView { tlb_mappings: self.tlb_mappings.insert(mapping), ..self }
    }

    pub axiom fn tracked_tlb_soft_fault(tracked &mut self, vaddr: Vaddr)
        requires
            old(self).inv(),
            old(self).addr_transl(vaddr) is None,
        ensures
            *final(self) == old(self).tlb_soft_fault(vaddr),
            final(self).inv(),
    ;

    pub open spec fn pt_map(self, m: Mapping) -> Self {
        let pt_mappings = self.pt_mappings.insert(m);
        let unmapped_pas = self.unmapped_pas.difference(
            Set::new(|pa: usize| m.pa_range.start <= pa < m.pa_range.end),
        );
        GlobalMemView { pt_mappings, unmapped_pas, ..self }
    }

    pub axiom fn tracked_pt_map(&mut self, m: Mapping)
        requires
            forall|pa: Paddr|
                m.pa_range.start <= pa < m.pa_range.end ==> old(self).unmapped_pas.contains(pa),
            old(self).inv(),
        ensures
            *final(self) == old(self).pt_map(m),
    ;

    pub open spec fn pt_unmap(self, m: Mapping) -> Self {
        let pt_mappings = self.pt_mappings.remove(m);
        let unmapped_pas = self.unmapped_pas.union(
            Set::new(|pa: usize| m.pa_range.start <= pa < m.pa_range.end),
        );
        GlobalMemView { pt_mappings, unmapped_pas, ..self }
    }

    pub axiom fn tracked_pt_unmap(&mut self, m: Mapping)
        requires
            old(self).pt_mappings.contains(m),
            old(self).inv(),
        ensures
            *final(self) == old(self).pt_unmap(m),
            final(self).inv(),
    ;

    pub proof fn lemma_va_mapping_unique(self, va: usize)
        requires
            self.inv(),
            // Some mapping must cover `va` for the filter to be non-empty.
            self.addr_transl(va) is Some,
        ensures
            self.tlb_mappings.filter(
                |m: Mapping| m.va_range.start <= va < m.va_range.end,
            ).is_singleton(),
    {
        let f = self.tlb_mappings.filter(|m: Mapping| m.va_range.start <= va < m.va_range.end);
        // addr_transl is Some iff the filter is non-empty.
        assert(f.len() > 0);
        // Pairwise disjointness on tlb_mappings (from inv) plus both
        // mappings covering va forces equality.
        assert forall|m: Mapping, n: Mapping| f.contains(m) && f.contains(n) implies m == n by {
            assert(self.tlb_mappings.contains(m));
            assert(self.tlb_mappings.contains(n));
            assert(m.va_range.start <= va < m.va_range.end);
            assert(n.va_range.start <= va < n.va_range.end);
            // If m != n, pairwise disjointness gives va-disjoint, contradicting va ∈ both.
        };
    }
}

} // verus!