Skip to main content

vm_space_cursor_embedded

ostd::specs::mm::vm_space_embedding

Function vm_space_cursor_embedded 

Source 
pub proof fn vm_space_cursor_embedded<'a, 'rcu>(tracked 
    vm_space: &VmSpaceOwner,
    va: Range<Vaddr>,
) -> tracked res : Option<CursorOwner<'rcu, UserPtConfig>>
Expand description
requires
vm_space.inv(),
ensures
res matches Some(c) ==> c.inv(),

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

Real exec ensures (paraphrased from vm_space.rs:201-209): when cursor_new_success_conditions(va) holds, the call returns Ok(Cursor) with a tracked Some(CursorOwner) whose inv() holds. Stage 2 axiomatizes a coarser model: returns Some (with inv()) or None, with no precondition relating to the success conditions. This over-approximates the success case (the embedding allows opens that would fail in exec); it never under-approximates, which is what matters for soundness of inductive invariant preservation.