Skip to main content

PageTableOwner

ostd::specs::mm::page_table

Struct PageTableOwner 

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

§Verification Design

PageTableOwner is a wrapper around OwnerSubtree, which is a [vstd_extra::ghost_tree::Node] 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§

Source§

impl<C: PageTableConfig> PageTableOwner<C>

Source

pub uninterp spec fn new_cursor_owner_spec<'rcu>(self) -> (Self, CursorOwner<'rcu, C>)

Source§

impl<C: PageTableConfig> PageTableOwner<C>

Source

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

{
    &&& parent.children[i] is Some
    &&& parent.children[i]->0.value.path.len() == parent.value.node().tree_level + 1
    &&& (parent.children[i]->0
        .value
        .match_pte(
            parent.value.node().children_perm.value()[i],
            parent.value.node().level,
        )
        || (parent.value.node().level == NR_LEVELS && C::LEADING_BITS_spec() == 0
            && parent.children[i]->0
                .value
                .borrowed_match_pte(
                    parent.value.node().children_perm.value()[i],
                    parent.value.node().level,
                )))
    &&& parent.children[i]->0.value.path == parent.value.path.push_tail(i as usize)
    &&& parent.children[i]->0.value.parent_level == parent.value.node().level

}

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

Source

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.children[i]->0)
                        .pt_inv_at_depth((depth - 1) as nat)
        }
    } else {
        forall |i: int| 0 <= i < NR_ENTRIES ==> self.0.children[i] is None
    }
}

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.

Source

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.

Source

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.children[i]->0).pt_inv(),
Source

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.children[i] is None,
Source

pub proof fn 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.children[j] is None,
ensures
self.pt_inv_at_depth(depth),

pt_inv_at_depth(depth) for a non-node subtree whose grandchildren are all None. Used by allocated_empty_node_pt_inv for the absent children of a freshly-allocated PT node.

Source

pub proof fn allocated_empty_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
        ==> {
            let c = #[trigger] owner.children[i];
            &&& c is Some
            &&& c->0.value.is_absent()
            &&& c->0.value.path.len() == owner.value.node().tree_level + 1
            &&& c->0
                .value
                .match_pte(
                    owner.value.node().children_perm.value()[i],
                    owner.value.node().level,
                )
            &&& c->0.value.path == owner.value.path.push_tail(i as usize)
            &&& c->0.value.parent_level == owner.value.node().level

        }
},
allocated_empty_node_grandchildren_none(owner),
ensures
PageTableOwner(owner).pt_inv(),

pt_inv for a freshly-allocated PT node after alloc_if_none’s rebase.

Discharges the long-standing assume that blocked closing continuation_inv_holds_after_child_restore: combines the per-edge facts threaded through alloc_if_none’s ensures (paths rebased, match_pte, parent_level) with allocated_empty_node_grandchildren_none to drive pt_inv_at_depth to its non-node base case at every absent child.

Source

pub open spec fn top_level_indices_absent(self) -> bool

{
    let range = C::TOP_LEVEL_INDEX_RANGE_spec();
    self.0.value.is_node()
        ==> forall |i: int| {
            0 <= i < NR_ENTRIES && !(range.start <= i < range.end)
                ==> self.0.children[i] is Some && self.0.children[i]->0.value.is_absent()
        }
}

For a top-level (root) page table, entries at indices outside of C::TOP_LEVEL_INDEX_RANGE_spec() are absent. This ensures that UserPtConfig and KernelPtConfig page tables manage disjoint portions of the virtual address space.

Source

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 as usize))
            } else {
                Set::empty()
            }
        })
}
Source

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(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![]
    }
}
Source

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.children[i] is Some,
#[trigger]
PageTableOwner(self.0.children[i]->0).view_rec(path.push_tail(i as usize)).contains(m),
ensures
self.view_rec(path).contains(m),
Source

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 as usize))
                    .contains(m)
        }
},
Source

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 as usize))
        .contains(m),
Source

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

requires
path.inv(),
path.len() < INC_LEVELS - 1,
i < NR_ENTRIES,
ensures
vaddr(path.push_tail(i))
    == vaddr(path) + i * page_size((INC_LEVELS - path.len() - 1) as PagingLevel),
vaddr(path) + (i + 1) * page_size((INC_LEVELS - path.len() - 1) as PagingLevel)
    <= usize::MAX,

