Module obligation_demo 

Demonstration of the linear-drop obligation mechanism.

Concrete workbench showing what verification looks like when a must-drop resource is honored vs. silently leaked. clean_inv() is the boundary that breaks on leaks.

After the per-frame migration there is a single must-drop ledger: the per-instance frame_obligations multiset. Both Frame<M> and Segment<M> use it.

• Frame<M>: ManuallyDrop::new(frame, ..) mints one entry at frame.key() (paired with the recovery path); Frame::drop / ManuallyDrop::new redeem one.
• Segment<M>: records one entry per frame it holds (minted by crate::specs::mm::frame::segment::tracked_mint_seg_obligations, drained on Segment::drop).

Leaking either leaves frame_obligations non-empty, breaking the frame_obligations.len() == 0 conjunct of clean_inv.

How to use

• As-shipped, demo_honored verifies.
• To see the leak case rejected, flip the demo_leak cfg gate on [demo_leaked_when_enabled] and re-run cargo dv verify --targets ostd. The expected error is documented in the comments above that function.

Functions

demo_honored