Module frame 

Embedding of Frame lifecycle operations: allocate (from_unused), acquire-by-paddr (from_in_use), and drop.

A frame “handle” in the embedding is just a paddr-bearing super::FrameEntry in super::VmStore::frames. The proof-side ownership is in regions.slot_owners[frame_to_index(paddr)] (refcount + perms), which the embedded axioms mutate per the corresponding _spec helpers in crate::specs::mm::frame::meta_specs.

Methods modeled

• Frame::from_unused: allocate a fresh handle on a previously-unused slot.
• Frame::from_in_use: acquire a new handle on an already-in-use slot (refcount++).
• Frame drop (via crate::mm::frame::Frame’s TrackDrop impl): release one handle (refcount–).

Model gaps

• Generic M: AnyFrameMeta: Frame::from_unused takes a metadata: M parameter and threads it through PointsTo<MetaSlot, Metadata<M>>. We don’t model the metadata type — get_from_unused_spec itself ignores M and just commits to usage == PageUsage::Frame.
• Drop-last-in-place teardown: when ref_count == 1, dropping the handle invokes the metadata destructor (which may require storage.is_init, in_list.value() == 0). We model this by carrying the relevant precondition into the drop axiom but leaving the post-state uncommitted on those fields.

Functions

drop_pre

frame_drop_embedded

frame_from_in_use_embedded

frame_from_unused_embedded