Struct PageTableOwner 

pub struct PageTableOwner<C: PageTableConfig>(pub OwnerSubtree<C>);

Verification Design

PageTableOwner is a wrapper around OwnerSubtree, which is a TreeNode. in a tree of EntryOwners. In turn, EntryOwner carries a enum that may be a FrameEntryOwner if the entry is a leaf node that maps a frame, or a NodeOwner if the entry is a sub-table. The root of the top-level page table owner should always be a NodeOwner.

Tuple Fields

0: OwnerSubtree<C>

Implementations

impl<C: PageTableConfig> PageTableOwner<C>

pub open spec fn query_leaf(self, va: Vaddr) -> Option<EntryOwner<C>>

{
    if self.0.value().is_frame() {
        Some(self.0.value())
    } else if self.0.value().is_node() && self.0.level() < INC_LEVELS - 1 {
        let idx = pte_index_spec::<C>(va, self.0.value().node().level());
        if 0 <= idx < NR_ENTRIES && self.0.has_child(idx as int) {
            PageTableOwner(self.0.child(idx as int)).query_leaf(va)
        } else {
            None
        }
    } else {
        None
    }
}

Resolves the actual leaf owner, retaining its tracked/untracked identity.

pub open spec fn pt_edge_at(parent: OwnerSubtree<C>, i: int) -> bool

{
    &&& parent.has_child(i)
    &&& parent.child(i).value().path.len() == parent.value().node().tree_level + 1
    &&& (parent
        .child(i)
        .value()
        .match_pte(
            parent.value().node().children_perm.value()[i],
            parent.value().node().level(),
        )
        || (parent.value().node().level() == NR_LEVELS && leading_bits_spec::<C>() == 0
            && parent
                .child(i)
                .value()
                .borrowed_match_pte(
                    parent.value().node().children_perm.value()[i],
                    parent.value().node().level(),
                )))
    &&& parent.child(i).value().path == parent.value().path.push_tail(i)
    &&& parent.child(i).value().parent_level == parent.value().node().level()

}

Per-edge constraint between a node-parent and its child at index i.

pub open spec fn pt_inv_at_depth(self, depth: nat) -> bool

{
    if depth == 0 {
        true
    } else if self.0.value().is_node() {
        forall |i: int| {
            0 <= i < NR_ENTRIES
                ==> Self::pt_edge_at(self.0, i)
                    && PageTableOwner(self.0.child(i))
                        .pt_inv_at_depth((depth - 1) as nat)
        }
    } else {
        forall |i: int| 0 <= i < NR_ENTRIES ==> !self.0.has_child(i)
    }
}

Depth-indexed PT-specific per-edge invariant. depth is a manifest fuel counter that decreases at each recursive call, so termination doesn’t depend on tree structure.

pub open spec fn pt_inv(self) -> bool

{
    &&& self.0.inv()
    &&& self.pt_inv_at_depth((INC_LEVELS - self.0.level()) as nat)

}

PT-specific tree invariant. Wraps self.0.inv() (the ghost tree’s structural invariants) and adds path identity, match_pte, parent_level, “nodes have all children Some”, and “non-nodes have all children None” recursively via pt_inv_at_depth.

pub proof fn pt_inv_unroll(self, i: int)

requires

self.pt_inv(),

self.0.value().is_node(),

0 <= i < NR_ENTRIES,

ensures

Self::pt_edge_at(self.0, i),

PageTableOwner(self.0.child(i)).pt_inv(),

pub proof fn pt_inv_non_node(self, i: int)

requires

self.pt_inv(),

!self.0.value().is_node(),

0 <= i < NR_ENTRIES,

ensures

!self.0.has_child(i),

pub proof fn lemma_non_node_pt_inv_at_depth(self, depth: nat)

requires

!self.0.value().is_node(),

forall |j: int| 0 <= j < NR_ENTRIES ==> !#[trigger] self.0.has_child(j),

ensures

self.pt_inv_at_depth(depth),

pt_inv_at_depth(depth) for a non-node subtree whose grandchildren are all None.

pub proof fn lemma_fresh_node_pt_inv(owner: OwnerSubtree<C>)

requires

owner.inv(),

owner.value().is_node(),

owner.children().len() == NR_ENTRIES,

