Skip to main content

vm_space_cursor_mut_embedded

ostd::specs::mm::embedding::cursor

Function vm_space_cursor_mut_embedded 

Source 
pub proof fn vm_space_cursor_mut_embedded<'a, 'rcu>(tracked 
    vm_space: &VmSpaceOwner,
tracked     regions: &mut MetaRegionOwners,
    va: Range<Vaddr>,
) -> tracked res : Option<(CursorOwner<'rcu, UserPtConfig>, Guards<'rcu>)>
Expand description
requires
vm_space.inv(),
old(regions).inv(),
ensures
final(regions).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<'rcu, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},
res matches Some(
    (c, g),
) ==> {
    &&& c.inv()
    &&& c.children_not_locked(g)
    &&& c.nodes_locked(g)
    &&& !c.popped_too_high
    &&& c.metaregion_sound(*final(regions))

},

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