Struct ListStore 

pub struct ListStore<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub regions: MetaRegionOwners,
    pub lists: Map<ListId, LinkedListOwner<M>>,
    pub loose: Map<LooseId, UniqueFrameOwner<Link<M>>>,
    pub cursors: Map<CursorId, CursorOwner<M>>,
}

One-step-soundness store for the frame LinkedList. Holds the shared regions, the set of held lists, the pool of loose (push-eligible) UniqueFrame<Link<M>> handles, and the live cursors.

A cursor checks out its list: a live CursorMut borrows the LinkedList exclusively, so while a cursor exists its LinkedListOwner lives inside the CursorOwner (cursors) rather than in lists. Dropping the cursor returns the list to lists.

Fields

regions: MetaRegionOwners

lists: Map<ListId, LinkedListOwner<M>>

loose: Map<LooseId, UniqueFrameOwner<Link<M>>>

cursors: Map<CursorId, CursorOwner<M>>

Implementations

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

pub open spec fn inv(self) -> bool

{
    &&& self.regions.inv()
    &&& forall |id: ListId| {
        #[trigger] self.lists.dom().contains(id)
            ==> {
                &&& self.lists[id].inv()
                &&& self.lists[id].relate_region(self.regions)

            }
    }
    &&& forall |lid: LooseId| {
        #[trigger] self.loose.dom().contains(lid)
            ==> {
                &&& self.loose[lid].inv()
                &&& self.loose[lid].global_inv(self.regions)
                &&& self.loose[lid].frame_link_inv(self.regions)
                &&& self
                    .regions
                    .slot_owners[self.loose[lid].slot_index]
                    .in_list_perm
                    .value() == 0

            }
    }
    &&& forall |id1: ListId, id2: ListId| {
        self.lists.dom().contains(id1) && self.lists.dom().contains(id2)
            && self.lists[id1].list_id == self.lists[id2].list_id
            && self.lists[id1].list_id != 0 ==> id1 == id2
    }
    &&& forall |lid1: LooseId, lid2: LooseId| {
        self.loose.dom().contains(lid1) && self.loose.dom().contains(lid2)
            && self.loose[lid1].slot_index == self.loose[lid2].slot_index
            ==> lid1 == lid2
    }
    &&& self.lists.dom().disjoint(self.cursors.dom())
    &&& forall |cid: CursorId| {
        #[trigger] self.cursors.dom().contains(cid)
            ==> {
                &&& self.cursors[cid].list_own.inv()
                &&& self.cursors[cid].wf_with_region(self.regions)

            }
    }
    &&& forall |id: ListId, cid: CursorId| {
        self.lists.dom().contains(id) && self.cursors.dom().contains(cid)
            && self.lists[id].list_id == self.cursors[cid].list_own.list_id
            && self.lists[id].list_id != 0 ==> false
    }
    &&& forall |cid1: CursorId, cid2: CursorId| {
        self.cursors.dom().contains(cid1) && self.cursors.dom().contains(cid2)
            && self.cursors[cid1].list_own.list_id == self.cursors[cid2].list_own.list_id
            && self.cursors[cid1].list_own.list_id != 0 ==> cid1 == cid2
    }
    &&& forall |id: ListId| {
        #[trigger] self.lists.dom().contains(id)
            ==> list_registry_ok(self.regions, self.lists[id])
    }
    &&& forall |cid: CursorId| {
        #[trigger] self.cursors.dom().contains(cid)
            ==> list_registry_ok(self.regions, self.cursors[cid].list_own)
    }

}

The store’s top-level invariant.

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

pub proof fn step_size(tracked &self, id: ListId) -> res : nat

requires

self.inv(),

self.lists.dom().contains(id),

ensures

res == self.lists[id].list.len(),

LinkedList::size: the number of links in list id. A read-only query — the store is unchanged.

pub proof fn step_is_empty(tracked &self, id: ListId) -> res : bool

requires

self.inv(),

self.lists.dom().contains(id),

ensures

res <==> self.lists[id].list.len() == 0,

LinkedList::is_empty: whether list id has no links. Read-only.

pub proof fn step_contains(tracked &self, id: ListId, frame: Paddr) -> res : bool

requires

self.inv(),

self.lists.dom().contains(id),

ensures