forall |i: int| {
    0 <= i < NR_ENTRIES
        ==> {
            &&& #[trigger] owner.has_child(i)
            &&& !owner.child(i).value().is_node()
            &&& owner.child(i).value().path.len() == owner.value().node().tree_level + 1
            &&& owner
                .child(i)
                .value()
                .match_pte(
                    owner.value().node().children_perm.value()[i],
                    owner.value().node().level(),
                )
            &&& owner.child(i).value().path == owner.value().path.push_tail(i)
            &&& owner.child(i).value().parent_level == owner.value().node().level()

        }
},

allocated_empty_node_grandchildren_none(owner),

ensures

PageTableOwner(owner).pt_inv(),

A fresh node with correctly rebased absent or frame children satisfies pt_inv.

pub proof fn lemma_split_node_view(self, old: Self)

requires

self.0.inv(),

old.0.inv(),

self.0.value().is_node(),

old.0.value().is_frame(),

self.0.value().path == old.0.value().path,

old.0.value().path.len() == old.0.level(),

old.0.level() + old.0.value().parent_level == INC_LEVELS,

1 < old.0.value().parent_level < NR_LEVELS,

forall |i: int| {
    0 <= i < NR_ENTRIES
        ==> {
            let child = self.0.child(i).value();
            &&& #[trigger] self.0.has_child(i)
            &&& child.is_frame()
            &&& child.path == old.0.value().path.push_tail(i)
            &&& child.parent_level == old.0.value().parent_level - 1
            &&& child.frame().prop == old.0.value().frame().prop
            &&& child.frame().mapped_pa
                == old.0.value().frame().mapped_pa
                    + i
                        * page_size::<
                            PagingConsts,
                        >((old.0.value().parent_level - 1) as PagingLevel)

        }
},

ensures

self.view_rec(self.0.value().path)
    == Set::<int>::range(0, NR_ENTRIES as int)
        .map(|i: int| CursorView::<
            C,
        >::split_index(
            old.view_rec(old.0.value().path).choose(),
            page_size::<PagingConsts>((old.0.value().parent_level - 1) as PagingLevel),
            i as usize,
        )),

The frames produced by a huge-page split have exactly the split mapping view.

pub open spec fn view_rec_node_children( self, path: TreePath<NR_ENTRIES>, ) -> Seq<Set<Mapping>>

{
    self.0
        .children()
        .map(|i, child: Option<OwnerSubtree<C>>| {
            if child is Some {
                PageTableOwner(child->0).view_rec(path.push_tail(i))
            } else {
                Set::empty()
            }
        })
}

pub open spec fn view_rec(self, path: TreePath<NR_ENTRIES>) -> Set<Mapping>

{
    if self.0.value().is_frame() {
        let va = vaddr_of::<C>(path);
        let pt_level = INC_LEVELS - path.len();
        let page_size = page_size::<PagingConsts>(pt_level as PagingLevel);
        set![
            Mapping { va_range : Range { start : va as int, end : va + page_size },
            pa_range : Range { start : self.0.value().frame().mapped_pa, end : (self.0
            .value().frame().mapped_pa + page_size) as Paddr, }, page_size : page_size,
            property : self.0.value().frame().prop, }
        ]
    } else if self.0.value().is_node() && path.len() < INC_LEVELS - 1 {
        self.view_rec_node_children(path).to_set().flatten()
    } else {
        set![]
    }
}

pub broadcast proof fn lemma_view_rec_contains_intro( self, path: TreePath<NR_ENTRIES>, m: Mapping, i: int, )

requires

self.0.inv(),

path.len() < INC_LEVELS - 1,

self.0.value().is_node(),

0 <= i < self.0.children().len(),

self.0.has_child(i),

#[trigger]
PageTableOwner(self.0.children()[i]->0).view_rec(path.push_tail(i)).contains(m),

ensures

self.view_rec(path).contains(m),

pub broadcast proof fn lemma_view_rec_contains(self, path: TreePath<NR_ENTRIES>)

requires

self.0.inv(),

path.len() < INC_LEVELS - 1,

self.0.value().is_node(),

ensures

forall |m: Mapping| {
    self.view_rec(path).contains(m)
        ==> exists |i: int| {
            0 <= i < self.0.children().len() && self.0.children()[i] is Some
                && PageTableOwner(self.0.children()[i]->0)
                    .view_rec(path.push_tail(i))
                    .contains(m)
        }
},

pub proof fn view_rec_contains_choose( self, path: TreePath<NR_ENTRIES>, m: Mapping, ) -> i : int

requires

self.0.inv(),

path.len() < INC_LEVELS - 1,

