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 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 vaddr = vaddr(path);
        let pt_level = INC_LEVELS - path.len();
        let page_size = page_size(pt_level as PagingLevel);
        set![
            Mapping { va_range : Range { start : vaddr, end : (vaddr + page_size) as
            Vaddr }, 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 view_rec_vaddr_range(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),
ensures
vaddr(path) <= m.va_range.start < m.va_range.end
    <= vaddr(path) + page_size((INC_LEVELS - path.len()) as PagingLevel),
Source

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

requires
self.0.inv(),
path.len() <= INC_LEVELS - 1,
path.len() == self.0.level,
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_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 relate_region_pred( regions: MetaRegionOwners, ) -> FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>

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

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

{ self.0.tree_predicate_map(self.0.value.path, Self::relate_region_pred(regions)) }
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.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())]
                    .path_if_in_pt is Some

            }
    }
}

Predicate: all nodes in the tree have their paths tracked in regions

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())]
            .path_if_in_pt is Some
        &&& regions
            .slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())]
            .path_if_in_pt
            .unwrap() == 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(pt_level) where pt_level = INC_LEVELS - path.len() (the paging level of the subtree root).

For frames: the mapping has exactly page_size(pt_level). For nodes: children have longer paths, so their mappings have strictly smaller page sizes.

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(pt_level), i.e., page_size <= page_size(pt_level - 1). This is because node mappings come from children whose paths are one level deeper.

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(),
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(),
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 inv_implies_path_correct( subtree: OwnerSubtree<C>, path: TreePath<NR_ENTRIES>, )

requires
subtree.inv(),
path.inv(),
path.len() <= INC_LEVELS - 1,
path.len() == subtree.level,
subtree.value.path == path,
ensures
subtree.tree_predicate_map(path, Self::path_correct_pred()),

If a subtree satisfies inv() and the root entry’s path field equals the structural root path, then the subtree satisfies tree_predicate_map(path, path_correct_pred()). This is proved by induction using rel_children (which stores child.path == parent.path.push_tail(i)) from Node::inv_children().

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::relate_region_pred(regions)),
subtree.tree_predicate_map(path_j, Self::path_tracked_pred(regions)),
old_entry.meta_slot_paddr() is Some,
old_entry.relate_region(regions),
regions
    .slot_owners[frame_to_index(old_entry.meta_slot_paddr().unwrap())]
    .path_if_in_pt is Some,
!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),
    ),

For entries in a subtree rooted at path_j whose path_j is not a prefix of old_entry.path, no entry in the subtree shares a physical address with old_entry.

Proof sketch: by inv_implies_path_correct, every entry e at structural position p has e.path == p. Since !is_prefix_of(path_j, old_entry.path), no structural position in the subtree equals old_entry.path. Combined with relate_region + path_tracked_pred uniqueness (via same_paddr_implies_same_path), same paddr would force same path — contradiction.

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(),
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.0.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)].path_if_in_pt == Some(entry.path),
m.va_range.start == vaddr(entry.path),
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.0.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.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.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> 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>