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

Source§

impl<C: PageTableConfig> PageTableOwner<C>

Source

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 && C::LEADING_BITS_spec() == 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.

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

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.child(i)).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.has_child(i),
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.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. 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
        ==> {
            &&& #[trigger] owner.has_child(i)
            &&& owner.child(i).value().is_absent()
            &&& 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(),

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

Discharges the long-standing assume that blocked closing lemma_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 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()
            }
        })
}
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::<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![]
    }
}
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.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),
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))
                    .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)).contains(m),
Source

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,

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::<PagingConsts>((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[0] < t,
self.view_rec(path).contains(m),
ensures
(path[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.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. 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.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::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 EntryOwner::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.subtree_satisfies(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: 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.

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

Source

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

requires
self.inv(),
self.metaregion_sound(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],
self
    .0
    .subtree_satisfies(
        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
    .subtree_satisfies(
        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::<PagingConsts>(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.ref_count(sub_idx) != REF_COUNT_UNUSED
                                        && r1.ref_count(sub_idx) > 0
                                        && r1.ref_count(sub_idx) <= 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: 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
        ),
    ),
subtree
    .subtree_satisfies(
        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::<PagingConsts>(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.ref_count(sub_idx) != REF_COUNT_UNUSED
                                        && r1.ref_count(sub_idx) > 0
                                        && r1.ref_count(sub_idx) <= REF_COUNT_MAX)
                            }
                    }
                }
        },
    ),
ensures
subtree.subtree_satisfies(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_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).

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.subtree_satisfies(path, Self::not_in_scope_pred()),

subtree_satisfies 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::<PagingConsts>((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::<PagingConsts>(((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[i] == path[i]

}

Spec function: path1 is a prefix of path2

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

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.subtree_satisfies(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> !RefUnwindSafe for PageTableOwner<C>

§

impl<C> Freeze for PageTableOwner<C>
where <C as PageTableConfig>::Perm: Freeze,

§

impl<C> Send for PageTableOwner<C>
where <C as PageTableConfig>::Perm: Send,

§

impl<C> Sync for PageTableOwner<C>
where <C as PageTableConfig>::Perm: Sync,

§

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

§

impl<C> UnsafeUnpin for PageTableOwner<C>
where <C as PageTableConfig>::Perm: UnsafeUnpin,

§

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

impl<T> Conv for T

§

fn conv<T>(self) -> T
where Self: Into<T>,

Converts self into T using Into<T>. Read more
§

impl<T> FmtForward for T

§

fn fmt_binary(self) -> FmtBinary<Self>
where Self: Binary,

Causes self to use its Binary implementation when Debug-formatted.
§

fn fmt_display(self) -> FmtDisplay<Self>
where Self: Display,

Causes self to use its Display implementation when Debug-formatted.
§

fn fmt_lower_exp(self) -> FmtLowerExp<Self>
where Self: LowerExp,

Causes self to use its LowerExp implementation when Debug-formatted.
§

fn fmt_lower_hex(self) -> FmtLowerHex<Self>
where Self: LowerHex,

Causes self to use its LowerHex implementation when Debug-formatted.
§

fn fmt_octal(self) -> FmtOctal<Self>
where Self: Octal,

Causes self to use its Octal implementation when Debug-formatted.
§

fn fmt_pointer(self) -> FmtPointer<Self>
where Self: Pointer,

Causes self to use its Pointer implementation when Debug-formatted.
§

fn fmt_upper_exp(self) -> FmtUpperExp<Self>
where Self: UpperExp,

Causes self to use its UpperExp implementation when Debug-formatted.
§

fn fmt_upper_hex(self) -> FmtUpperHex<Self>
where Self: UpperHex,

Causes self to use its UpperHex implementation when Debug-formatted.
§

fn fmt_list(self) -> FmtList<Self>
where &'a Self: for<'a> IntoIterator,

Formats each item in a sequence. 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

§

impl<T> FromSpecImpl<T> for T

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> T

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

§

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

§

fn pipe<R>(self, func: impl FnOnce(Self) -> R) -> R
where Self: Sized,

Pipes by value. This is generally the method you want to use. Read more
§

fn pipe_ref<'a, R>(&'a self, func: impl FnOnce(&'a Self) -> R) -> R
where R: 'a,

Borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_ref_mut<'a, R>(&'a mut self, func: impl FnOnce(&'a mut Self) -> R) -> R
where R: 'a,

Mutably borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_borrow<'a, B, R>(&'a self, func: impl FnOnce(&'a B) -> R) -> R
where Self: Borrow<B>, B: 'a + ?Sized, R: 'a,

Borrows self, then passes self.borrow() into the pipe function. Read more
§

fn pipe_borrow_mut<'a, B, R>( &'a mut self, func: impl FnOnce(&'a mut B) -> R, ) -> R
where Self: BorrowMut<B>, B: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.borrow_mut() into the pipe function. Read more
§

fn pipe_as_ref<'a, U, R>(&'a self, func: impl FnOnce(&'a U) -> R) -> R
where Self: AsRef<U>, U: 'a + ?Sized, R: 'a,

Borrows self, then passes self.as_ref() into the pipe function.
§

fn pipe_as_mut<'a, U, R>(&'a mut self, func: impl FnOnce(&'a mut U) -> R) -> R
where Self: AsMut<U>, U: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.as_mut() into the pipe function.
§

fn pipe_deref<'a, T, R>(&'a self, func: impl FnOnce(&'a T) -> R) -> R
where Self: Deref<Target = T>, T: 'a + ?Sized, R: 'a,

Borrows self, then passes self.deref() into the pipe function.
§

fn pipe_deref_mut<'a, T, R>( &'a mut self, func: impl FnOnce(&'a mut T) -> R, ) -> R
where Self: DerefMut<Target = T> + Deref, T: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.deref_mut() into the pipe function.
§

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

§

impl<T> Tap for T

§

fn tap(self, func: impl FnOnce(&Self)) -> Self

Immutable access to a value. Read more
§

fn tap_mut(self, func: impl FnOnce(&mut Self)) -> Self

Mutable access to a value. Read more
§

fn tap_borrow<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Immutable access to the Borrow<B> of a value. Read more
§

fn tap_borrow_mut<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Mutable access to the BorrowMut<B> of a value. Read more
§

fn tap_ref<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Immutable access to the AsRef<R> view of a value. Read more
§

fn tap_ref_mut<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Mutable access to the AsMut<R> view of a value. Read more
§

fn tap_deref<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Immutable access to the Deref::Target of a value. Read more
§

fn tap_deref_mut<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Mutable access to the Deref::Target of a value. Read more
§

fn tap_dbg(self, func: impl FnOnce(&Self)) -> Self

Calls .tap() only in debug builds, and is erased in release builds.
§

fn tap_mut_dbg(self, func: impl FnOnce(&mut Self)) -> Self

Calls .tap_mut() only in debug builds, and is erased in release builds.
§

fn tap_borrow_dbg<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Calls .tap_borrow() only in debug builds, and is erased in release builds.
§

fn tap_borrow_mut_dbg<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Calls .tap_borrow_mut() only in debug builds, and is erased in release builds.
§

fn tap_ref_dbg<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Calls .tap_ref() only in debug builds, and is erased in release builds.
§

fn tap_ref_mut_dbg<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Calls .tap_ref_mut() only in debug builds, and is erased in release builds.
§

fn tap_deref_dbg<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Calls .tap_deref() only in debug builds, and is erased in release builds.
§

fn tap_deref_mut_dbg<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Calls .tap_deref_mut() only in debug builds, and is erased in release builds.
§

impl<T> TryConv for T

§

fn try_conv<T>(self) -> Result<T, Self::Error>
where Self: TryInto<T>,

Attempts to convert self into T using TryInto<T>. Read more
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>