Function cursor_mut_map_embedded 

pub proof fn cursor_mut_map_embedded<'rcu>(
    tracked owner: &mut CursorOwner<'rcu, UserPtConfig>,
    tracked regions: &mut MetaRegionOwners,
    tracked guards: &mut Guards<'rcu>,
    tracked tlb_model: &mut TlbModel,
    paddr: Paddr,
    prop: PageProperty,
)

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,

old(tlb_model).inv(),

valid_frame_paddr(paddr),

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(tlb_model).inv(),

final(regions).slots == old(regions).slots,

forall |i: int| (
    final(regions).slot_owners[i].in_list_perm
        == old(regions).slot_owners[i].in_list_perm
),

forall |i: int| {
    i != frame_to_index(paddr)
        && old(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},

forall |i: int| {
    old(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
        ==> final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
},

final(regions).slot_owner(paddr).ref_count()
    == old(regions).slot_owner(paddr).ref_count(),

final(regions).slot_owner(paddr).paths_in_pt.len()
    == old(regions).slot_owner(paddr).paths_in_pt.len() + 1,

final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,

final(regions).slot_owner(paddr).storage_perm()
    == old(regions).slot_owner(paddr).storage_perm(),

forall |i: int| (
    final(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
),

forall |i: int| {
    i != frame_to_index(paddr)
        && old(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
        && final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
        ==> final(regions).slot_owners[i].usage !is Frame
},

forall |c: CursorOwner<'rcu, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::vm_space::CursorMut::map.

Exec requires:

• tlb_model.inv()
• invariants(cursor_owner, regions, guards) (incl. !popped_too_high)
• item_wf(frame, prop, entry_owner, regions) — MODEL GAP.

Does not require in_locked_range(): an out-of-range cursor panics at map’s assert!(va < barrier_va.end) (the real map_panic_conditions out-of-range abort); the exec re-derives in_locked_range from that panic + the cursor invariant. This axiom soundly models the returning path.