Function frame_from_unused_embedded 

pub proof fn frame_from_unused_embedded(
    tracked regions: &mut MetaRegionOwners,
    paddr: Paddr,
) -> tracked res : Option<()>

requires

old(regions).inv(),

valid_frame_paddr(paddr) ==> old(regions).contains(frame_to_index(paddr)),

ensures

final(regions).inv(),

!valid_frame_paddr(paddr) ==> res is None,

res is Some
    ==> MetaSlot::get_from_unused_spec(paddr, false, *old(regions), *final(regions)),

res is Some ==> MetaSlot::slot_perm_reparked_spec(paddr, *old(regions), *final(regions)),

res is None ==> *final(regions) == *old(regions),

forall |c: CursorOwner<'_, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::frame::Frame::from_unused