Skip to main content

segment_next_embedded

ostd::specs::mm::embedding::segment

Function segment_next_embedded 

Source 
pub proof fn segment_next_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
Expand description
requires
old(regions).inv(),
paddr % PAGE_SIZE == 0,
paddr < MAX_PADDR,
old(regions).slots.contains_key(frame_to_index(paddr)),
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() >= 1,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
    <= crate::specs::mm::frame::meta_owners::REF_COUNT_MAX,
old(regions).slot_owners[frame_to_index(paddr)].usage == PageUsage::Frame,
ensures
final(regions).inv(),
final(regions).slots =~= old(regions).slots,
{
    let idx = frame_to_index(paddr);
    let so_old = old(regions).slot_owners[idx];
    let so_new = final(regions).slot_owners[idx];
    &&& so_new.inner_perms.ref_count == so_old.inner_perms.ref_count
    &&& so_new.usage == so_old.usage
    &&& so_new.self_addr == so_old.self_addr
    &&& so_new.paths_in_pt == so_old.paths_in_pt
    &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
    &&& so_new.inner_perms.storage == so_old.inner_perms.storage
    &&& so_new.inner_perms.vtable_ptr == so_old.inner_perms.vtable_ptr

},
forall |i: usize| {
    i != frame_to_index(paddr)
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},
forall |c: CursorOwner<'_, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::frame::Segment::next’s “pop one frame” effect. At the popped paddr (= range.start pre):

  • raw_count -= 1 (the segment’s forgotten reference at this frame is consumed by Frame::from_raw).
  • ref_count UNCHANGED (the rc contribution “transfers” from the segment’s forgotten reference to the newly-restored Frame<M> handle that the caller now owns).
  • all other slot fields (usage, paths_in_pt, storage, …) preserved.

Slots outside the popped paddr are fully preserved.

Preconditions mirror exec next: the segment has at least one frame in its range; the popped frame’s slot is currently forgotten (raw_count >= 1) with a live SHARED rc.