Skip to main content

cursor_jump_embedded

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

Function cursor_jump_embedded 

Source 
pub proof fn cursor_jump_embedded<'rcu>(tracked 
    owner: &mut CursorOwner<'rcu, UserPtConfig>,
tracked     regions: &mut MetaRegionOwners,
tracked     guards: &mut Guards<'rcu>,
    va: Vaddr,
)
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::jump / crate::mm::vm_space::CursorMut::jump.

Exec requires invariants(owner, regions, guards) (which includes !owner.popped_too_high). It does not require owner.in_locked_range(): the exec requires was relaxed. A drifted cursor that cannot be repositioned within the target node aborts the program (a sound panic_diverge, mirroring the real pop_level unwrap panic), so an out-of-range cursor is a safety non-issue — in_locked_range now only governs the success postcondition, and this axiom soundly models the returning path.