Struct Linked List Owner &nbsp; Copy item path

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M>

pub open spec fn inv_at(self, i: int) -> bool

{
    &&& self.perms.contains_key(i)
    &&& self.perms[i].addr() == self.list[i].paddr
    &&& self.perms[i].points_to.addr() == self.list[i].paddr
    &&& self.perms[i].wf(&self.perms[i].inner_perms)
    &&& self.perms[i].addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= self.perms[i].addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& self.perms[i].is_init()
    &&& self.perms[i].value().metadata.wf(self.list[i])
    &&& i == 0 <==> self.perms[i].value().metadata.prev is None
    &&& i == self.list.len() - 1 <==> self.perms[i].value().metadata.next is None
    &&& 0 < i
        ==> {
            &&& self.perms[i].value().metadata.prev is Some
            &&& self.perms[i].value().metadata.prev.unwrap().addr()
                == self.perms[i - 1].addr()
            &&& self.perms[i].value().metadata.prev.unwrap().ptr
                == self.perms[i - 1].points_to.pptr()

        }
    &&& i < self.list.len() - 1
        ==> {
            &&& self.perms[i].value().metadata.next is Some
            &&& self.perms[i].value().metadata.next.unwrap().addr()
                == self.perms[i + 1].addr()
            &&& self.perms[i].value().metadata.next.unwrap().ptr
                == self.perms[i + 1].points_to.pptr()

        }
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}

pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel>

{
    if owners.len() == 0 {
        Seq::<LinkModel>::empty()
    } else {
        seq![owners[0].view()].add(Self::view_helper(owners.remove(0)))
    }
}

pub proof fn view_preserves_len(owners: Seq<LinkOwner>)

ensures

Self::view_helper(owners).len() == owners.len(),

pub proof fn view_helper_index(owners: Seq<LinkOwner>, i: int)

requires

0 <= i < owners.len(),

ensures

Self::view_helper(owners)[i] == owners[i].view(),

Proves that view_helper preserves indexing: view_helper(s)[i] == s[i].view()

pub proof fn view_helper_remove(owners: Seq<LinkOwner>, i: int)

requires

0 <= i < owners.len(),

ensures

Self::view_helper(owners.remove(i)) =~= Self::view_helper(owners).remove(i),

Proves that view_helper commutes with remove: view_helper(s.remove(i)) =~= view_helper(s).remove(i)

pub proof fn view_helper_insert(owners: Seq<LinkOwner>, i: int, v: LinkOwner)

requires

0 <= i <= owners.len(),

ensures

Self::view_helper(owners.insert(i, v)) =~= Self::view_helper(owners).insert(i, v.view()),

Proves that view_helper commutes with insert: view_helper(s.insert(i, v)) =~= view_helper(s).insert(i, v.view())

Trait Implementations§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for LinkedListOwner<M>

open spec fn inv(self) -> bool

{ forall |i: int| 0 <= i < self.list.len() ==> self.inv_at(i) }

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

{
    LinkedListModel {
        list: Self::view_helper(self.list),
    }
}

type V = LinkedListModel

Auto Trait Implementations§

impl<M> Freeze for LinkedListOwner<M>

impl<M> !RefUnwindSafe for LinkedListOwner<M>

impl<M> Send for LinkedListOwner<M>
where M: Send,

impl<M> Sync for LinkedListOwner<M>
where M: Sync,

impl<M> Unpin for LinkedListOwner<M>
where M: Unpin,

impl<M> UnwindSafe for LinkedListOwner<M>
where M: 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