Skip to main content

vm_space_new_embedded

ostd::specs::mm::embedding::vm_space

Function vm_space_new_embedded 

Source 
pub proof fn vm_space_new_embedded<'a>(tracked regions: &mut MetaRegionOwners) -> tracked res : VmSpaceOwner
Expand description
requires
old(regions).inv(),
ensures
final(regions).inv(),
res.inv(),
final(regions).slots =~= old(regions).slots,
forall |i: usize| (
    final(regions).slot_owners[i].inner_perms.in_list
        == old(regions).slot_owners[i].inner_perms.in_list
),
forall |i: usize| (
    final(regions).slot_owners[i] != old(regions).slot_owners[i]
        ==> {
            &&& old(regions).slot_owners[i].inner_perms.ref_count.value()
                == REF_COUNT_UNUSED
            &&& final(regions).slot_owners[i].inner_perms.ref_count.value()
                != REF_COUNT_UNUSED
            &&& final(regions).slot_owners[i].usage != PageUsage::Frame

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

Mirror of crate::mm::vm_space::VmSpace::new.

metaregion_sound_preserves: any CursorOwner sound w.r.t. the old regions is still sound w.r.t. the new regions. Mirrors the underlying create_user_page_table regions-preservation property.