Struct Page Table Owner &nbsp; Copy item path

impl<C: PageTableConfig> PageTableOwner<C>

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

impl<C: PageTableConfig> PageTableOwner<C>

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

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

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),

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

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,

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.

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

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

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

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

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

    }
}

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

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

pub 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

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

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),

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

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

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,

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)),

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.

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,

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(),

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§

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

open spec fn inv(self) -> bool

{
    &&& self.0.inv()
    &&& 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())

}

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

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

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

type V = PageTableView

Auto Trait Implementations§

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§

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

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

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

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

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

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

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

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, U> Into for T
where U: From<T>,

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 for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

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

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom>::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>

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

type Error = >::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, >::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 for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool