Function list_drop_embedded 

pub proof fn list_drop_embedded<M: AnyFrameMeta + Repr<MetaSlotSmall>>(
    tracked regions: &mut MetaRegionOwners,
    tracked owner: LinkedListOwner<M>,
)

requires

old(regions).inv(),

owner.inv(),

owner.relate_region(*old(regions)),

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

forall |i: int| {
    0 <= i < owner.list.len()
        ==> old(regions)
            .slot_owners[meta_to_index(owner.list[i].paddr)]
            .paths_in_pt
            .is_empty()
},

ensures

final(regions).inv(),

final(regions).slots.dom() =~= old(regions).slots.dom(),

owner.list.len() == 0 ==> *final(regions) == *old(regions),

forall |i: int| {
    0 <= i < owner.list.len()
        ==> {
            let idx = meta_to_index(owner.list[i].paddr);
            &&& final(regions).slot_owners[idx].ref_count() == REF_COUNT_UNUSED
            &&& final(regions).slot_owners[idx].in_list_perm.value() == 0

        }
},

forall |idx: int| {
    (forall |i: int| {
        0 <= i < owner.list.len()
            ==> idx != #[trigger] meta_to_index(owner.list[i].paddr)
    })
        ==> final(regions).slot_owners[idx] == old(regions).slot_owners[idx]
            && final(regions).slots[idx] == old(regions).slots[idx]
            && final(regions).frame_obligations.count(idx)
                == old(regions).frame_obligations.count(idx)
},

forall |l: LinkedListOwner<M>| {
    l.inv() && l.relate_region(*old(regions)) && l.list_id != owner.list_id
        ==> l.relate_region(*final(regions))
},

forall |l: LinkedListOwner<M>| {
    l.inv() && l.relate_region(*old(regions)) && list_registry_ok(*old(regions), l)
        && l.list_id != owner.list_id ==> list_registry_ok(*final(regions), l)
},

forall |fo: UniqueFrameOwner<Link<M>>| {
    fo.global_inv(*old(regions)) && fo.frame_link_inv(*old(regions))
        && old(regions).slot_owners[fo.slot_index].in_list_perm.value() == 0
        ==> fo.global_inv(*final(regions)) && fo.frame_link_inv(*final(regions))
            && final(regions).slot_owners[fo.slot_index].in_list_perm.value() == 0
},

Trusted reflection of the crate::mm::frame::LinkedList’s Drop/TrackDrop.