res
    <==> (valid_frame_paddr(frame)
        && exists |i: int| {
            0 <= i < self.lists[id].list.len()
                && #[trigger] meta_to_index(self.lists[id].list[i].paddr)
                    == frame_to_index(frame)
        }),

LinkedList::contains: whether frame is a link of list id.

pub proof fn step_list_new(tracked &mut self) -> res : ListId

requires

old(self).inv(),

ensures

final(self).inv(),

final(self).regions == old(self).regions,

final(self).loose == old(self).loose,

!old(self).lists.dom().contains(res),

final(self).lists == old(self).lists.insert(res, final(self).lists[res]),

final(self).lists[res].list.len() == 0,

LinkedList::new: register a fresh empty list.

pub proof fn step_list_drop(tracked &mut self, id: ListId)

requires

old(self).inv(),

old(self).lists.dom().contains(id),

forall |i: int| {
    0 <= i < old(self).lists[id].list.len()
        ==> old(self)
            .regions
            .frame_obligations
            .count(#[trigger] meta_to_index(old(self).lists[id].list[i].paddr)) == 0
},

ensures

final(self).inv(),

!final(self).lists.dom().contains(id),

final(self).loose == old(self).loose,

final(self).cursors == old(self).cursors,

Drop of LinkedList id. Faithful to the verified destructor.

pub proof fn step_push_front(tracked &mut self, id: ListId, lid: LooseId)

requires

old(self).inv(),

old(self).lists.dom().contains(id),

old(self).loose.dom().contains(lid),

ensures

final(self).inv(),

LinkedList::push_front: move the loose handle lid to the front of list id. The frame is forgotten into the list (its drop-obligation consumed); the loose entry is removed.

pub proof fn step_pop_front(tracked &mut self, id: ListId) -> res : Option<LooseId>

requires

old(self).inv(),

old(self).lists.dom().contains(id),

ensures

final(self).inv(),

old(self).lists[id].list.len() == 0 ==> res is None && *final(self) == *old(self),

old(self).lists[id].list.len() > 0 ==> res is Some,

LinkedList::pop_front: pop the front link of list id back into the loose pool as a fresh UniqueFrame<Link<M>>. Requires the list be non-empty. Returns the fresh loose id.

pub proof fn step_push_back(tracked &mut self, id: ListId, lid: LooseId)

requires

old(self).inv(),

old(self).lists.dom().contains(id),

old(self).loose.dom().contains(lid),

ensures

final(self).inv(),

LinkedList::push_back: move the loose handle lid to the back of list id. Same global effect as Self::step_push_front — only the link’s position within the list differs.

pub proof fn step_pop_back(tracked &mut self, id: ListId) -> res : Option<LooseId>

requires

old(self).inv(),

old(self).lists.dom().contains(id),

ensures

final(self).inv(),

old(self).lists[id].list.len() == 0 ==> res is None && *final(self) == *old(self),

old(self).lists[id].list.len() > 0 ==> res is Some,

LinkedList::pop_back: pop the back link of list id back into the loose pool. Same global effect as Self::step_pop_front — only which link is removed differs.

pub proof fn step_insert_before_at(tracked &mut self, id: ListId, n: int, lid: LooseId)

requires

old(self).inv(),

old(self).lists.dom().contains(id),

old(self).loose.dom().contains(lid),

0 <= n <= old(self).lists[id].list.len(),

ensures

final(self).inv(),

The general form of Self::step_push_front / Self::step_push_back; same global effect.

pub proof fn step_take_at(tracked &mut self, id: ListId, n: int) -> res : Option<LooseId>

requires

old(self).inv(),

old(self).lists.dom().contains(id),

ensures

final(self).inv(),

!(0 <= n < old(self).lists[id].list.len()) ==> res is None && *final(self) == *old(self),

0 <= n < old(self).lists[id].list.len() ==> res is Some,

Cursor take_current at an arbitrary position n: pop the link at index n (0 <= n < len) of list id back into the loose pool. The general form of Self::step_pop_front / Self::step_pop_back; same global effect.

pub proof fn step_cursor_front_mut(tracked &mut self, id: ListId)

requires

old(self).inv(),

old(self).lists.dom().contains(id),

ensures

final(self).inv(),

!final(self).lists.dom().contains(id),

final(self).cursors.dom().contains(id),

final(self).cursors[id] == CursorOwner::front_owner(old(self).lists[id]),

LinkedList::cursor_front_mut: check list id out into a cursor positioned at the front (index 0). The list leaves lists and enters cursors under the same id (its borrow).

pub proof fn step_cursor_back_mut(tracked &mut self, id: ListId)

requires

old(self).inv(),

old(self).lists.dom().contains(id),

ensures

final(self).inv(),

!final(self).lists.dom().contains(id),

final(self).cursors.dom().contains(id),

final(self).cursors[id] == CursorOwner::back_owner(old(self).lists[id]),

LinkedList::cursor_back_mut: check list id out into a cursor at the back (the last element, or the ghost slot when empty).

pub proof fn step_cursor_mut_at(tracked &mut self, id: ListId, frame: Paddr) -> res : bool

requires

old(self).inv(),

old(self).lists.dom().contains(id),

ensures

final(self).inv(),

res
    == (exists |i: int| {
        0 <= i < old(self).lists[id].list.len()
            && #[trigger] meta_to_index(old(self).lists[id].list[i].paddr)
                == frame_to_index(frame)
    }),

res
    ==> !final(self).lists.dom().contains(id) && final(self).cursors.dom().contains(id)
        && exists |i: int| {
            0 <= i < old(self).lists[id].list.len()
                && #[trigger] meta_to_index(old(self).lists[id].list[i].paddr)
                    == #[trigger] frame_to_index(frame)
                && final(self).cursors[id]
                    == CursorOwner::cursor_mut_at_owner(old(self).lists[id], i)
        },

!res ==> *final(self) == *old(self),

LinkedList::cursor_mut_at.

pub proof fn step_move_next(tracked &mut self, id: CursorId)

requires

old(self).inv(),

old(self).cursors.dom().contains(id),

ensures

final(self).inv(),

final(self).regions == old(self).regions,

final(self).cursors[id] == old(self).cursors[id].move_next_owner_spec(),

CursorMut::move_next.

pub proof fn step_move_prev(tracked &mut self, id: CursorId)

requires

old(self).inv(),

old(self).cursors.dom().contains(id),

ensures

final(self).inv(),

final(self).regions == old(self).regions,

final(self).cursors[id] == old(self).cursors[id].move_prev_owner_spec(),

CursorMut::move_prev.

pub proof fn step_current_meta(tracked &self, id: CursorId) -> res : Option<LinkOwner>

requires

self.inv(),

self.cursors.dom().contains(id),

ensures

res == self.cursors[id].current(),

res.is_some() <==> 0 <= self.cursors[id].index < self.cursors[id].length(),

CursorMut::current_meta.

pub proof fn step_as_list(tracked &self, id: CursorId) -> res : Seq<LinkOwner>

requires

self.inv(),

self.cursors.dom().contains(id),

ensures

res == self.cursors[id].list_own.list,

res.len() == self.cursors[id].length(),

CursorMut::as_list: borrow the cursor’s checked-out list for reading. A pure no-op.

pub proof fn step_cursor_drop(tracked &mut self, id: CursorId)

requires

old(self).inv(),

old(self).cursors.dom().contains(id),

ensures

final(self).inv(),

!final(self).cursors.dom().contains(id),

final(self).lists.dom().contains(id),

final(self).lists[id] == old(self).cursors[id].list_own,

Drop of a CursorMut: check the cursor’s list back into lists under its home id, ending the borrow. Inverse of Self::step_cursor_front_mut et al.

pub proof fn step_cursor_insert_before(tracked &mut self, id: CursorId, lid: LooseId)

requires

old(self).inv(),

old(self).cursors.dom().contains(id),

old(self).loose.dom().contains(lid),

ensures

final(self).inv(),

CursorMut::insert_before.

pub proof fn step_cursor_take_current(tracked &mut self, id: CursorId) -> res : Option<LooseId>

requires

old(self).inv(),

old(self).cursors.dom().contains(id),

ensures

final(self).inv(),

!(0 <= old(self).cursors[id].index < old(self).cursors[id].length())
    ==> res is None && *final(self) == *old(self),

0 <= old(self).cursors[id].index < old(self).cursors[id].length() ==> res is Some,

CursorMut::take_current: through the checked-out cursor id,