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

Function segment_from_unused_embedded

pub proof fn segment_from_unused_embedded(tracked 
    regions: &mut MetaRegionOwners,
    range: Range<Paddr>,
) -> res : Option<()>

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)
        ==> old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
            == REF_COUNT_UNUSED
},

forall |paddr: Paddr| {
    (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
        ==> old(regions).slots.contains_key(frame_to_index(paddr))
},

ensures

final(regions).inv(),

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

res is Some
    ==> forall |paddr: Paddr| {
        (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
            ==> {
                let idx = frame_to_index(paddr);
                let so = final(regions).slot_owners[idx];
                &&& so.usage == PageUsage::Frame
                &&& so.inner_perms.ref_count.value() == 1
                &&& so.paths_in_pt.is_empty()
                &&& so.inner_perms.in_list.value() == 0
                &&& so.inner_perms.storage.is_init()

            }
    },

res is Some
    ==> 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]
    },

res is None ==> *final(regions) == *old(regions),

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

Mirror of crate::mm::frame::Segment::from_unused for a contiguous range. On Some, every frame in range:

transitions from REF_COUNT_UNUSED to 1,
has usage set to Frame,
has raw_count bumped to 1 (the segment’s forgotten reference),
and its slot perm is re-parked in regions.slots (Design B).

None covers misalignment / out-of-bound / empty-range — same shape as the exec Result<_, GetFrameError> return.

Preconditions mirror the exec contract: every frame slot in range must currently be UNUSED (via paddr_range_not_in_use). In practice the embedding’s caller establishes this from structural_inv’s slot-perm coverage + accounting clause 1 (UNUSED ⟹ no users) once the range is known UNUSED.

segment_from_unused_embedded

Function segment_from_unused_embedded Copy item path

Function segment_from_unused_embedded