Struct CursorView 

pub struct CursorView<C: PageTableConfig> {
    pub cur_va: Vaddr,
    pub mappings: Set<Mapping>,
    pub phantom: PhantomData<C>,
}

Fields

cur_va: Vaddr

mappings: Set<Mapping>

phantom: PhantomData<C>

Implementations

impl<C: PageTableConfig> CursorView<C>

pub open spec fn non_overlapping(self) -> bool

{
    forall |m: Mapping, n: Mapping| {
        self.mappings.contains(m)
            ==> (self.mappings.contains(n)
                ==> (m != n
                    ==> m.va_range.end <= n.va_range.start
                        || n.va_range.end <= m.va_range.start))
    }
}

Mappings in the view are non-overlapping. This is a consequence of the page table tree structure: distinct paths map to disjoint VA ranges.

impl<C: PageTableConfig> CursorView<C>

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.

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,
    }
}

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
}

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

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
}

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

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 jump_spec(self, va: usize) -> Self

{
    CursorView {
        cur_va: va as Vaddr,
        ..self
    }
}

Jump just sets the current virtual address to the given address.

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 }

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

{
    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);
            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
}

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

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_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
    }
}

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;
    &&& new_view.cur_va >= end
    &&& forall |m: Mapping| {
        #[trigger] self.mappings.contains(m)
            && (m.va_range.end <= start || m.va_range.start >= end)
            ==> new_view.mappings.contains(m)
    }
    &&& 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
            }
    }
    &&& 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
                }
    }

}

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.

impl<C: PageTableConfig> CursorView<C>

pub proof fn split_if_mapped_huge_spec_preserves_present(v: Self, new_size: usize)

requires

v.inv(),

v.present(),

new_size > 0,

v.query_mapping().page_size > 0,

v.query_mapping().page_size % new_size == 0,

ensures

v.split_if_mapped_huge_spec(new_size).present(),

After split_if_mapped_huge_spec(new_size), a sub-mapping at cur_va still exists. The witness is split_index(m, new_size, k) where k = (cur_va - m.va_range.start) / new_size.

pub proof fn split_if_mapped_huge_spec_decreases_page_size(v: Self, new_size: usize)

requires

v.inv(),

v.present(),

new_size > 0,

v.query_mapping().page_size > new_size,

v.query_mapping().page_size % new_size == 0,

ensures

v.split_if_mapped_huge_spec(new_size).present(),

v.split_if_mapped_huge_spec(new_size).query_mapping().page_size
    < v.query_mapping().page_size,

After split_if_mapped_huge_spec(new_size) on a valid view, the mapping at cur_va has page_size == new_size < m.page_size.

The sub-mapping split_index(m, new_size, k) has page_size = new_size. No other mapping from the original view covers cur_va (non-overlapping), so query_mapping() must return a sub-mapping with page_size = new_size.

pub proof fn split_if_mapped_huge_spec_preserves_inv(v: Self, new_size: usize)

requires

v.inv(),

v.present(),

new_size > 0,

v.query_mapping().page_size > new_size,

v.query_mapping().page_size % new_size == 0,

set![4096usize, 2097152, 1073741824].contains(new_size),

ensures

v.split_if_mapped_huge_spec(new_size).inv(),

split_if_mapped_huge_spec preserves CursorView::inv().

Requires: v.inv(), v.present(), the mapping at cur_va has page_size > new_size, page_size % new_size == 0, and new_size is itself a valid page size.

pub broadcast proof fn lemma_split_while_huge_preserves_cur_va(self, size: usize)

requires

self.inv(),

size >= PAGE_SIZE,

ensures

#[trigger] self.split_while_huge(size).cur_va == self.cur_va,

split_while_huge only modifies mappings, not cur_va.

pub proof fn lemma_split_while_huge_preserves_inv(self, size: usize)

requires

self.inv(),

size >= PAGE_SIZE,

ensures

self.split_while_huge(size).inv(),

split_while_huge preserves CursorView::inv().

pub proof fn split_while_huge_compose(self, s1: usize, s2: usize)

requires

self.inv(),

s1 >= PAGE_SIZE,

s2 <= s1,

ensures

self.split_while_huge(s2) == self.split_while_huge(s1).split_while_huge(s2),