Closed-form for vaddr(path.push_tail(i)) by case-split on path.len() ∈ {0,1,2,3}.

Source

pub proof fn 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((INC_LEVELS - path.len()) as PagingLevel),
Source

pub proof fn 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.index(0) < t,
self.view_rec(path).contains(m),
ensures
(path.index(0)) * 0x80_0000_0000int + C::LEADING_BITS_spec() * 0x1_0000_0000_0000int
    <= m.va_range.start,
m.va_range.start < m.va_range.end,
m.va_range.end <= t * 0x80_0000_0000int + C::LEADING_BITS_spec() * 0x1_0000_0000_0000int,

Any mapping in a subtree’s view_rec has its VA range within the 2^39-sized cell of the subtree’s top-level index path[0], shifted by the config’s LEADING_BITS high-half base. With path[0] < t, the range end is <= t * 2^39 + LEADING_BITS * 2^48 — the per-config VA bound that discharges the user/kernel isolation theorems.

Source

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

requires
PageTableOwner(subtree).pt_inv(),
subtree.value.path == path,
ensures
subtree.tree_predicate_map(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. PageTableOwner::inv() already bundles this (see the Inv impl below) but only for node-rooted trees; callers that need it for an arbitrary pt_inv subtree (including the leaf/frame-rooted child subtrees of a cursor continuation) need a standalone form not gated on value.is_node().

Source

pub proof fn 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.tree_predicate_map(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
    .tree_predicate_map(
        path,
        |e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>| {
            e.is_frame() ==> e.path != removed_path
        },
    ),

Forward dual of Self::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.

Source

pub proof fn 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,
Source

pub proof fn 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}.

Structural induction using the invariant that parent_level of each subtree equals INC_LEVELS - tree_level, chained through rel_children. At a leaf frame, parent_level < NR_LEVELS (from the tightened inv_base) ensures the page size is one of the allowed values.

Source

pub proof fn 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().

Structural induction on the subtree. At a leaf frame, the PA-side clauses follow from FrameEntryOwner::inv_base, the VA-size clause by construction, the page-size clause from the tightened parent_level < NR_LEVELS constraint plus the arithmetic identity page_size(k) ∈ {4K, 2M, 1G} for k ∈ {1, 2, 3}, and VA alignment

  • no-overflow via lemma_vaddr_path_alignment_and_bound.
Source

pub proof fn 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.

Source

pub proof fn 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.)

Source

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

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

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

pub proof fn 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: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
forall |k: usize| 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.

Source

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

requires
subtree.inv(),
subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r0)),
r0.slot_owners == r1.slot_owners,
forall |k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
forall |k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
ensures
subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r1)),

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

Source

pub proof fn metaregion_sound_preserved_one_slot_changed( self, r0: MetaRegionOwners, r1: MetaRegionOwners, changed_idx: usize, )

requires
self.inv(),
self.metaregion_sound(r0),
forall |i: usize| i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
r0.slot_owners.dom() == r1.slot_owners.dom(),
forall |k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
forall |k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
self
    .0
    .tree_predicate_map(
        self.0.value.path,
        |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| (
            e.meta_slot_paddr() is Some
                ==> frame_to_index(e.meta_slot_paddr()->0) != changed_idx
        ),
    ),
self
    .0
    .tree_predicate_map(
        self.0.value.path,
        |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| {
            e.is_frame() && e.parent_level > 1
                ==> {
                    let pa = e.frame().mapped_pa;
                    let nr_pages = page_size(e.parent_level) / PAGE_SIZE;
                    forall |j: usize| {
                        0 < j < nr_pages
                            ==> {
                                let sub_idx = #[trigger]
                                frame_to_index((pa + j * PAGE_SIZE) as usize);
                                sub_idx != changed_idx
                                    || (r1.slots.contains_key(sub_idx)
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                            != REF_COUNT_UNUSED
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                            <= REF_COUNT_MAX)
                            }
                    }
                }
        },
    ),
ensures
self.metaregion_sound(r1),

PageTableOwner::metaregion_sound is preserved across a single slot_owner change at index changed_idx, provided no entry in the tree references changed_idx (neither as its primary slot nor as a huge-frame sub-page slot). This is the right shape for borrow-style operations that bump raw_count at one slot.

