Skip to main content

CursorContinuation

ostd::specs::mm::page_table::cursor::owners

Struct CursorContinuation 

Source 
pub struct CursorContinuation<'rcu, C: PageTableConfig> {
    pub entry_own: EntryOwner<C>,
    pub idx: usize,
    pub tree_level: nat,
    pub children: Seq<Option<OwnerSubtree<C>>>,
    pub path: TreePath<NR_ENTRIES>,
    pub guard: PageTableGuard<'rcu, C>,
}

Fields§

§entry_own: EntryOwner<C>§idx: usize§tree_level: nat§children: Seq<Option<OwnerSubtree<C>>>§path: TreePath<NR_ENTRIES>§guard: PageTableGuard<'rcu, C>

Implementations§

Source§

impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C>

Source

pub proof fn as_page_table_owner_preserves_view_mappings(self)

requires
self.inv(),
self.all_some(),
ensures
self.as_page_table_owner().view_rec(self.path()) == self.view_mappings(),
self.as_subtree().inv(),
PageTableOwner(self.as_subtree()).pt_inv(),
Source

pub proof fn view_mappings_take_child(self)

requires
self.inv(),
self.all_some(),
ensures
self.take_child_spec().1.view_mappings()
    == self.view_mappings() - self.view_mappings_take_child_spec(),
Source

pub proof fn view_mappings_put_child(self, child: OwnerSubtree<C>)

requires
self.inv(),
child.inv(),
self.all_but_index_some(),
ensures
self.put_child_spec(child).view_mappings()
    == self.view_mappings()
        + PageTableOwner(child).view_rec(self.path().push_tail(self.idx as usize)),
Source§

impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C>

Source

pub open spec fn path(self) -> TreePath<NR_ENTRIES>

{ self.entry_own.path }
Source

pub open spec fn child(self) -> OwnerSubtree<C>

{ self.children[self.idx as int].unwrap() }
Source

pub open spec fn take_child_spec(self) -> (OwnerSubtree<C>, Self)

{
    let child = self.children[self.idx as int].unwrap();
    let cont = Self {
        children: self.children.remove(self.idx as int).insert(self.idx as int, None),
        ..self
    };
    (child, cont)
}
Source

pub proof fn take_child(tracked &mut self) -> res : OwnerSubtree<C>

requires
old(self).inv(),
old(self).idx < old(self).children.len(),
old(self).children[old(self).idx as int] is Some,
ensures
res == old(self).take_child_spec().0,
*final(self) == old(self).take_child_spec().1,
res.inv(),
Source

pub open spec fn put_child_spec(self, child: OwnerSubtree<C>) -> Self

{
    Self {
        children: self
            .children
            .remove(self.idx as int)
            .insert(self.idx as int, Some(child)),
        ..self
    }
}
Source

pub proof fn put_child(tracked &mut self, tracked child: OwnerSubtree<C>)

requires
old(self).idx < old(self).children.len(),
old(self).children[old(self).idx as int] is None,
ensures
*final(self) == old(self).put_child_spec(child),
Source

pub proof fn take_put_child(self)

requires
self.idx < self.children.len(),
self.children[self.idx as int] is Some,
ensures
self.take_child_spec().1.put_child_spec(self.take_child_spec().0) == self,
Source

