ostd/specs/mm/page_table/cursor/

page_table_cursor_specs.rs

use vstd::{prelude::*, set_lib::*};
use vstd_extra::{arithmetic::*, ownership::*};

use crate::specs::{
    arch::NR_ENTRIES,
    mm::page_table::{cursor::owners::*, *},
};

use crate::arch::mm::PagingConsts;
use crate::mm::{
    Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_prop::PageProperty, page_table::*,
};
use core::ops::Range;

verus! {

/// A `CursorView` is not aware that the underlying structure of the page table is a tree.
/// It treats the page table as an array of mappings of various sizes, and the cursor itself as the
/// current virtual address, moving from low to high addresses. These functions specify its behavior
/// and provide a simple interface for reasoning about its behavior.
impl<C: PageTableConfig> CursorView<C> {
    pub open spec fn item_into_mapping(va: Vaddr, item: C::Item) -> Mapping {
        let (paddr, level, prop, _perm) = C::item_into_raw(item);
        let size = page_size::<PagingConsts>(level);
        Mapping {
            va_range: va as int..va + size,
            pa_range: paddr..(paddr + size) as Paddr,
            page_size: size,
            property: prop,
        }
    }

    /// This function checks if the current virtual address is mapped. It does not correspond
    /// to a cursor method itself, but defines what it means for an entry to present:
    /// there is a mapping whose virtual address range contains the current virtual address.
    pub open spec fn present(self) -> bool {
        self.mappings.filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end).len()
            > 0
    }

    pub open spec fn query_mapping(self) -> Mapping
        recommends
            self.present(),
    {
        self.mappings.filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end).choose()
    }

    pub open spec fn query(self, paddr: Paddr, size: usize, prop: PageProperty) -> bool {
        let m = self.query_mapping();
        m.pa_range.start == paddr && m.page_size == size && m.property == prop
    }

    pub open spec fn query_range(self) -> Range<int> {
        self.query_mapping().va_range
    }

    /// The VA range of the current slot when mapping a page of the given size.
    /// Works for both present and absent mappings: when present, equals query_range() for
    /// a mapping of that size; when absent, returns the aligned range that would be mapped.
    pub open spec fn cur_slot_range(self, size: usize) -> Range<int> {
        let start = nat_align_down(self.cur_va as nat, size as nat) as int;
        start..start + size
    }

    /// This predicate specifies the behavior of the `query` method. It states that the current item
    /// in the page table matches the given item, mapped at the resulting virtual address range.
    pub open spec fn query_item_spec(self, item: C::Item) -> Option<Range<Vaddr>>
        recommends
            self.present(),
    {
        let (paddr, level, prop, _perm) = C::item_into_raw_spec(item);
        let size = page_size::<PagingConsts>(level);
        if self.query(paddr, size, prop) {
            let r = self.query_range();
            Some(r.start as Vaddr..r.end as Vaddr)
        } else {
            None
        }
    }

    /// Jump just sets the current virtual address to the given address.
    pub open spec fn jump_spec(self, va: usize) -> Self {
        CursorView { cur_va: va as Vaddr, ..self }
    }

    /// Post-map cursor position: always advance by `size` from the aligned base.
    /// Matches `cursor.map` exec semantics (always calls `move_forward`, advancing by
    /// `page_size(level)` regardless of alignment).
    ///
    /// Do NOT substitute `vstd_extra::arithmetic::nat_align_up` here — that function
    /// leaves already-aligned inputs unchanged, which would mismatch exec.
    pub open spec fn align_up_spec(self, size: usize) -> Vaddr {
        (nat_align_down(self.cur_va as nat, size as nat) + size as nat) as Vaddr
    }

    pub open spec fn split_index(m: Mapping, new_size: usize, n: usize) -> Mapping {
        Mapping {
            va_range: m.va_range.start + n * new_size..m.va_range.start + (n + 1) * new_size,
            pa_range: (m.pa_range.start + n * new_size) as usize..(m.pa_range.start + (n + 1)
                * new_size) as usize,
            page_size: new_size,
            property: m.property,
        }
    }

    pub open spec fn split_if_mapped_huge_spec(self, new_size: usize) -> Self {
        let m = self.query_mapping();
        let size = m.page_size;
        let new_mappings = Set::<int>::range(0int, (size / new_size) as int).map(
            |n: int| Self::split_index(m, new_size, n as usize),
        );
        CursorView { cur_va: self.cur_va, mappings: self.mappings - set![m] + new_mappings, ..self }
    }

    pub open spec fn split_while_huge(self, size: usize) -> Self
        decreases self.query_mapping().page_size,
        when self.inv()
    {
        if self.present() {
            let m = self.query_mapping();
            if m.page_size > size {
                let new_size = m.page_size / NR_ENTRIES;
                let new_self = self.split_if_mapped_huge_spec(new_size);
                proof {
                    let f = self.mappings.filter(
                        |m2: Mapping| m2.va_range.start <= self.cur_va < m2.va_range.end,
                    );
                    vstd::set::lemma_set_choose_len(f);
                    assert(self.mappings.contains(m));
                    assert(m.inv());
                    assert(m.page_size % (m.page_size / 512usize) == 0) by {
                        if m.page_size == 4096 {
                            assert(4096usize % (4096usize / 512usize) == 0) by (compute_only);
                        } else if m.page_size == 2097152 {
                            assert(2097152usize % (2097152usize / 512usize) == 0) by (compute_only);
                        } else {
                            assert(1073741824usize % (1073741824usize / 512usize) == 0)
                                by (compute_only);
                        }
                    };
                    Self::split_if_mapped_huge_spec_preserves_present(self, new_size);
                    Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
                }
                new_self.split_while_huge(size)
            } else {
                self
            }
        } else {
            self
        }
    }

    pub open spec fn remove_subtree(self, size: usize) -> Set<Mapping> {
        let start = nat_align_down(self.cur_va as nat, size as nat) as Vaddr;
        let subtree = self.mappings.filter(|m: Mapping| start <= m.va_range.start < start + size);
        self.mappings - subtree
    }

    /// Inserts a mapping into the cursor. If there were previously mappings there,
    /// they are removed. Note that multiple mappings might be removed if they overlap with
    /// a new large mapping.
    pub open spec fn map_spec(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self {
        let new = Mapping {
            va_range: self.cur_slot_range(size),
            pa_range: paddr..(paddr + size) as usize,
            page_size: size,
            property: prop,
        };
        let split_self = self.split_while_huge(size);
        CursorView {
            cur_va: split_self.align_up_spec(size),
            mappings: split_self.remove_subtree(size) + set![new],
            ..split_self
        }
    }

    pub open spec fn map_simple(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self {
        let new = Mapping {
            va_range: self.cur_slot_range(size),
            pa_range: paddr..(paddr + size) as usize,
            page_size: size,
            property: prop,
        };
        CursorView { cur_va: self.cur_va, mappings: self.mappings + set![new], ..self }
    }

    /// Unmaps a range of virtual addresses from the current address up to `len` bytes.
    /// It returns the number of mappings that were removed.
    ///
    /// Because the implementation may split huge pages that straddle the range
    /// boundaries, the spec first applies `split_while_huge` at both `cur_va`
    /// and `cur_va + len` to obtain a "base" set of mappings where all boundary
    /// entries are at the finest granularity.  Mappings whose `va_range.start`
    /// falls in `[cur_va, cur_va + len)` are then removed from this base.
    pub open spec fn unmap_spec(self, len: usize, new_view: Self, num_unmapped: usize) -> bool {
        let start = self.cur_va;
        let end = (self.cur_va + len) as Vaddr;
        // Cursor advanced past the range.
        &&& new_view.cur_va
            >= end
        // Mappings fully outside [start, end) are preserved.
        // (A mapping that straddles a boundary may be split, but its sub-mappings
        // outside the range are present — see refinement clause.)
        &&& forall|m: Mapping| #[trigger]
            self.mappings.contains(m) && (m.va_range.end <= start || m.va_range.start >= end)
                ==> new_view.mappings.contains(
                m,
            )
        // No mapping in the new view starts inside [start, end), UNLESS it is
        // a sub-mapping of an old entry that straddled the start boundary.
        // (When a huge page straddles `start`, splitting it produces sub-mappings
        // whose `start` may fall inside [start, end) but before the cursor.)
        &&& forall|m: Mapping|
            new_view.mappings.contains(m) && start <= m.va_range.start < end ==> exists|
                parent: Mapping,
            | #[trigger]
                self.mappings.contains(parent) && parent.va_range.start < start
                    && parent.va_range.start <= m.va_range.start && m.va_range.end
                    <= parent.va_range.end && m.pa_range.start == (parent.pa_range.start + (
                m.va_range.start - parent.va_range.start)) as Paddr && m.property
                    == parent.property
            // New mappings are either from the old view or are sub-mappings of
            // old entries that straddled a boundary (refinement).
        &&& forall|m: Mapping| #[trigger]
            new_view.mappings.contains(m) ==> self.mappings.contains(m) || exists|parent: Mapping|
             #[trigger]
                self.mappings.contains(parent) && parent.va_range.start <= m.va_range.start
                    && m.va_range.end <= parent.va_range.end && m.pa_range.start == (
                parent.pa_range.start + (m.va_range.start - parent.va_range.start)) as Paddr
                    && m.property == parent.property
    }
}

} // verus!