Skip to main content

frame_drop_embedded

ostd::specs::mm::embedding::frame

Function frame_drop_embedded 

Source 
pub proof fn frame_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
Expand description
requires
old(regions).inv(),
old(regions).slots.contains_key(frame_to_index(paddr)),
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() > 0,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
    != REF_COUNT_UNUSED,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
    <= REF_COUNT_MAX,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1
    ==> {
        &&& old(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage.is_init()
        &&& old(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list.value()
            == 0
        &&& old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty()

    },
ensures
final(regions).inv(),
forall |i: usize| {
    i != frame_to_index(paddr)
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},
final(regions).slots =~= old(regions).slots,
final(regions).slot_owners.dom() =~= old(regions).slot_owners.dom(),
final(regions).slot_owners[frame_to_index(paddr)].self_addr
    == old(regions).slot_owners[frame_to_index(paddr)].self_addr,
final(regions).slot_owners[frame_to_index(paddr)].usage
    == old(regions).slot_owners[frame_to_index(paddr)].usage,
final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt
    == old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1
    ==> final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
final(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list
    == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1
    ==> final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
        == REF_COUNT_UNUSED,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() > 1
    ==> final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
        == (old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
            - 1) as u64,
old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() > 1
    ==> final(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage
        == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage,
forall |c: CursorOwner<'_, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::frame::Frame’s Drop::drop — the single real drop, whose (now strengthened) drop_requires / drop_ensures it reflects verbatim. One axiom; the refcount transition is a single postcondition that covers both behaviors the exec drop performs:

  • old.ref_count == 1: last-ref teardown — slot → REF_COUNT_UNUSED.
  • old.ref_count > 1: refcount decremented by one (slot stays SHARED).

requires mirrors Frame::drop_requires (the expressible parts) verbatim — no extra conjunct.

The metaregion_sound-preserves clause below is sound because of the refcount semantics, not because of any caller obligation: a page-table mapping is itself a reference (reference_count() counts “all the mappings in the page table that point to the frame”). So ref_count == 1 already implies no cursor’s OwnerSubtree maps the slot — were it mapped, that mapping would push ref_count >= 2. Hence the ref_count == 1 UNUSED transition cannot break any cursor’s EntryOwner::metaregion_sound, and ref_count > 1 keeps the slot SHARED. (Not provable from drop_ensures alone, but sound to assert here — same epistemic status as the other _embedded axioms reflecting real exec behavior.)