Struct CursorOwner 

pub struct CursorOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub list_own: LinkedListOwner<M>,
    pub index: int,
}

Fields

list_own: LinkedListOwner<M>

index: int

Implementations

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

pub open spec fn length(self) -> int

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

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

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

}

Region-based analog of CursorOwner::inv: replaces list_own.inv() (over the owned perms) with list_own.relate_region(regions) (over the region permissions).

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

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

pub open spec fn list_insert( cursor: Self, link: LinkOwner, repr_perm: LinkInnerPerms<M>, metadata_perms: MetadataPerm, list_id: u64, ) -> (Self, LinkOwner)

{
    let link = LinkOwner {
        paddr: link.paddr,
        in_list: list_id,
    };
    (
        Self {
            list_own: LinkedListOwner::<M> {
                list: cursor.list_own.list.insert(cursor.index, link),
                repr_perms: cursor.list_own.repr_perms.insert(cursor.index, repr_perm),
                metadata_perms: cursor
                    .list_own
                    .metadata_perms
                    .insert(cursor.index, metadata_perms),
                list_id,
                _marker: PhantomData,
            },
            index: cursor.index + 1,
        },
        link,
    )
}

pub proof fn tracked_list_insert( tracked cursor: &mut Self, tracked link: &mut LinkOwner, tracked repr_perm: LinkInnerPerms<M>, tracked metadata_perms: MetadataPerm, list_id: u64, )

requires

list_id != 0,

0 <= old(cursor).index <= old(cursor).list_own.list.len(),

old(cursor).list_own.repr_perms.len() == old(cursor).list_own.list.len(),

old(cursor).list_own.metadata_perms.len() == old(cursor).list_own.list.len(),

old(cursor).list_own.list.len() > 0 ==> list_id == old(cursor).list_own.list_id,

old(cursor).list_own.list_id != 0 ==> list_id == old(cursor).list_own.list_id,

ensures

({
    let res = Self::list_insert(
        *old(cursor),
        *old(link),
        repr_perm,
        metadata_perms,
        list_id,
    );
    res.0 == *final(cursor) && res.1 == *final(link)
}),

Tracked update to the cursor’s owner state when a new link is inserted before the current position. The inserted link’s paddr is unchanged and its in_list is stamped with list_id — the (non-zero) id the concrete lazy_get_id resolved. The cursor’s list gains link at old.index, adopts list_id (which equals the old id when that was already non-zero), and index advances by one. In the borrow model, the link’s tracked permission remains parked in MetaRegionOwners.slots; this axiom doesn’t need to take or carry a perm.

pub open spec fn front_owner(list_own: LinkedListOwner<M>) -> Self

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

pub open spec fn cursor_mut_at_owner(list_own: LinkedListOwner<M>, index: int) -> Self

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

pub proof fn tracked_cursor_mut_at_owner( tracked list_own: LinkedListOwner<M>, index: int, ) -> tracked Self

returns

Self::cursor_mut_at_owner(list_own, index),

pub proof fn tracked_front_owner(tracked list_own: LinkedListOwner<M>) -> tracked Self

returns

Self::front_owner(list_own),

pub open spec fn back_owner(list_own: LinkedListOwner<M>) -> Self

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

pub proof fn tracked_back_owner(tracked list_own: LinkedListOwner<M>) -> tracked res : Self

ensures

res == Self::back_owner(list_own),

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

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

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

}

pub proof fn remove_owner_spec_implies_model_spec(self, post: Self)

requires

self.remove_owner_spec(post),

0 <= self.index < self.length(),

ensures

post@ == self@.remove(),

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

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

}

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

requires

self.insert_owner_spec(link, post),

0 <= self.index <= self.length(),

ensures

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

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,
            index: 0,
        }
    } else if self.index == self.length() - 1 {
        Self {
            list_own: self.list_own,
            index: self.index + 1,
        }
    } else {
        Self {
            list_own: self.list_own,
            index: self.index + 1,
        }
    }
}

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,
            index: self.index - 1,
        }
    } else if self.index == 0 {
        Self {
            list_own: self.list_own,
            index: self.length(),
        }
    } else {
        Self {
            list_own: self.list_own,
            index: self.index - 1,
        }
    }
}

Trait Implementations

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

open spec fn inv(self) -> bool

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

}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for CursorOwner<M>

proof fn view_preserves_inv(self)

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for CursorOwner<M>

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

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

type V = CursorModel