Skip to main content

frame_drop_embedded

ostd::specs::mm::embedding::frame

Function frame_drop_embedded 

Source 
pub proof fn frame_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
Expand description
requires
old(regions).inv(),
old(regions).contains(frame_to_index(paddr)),
old(regions).slot_owner(paddr).ref_count() > 0,
old(regions).slot_owner(paddr).ref_count() != REF_COUNT_UNUSED,
old(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX,
old(regions).slot_owner(paddr).ref_count() == 1
    ==> {
        &&& old(regions).slot_owner(paddr).storage_perm().is_init()
        &&& old(regions).slot_owner(paddr).in_list_perm.value() == 0
        &&& old(regions).slot_owner(paddr).paths_in_pt.is_empty()

    },
ensures
final(regions).inv(),
forall |i: int| {
    i != frame_to_index(paddr)
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},
final(regions).slots == old(regions).slots,
final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
final(regions).slot_owner(paddr).slot_vaddr == old(regions).slot_owner(paddr).slot_vaddr,
final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
final(regions).slot_owner(paddr).paths_in_pt
    == old(regions).slot_owner(paddr).paths_in_pt,
old(regions).slot_owner(paddr).ref_count() == 1
    ==> final(regions).slot_owner(paddr).paths_in_pt.is_empty(),
final(regions).slot_owner(paddr).in_list_perm
    == old(regions).slot_owner(paddr).in_list_perm,
old(regions).slot_owner(paddr).ref_count() == 1
    ==> final(regions).slot_owner(paddr).ref_count() == REF_COUNT_UNUSED,
old(regions).slot_owner(paddr).ref_count() > 1
    ==> final(regions).slot_owner(paddr).ref_count()
        == (old(regions).slot_owner(paddr).ref_count() - 1) as u64,
old(regions).slot_owner(paddr).ref_count() > 1
    ==> final(regions).slot_owner(paddr).storage_perm()
        == old(regions).slot_owner(paddr).storage_perm(),
forall |c: CursorOwner<'_, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::frame::Frame’s Drop::drop.