Struct Cursor Owner &nbsp; Copy item path

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

pub open spec fn max_steps_subtree(level: usize) -> usize

{
    if level <= 1 {
        NR_ENTRIES()
    } else {
        (NR_ENTRIES() * (Self::max_steps_subtree((level - 1) as usize) + 1)) as usize
    }
}

The number of steps it will take to walk through every node of a full page table at level level

pub open spec fn max_steps_partial(self, level: usize) -> usize

{
    if level == NR_LEVELS() {
        0
    } else {
        let cont = self.continuations[(level - 1) as int];
        let steps = Self::max_steps_subtree(level) * (NR_ENTRIES() - cont.idx);
        let remaining_steps = self.max_steps_partial((level + 1) as usize);
        (steps + remaining_steps) as usize
    }
}

The number of steps it will take to walk through the remaining entries of the page table starting at the given level.

pub open spec fn max_steps(self) -> usize

{ self.max_steps_partial(self.level as usize) }

pub proof fn max_steps_partial_inv(self, other: Self, level: usize)

requires

self.inv(),

other.inv(),

self.level == other.level,

self.level <= level <= NR_LEVELS(),

forall |i: int| {
    self.level - 1 <= i < NR_LEVELS()
        ==> self.continuations[i].idx == other.continuations[i].idx
},

ensures

self.max_steps_partial(level) == other.max_steps_partial(level),

