Function list_registry_ok 

pub open spec fn list_registry_ok<M: AnyFrameMeta + Repr<MetaSlotSmall>>(
    regions: MetaRegionOwners,
    lo: LinkedListOwner<M>,
) -> bool

{
    &&& forall |i: int| {
        0 <= i < lo.list.len()
            ==> regions.slot_owners[meta_to_index(lo.list[i].paddr)].in_list_perm.value()
                == lo.list_id
    }
    &&& lo.list_id != 0
        ==> forall |idx: int| {
            regions.contains(idx)
                && regions.slot_owners[idx].in_list_perm.value() == lo.list_id
                ==> exists |i: int| {
                    0 <= i < lo.list.len()
                        && #[trigger] meta_to_index(lo.list[i].paddr) == 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.