Skip to main content

unique_from_unused_embedded

ostd::specs::mm::embedding::unique

Function unique_from_unused_embedded 

Source 
pub proof fn unique_from_unused_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
Expand description
requires
old(regions).inv(),
has_safe_slot(paddr),
old(regions).slots.contains_key(frame_to_index(paddr)),
old(regions).slot_owners[frame_to_index(paddr)].usage is Unused,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
    == REF_COUNT_UNUSED,
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.usage == PageUsage::Frame
    &&& so_new.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
    &&& so_new.inner_perms.in_list.value() == 0
    &&& so_new.inner_perms.storage.is_init()
    &&& so_new.paths_in_pt == so_old.paths_in_pt
    &&& so_new.slot_vaddr == so_old.slot_vaddr

},
forall |i: usize| {
    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::from_unused. The slot at paddr transitions from a free slot (usage == Unused, rc == REF_COUNT_UNUSED) to an exclusively-held one (usage == Frame, rc == REF_COUNT_UNIQUE), with its metadata storage initialised, in_list == 0, and paths_in_pt preserved (it was empty — a free slot has no mappings). The slot perm is re-parked in regions.slots (Design B; the exec slots.tracked_insert at unique.rs:100), so the slots domain is preserved.

Preconditions mirror the exec contract (usage is Unused) plus the embedding-natural rc == REF_COUNT_UNUSED (which delivers, via [super::accounting_inv] clause 1, the “no users” facts needed to re-establish clause 0 at the freshly-UNIQUE slot).