Module list_store 

Self-contained one-step-soundness harness for the frame LinkedList (crate::mm::frame::LinkedList) — the embedding’s companion to super::VmStore, specialised to linked-list operations.

Why a separate, generic store

Unlike VmStore (which fixes concrete configs such as UserPtConfig), ListStore<M> is generic over the link metadata M. The kernel’s LinkedList<M> is a generic library with no canonical concrete instantiation in ostd, and LinkedListOwner<M> cannot be type-erased to dyn: its per-link permission is the associated type <M as Repr<MetaSlotSmall>>::Perm, embedded in LinkInnerPerms<M>, so the trait is not object-safe (cf. Frame<dyn AnyFrameMeta>, which works only because it exposes no associated type post-erasure).

Why in_list is a non-issue here

ListStore<M> requires only regions.inv() (MetaRegionOwners::inv), which — unlike VmStore::structural_inv — does not constrain in_list. A listed frame sits at rc == REF_COUNT_UNIQUE with in_list == list_id != 0; the UNIQUE branch of MetaSlotOwner::inv pins only storage/vtable_ptr init, leaving in_list free. So listed frames are admitted with no invariant weakening — the in_list == 0 constraint is purely a VmStore concern and does not arise in this harness.

State

• regions: the shared metadata-region ownership.
• lists: held LinkedListOwners. Each link is a forgotten UniqueFrame<Link<M>> (its drop-obligation was consumed by into_raw on push); the owner’s LinkedListOwner::relate_region ties every link to its UNIQUE region slot and pins the next/prev pointer wiring.
• loose: held-but-unlisted UniqueFrameOwners — live UniqueFrame<Link<M>> handles (drop-obligation present) eligible to be pushed. push moves one from loose into a list; pop moves a list’s end link out into loose.

Roadmap

Landed: the store + invariant, the front/back allocate-build-teardown suite (new, push_front / pop_front, push_back / pop_back), the general cursor surgery — insert_before / take_current at an arbitrary index (ListStore::step_insert_before_at / ListStore::step_take_at), which subsume the front/back ops — the read-only accessors (ListStore::step_size / ListStore::step_is_empty), and the full persistent cursor lifecycle: a cursor checks its list out of lists into cursors (ListStore::step_cursor_front_mut / step_cursor_back_mut / step_cursor_mut_at), walks it (step_move_next / step_move_prev / step_current_meta), mutates through it (step_cursor_insert_before / step_cursor_take_current), and checks it back in on drop (ListStore::step_cursor_drop).

Structs

ListStore

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.

Functions

axiom_empty_list_owner

fresh_list_id

fresh_loose_id

insert_before_at_embedded

lemma_fresh_list_id_not_in_dom

lemma_fresh_loose_id_not_in_dom

list_drop_embedded

list_registry_ok

pop_back_embedded

pop_front_embedded

push_back_embedded

push_front_embedded

take_at_embedded

Type Aliases

CursorId

Logical identifier for a live CursorOwner in the store. A cursor is keyed by the home ListId whose list it checked out, so a list is cursored iff its id is in cursors (and then absent from lists).

ListId

Logical identifier for a held LinkedListOwner in the store.

LooseId

Logical identifier for a loose (held-but-unlisted) UniqueFrame<Link<M>> in the store.