Skip to main content

frame_from_in_use_embedded

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

Function frame_from_in_use_embedded 

Source 
pub proof fn frame_from_in_use_embedded(tracked 
    regions: &mut MetaRegionOwners,
    paddr: Paddr,
) -> tracked res : Option<()>
Expand description
requires
old(regions).inv(),
has_safe_slot(paddr) ==> old(regions).slots.contains_key(frame_to_index(paddr)),
ensures
final(regions).inv(),
!has_safe_slot(paddr) ==> res is None,
res is Some ==> MetaSlot::get_from_in_use_success(paddr, *old(regions), *final(regions)),
res is None ==> *final(regions) == *old(regions),
res is Some
    ==> {
        let so = final(regions).slot_owners[frame_to_index(paddr)];
        &&& so.inner_perms.ref_count.value() != REF_COUNT_UNUSED
        &&& so.inner_perms.ref_count.value() != REF_COUNT_UNIQUE
        &&& so.inner_perms.storage.is_init()
        &&& so.usage == PageUsage::Frame

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

Mirror of crate::mm::frame::Frame::from_in_use. On Some, inner_perms.ref_count increments by 1 at frame_to_index(paddr) and all other slots are preserved.