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_perm: GuardPerm<'rcu, C>,
}

Fields§

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

Implementations§

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,
*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
*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_perm: GuardPerm<'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_perm: guard_perm,
    };
    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, tracked guard_perm: Tracked<GuardPerm<'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_perm@).0,
*self == old(self).make_cont_spec(idx, guard_perm@).1,
Source

pub open spec fn restore_spec(self, child: Self) -> (Self, GuardPerm<'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_perm,
    )
}
Source

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

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

pub open spec fn new_spec( owner_subtree: OwnerSubtree<C>, idx: usize, guard_perm: GuardPerm<'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_perm: guard_perm,
    }
}
Source

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

ensures
res == Self::new_spec(owner_subtree, idx, guard_perm),
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 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 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
                &&& <EntryOwner<
                    C,
                > as TreeNodeValue<
                    NR_LEVELS,
                >>::rel_children(self.entry_own, i, Some(child.unwrap().value))
                &&& 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 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,
<EntryOwner<
    C,
> as TreeNodeValue<
    NR_LEVELS,
>>::rel_children(self.entry_own, i, Some(self.children[i].unwrap().value)),
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.entry_own.is_node()
    &&& self.entry_own.inv()
    &&& !self.entry_own.in_scope
    &&& self.entry_own.node.unwrap().relate_guard_perm(self.guard_perm)
    &&& 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
*self == old(self).inc_index(),
Source

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

{ guards.lock_held(self.guard_perm.value().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 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(),
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(),
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 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

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

requires
entry.node_matching(child_value, parent_owner, guard_perm),
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
<EntryOwner<
    C,
> as TreeNodeValue<NR_LEVELS>>::rel_children(entry_own, idx as int, Some(child_value)),

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)

requires
self.entry_own.is_node(),
self.entry_own.inv(),
self.entry_own.node.unwrap().relate_guard_perm(self.guard_perm),
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,
<EntryOwner<
    C,
> as TreeNodeValue<
    NR_LEVELS,
>>::rel_children(
    self.entry_own,
    self.idx as int,
    Some(self.children[self.idx as int].unwrap().value),
),
!self.children[self.idx as int].unwrap().value.in_scope,
ensures
self.inv(),

After restoring entry_own.node = Some(parent_owner) and putting the child back at idx, the continuation invariant holds. The child at idx may have been modified (e.g., by split_if_mapped_huge or protect) but must satisfy inv(), have the correct path/parent_level/level, satisfy rel_children, and have !in_scope.

Source

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

requires
self.inv(),
old(regions).slots.contains_key(frame_to_index(paddr)),
ensures
regions.slot_owners == old(regions).slot_owners,
regions.slots == old(regions).slots.remove(frame_to_index(paddr)),
res.value
    == EntryOwner::<
        C,
    >::new_frame_spec(
        paddr,
        self.path().push_tail(self.idx as usize),
        self.level(),
        prop,
        old(regions).slots[frame_to_index(paddr)],
    ),
res.inv(),
res.level == self.tree_level + 1,
res == OwnerSubtree::new_val(res.value, res.level as nat),

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