Function try_from_shared_embedded 

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

requires

old(regions).inv(),

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

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

old(regions).slot_owner(paddr).usage is Frame,

old(regions).slot_owner(paddr).paths_in_pt.is_empty(),

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() == REF_COUNT_UNIQUE
    &&& so_new.usage == so_old.usage
    &&& 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.slot_vaddr == so_old.slot_vaddr

},

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::UniqueFrame::try_from_shared’s success path (the CAS 1 → REF_COUNT_UNIQUE succeeded). The slot transitions from a sole-reference shared frame (rc == 1, usage == Frame, no PTE) to an exclusive UNIQUE one, with usage, paths_in_pt (empty), in_list (0), storage, vtable_ptr, and slot_vaddr preserved. (The failure path — rc != 1 — leaves regions untouched and is modeled in the step as a no-op.)