Skip to main content

ListStore

ostd::specs::mm::embedding::list_store

Struct ListStore 

Source 
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>>,
}
Expand description

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§

Source§

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

Source

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]
                    .inner_perms
                    .in_list
                    .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.

Source§

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

Source

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.

Source

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.

Source

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

requires
self.inv(),
self.lists.dom().contains(id),
ensures
res
    <==> (has_safe_slot(frame)
        && exists |i: int| {
            0 <= i < self.lists[id].list.len()
                && self.lists[id].slot_index_at(i) == frame_to_index(frame)
        }),

LinkedList::contains: whether frame is a link of list id. A read-only query mirroring exec contains(frame) -> bool. res holds iff frame is a safe managed slot AND one of the list’s links: for a real (non-zero) id the membership registry (list_registry_ok, an inv clause) makes the in_list[frame] == list_id comparison an exact membership test; an empty/never-pushed list (list_id == 0, hence empty) or a frame that is not a safe slot (which exec’s get_slot rejects) contains nothing.

Source

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. No region change; the new list is empty with list_id == 0 (minted on first push). Returns the fresh list id.

Source

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] old(self).lists[id].slot_index_at(i)) == 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: tear the whole list down, freeing every link’s frame (slot → UNUSED, in_list → 0) and removing the list from the store. Faithful to the verified destructor (each link is popped and UniqueFrame::dropped — no orphaning).

The per-link frame_obligations.count == 0 precondition mirrors the exec drop_requires (listed frames are forgotten); the accounting-free ListStore cannot itself supply it, so it is left to the caller. The freed frames leave the store entirely (they return to the allocator’s UNUSED pool, tracked by nobody here).

Source

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.

Source

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.

Source

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.

Source

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.

Source

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(),

Cursor insert_before at an arbitrary position n: move the loose handle lid into list id at index n (0 <= n <= len). The general form of Self::step_push_front / Self::step_push_back; same global effect.

Source

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.

Source

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).

Source

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).

Source

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()
            && old(self).lists[id].slot_index_at(i) == 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()
                && old(self).lists[id].slot_index_at(i) == 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: search list id for frame and, if it is one of the list’s links, check the list out into a cursor positioned at that link; otherwise (the frame is absent — or not a safe managed slot, which can never be a link) leave the store unchanged. Mirrors exec cursor_mut_at(frame) -> Option<CursorMut> (the Some/None outcome is returned as res).

Source

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: advance cursor id one step toward the back (wrapping through the ghost slot). Pure position change.

Source

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: retreat cursor id one step toward the front (wrapping through the ghost slot). Pure position change.

Source

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: read the link the cursor id is on. A read-only query — returns the current LinkOwner (None at the ghost slot); the store is unchanged.

Source

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 — &self on the store, so regions / lists / loose / cursors are all untouched; it merely exposes the list’s contents (the model Seq of links). Modeled for completeness, to demonstrate the read-only view changes nothing.

Source

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.

Source

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: through the checked-out cursor id, move the loose handle lid into the cursor’s list at the current position (index n), advancing the cursor to n + 1. The general Self::step_insert_before_at, but on the list parked in cursors rather than lists — so every held list is an “other list” preserved by the axiom’s frame.

Source

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, pop the link the cursor is on (index n, requires the cursor be on an element) back into the loose pool, leaving the cursor at the same index (now on the following link). The general Self::step_take_at on a cursored list. Returns the fresh loose id.

Auto Trait Implementations§

§

impl<M> Freeze for ListStore<M>

§

impl<M> !RefUnwindSafe for ListStore<M>

§

impl<M> Send for ListStore<M>

§

impl<M> Sync for ListStore<M>

§

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

§

impl<M> UnsafeUnpin for ListStore<M>

§

impl<M> UnwindSafe for ListStore<M>
where M: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

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

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

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<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::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>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::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<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A