Function frame_drop_embedded 

pub proof fn frame_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)

requires

old(regions).inv(),

old(regions).contains(frame_to_index(paddr)),

old(regions).slot_owner(paddr).ref_count() > 0,

old(regions).slot_owner(paddr).ref_count() != REF_COUNT_UNUSED,

old(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX,

old(regions).slot_owner(paddr).ref_count() == 1
    ==> {
        &&& old(regions).slot_owner(paddr).storage_perm().is_init()
        &&& old(regions).slot_owner(paddr).in_list_perm.value() == 0
        &&& old(regions).slot_owner(paddr).paths_in_pt.is_empty()

    },

ensures

final(regions).inv(),

forall |i: int| {
    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_owner(paddr).slot_vaddr == old(regions).slot_owner(paddr).slot_vaddr,

final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,

final(regions).slot_owner(paddr).paths_in_pt
    == old(regions).slot_owner(paddr).paths_in_pt,

old(regions).slot_owner(paddr).ref_count() == 1
    ==> final(regions).slot_owner(paddr).paths_in_pt.is_empty(),

final(regions).slot_owner(paddr).in_list_perm
    == old(regions).slot_owner(paddr).in_list_perm,

old(regions).slot_owner(paddr).ref_count() == 1
    ==> final(regions).slot_owner(paddr).ref_count() == REF_COUNT_UNUSED,

old(regions).slot_owner(paddr).ref_count() > 1
    ==> final(regions).slot_owner(paddr).ref_count()
        == (old(regions).slot_owner(paddr).ref_count() - 1) as u64,

old(regions).slot_owner(paddr).ref_count() > 1
    ==> final(regions).slot_owner(paddr).storage_perm()
        == old(regions).slot_owner(paddr).storage_perm(),

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.)