Skip to main content

cursor_mut_protect_next_embedded

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

Function cursor_mut_protect_next_embedded 

Source 
pub proof fn cursor_mut_protect_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::CursorMut::protect_next.

Exec requires (line 1443-1450):

  • invariants(owner, regions, guards)
  • forall |p: PageProperty| op.requires((p,)) — MODEL GAP (closure).
  • The trackedness-preservation closure constraint — MODEL GAP.

Does NOT require in_locked_range() directly.