Composition law for split_while_huge: splitting to a finer target s2 <= s1 is the same as first splitting to s1 and then further splitting to s2.

pub proof fn split_while_huge_noop_implies_page_size_le(self, size: usize)

requires

self.inv(),

size >= PAGE_SIZE,

self.split_while_huge(size) == self,

self.present(),

ensures

self.query_mapping().page_size <= size,

When split_while_huge(size) is a no-op and the view is present(), the mapping at cur_va already has page_size <= size.

pub proof fn split_while_huge_one_step(self, size: usize)

requires

self.inv(),

self.present(),

self.query_mapping().page_size > size,

self.query_mapping().page_size / NR_ENTRIES == size,

self.query_mapping().page_size % size == 0,

set![4096usize, 2097152, 1073741824].contains(size),

ensures

self.split_while_huge(size).mappings == self.split_if_mapped_huge_spec(size).mappings,

When the mapping at cur_va is exactly one split-step above size (i.e. query_mapping().page_size / NR_ENTRIES == size), one step of split_while_huge equals split_if_mapped_huge_spec:

self.split_while_huge(size) == self.split_if_mapped_huge_spec(size)

This is because split_while_huge takes one step split_if_mapped_huge_spec(m.page_size / NR_ENTRIES) = split_if_mapped_huge_spec(size), then the sub-mapping at cur_va has page_size == size <= size, so it stops.

pub proof fn split_while_huge_locality(self, size: usize, m2: Mapping)

requires

self.inv(),

size >= PAGE_SIZE,

self.mappings.contains(m2),

!(m2.va_range.start <= self.cur_va < m2.va_range.end),

ensures

self.split_while_huge(size).mappings.contains(m2),

Locality of split_while_huge: a mapping m2 that is in self.mappings and whose VA range does not contain cur_va is preserved.

pub proof fn split_if_mapped_huge_spec_refinement(self, new_size: usize, e: Mapping)

requires

self.inv(),

self.present(),

new_size > 0,

self.query_mapping().page_size > new_size,

self.query_mapping().page_size % new_size == 0,

self.split_if_mapped_huge_spec(new_size).mappings.contains(e),

ensures

self.mappings.contains(e)
    || {
        let parent = self.query_mapping();
        &&& self.mappings.contains(parent)
        &&& parent.va_range.start <= e.va_range.start
        &&& e.va_range.end <= parent.va_range.end
        &&& e.pa_range.start
            == (parent.pa_range.start + (e.va_range.start - parent.va_range.start))
                as Paddr
        &&& e.property == parent.property

    },

Refinement: every mapping in split_while_huge(size).mappings is either from self.mappings or a sub-mapping of an entry in self.mappings. Base lemma: every mapping in split_if_mapped_huge_spec(new_size).mappings is either from the original mappings or a sub-mapping of query_mapping().

pub proof fn split_while_huge_refinement(self, size: usize, m: Mapping)

requires

self.inv(),

size >= PAGE_SIZE,

self.split_while_huge(size).mappings.contains(m),

ensures

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
    },

pub proof fn split_while_huge_disjoint(self, size: usize, other: Set<Mapping>)

requires

self.inv(),

size >= PAGE_SIZE,

forall |m: Mapping, x: Mapping| {
    #[trigger] self.mappings.contains(m) && #[trigger] other.contains(x)
        ==> Mapping::disjoint_vaddrs(m, x)
},

ensures

self.split_while_huge(size).mappings.disjoint(other),

split_while_huge produces a set disjoint from any set that is pairwise VA-disjoint from self.mappings.

Set-disjointness of other from self.mappings is not sufficient (counterexample: other = {split_index(m, k, 0)} collides with the first sub-mapping after one split step). We need VA-disjointness so that sub-mappings — which lie strictly inside the parent’s va_range and hence have distinct va_ranges from anything in other — cannot equal any element of other.

Trait Implementations

impl<C: PageTableConfig> Inv for CursorView<C>

open spec fn inv(self) -> bool

{
    &&& forall |m: Mapping| self.mappings.contains(m) ==> m.inv()
    &&& forall |m: Mapping| {
        self.mappings.contains(m)
            ==> {
                &&& vaddr_range_spec::<C>().start <= m.va_range.start
                &&& m.va_range.end <= vaddr_range_spec::<C>().end + 1

            }
    }
    &&& self.non_overlapping()

}