ostd::specs::mm::frame::linked_list::linked_list_owners

Struct CursorOwner

pub struct CursorOwner<M: AnyFrameMeta + Repr<MetaSlot>> {
    pub list_own: LinkedListOwner<M>,
    pub list_perm: PointsTo<LinkedList<M>>,
    pub index: int,
}

Fields§

§list_own: LinkedListOwner<M>§list_perm: PointsTo<LinkedList<M>>§index: int

Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlot>> CursorOwner<M>

Source

pub open spec fn length(self) -> int

{ self.list_own.list.len() as int }

Source

pub open spec fn current(self) -> Option<LinkOwner>

{
    if 0 <= self.index < self.length() {
        Some(self.list_own.list[self.index])
    } else {
        None
    }
}

Source

pub exec fn list_insert( verus_tmp_cursor: Tracked<&mut Self>, verus_tmp_link: Tracked<&mut LinkOwner>, verus_tmp_perm: Tracked<&PointsTo<MetaSlot, Link<M>>>, )

ensures

cursor.list_own.list == old(cursor).list_own.list.insert(old(cursor).index, *old(link)),

cursor.list_own.list_id == old(cursor).list_own.list_id,

forall |idx: int| 0 <= idx < cursor.length() ==> cursor.list_own.perms.contains_key(idx),

forall |idx: int| {
    0 <= idx < cursor.index
        ==> cursor.list_own.perms[idx] == old(cursor).list_own.perms[idx]
},

forall |idx: int| {
    old(cursor).index < idx <= old(cursor).length()
        ==> cursor.list_own.perms[idx] == old(cursor).list_own.perms[idx - 1]
},

cursor.list_own.perms[old(cursor).index] == perm,

cursor.index == old(cursor).index + 1,

cursor.list_perm == old(cursor).list_perm,

*link == *old(link),

Source

pub open spec fn front_owner_spec( list_own: LinkedListOwner<M>, list_perm: PointsTo<LinkedList<M>>, ) -> Self

{
    CursorOwner::<M> {
        list_own: list_own,
        list_perm: list_perm,
        index: 0,
    }
}

Source

pub proof fn front_owner( list_own: LinkedListOwner<M>, list_perm: PointsTo<LinkedList<M>>, ) -> res : Self

ensures

res == Self::front_owner_spec(list_own, list_perm),

Source

pub open spec fn back_owner_spec( list_own: LinkedListOwner<M>, list_perm: PointsTo<LinkedList<M>>, ) -> Self

{
    CursorOwner::<M> {
        list_own: list_own,
        list_perm: list_perm,
        index: if list_own.list.len() > 0 { list_own.list.len() as int - 1 } else { 0 },
    }
}

Source

pub proof fn back_owner( list_own: LinkedListOwner<M>, list_perm: PointsTo<LinkedList<M>>, ) -> res : Self

ensures

res == Self::back_owner_spec(list_own, list_perm),

Source

pub open spec fn ghost_owner_spec( list_own: LinkedListOwner<M>, list_perm: PointsTo<LinkedList<M>>, ) -> Self

{
    CursorOwner::<M> {
        list_own: list_own,
        list_perm: list_perm,
        index: list_own.list.len() as int,
    }
}

Source

pub proof fn ghost_owner( list_own: LinkedListOwner<M>, list_perm: PointsTo<LinkedList<M>>, ) -> res : Self

ensures

res == Self::ghost_owner_spec(list_own, list_perm),

Source §

impl<M: AnyFrameMeta + Repr<MetaSlot>> CursorOwner<M>

Source

pub open spec fn remove_owner_spec(self, post: Self) -> bool

recommends

self.index < self.length(),

{
    &&& post.list_own.list == self.list_own.list.remove(self.index)
    &&& post.index == self.index

}

Source

pub proof fn remove_owner_spec_implies_model_spec(self, post: Self)

requires

self.remove_owner_spec(post),

ensures

post@ == self@.remove(),

Source

pub open spec fn insert_owner_spec(self, link: LinkOwner, post: Self) -> bool

recommends

self.index < self.length(),

{
    &&& post.list_own.list == self.list_own.list.insert(self.index, link)
    &&& post.list_own.list_id == self.list_own.list_id
    &&& post.index == self.index + 1

}

Source

pub proof fn insert_owner_spec_implies_model_spec(self, link: LinkOwner, post: Self)

requires

self.insert_owner_spec(link, post),

ensures

post@ == self@.insert(link@),

Source

pub open spec fn move_next_owner_spec(self) -> Self

{
    if self.length() == 0 {
        self
    } else if self.index == self.length() {
        Self {
            list_own: self.list_own,
            list_perm: self.list_perm,
            index: 0,
        }
    } else if self.index == self.length() - 1 {
        Self {
            list_own: self.list_own,
            list_perm: self.list_perm,
            index: self.index + 1,
        }
    } else {
        Self {
            list_own: self.list_own,
            list_perm: self.list_perm,
            index: self.index + 1,
        }
    }
}

Source

pub open spec fn move_prev_owner_spec(self) -> Self

{
    if self.length() == 0 {
        self
    } else if self.index == self.length() {
        Self {
            list_own: self.list_own,
            list_perm: self.list_perm,
            index: self.index - 1,
        }
    } else if self.index == 0 {
        Self {
            list_own: self.list_own,
            list_perm: self.list_perm,
            index: self.length(),
        }
    } else {
        Self {
            list_own: self.list_own,
            list_perm: self.list_perm,
            index: self.index - 1,
        }
    }
}

Trait Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlot>> Inv for CursorOwner<M>

Source §

open spec fn inv(self) -> bool

{
    &&& 0 <= self.index <= self.length()
    &&& self.list_own.inv()

}

Source §

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

{
    let list = self.list_own.view();
    CursorModel {
        fore: list.list.take(self.index),
        rear: list.list.skip(self.index),
        list_model: list,
    }
}

Source §