self.view_rec(path).contains(m),

self.0.value().is_node(),

ensures

0 <= i < self.0.children().len() && self.0.children()[i] is Some
    && PageTableOwner(self.0.children()[i]->0).view_rec(path.push_tail(i)).contains(m),

pub proof fn lemma_vaddr_push_tail_eq(path: TreePath<NR_ENTRIES>, i: int)

requires

path.inv(),

path.len() < INC_LEVELS - 1,

0 <= i < NR_ENTRIES,

ensures

vaddr(path.push_tail(i))
    == vaddr(path)
        + i * page_size::<PagingConsts>((INC_LEVELS - path.len() - 1) as PagingLevel),

vaddr(path)
    + (i + 1) * page_size::<PagingConsts>((INC_LEVELS - path.len() - 1) as PagingLevel)
    <= usize::MAX,

Appending an index advances the VA by the entry size at that depth.

pub proof fn lemma_view_rec_vaddr_range(self, path: TreePath<NR_ENTRIES>, m: Mapping)

requires

self.pt_inv(),

path.inv(),

path.len() <= INC_LEVELS - 1,

path.len() == self.0.level(),

self.0.value().parent_level == (INC_LEVELS - self.0.level()) as PagingLevel,

self.view_rec(path).contains(m),

ensures

vaddr_of::<C>(path) <= m.va_range.start,

m.va_range.start < m.va_range.end,

m.va_range.end
    <= vaddr_of::<C>(path)
        + page_size::<PagingConsts>((INC_LEVELS - path.len()) as PagingLevel),

pub proof fn lemma_view_rec_top_index_va_bound( self, path: TreePath<NR_ENTRIES>, m: Mapping, t: int, )

requires

self.pt_inv(),

path.inv(),

1 <= path.len() <= INC_LEVELS - 1,

path.len() == self.0.level(),

self.0.value().parent_level == (INC_LEVELS - self.0.level()) as PagingLevel,

path[0] < t,

self.view_rec(path).contains(m),

ensures

(path[0]) * page_size::<C>(C::NR_LEVELS()) + page_table_coverage_start_spec::<C>()
    <= m.va_range.start,

m.va_range.start < m.va_range.end,

m.va_range.end
    <= t * page_size::<C>(C::NR_LEVELS()) + page_table_coverage_start_spec::<C>(),

Bounds subtree mappings by their top-level slot and the configuration’s upper-address contribution, using the configured top-level page size.

pub proof fn lemma_pt_inv_implies_path_correct( subtree: OwnerSubtree<C>, path: TreePath<NR_ENTRIES>, )

requires

PageTableOwner(subtree).pt_inv(),

subtree.value().path == path,

ensures

subtree.subtree_satisfies(path, Self::path_correct_pred()),

pt_inv (plus the root’s recorded path) lifts to a full path_correct_pred tree predicate: every entry’s .path field equals its structural position. This also applies to leaf/frame-rooted child subtrees of a cursor continuation.

pub proof fn lemma_no_frame_with_path_rec( self, path: TreePath<NR_ENTRIES>, removed_path: TreePath<NR_ENTRIES>, ambient: Set<Mapping>, )

requires

self.pt_inv(),

path.inv(),

path.len() <= INC_LEVELS - 1,

path.len() == self.0.level(),

self.0.value().parent_level == (INC_LEVELS - self.0.level()) as PagingLevel,

self.0.value().path == path,

self.0.subtree_satisfies(path, Self::path_correct_pred()),

forall |mm: Mapping| self.view_rec(path).contains(mm) ==> ambient.contains(mm),

forall |mm: Mapping| {
    ambient.contains(mm) ==> mm.va_range.start != vaddr_of::<C>(removed_path)
},

ensures

self
    .0
    .subtree_satisfies(
        path,
        |e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>| {
            e.is_frame() ==> e.path != removed_path
        },
    ),

Forward dual of Self::lemma_view_rec_vaddr_range: in a pt_inv, path-correct subtree whose mappings are all contained in ambient, if no mapping in ambient starts at vaddr_of(removed_path), then no frame entry anywhere in the subtree carries removed_path as its path. A frame entry at structural position pos contributes exactly one mapping starting at vaddr_of(pos); path-correctness makes pos == entry.path, so a frame with .path == removed_path would force a mapping starting at vaddr_of(removed_path) into ambient — a contradiction.

pub proof fn lemma_view_rec_disjoint_vaddrs( self, path: TreePath<NR_ENTRIES>, m1: Mapping, m2: Mapping, )