pub open spec fn push_level_owner_spec(self, guard_perm: GuardPerm<'rcu, C>) -> Self

{
    let cont = self.continuations[self.level - 1];
    let (child, cont) = cont
        .make_cont_spec(self.va.index[self.level - 2] as usize, guard_perm);
    let new_continuations = self.continuations.insert(self.level - 1, cont);
    let new_continuations = new_continuations.insert(self.level - 2, child);
    let new_level = (self.level - 1) as u8;
    Self {
        continuations: new_continuations,
        level: new_level,
        popped_too_high: false,
        ..self
    }
}

pub proof fn push_level_owner_decreases_steps(self, guard_perm: GuardPerm<'rcu, C>)

requires

self.inv(),

self.level > 0,

ensures

self.push_level_owner_spec(guard_perm).max_steps() < self.max_steps(),

pub proof fn push_level_owner_preserves_va(self, guard_perm: GuardPerm<'rcu, C>)

requires

self.inv(),

self.level > 1,

ensures

self.push_level_owner_spec(guard_perm).va == self.va,

self.push_level_owner_spec(guard_perm).continuations[self.level - 2].idx
    == self.va.index[self.level - 2],

pub proof fn push_level_owner_preserves_invs( self, guard_perm: GuardPerm<'rcu, C>, regions: MetaRegionOwners, guards: Guards<'rcu, C>, )

requires

self.inv(),

self.level > 1,

self.only_current_locked(guards),

self.nodes_locked(guards),

self.relate_region(regions),

ensures

self.push_level_owner_spec(guard_perm).inv(),

self.push_level_owner_spec(guard_perm).children_not_locked(guards),

self.push_level_owner_spec(guard_perm).nodes_locked(guards),

self.push_level_owner_spec(guard_perm).relate_region(regions),

pub proof fn push_level_owner(tracked &mut self, tracked guard_perm: Tracked<GuardPerm<'rcu, C>>)

requires

old(self).inv(),

old(self).level > 1,

ensures

*self == old(self).push_level_owner_spec(guard_perm@),

pub open spec fn pop_level_owner_spec(self) -> (Self, GuardPerm<'rcu, C>)

{
    let child = self.continuations[self.level - 1];
    let cont = self.continuations[self.level as int];
    let (new_cont, guard_perm) = cont.restore_spec(child);
    let new_continuations = self.continuations.insert(self.level as int, new_cont);
    let new_continuations = new_continuations.remove(self.level - 1);
    let new_level = (self.level + 1) as u8;
    let popped_too_high = if new_level >= self.guard_level { true } else { false };
    (
        Self {
            continuations: new_continuations,
            level: new_level,
            popped_too_high: popped_too_high,
            ..self
        },
        guard_perm,
    )
}

pub proof fn pop_level_owner_preserves_inv(self)

requires

self.inv(),

self.level < NR_LEVELS(),

self.in_locked_range(),

ensures

self.pop_level_owner_spec().0.inv(),

pub proof fn pop_level_owner_preserves_invs( self, guards: Guards<'rcu, C>, regions: MetaRegionOwners, )

requires

self.inv(),

self.level < NR_LEVELS(),

self.children_not_locked(guards),

self.nodes_locked(guards),

self.relate_region(regions),

ensures

self.pop_level_owner_spec().0.inv(),

self.pop_level_owner_spec().0.children_not_locked(guards),

self.pop_level_owner_spec().0.nodes_locked(guards),

self.pop_level_owner_spec().0.relate_region(regions),

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

requires

old(self).inv(),

old(self).level < NR_LEVELS(),

ensures

*self == old(self).pop_level_owner_spec().0,

guard_perm == old(self).pop_level_owner_spec().1,

pub open spec fn move_forward_owner_spec(self) -> Self

recommends

self.inv(),

self.level < NR_LEVELS(),

self.in_locked_range(),

{
    if self.index() + 1 < NR_ENTRIES() {
        self.inc_index()
    } else if self.level < NR_LEVELS() {
        self.pop_level_owner_spec().0.move_forward_owner_spec()
    } else {
        Self {
            popped_too_high: false,
            ..self
        }
    }
}

pub proof fn move_forward_increases_va(self)

requires

self.inv(),

self.level <= NR_LEVELS(),

self.in_locked_range(),

ensures

self.move_forward_owner_spec().va.to_vaddr() > self.va.to_vaddr(),

pub proof fn move_forward_not_popped_too_high(self)

requires

self.inv(),

self.level <= NR_LEVELS(),

self.in_locked_range(),

ensures

!self.move_forward_owner_spec().popped_too_high,

pub proof fn move_forward_owner_decreases_steps(self)

requires

self.inv(),

self.level <= NR_LEVELS(),

ensures

self.move_forward_owner_spec().max_steps() < self.max_steps(),

pub proof fn move_forward_preserves_invs( self, guards: Guards<'rcu, C>, regions: MetaRegionOwners, )

requires

self.inv(),

self.level <= NR_LEVELS(),

self.in_locked_range(),

self.children_not_locked(guards),

self.nodes_locked(guards),

self.relate_region(regions),

ensures

self.move_forward_owner_spec().children_not_locked(guards),

self.move_forward_owner_spec().nodes_locked(guards),

self.move_forward_owner_spec().relate_region(regions),

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

pub open spec fn node_unlocked( guards: Guards<'rcu, C>, ) -> FnSpec<(EntryOwner<C>, TreePath<CONST_NR_ENTRIES>), bool>

{
    |owner: EntryOwner<C>, path: TreePath<CONST_NR_ENTRIES>| {
        owner.is_node() ==> guards.unlocked(owner.node.unwrap().meta_perm.addr())
    }
}

pub open spec fn node_unlocked_except( guards: Guards<'rcu, C>, addr: usize, ) -> FnSpec<(EntryOwner<C>, TreePath<CONST_NR_ENTRIES>), bool>

{
    |owner: EntryOwner<C>, path: TreePath<CONST_NR_ENTRIES>| {
        owner.is_node()
            ==> (owner.node.unwrap().meta_perm.addr() != addr
                ==> guards.unlocked(owner.node.unwrap().meta_perm.addr()))
    }
}

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

{
    forall |i: int| {
        self.level - 1 <= i < NR_LEVELS()
            ==> { self.continuations[i].map_children(Self::node_unlocked(guards)) }
    }
}

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

{
    forall |i: int| {
        self.level - 1 <= i < NR_LEVELS()
            ==> self
                .continuations[i]
                .map_children(
                    Self::node_unlocked_except(
                        guards,
                        self.cur_entry_owner().node.unwrap().meta_perm.addr(),
                    ),
                )
    }
}

pub proof fn never_drop_preserves_nodes_locked( self, guard: PageTableGuard<'rcu, C>, guards0: Guards<'rcu, C>, guards1: Guards<'rcu, C>, )

requires

self.inv(),

self.nodes_locked(guards0),

<PageTableGuard<'rcu, C> as Undroppable>::constructor_requires(guard, guards0),

<PageTableGuard<'rcu, C> as Undroppable>::constructor_ensures(guard, guards0, guards1),

forall |i: int| {
    self.level - 1 <= i < NR_LEVELS()
        ==> self.continuations[i].guard_perm.value().inner.inner@.ptr.addr()
            != guard.inner.inner@.ptr.addr()
},

ensures

self.nodes_locked(guards1),

pub proof fn never_drop_preserves_children_not_locked( self, guard: PageTableGuard<'rcu, C>, guards0: Guards<'rcu, C>, guards1: Guards<'rcu, C>, )

requires

self.inv(),

self.children_not_locked(guards0),

<PageTableGuard<'rcu, C> as Undroppable>::constructor_requires(guard, guards0),

<PageTableGuard<'rcu, C> as Undroppable>::constructor_ensures(guard, guards0, guards1),

ensures

self.children_not_locked(guards1),

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

requires

self.inv(),

OwnerSubtree::implies(f, g),

forall |i: int| {
    self.level - 1 <= i < NR_LEVELS() ==> self.continuations[i].map_children(f)
},

ensures

forall |i: int| {
    self.level - 1 <= i < NR_LEVELS() ==> self.continuations[i].map_children(g)
},

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

{
    forall |i: int| {
        self.level - 1 <= i < NR_LEVELS()
            ==> { self.continuations[i].node_locked(guards) }
    }
}

pub open spec fn index(self) -> usize

{ self.continuations[self.level - 1].idx }

pub open spec fn inc_index(self) -> Self

{
    Self {
        continuations: self
            .continuations
            .insert(self.level - 1, self.continuations[self.level - 1].inc_index()),
        va: AbstractVaddr {
            offset: self.va.offset,
            index: self
                .va
                .index
                .insert(
                    self.level - 1,
                    self.continuations[self.level - 1].inc_index().idx as int,
                ),
        },
        popped_too_high: false,
        ..self
    }
}

pub proof fn do_inc_index(tracked &mut self)

requires

old(self).inv(),

old(self).continuations[old(self).level - 1].idx + 1 < NR_ENTRIES(),

old(self).in_locked_range(),

ensures

self.inv(),

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

pub proof fn inc_index_increases_va(self)

requires

self.inv(),

ensures

self.inc_index().va.to_vaddr() > self.va.to_vaddr(),

pub open spec fn cur_va(self) -> Vaddr

{ self.va.to_vaddr() }

pub proof fn inv_continuation(self, i: int)

requires

self.inv(),

self.level - 1 <= i <= NR_LEVELS() - 1,

ensures

self.continuations.contains_key(i),

self.continuations[i].inv(),

self.continuations[i].children.len() == NR_ENTRIES(),

pub open spec fn cur_entry_owner(self) -> EntryOwner<C>

{ self.continuations[self.level - 1].children[self.index() as int].unwrap().value }

pub open spec fn locked_range(self) -> Range<Vaddr>

{
    let start = self.prefix.align_down(self.guard_level as int).to_vaddr();
    let end = self.prefix.align_up(self.guard_level as int).to_vaddr();
    Range { start, end }
}

pub open spec fn in_locked_range(self) -> bool

{ self.locked_range().start <= self.va.to_vaddr() < self.locked_range().end }

pub open spec fn above_locked_range(self) -> bool

{ self.va.to_vaddr() >= self.locked_range().end }

pub proof fn prefix_in_locked_range(self)

requires

forall |i: int| i >= self.guard_level ==> self.va.index[i] == self.prefix.index[i],

ensures

self.in_locked_range(),

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

{
    let f = |owner: EntryOwner<C>, path: TreePath<CONST_NR_ENTRIES>| {
        owner.is_node() ==> owner.node.unwrap().relate_region(regions)
    };
    forall |i: int| {
        self.level - 1 <= i < NR_LEVELS() ==> self.continuations[i].map_children(f)
    }
}

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

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

{
    if self.level == NR_LEVELS() {
        PageTableOwner(self.continuations[self.level - 1].into_subtree())
    } else {
        self.pop_level_owner_spec().0.into_pt_owner_rec()
    }
}

Trait Implementations§

impl<'rcu, C: PageTableConfig> Inv for CursorOwner<'rcu, C>

open spec fn inv(self) -> bool

{
    &&& self.va.inv()
    &&& 1 <= self.level <= NR_LEVELS()
    &&& self.guard_level <= NR_LEVELS()
    &&& self.popped_too_high ==> self.level >= self.guard_level && self.in_locked_range()
    &&& !self.popped_too_high
        ==> self.level < self.guard_level || self.above_locked_range()
    &&& self.continuations[self.level - 1].all_some()
    &&& forall |i: int| {
        self.level <= i < NR_LEVELS()
            ==> { (#[trigger] self.continuations[i]).all_but_index_some() }
    }
    &&& self.prefix.inv()
    &&& forall |i: int| i < self.guard_level ==> self.prefix.index[i] == 0
    &&& self.level <= 4
        ==> {
            &&& self.continuations.contains_key(3)
            &&& self.continuations[3].inv()
            &&& self.continuations[3].level() == 4
            &&& self.continuations[3].entry_own.parent_level == 5
            &&& self.va.index[3] == self.continuations[3].idx

        }
    &&& self.level <= 3
        ==> {
            &&& self.continuations.contains_key(2)
            &&& self.continuations[2].inv()
            &&& self.continuations[2].level() == 3
            &&& self.continuations[2].entry_own.parent_level == 4
            &&& self.va.index[2] == self.continuations[2].idx
            &&& self.continuations[2].guard_perm.value().inner.inner@.ptr.addr()
                != self.continuations[3].guard_perm.value().inner.inner@.ptr.addr()

        }
    &&& self.level <= 2
        ==> {
            &&& self.continuations.contains_key(1)
            &&& self.continuations[1].inv()
            &&& self.continuations[1].level() == 2
            &&& self.continuations[1].entry_own.parent_level == 3
            &&& self.va.index[1] == self.continuations[1].idx
            &&& self.continuations[1].guard_perm.value().inner.inner@.ptr.addr()
                != self.continuations[2].guard_perm.value().inner.inner@.ptr.addr()
            &&& self.continuations[1].guard_perm.value().inner.inner@.ptr.addr()
                != self.continuations[3].guard_perm.value().inner.inner@.ptr.addr()

        }
    &&& self.level == 1
        ==> {
            &&& self.continuations.contains_key(0)
            &&& self.continuations[0].inv()
            &&& self.continuations[0].level() == 1
            &&& self.continuations[0].entry_own.parent_level == 2
            &&& self.va.index[0] == self.continuations[0].idx
            &&& self.continuations[0].guard_perm.value().inner.inner@.ptr.addr()
                != self.continuations[1].guard_perm.value().inner.inner@.ptr.addr()
            &&& self.continuations[0].guard_perm.value().inner.inner@.ptr.addr()
                != self.continuations[2].guard_perm.value().inner.inner@.ptr.addr()
            &&& self.continuations[0].guard_perm.value().inner.inner@.ptr.addr()
                != self.continuations[3].guard_perm.value().inner.inner@.ptr.addr()

        }

}

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

{
    CursorView {
        cur_va: self.cur_va(),
        mappings: self.into_pt_owner_rec().view().mappings,
        phantom: PhantomData,
    }
}

type V = CursorView<C>

Auto Trait Implementations§

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

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

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

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

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

impl<'rcu, C> !UnwindSafe for CursorOwner<'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