Source

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

requires
subtree.inv(),
subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r0)),
forall |i: usize| i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
r0.slot_owners.dom() == r1.slot_owners.dom(),
forall |k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
forall |k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
subtree
    .tree_predicate_map(
        path,
        |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| (
            e.meta_slot_paddr() is Some
                ==> frame_to_index(e.meta_slot_paddr()->0) != changed_idx
        ),
    ),
subtree
    .tree_predicate_map(
        path,
        |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| {
            e.is_frame() && e.parent_level > 1
                ==> {
                    let pa = e.frame().mapped_pa;
                    let nr_pages = page_size(e.parent_level) / PAGE_SIZE;
                    forall |j: usize| {
                        0 < j < nr_pages
                            ==> {
                                let sub_idx = #[trigger]
                                frame_to_index((pa + j * PAGE_SIZE) as usize);
                                sub_idx != changed_idx
                                    || (r1.slots.contains_key(sub_idx)
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                            != REF_COUNT_UNUSED
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                            <= REF_COUNT_MAX)
                            }
                    }
                }
        },
    ),
ensures
subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r1)),
Source

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_owners[frame_to_index(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).

Source

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

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

    }
}
Source

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

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

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

{ |entry: EntryOwner<C>, _path: TreePath<NR_ENTRIES>| true }
Source

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

requires
subtree.inv(),
ensures
subtree.tree_predicate_map(path, Self::not_in_scope_pred()),

tree_predicate_map for the trivial not_in_scope_pred.

Source

pub proof fn 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((INC_LEVELS - path.len()) as PagingLevel),

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

Source

pub proof fn 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(((INC_LEVELS - path.len()) - 1) as PagingLevel),

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

Source

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.index(i) == path.index(i)

}

Spec function: path1 is a prefix of path2

Source

pub proof fn prefix_transitive<const N: usize>( p1: TreePath<N>, p2: TreePath<N>, p3: TreePath<N>, )

requires
Self::is_prefix_of(p1, p2),
Self::is_prefix_of(p2, p3),
ensures
Self::is_prefix_of(p1, p3),

Transitivity of is_prefix_of

Source

pub proof fn prefix_push_different_indices( prefix: TreePath<NR_ENTRIES>, path: TreePath<NR_ENTRIES>, i: usize, j: usize, )

requires
prefix.inv(),
path.inv(),
i != j,
Self::is_prefix_of(prefix.push_tail(i), path),
ensures
!Self::is_prefix_of(prefix.push_tail(j), path),
Source

pub proof fn prefix_push_tail_implies_prefix<const N: usize>( prefix: TreePath<N>, path: TreePath<N>, i: usize, )

requires
prefix.inv(),
path.inv(),
0 <= i < N,
Self::is_prefix_of(prefix.push_tail(i), path),
ensures
Self::is_prefix_of(prefix, path),
Source

pub open spec fn is_at_pred( entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>, ) -> FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>

{
    |entry0: EntryOwner<C>, path0: TreePath<NR_ENTRIES>| {
        path0 == path ==> entry0 == entry
    }
}
Source

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

{
    |entry: EntryOwner<C>, path0: TreePath<NR_ENTRIES>| {
        Self::is_prefix_of(path0, path) ==> (!entry.is_node() ==> path == path0)
    }
}
Source

pub proof fn is_at_pred_eq( path: TreePath<NR_ENTRIES>, entry1: EntryOwner<C>, entry2: EntryOwner<C>, )

requires
entry1.inv(),
OwnerSubtree::implies(Self::is_at_pred(entry1, path), Self::is_at_pred(entry2, path)),
ensures
entry1 == entry2,
Source

pub proof fn is_at_holds_when_on_wrong_path( subtree: OwnerSubtree<C>, root_path: TreePath<NR_ENTRIES>, dest_path: TreePath<NR_ENTRIES>, entry: EntryOwner<C>, )

requires
subtree.inv(),
PageTableOwner(subtree).pt_inv(),
dest_path.inv(),
!Self::is_prefix_of(root_path, dest_path),
root_path.len() <= INC_LEVELS - 1,
root_path.len() == subtree.level,
ensures
subtree.tree_predicate_map(root_path, Self::is_at_pred(entry, dest_path)),
Source

