Function segment_clone_embedded 

pub proof fn segment_clone_embedded(
    tracked regions: &mut MetaRegionOwners,
    range: Range<Paddr>,
)

requires

old(regions).inv(),

range.start % PAGE_SIZE == 0,

range.end % PAGE_SIZE == 0,

range.start < range.end,

range.end <= MAX_PADDR,

forall |paddr: Paddr| {
    (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
        ==> {
            let so = old(regions).slot_owner(paddr);
            &&& so.usage is Frame
            &&& so.ref_count() >= 1
            &&& so.ref_count() + 1 <= REF_COUNT_MAX

        }
},

ensures

final(regions).inv(),

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

forall |paddr: Paddr| {
    (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
        ==> {
            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() == (so_old.ref_count() + 1) as u64
            &&& 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 < max_meta_slots() && !(range.start <= index_to_frame(i) < range.end)
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},

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