pub open spec fn make_cont_spec( self, idx: usize, guard: PageTableGuard<'rcu, C>, ) -> (Self, Self)

{
    let child = Self {
        entry_own: self.children[self.idx as int].unwrap().value,
        tree_level: (self.tree_level + 1) as nat,
        idx: idx,
        children: self.children[self.idx as int].unwrap().children,
        path: self.path.push_tail(self.idx as usize),
        guard: guard,
    };
    let cont = Self {
        children: self.children.update(self.idx as int, None),
        ..self
    };
    (child, cont)
}
Source

pub proof fn make_cont(tracked &mut self, idx: usize, guard: PageTableGuard<'rcu, C>) -> res : Self

requires
old(self).all_some(),
old(self).idx < NR_ENTRIES,
idx < NR_ENTRIES,
ensures
res == old(self).make_cont_spec(idx, guard).0,
*final(self) == old(self).make_cont_spec(idx, guard).1,
Source

pub open spec fn restore_spec(self, child: Self) -> (Self, PageTableGuard<'rcu, C>)

{
    let child_node = OwnerSubtree {
        value: child.entry_own,
        level: child.tree_level,
        children: child.children,
    };
    (
        Self {
            children: self.children.update(self.idx as int, Some(child_node)),
            ..self
        },
        child.guard,
    )
}
Source

pub proof fn restore(tracked &mut self, tracked child: Self) -> tracked guard : PageTableGuard<'rcu, C>

ensures
*final(self) == old(self).restore_spec(child).0,
guard == old(self).restore_spec(child).1,
Source

pub open spec fn new_spec( owner_subtree: OwnerSubtree<C>, idx: usize, guard: PageTableGuard<'rcu, C>, ) -> Self

{
    Self {
        entry_own: owner_subtree.value,
        idx: idx,
        tree_level: owner_subtree.level,
        children: owner_subtree.children,
        path: TreePath::new(Seq::empty()),
        guard: guard,
    }
}
Source

pub proof fn new(tracked owner_subtree: OwnerSubtree<C>, idx: usize, guard: PageTableGuard<'rcu, C>, ) -> tracked res : Self

ensures
res == Self::new_spec(owner_subtree, idx, guard),
Source

pub open spec fn map_children( self, f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, ) -> bool

{
    forall |i: int| {
        0 <= i < self.children.len()
            ==> (self.children[i] is Some
                ==> self
                    .children[i]
                    .unwrap()
                    .tree_predicate_map(self.path().push_tail(i as usize), f))
    }
}
Source

pub open spec fn level(self) -> PagingLevel

{ self.entry_own.node.unwrap().level }
Source

pub open spec fn inv_children(self) -> bool

{
    self.children
        .all(|child: Option<OwnerSubtree<C>>| child is Some ==> child.unwrap().inv())
}
Source

pub proof fn inv_children_unroll(self, i: int)

requires
self.inv_children(),
0 <= i < self.children.len(),
self.children[i] is Some,
ensures
self.children[i].unwrap().inv(),
Source

pub proof fn inv_children_unroll_all(self)

requires
self.inv_children(),
ensures
forall |i: int| {
    0 <= i < self.children.len()
        ==> (self.children[i] is Some ==> self.children[i].unwrap().inv())
},
Source

pub open spec fn inv_children_rel_pred( self, ) -> FnSpec<(int, Option<OwnerSubtree<C>>), bool>

{
    |i: int, child: Option<OwnerSubtree<C>>| {
        child is Some
            ==> {
                &&& child.unwrap().value.parent_level == self.level()
                &&& child.unwrap().level == self.tree_level + 1
                &&& !child.unwrap().value.in_scope
                &&& child.unwrap().value.path.len()
                    == self.entry_own.node.unwrap().tree_level + 1
                &&& child
                    .unwrap()
                    .value
                    .match_pte(
                        self.entry_own.node.unwrap().children_perm.value()[i],
                        self.entry_own.node.unwrap().level,
                    )
                &&& child.unwrap().value.path == self.path().push_tail(i as usize)

            }
    }
}
Source

pub open spec fn inv_children_rel(self) -> bool

{ forall_seq(self.children, self.inv_children_rel_pred()) }
Source

pub open spec fn pt_inv_children_pred() -> FnSpec<(int, Option<OwnerSubtree<C>>), bool>

{
    |i: int, child: Option<OwnerSubtree<C>>| (
        child is Some ==> PageTableOwner(child.unwrap()).pt_inv()
    )
}
Source

pub open spec fn pt_inv_children(self) -> bool

{ forall_seq(self.children, Self::pt_inv_children_pred()) }
Source

pub proof fn pt_inv_children_unroll(self, i: int)

requires
self.pt_inv_children(),
0 <= i < self.children.len(),
self.children[i] is Some,
ensures
PageTableOwner(self.children[i].unwrap()).pt_inv(),
Source

pub proof fn inv_children_rel_unroll(self, i: int)

requires
self.inv_children_rel(),
0 <= i < self.children.len(),
self.children[i] is Some,
ensures
self.children[i].unwrap().value.parent_level == self.level(),
self.children[i].unwrap().level == self.tree_level + 1,
!self.children[i].unwrap().value.in_scope,
self.children[i].unwrap().value.path.len() == self.entry_own.node.unwrap().tree_level + 1,
self
    .children[i]
    .unwrap()
    .value
    .match_pte(
        self.entry_own.node.unwrap().children_perm.value()[i],
        self.entry_own.node.unwrap().level,
    ),
self.children[i].unwrap().value.path == self.path().push_tail(i as usize),
Source

pub open spec fn inv(self) -> bool

{
    &&& self.children.len() == NR_ENTRIES
    &&& 0 <= self.idx < NR_ENTRIES
    &&& self.inv_children()
    &&& self.inv_children_rel()
    &&& self.pt_inv_children()
    &&& self.entry_own.is_node()
    &&& self.entry_own.inv()
    &&& !self.entry_own.in_scope
    &&& self.entry_own.node.unwrap().relate_guard(self.guard)
    &&& self.tree_level == INC_LEVELS - self.level() - 1
    &&& self.tree_level < INC_LEVELS - 1
    &&& self.path().len() == self.tree_level

}
Source

pub open spec fn all_some(self) -> bool

{ forall |i: int| 0 <= i < NR_ENTRIES ==> self.children[i] is Some }
Source

pub open spec fn all_but_index_some(self) -> bool

{
    &&& forall |i: int| 0 <= i < self.idx ==> self.children[i] is Some
    &&& forall |i: int| self.idx < i < NR_ENTRIES ==> self.children[i] is Some
    &&& self.children[self.idx as int] is None

}
Source

pub open spec fn inc_index(self) -> Self

{
    Self {
        idx: (self.idx + 1) as usize,
        ..self
    }
}
Source

pub proof fn do_inc_index(tracked &mut self)

requires
old(self).idx + 1 < NR_ENTRIES,
ensures
*final(self) == old(self).inc_index(),
Source

pub open spec fn node_locked(self, guards: Guards<'rcu, C>) -> bool

{ guards.lock_held(self.guard.inner.inner@.ptr.addr()) }
Source

pub open spec fn view_mappings(self) -> Set<Mapping>

{
    Set::new(|m: Mapping| {
        exists |i: int| {
            0 <= i < self.children.len() && self.children[i] is Some
                && PageTableOwner(self.children[i].unwrap())
                    .view_rec(self.path().push_tail(i as usize))
                    .contains(m)
        }
    })
}
Source

pub open spec fn as_subtree(self) -> OwnerSubtree<C>

{
    OwnerSubtree {
        value: self.entry_own,
        level: self.tree_level,
        children: self.children,
    }
}
Source

pub open spec fn as_page_table_owner(self) -> PageTableOwner<C>

{ PageTableOwner(self.as_subtree()) }
Source

pub open spec fn view_mappings_take_child_spec(self) -> Set<Mapping>

{
    PageTableOwner(self.children[self.idx as int].unwrap())
        .view_rec(self.path().push_tail(self.idx as usize))
}
Source

pub proof fn rel_children_from_node_matching( entry: &Entry<'_, 'rcu, C>, child_value: EntryOwner<C>, parent_owner: NodeOwner<C>, guard: PageTableGuard<'rcu, C>, entry_own: EntryOwner<C>, idx: usize, )

requires
entry.node_matching(child_value, parent_owner, guard),
entry.idx == idx,
entry_own.node == Some(parent_owner),
child_value.path == entry_own.path.push_tail(idx),
child_value.path.len() == parent_owner.tree_level + 1,
ensures
child_value.path.len() == parent_owner.tree_level + 1,
child_value.match_pte(parent_owner.children_perm.value()[idx as int], parent_owner.level),
child_value.path == entry_own.path.push_tail(idx),
child_value.parent_level == parent_owner.level,

Proves rel_children for a child that was taken from the continuation, modified (by protect, alloc_if_none, or split_if_mapped_huge), and placed back at the same index.

The key inputs are:

  • node_matching from the operation’s postcondition (provides match_pte)
  • The child’s path and path length (preserved by the operation)
  • The entry’s path (unchanged through the reconstruction) Proves rel_children from node_matching. After taking a child from a continuation, modifying it (protect/alloc/split), and restoring entry_own.node = Some(parent_owner), rel_children holds for any entry_own that has node == Some(parent_owner) and the correct path.
Source

pub proof fn continuation_inv_holds_after_child_restore( self, cont_old: Self, parent_old: NodeOwner<C>, )

requires
cont_old.inv(),
cont_old.entry_own.node == Some(parent_old),
self.children.len() == cont_old.children.len(),
self.idx == cont_old.idx,
self.tree_level == cont_old.tree_level,
self.guard == cont_old.guard,
self.path == cont_old.path,
self.entry_own.frame == cont_old.entry_own.frame,
self.entry_own.locked == cont_old.entry_own.locked,
self.entry_own.absent == cont_old.entry_own.absent,
self.entry_own.in_scope == cont_old.entry_own.in_scope,
self.entry_own.path == cont_old.entry_own.path,
self.entry_own.parent_level == cont_old.entry_own.parent_level,
self.entry_own.is_node(),
self.entry_own.inv(),
self.entry_own.node.unwrap().relate_guard(self.guard),
self.entry_own.node.unwrap().level == parent_old.level,
self.entry_own.node.unwrap().tree_level == parent_old.tree_level,
forall |j: int| {
    0 <= j < NR_ENTRIES && j != self.idx as int
        ==> #[trigger] self.entry_own.node.unwrap().children_perm.value()[j]
            == parent_old.children_perm.value()[j]
},
forall |j: int| {
    0 <= j < NR_ENTRIES && j != self.idx as int
        ==> #[trigger] self.children[j] == cont_old.children[j]
},
self.children.len() == NR_ENTRIES,
0 <= self.idx < NR_ENTRIES,
self.tree_level == INC_LEVELS - self.level() - 1,
self.tree_level < INC_LEVELS - 1,
self.path().len() == self.tree_level,
self.children[self.idx as int] is Some,
self.children[self.idx as int].unwrap().inv(),
self.children[self.idx as int].unwrap().value.parent_level == self.level(),
self.children[self.idx as int].unwrap().value.path
    == self.path().push_tail(self.idx as usize),
self.children[self.idx as int].unwrap().level == self.tree_level + 1,
self.children[self.idx as int].unwrap().value.path.len()
    == self.entry_own.node.unwrap().tree_level + 1,
self
    .children[self.idx as int]
    .unwrap()
    .value
    .match_pte(
        self.entry_own.node.unwrap().children_perm.value()[self.idx as int],
        self.entry_own.node.unwrap().level,
    ),
!self.children[self.idx as int].unwrap().value.in_scope,
PageTableOwner(self.children[self.idx as int].unwrap()).pt_inv(),
ensures
self.inv(),

After restoring entry_own.node = Some(parent_owner) and putting the child back at idx, the continuation invariant holds.

Caller passes the pre-modification continuation cont_old and its parent_owner parent_old so we can recover the per-j != idx inv_children_rel/pt_inv_children facts from cont_old.inv(). Operations that take/restore (alloc_if_none, split_if_mapped_huge, protect, replace) all preserve the parent’s other PTEs and the children at j != idx.

Source

pub proof fn new_child(tracked &self, paddr: Paddr, prop: PageProperty, is_tracked: bool, tracked regions: &mut MetaRegionOwners, ) -> tracked res : OwnerSubtree<C>

requires
self.inv(),
self.level() < NR_LEVELS,
old(regions).slots.contains_key(frame_to_index(paddr)),
paddr % PAGE_SIZE == 0,
paddr < MAX_PADDR,
paddr % page_size(self.level()) == 0,
paddr + page_size(self.level()) <= MAX_PADDR,
self.path().push_tail(self.idx as usize).inv(),
ensures
final(regions).slot_owners == old(regions).slot_owners,
final(regions).slots == old(regions).slots,
res.value
    == EntryOwner::<
        C,
    >::new_frame_spec(
            paddr,
            self.path().push_tail(self.idx as usize),
            self.level(),
            prop,
            is_tracked,
        )
        .set_in_scope(false),
res.inv(),
res.level == self.tree_level + 1,
res == OwnerSubtree::new_val(res.value, res.level as nat),
Source§

impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C>

Source

pub proof fn map_children_lift( self, f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, g: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, )

requires
self.inv(),
self.map_children(f),
OwnerSubtree::implies(f, g),
ensures
self.map_children(g),

Lift map_children(f) to map_children(g) when implies(f, g).

Source

pub proof fn map_children_lift_skip_idx( self, cont0: Self, idx: int, f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, g: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, )

requires
0 <= idx < NR_ENTRIES,
OwnerSubtree::implies(f, g),
cont0.inv(),
cont0.map_children(f),
self.path() == cont0.path(),
self.children.len() == cont0.children.len(),
forall |j: int| 0 <= j < NR_ENTRIES && j != idx ==> self.children[j] == cont0.children[j],
self.children[idx] is Some
    ==> self
        .children[idx]
        .unwrap()
        .tree_predicate_map(self.path().push_tail(idx as usize), g),
ensures
self.map_children(g),

Lift map_children from f to g when siblings (j != idx) come from cont0 which had map_children(f), and the child at idx (if present) already satisfies g.

Source

pub proof fn as_subtree_restore(self, child: Self)

requires
self.inv(),
child.inv(),
self.all_but_index_some(),
child.all_some(),
ensures
self.restore_spec(child).0.as_subtree()
    == self.put_child_spec(child.as_subtree()).as_subtree(),

Auto Trait Implementations§

§

impl<'rcu, C> Freeze for CursorContinuation<'rcu, C>

§

impl<'rcu, C> !RefUnwindSafe for CursorContinuation<'rcu, C>

§

impl<'rcu, C> Send for CursorContinuation<'rcu, C>

§

impl<'rcu, C> Sync for CursorContinuation<'rcu, C>

§

impl<'rcu, C> Unpin for CursorContinuation<'rcu, C>
where <C as PageTableConfig>::E: Unpin, C: Unpin,

§

impl<'rcu, C> UnsafeUnpin for CursorContinuation<'rcu, C>

§

impl<'rcu, C> !UnwindSafe for CursorContinuation<'rcu, C>

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>