Skip to main content

list_registry_ok

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

Function list_registry_ok 

Source 
pub open spec fn list_registry_ok<M: AnyFrameMeta + Repr<MetaSlotSmall>>(
    regions: MetaRegionOwners,
    lo: LinkedListOwner<M>,
) -> bool
Expand description
{
    &&& forall |i: int| {
        0 <= i < lo.list.len()
            ==> regions.slot_owners[lo.slot_index_at(i)].inner_perms.in_list.value()
                == lo.list_id
    }
    &&& lo.list_id != 0
        ==> forall |idx: usize| {
            regions.slot_owners.contains_key(idx)
                && regions.slot_owners[idx].inner_perms.in_list.value() == lo.list_id
                ==> exists |i: int| 0 <= i < lo.list.len() && lo.slot_index_at(i) == idx
        }

}

The membership registry relating one (held or checked-out) list lo to the physical in_list tags in regions:

  • forward: every link’s region slot carries lo.list_id (the exec insert_before stamps it via store(lazy_get_id()));
  • reverse (only for a real, non-zero id): every region slot carrying that id is one of lo’s links — the global in_list-uniqueness the id allocator guarantees (a freshly minted id is system-wide unused; ids are never reused). Together they make in_list == list_id an exact membership test, which is exactly what crate::mm::frame::LinkedList::contains computes.