Skip to main content

segment_clone_embedded

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

Function segment_clone_embedded 

Source 
pub proof fn segment_clone_embedded(tracked 
    regions: &mut MetaRegionOwners,
    range: Range<Paddr>,
)
Expand description
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_owners[frame_to_index(paddr)];
            &&& so.usage == PageUsage::Frame
            &&& so.inner_perms.ref_count.value() >= 1
            &&& so.inner_perms.ref_count.value() + 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.inner_perms.ref_count.value()
                == (so_old.inner_perms.ref_count.value() + 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.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 < crate::specs::mm::frame::mapping::max_meta_slots()
        && !(range.start <= crate::specs::mm::frame::mapping::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))
},