Skip to main content

ostd/specs/mm/frame/
frame_lifecycle.rs

1// The lemma `Frame::lemma_from_raw_manuallydrop_general` previously lived
2// here. It bridged `Frame::from_raw`'s post-state (which cleared
3// `raw_count` to 0) to a subsequent `ManuallyDrop::new` (which bumped
4// `raw_count` back to 1). Under the borrow-protocol redesign,
5// `Frame::from_raw` mints the obligation directly and `ManuallyDrop::new`
6// consumes it — no intermediate bookkeeping debt to discharge.