pub proof fn path_in_tree_holds_when_on_wrong_path( subtree: OwnerSubtree<C>, root_path: TreePath<NR_ENTRIES>, dest_path: TreePath<NR_ENTRIES>, )

requires
subtree.inv(),
PageTableOwner(subtree).pt_inv(),
dest_path.inv(),
!Self::is_prefix_of(root_path, dest_path),
root_path.len() <= INC_LEVELS - 1,
root_path.len() == subtree.level,
ensures
subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),

Counterintuitive: the predicate is vacuously true when the path is not a prefix of the target path, because it is actually a liveness property: if we keep following the path, we will eventually reach it. This covers when we are not following it.

Source

pub proof fn 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.tree_predicate_map(path_j, Self::metaregion_sound_pred(regions)),
subtree.tree_predicate_map(path_j, Self::path_correct_pred()),
old_entry.is_node(),
old_entry.meta_slot_paddr() is Some,
regions.slot_owners[frame_to_index(old_entry.meta_slot_paddr()->0)].paths_in_pt
    == set![old_entry.path],
!Self::is_prefix_of(path_j, old_entry.path),
ensures
subtree
    .tree_predicate_map(
        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.

Source

pub proof fn is_at_eq_rec( subtree: OwnerSubtree<C>, root_path: TreePath<NR_ENTRIES>, dest_path: TreePath<NR_ENTRIES>, entry1: EntryOwner<C>, entry2: EntryOwner<C>, )

requires
subtree.inv(),
PageTableOwner(subtree).pt_inv(),
dest_path.inv(),
root_path.inv(),
Self::is_prefix_of(root_path, dest_path),
root_path.len() <= INC_LEVELS - 1,
root_path.len() == subtree.level,
subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),
subtree.tree_predicate_map(root_path, Self::is_at_pred(entry1, dest_path)),
subtree.tree_predicate_map(root_path, Self::is_at_pred(entry2, dest_path)),
ensures
entry1 == entry2,
Source

pub proof fn view_rec_inversion( self, path: TreePath<NR_ENTRIES>, regions: MetaRegionOwners, m: Mapping, ) -> entry : EntryOwner<C>

requires
self.pt_inv(),
path.len() == self.0.level,
self.view_rec(path).contains(m),
self.0.tree_predicate_map(path, Self::path_correct_pred()),
self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
ensures
Self::is_prefix_of(path, entry.path),
regions.slot_owners[frame_to_index(m.pa_range.start)].paths_in_pt == set![entry.path],
m.va_range.start == vaddr_of::<C>(entry.path),
m.page_size == page_size((INC_LEVELS - entry.path.len()) as PagingLevel),
entry.is_frame(),
m.property == entry.frame().prop,
self.0.tree_predicate_map(path, Self::is_at_pred(entry, entry.path)),
self.0.tree_predicate_map(path, Self::path_in_tree_pred(entry.path)),
entry.inv(),
Source

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

requires
self.pt_inv(),
path.len() <= INC_LEVELS - 1,
path.len() == self.0.level,
self.view_rec(path).contains(m1),
self.view_rec(path).contains(m2),
m1.pa_range.start == m2.pa_range.start,
m1.inv(),
m2.inv(),
self.0.tree_predicate_map(path, Self::path_tracked_pred(regions)),
self.0.tree_predicate_map(path, Self::path_correct_pred()),
self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
ensures
m1 == m2,
Source

pub broadcast group fn group_lemmas()

broadcast group

Trait Implementations§

Source§

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

Source§

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()
    &&& self.0.tree_predicate_map(self.0.value.path, Self::path_correct_pred())

}
Source§

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

Source§

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

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

type V = PageTableView

Auto Trait Implementations§

§

impl<C> Freeze for PageTableOwner<C>

§

impl<C> RefUnwindSafe for PageTableOwner<C>
where <C as PageTableConfig>::E: RefUnwindSafe,

§

impl<C> Send for PageTableOwner<C>

§

impl<C> Sync for PageTableOwner<C>

§

impl<C> Unpin for PageTableOwner<C>
where <C as PageTableConfig>::E: Unpin,

§

impl<C> UnsafeUnpin for PageTableOwner<C>

§

impl<C> UnwindSafe for PageTableOwner<C>
where <C as PageTableConfig>::E: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A