requires

self.pt_inv(),

path.inv(),

path.len() <= INC_LEVELS - 1,

path.len() == self.0.level(),

self.0.value().parent_level == (INC_LEVELS - self.0.level()) as PagingLevel,

self.view_rec(path).contains(m1),

self.view_rec(path).contains(m2),

m1 != m2,

ensures

m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start,

pub proof fn lemma_view_rec_mapping_page_size(self, path: TreePath<NR_ENTRIES>)

requires

self.pt_inv(),

path.len() <= INC_LEVELS - 1,

path.len() == self.0.level(),

self.0.value().parent_level == (INC_LEVELS - self.0.level()) as PagingLevel,

ensures

forall |m: Mapping| {
    #[trigger] self.view_rec(path).contains(m)
        ==> set![4096usize, 2097152usize, 1073741824usize].contains(m.page_size)
},

Every mapping in view_rec has page_size ∈ {4K, 2M, 1G}.

pub proof fn lemma_view_rec_mapping_inv(self, path: TreePath<NR_ENTRIES>)

requires

self.pt_inv(),

path.inv(),

path.len() <= INC_LEVELS - 1,

path.len() == self.0.level(),

self.0.value().parent_level == (INC_LEVELS - self.0.level()) as PagingLevel,

ensures

forall |m: Mapping| #[trigger] self.view_rec(path).contains(m) ==> m.inv(),

Every mapping in view_rec satisfies Mapping::inv().

pub proof fn lemma_view_rec_absent_empty(self, path: TreePath<NR_ENTRIES>)

requires

self.0.inv(),

self.0.value().is_absent(),

path.len() <= INC_LEVELS - 1,

ensures

self.view_rec(path) == set![],

An absent entry contributes no mappings - view_rec returns the empty set.

pub proof fn lemma_view_rec_nr_children_zero_empty(self, path: TreePath<NR_ENTRIES>)

requires

self.pt_inv(),

self.0.value().is_node(),

self.0.value().node().meta_own.nr_children.value() == 0,

self.0.value().node().count_consistent(),

path.len() <= INC_LEVELS - 1,

path.len() == self.0.level(),

ensures

self.view_rec(path) == set![],

A node with nr_children == 0 has no present PTEs, so all children are absent and the subtree contributes no mappings.

count_consistent ties nr_children to count_present(children_perm), so nr_children == 0 forces every PTE absent. pt_edge_at (from pt_inv) then forces each ghost child is_absent — its view_rec is ∅ — and lemma_view_rec_contains lifts that to the whole node’s view_rec. (At the top level the borrowed edge disjunct is ruled out: borrowed_match_pte needs a present PTE, which count_present == 0 denies.)

pub open spec fn metaregion_sound_pred( regions: MetaRegionOwners, ) -> FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>

{ |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions) }

pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool

{ self.0.subtree_satisfies(self.0.value().path, Self::metaregion_sound_pred(regions)) }

pub proof fn lemma_metaregion_sound_preserved_slot_owners_eq( self, r0: MetaRegionOwners, r1: MetaRegionOwners, )

requires

self.inv(),

self.metaregion_sound(r0),

r0.slot_owners == r1.slot_owners,

forall |k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),

forall |k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],

ensures

self.metaregion_sound(r1),

PageTableOwner::metaregion_sound is preserved across regions changes that (a) keep slot_owners exactly equal and (b) only grow the slots map (existing keys preserved with the same values). Both conditions are satisfied by Entry::to_ref and similar borrow_paddr operations.

pub proof fn lemma_metaregion_sound_preserved_slot_owners_eq_subtree( subtree: OwnerSubtree<C>, path: TreePath<NR_ENTRIES>, r0: MetaRegionOwners, r1: MetaRegionOwners, )

requires

subtree.inv(),

subtree.subtree_satisfies(path, Self::metaregion_sound_pred(r0)),

r0.slot_owners == r1.slot_owners,

forall |k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),

forall |k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],

ensures

subtree.subtree_satisfies(path, Self::metaregion_sound_pred(r1)),

Recursive helper: same preservation property, applied to an arbitrary subtree.

pub proof fn lemma_metaregion_sound_preserved_one_slot_changed_subtree( subtree: OwnerSubtree<C>, path: TreePath<NR_ENTRIES>, r0: MetaRegionOwners, r1: MetaRegionOwners, changed_idx: int, )

requires

