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

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,
)

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,

old(tlb_model).inv(),

has_safe_slot(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: usize| (
    final(regions).slot_owners[i].inner_perms.in_list
        == old(regions).slot_owners[i].inner_perms.in_list
),

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

forall |i: usize| {
    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[frame_to_index(paddr)].inner_perms.ref_count.value()
    == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value(),

final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.len()
    == old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.len() + 1,

final(regions).slot_owners[frame_to_index(paddr)].usage
    == old(regions).slot_owners[frame_to_index(paddr)].usage,

final(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage
    == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage,

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

forall |i: usize| {
    i != frame_to_index(paddr)
        && 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))
},

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.

cursor_mut_map_embedded

Function cursor_mut_map_embedded Copy item path

Function cursor_mut_map_embedded