Skip to main content

list_drop_embedded

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

Function list_drop_embedded 

Source 
pub proof fn list_drop_embedded<M: AnyFrameMeta + Repr<MetaSlotSmall>>(tracked 
    regions: &mut MetaRegionOwners,
tracked     owner: LinkedListOwner<M>,
)
Expand description
requires
old(regions).inv(),
owner.inv(),
owner.relate_region(*old(regions)),
forall |i: int| {
    0 <= i < owner.list.len()
        ==> old(regions).frame_obligations.count(owner.slot_index_at(i)) == 0
},
forall |i: int| {
    0 <= i < owner.list.len()
        ==> old(regions).slot_owners[owner.slot_index_at(i)].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 = owner.slot_index_at(i);
            &&& final(regions).slot_owners[idx].inner_perms.ref_count.value()
                == REF_COUNT_UNUSED
            &&& final(regions).slot_owners[idx].inner_perms.in_list.value() == 0

        }
},
forall |idx: usize| {
    (forall |i: int| 0 <= i < owner.list.len() ==> idx != owner.slot_index_at(i))
        ==> 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].inner_perms.in_list.value() == 0
        ==> fo.global_inv(*final(regions)) && fo.frame_link_inv(*final(regions))
            && final(regions).slot_owners[fo.slot_index].inner_perms.in_list.value() == 0
},

Trusted reflection of the (now-strengthened, verified) whole-list teardown crate::mm::frame::LinkedList’s Drop/TrackDrop. The destructor pops every link via take_current and UniqueFrame::drops the recovered frame, so each former link’s slot is freed — rc → REF_COUNT_UNUSED, in_list → 0 — not orphaned. owner is consumed (emptied). The per-link frame_obligations.count == 0 precondition mirrors the exec drop_requires (a listed frame was forgotten via into_raw); ListStore doesn’t track that accounting fact, so it is surfaced here for an accounting-aware caller to supply.

ensures mirror the verified drop_ensures (freed slots + full preservation of every out-of-list slot, slots.dom(), inv()) plus the sound companion frames (cf. the push/pop axioms): other lists / cursors keep relate_region + list_registry_ok, other loose frames are untouched, and — when the list was empty — the region is unchanged outright.