Skip to main content

PageTableOwner

ostd::specs::mm::page_table

Struct PageTableOwner 

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

Tuple Fields§

§0: OwnerSubtree<C>

Implementations§

Source§

impl<C: PageTableConfig> PageTableOwner<C>

Source

pub uninterp 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].unwrap().value.path.len()
        == parent.value.node.unwrap().tree_level + 1
    &&& parent
        .children[i]
        .unwrap()
        .value
        .match_pte(
            parent.value.node.unwrap().children_perm.value()[i],
            parent.value.node.unwrap().level,
        )
    &&& parent.children[i].unwrap().value.path == parent.value.path.push_tail(i as usize)
    &&& parent.children[i].unwrap().value.parent_level
        == parent.value.node.unwrap().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].unwrap())
                        .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].unwrap()).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 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].unwrap().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(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 as int + page_size
            as int }, pa_range : Range { start : self.0.value.frame.unwrap().mapped_pa,
            end : (self.0.value.frame.unwrap().mapped_pa + page_size) as Paddr, },
            page_size : page_size, property : self.0.value.frame.unwrap().prop, }
        ]
    } else if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
        Set::new(|m: Mapping| {
            exists |i: int| {
                0 <= i < self.0.children.len() && self.0.children[i] is Some
                    && PageTableOwner(self.0.children[i].unwrap())
                        .view_rec(path.push_tail(i as usize))
                        .contains(m)
            }
        })
    } else {
        set![]
    }
}
Source

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

requires
self.0.inv(),
path.len() < INC_LEVELS - 1,
path.len() == self.0.level,
self.view_rec(path).contains(m),
self.0.value.is_node(),
ensures
exists |i: int| {
    0 <= i < self.0.children.len() && self.0.children[i] is Some
        && PageTableOwner(self.0.children[i].unwrap())
            .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,
path.len() == self.0.level,
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].unwrap())
        .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)) as int
    == vaddr(path) as int
        + (i as int) * (page_size((INC_LEVELS - path.len() - 1) as PagingLevel) as int),
vaddr(path) as int
    + (i as int + 1) * (page_size((INC_LEVELS - path.len() - 1) as PagingLevel) as int)
    <= usize::MAX as int,

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) as int <= m.va_range.start,
m.va_range.start < m.va_range.end,
m.va_range.end
    <= vaddr_of::<C>(path) as int
        + page_size((INC_LEVELS - path.len()) as PagingLevel) as int,
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_finite(self, path: TreePath<NR_ENTRIES>)

requires
self.0.inv(),
path.len() <= INC_LEVELS - 1,
path.len() == self.0.level,
ensures
self.view_rec(path).finite(),

view_rec is finite: bounded by NR_ENTRIES branching and INC_LEVELS depth. Proven by induction on INC_LEVELS - path.len(), collapsing the Set::new existential into a flatten of a finite domain-map.

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.0.inv(),
self.0.value.is_node(),
self.0.value.node.unwrap().meta_own.nr_children.value() == 0,
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.

Axiom: the link between nr_children and the count of present PTEs is maintained by Entry::replace / Entry::new but not yet formalised as a NodeOwner invariant.

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().unwrap()) != 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.unwrap().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()
                                            != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                            > 0)
                            }
                    }
                }
        },
    ),
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().unwrap()) != 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.unwrap().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()
                                            != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
                                        && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                            > 0)
                            }
                    }
                }
        },
    ),
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().unwrap()))
                &&& regions
                    .slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())]
                    .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().unwrap()))
        &&& regions
            .slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())]
            .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>| !entry.in_scope }
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()),

Every entry in an OwnerSubtree has !in_scope. Follows from EntryOwner::inv() including !in_scope, propagated through the tree.

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 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)),
old_entry.is_node(),
old_entry.meta_slot_paddr() is Some,
regions.slot_owners[frame_to_index(old_entry.meta_slot_paddr().unwrap())].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) as int,
m.page_size == page_size((INC_LEVELS - entry.path.len()) as PagingLevel),
entry.is_frame(),
m.property == entry.frame.unwrap().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,

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.unwrap().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>

§

impl<C> Send for PageTableOwner<C>

§

impl<C> Sync for PageTableOwner<C>

§

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

§

impl<C> UnsafeUnpin for PageTableOwner<C>

§

impl<C> UnwindSafe for PageTableOwner<C>
where <C as PageTableConfig>::E: UnwindSafe, C: 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>