Skip to main content

unique_drop_embedded

ostd::specs::mm::embedding::unique

Function unique_drop_embedded 

Source 
pub proof fn unique_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
Expand description
requires
old(regions).inv(),
old(regions).slots.contains_key(frame_to_index(paddr)),
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
    == REF_COUNT_UNIQUE,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list.value() == 0,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage.is_init(),
old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
ensures
final(regions).inv(),
final(regions).slots =~= old(regions).slots,
{
    let idx = frame_to_index(paddr);
    let so_old = old(regions).slot_owners[idx];
    let so_new = final(regions).slot_owners[idx];
    &&& so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
    &&& so_new.usage == so_old.usage
    &&& so_new.paths_in_pt == so_old.paths_in_pt
    &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
    &&& so_new.slot_vaddr == so_old.slot_vaddr

},
forall |i: usize| {
    i != frame_to_index(paddr)
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},
forall |c: CursorOwner<'_, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::frame::UniqueFrame’s drop. The sole exclusive handle is released: the slot transitions rc == REF_COUNT_UNIQUE → rc == REF_COUNT_UNUSED (last-ref teardown via drop_last_in_place, uninitialising storage), with usage, paths_in_pt (empty), in_list (0), and slot_vaddr preserved.

Preconditions mirror UniqueFrame::wf_with_region (the parts expressible at the regions level): the slot is UNIQUE with in_list == 0, initialised storage, and no PTE mappings (paths_in_pt.is_empty()).