Function segment_next_embedded 

pub proof fn segment_next_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)

requires

old(regions).inv(),

valid_frame_paddr(paddr),

old(regions).contains(frame_to_index(paddr)),

old(regions).slot_owner(paddr).ref_count() >= 1,

old(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX,

old(regions).slot_owner(paddr).usage is 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.ref_count_perm == so_old.ref_count_perm
    &&& so_new.usage == so_old.usage
    &&& so_new.slot_vaddr == so_old.slot_vaddr
    &&& so_new.paths_in_pt == so_old.paths_in_pt
    &&& so_new.in_list_perm == so_old.in_list_perm
    &&& so_new.storage_perm() == so_old.storage_perm()
    &&& so_new.vtable_ptr_perm() == so_old.vtable_ptr_perm()

},

forall |i: int| {
    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.