Skip to main content

cursor_find_next_embedded

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

Function cursor_find_next_embedded 

Source 
pub proof fn cursor_find_next_embedded<'rcu>(tracked 
    owner: &mut CursorOwner<'rcu, UserPtConfig>,
tracked     regions: &mut MetaRegionOwners,
tracked     guards: &mut Guards<'rcu>,
    len: usize,
)
Expand description
requires
old(owner).inv(),
old(regions).inv(),
old(owner).children_not_locked(*old(guards)),
old(owner).nodes_locked(*old(guards)),
old(owner).metaregion_sound(*old(regions)),
!old(owner).popped_too_high,
ensures
final(owner).inv(),
final(regions).inv(),
final(owner).children_not_locked(*final(guards)),
final(owner).nodes_locked(*final(guards)),
final(owner).metaregion_sound(*final(regions)),
!final(owner).popped_too_high,
final(regions).slots =~= old(regions).slots,
forall |i: usize| final(regions).slot_owners[i] == old(regions).slot_owners[i],
forall |c: CursorOwner<'rcu, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::vm_space::Cursor::find_next / crate::mm::vm_space::CursorMut::find_next.

Exec requires invariants(owner, regions, guards). Does NOT require in_locked_range() (the method itself navigates from wherever the cursor sits).