Skip to main content

vm_space_new_embedded

ostd::specs::mm::vm_space_embedding

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(),

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

Real exec ensures: regions.inv() is preserved; new owner satisfies its invariant. Stage 1 axiomatizes only this; later stages may strengthen to capture the new owner’s page_table_owner content.