Skip to main content

segment_drop_embedded

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

Function segment_drop_embedded 

Source 
pub proof fn segment_drop_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.inner_perms.ref_count.value() >= 1
            &&& so.inner_perms.ref_count.value()
                <= crate::specs::mm::frame::meta_owners::REF_COUNT_MAX
            &&& so.usage == PageUsage::Frame
            &&& so.inner_perms.ref_count.value() == 1 ==> so.paths_in_pt.is_empty()

        }
},
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.usage == so_old.usage
            &&& so_new.paths_in_pt == so_old.paths_in_pt
            &&& so_new.self_addr == so_old.self_addr
            &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
            &&& so_old.inner_perms.ref_count.value() == 1
                ==> so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
            &&& so_old.inner_perms.ref_count.value() > 1
                ==> so_new.inner_perms.ref_count.value()
                    == (so_old.inner_perms.ref_count.value() - 1) as u64

        }
},
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))
},

Mirror of crate::mm::frame::Segment’s drop loop. Releases the segment’s forgotten reference at every frame in range: each frame’s rc and raw_count decrement by 1; if rc reaches 0, the slot transitions to UNUSED.

Preconditions: the segment relates to regions (each covered slot has raw_count == 1 from THIS segment’s contribution and rc >= 1). When the segment is the sole reference at a frame (rc == 1), the drop tears down that slot.

In the embedding, the per-segment raw_count == 1 form is generalized to raw_count == segment_cover_count, so after drop each covered slot’s raw_count is pre_cover_count - 1. This axiom asserts the slot-level decrement; the embedding’s [super::structural_inv] re-chains via segment removal.