subtree.inv(),

subtree.subtree_satisfies(path, Self::metaregion_sound_pred(r0)),

forall |i: int| i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],

r0.slot_owners.dom() == r1.slot_owners.dom(),

forall |k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),

forall |k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],

subtree
    .subtree_satisfies(
        path,
        |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| (
            e.meta_slot_paddr() is Some
                ==> frame_to_index(e.meta_slot_paddr()->0) != changed_idx
        ),
    ),

ensures

subtree.subtree_satisfies(path, Self::metaregion_sound_pred(r1)),

pub open spec fn path_tracked_pred( regions: MetaRegionOwners, ) -> FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>

{
    |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
        entry.is_node() && entry.meta_slot_paddr() is Some
            ==> {
                &&& regions
                    .slot_owners
                    .contains_key(frame_to_index(entry.meta_slot_paddr()->0))
                &&& regions.slot_owner(entry.meta_slot_paddr()->0).paths_in_pt
                    == set![entry.path]

            }
    }
}

Predicate: all entries in the tree have their paths correctly tracked in regions. Strengthened form: paths_in_pt == set![entry.path] (not just non-empty).

pub open spec fn path_correct_pred() -> FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>

{ |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| { entry.path == path } }

pub proof fn lemma_view_rec_page_size_bound( self, path: TreePath<NR_ENTRIES>, m: Mapping, )

requires

self.0.inv(),

path.len() <= INC_LEVELS - 1,

self.view_rec(path).contains(m),

ensures

m.page_size <= page_size::<PagingConsts>((INC_LEVELS - path.len()) as PagingLevel),

All mappings in a subtree’s view_rec have page_size <= page_size(INC_LEVELS - path.len()).

pub proof fn lemma_view_rec_node_page_size_bound( self, path: TreePath<NR_ENTRIES>, m: Mapping, )

requires

self.0.inv(),

self.0.value().is_node(),

path.len() < INC_LEVELS - 1,

self.view_rec(path).contains(m),

ensures

m.page_size <= page_size::<PagingConsts>(((INC_LEVELS - path.len()) - 1) as PagingLevel),

For a node subtree, all mappings have page_size <= page_size(INC_LEVELS - path.len() - 1).

pub open spec fn is_prefix_of<const N: usize>( prefix: TreePath<N>, path: TreePath<N>, ) -> bool

{
    &&& prefix.len() <= path.len()
    &&& forall |i: int| 0 <= i < prefix.len() ==> prefix[i] == path[i]

}

Spec function: path1 is a prefix of path2

pub proof fn lemma_neq_old_from_path_disjoint( subtree: OwnerSubtree<C>, path_j: TreePath<NR_ENTRIES>, old_entry: EntryOwner<C>, regions: MetaRegionOwners, )

requires

subtree.inv(),

subtree.value().path == path_j,

path_j.len() == subtree.level(),

path_j.inv(),

path_j.len() <= INC_LEVELS - 1,

subtree.subtree_satisfies(path_j, Self::metaregion_sound_pred(regions)),

subtree.subtree_satisfies(path_j, Self::path_correct_pred()),

old_entry.is_node(),

old_entry.meta_slot_paddr() is Some,

regions.slot_owner(old_entry.meta_slot_paddr()->0).paths_in_pt == set![old_entry.path],

!Self::is_prefix_of(path_j, old_entry.path),

ensures

subtree
    .subtree_satisfies(
        path_j,
        |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| e.meta_slot_paddr_neq(old_entry),
    ),

Entries in a subtree whose structural path is disjoint from old_entry.path have different physical addresses from old_entry.

pub broadcast group fn group_lemmas()

broadcast group

Trait Implementations

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

open spec fn inv(self) -> bool

{
    &&& self.0.inv()
    &&& self.pt_inv_at_depth((INC_LEVELS - self.0.level()) as nat)
    &&& self.0.value().is_node()
    &&& self.0.value().path.len() <= INC_LEVELS - 1
    &&& self.0.value().path.inv()
    &&& self.0.value().path.len() == self.0.level()
    &&& self.0.value().parent_level == (INC_LEVELS - self.0.level()) as PagingLevel
    &&& self.0.value().node().tree_level == self.0.value().path.len()

}

impl<C: PageTableConfig> View for PageTableOwner<C>

open spec fn view(&self) -> <Self as View>::V

{
    let mappings = self.view_rec(self.0.value().path);
    PageTableView { mappings }
}

type V = PageTableView