Struct Cursor Continuation &nbsp; Copy item path

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

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

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

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

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

requires

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,

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

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

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,

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

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,

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

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,

pub open spec fn map_children( self, f: FnSpec<(EntryOwner<C>, TreePath<CONST_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))
    }
}

pub open spec fn level(self) -> PagingLevel

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

pub open spec fn inv(self) -> bool

{
    &&& self.children.len() == NR_ENTRIES()
    &&& 0 <= self.idx < NR_ENTRIES()
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES()
            ==> (self.children[i] is Some
                ==> {
                    &&& self.children[i].unwrap().value.parent_level == self.level()
                    &&& self.children[i].unwrap().inv()
                    &&& self.children[i].unwrap().level == self.tree_level + 1

                })
    }
    &&& self.entry_own.is_node()
    &&& self.entry_own.inv()
    &&& self.entry_own.node.unwrap().relate_guard_perm(self.guard_perm)
    &&& self.tree_level == INC_LEVELS() - self.level()
    &&& self.tree_level < INC_LEVELS() - 1

}

pub open spec fn all_some(self) -> bool

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

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

}

pub open spec fn inc_index(self) -> Self

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

pub proof fn do_inc_index(tracked &mut self)

requires

old(self).idx + 1 < NR_ENTRIES(),

ensures

*self == old(self).inc_index(),

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

{ guards.lock_held(self.guard_perm.value().inner.inner@.ptr.addr()) }

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

{
    &&& self.entry_own.node.unwrap().relate_region(regions)
    &&& forall |i: int| {
        0 <= i < self.children.len() && self.children[i] is Some
            ==> PageTableOwner(self.children[i].unwrap())
                .relate_region_rec(
                    self.entry_own.node.unwrap().path.push_tail(i as usize),
                    regions,
                )
    }

}

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

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

{
    Node {
        value: self.entry_own,
        children: self.children,
        level: self.tree_level,
    }
}

pub proof fn into_subtree_inv(self)

requires

self.inv(),

self.all_some(),

ensures

self.into_subtree().inv(),

Auto Trait Implementations§

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

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

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