ostd/mm/frame/
obligation_demo.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Demonstration of the linear-drop obligation mechanism.
3//!
4//! Concrete workbench showing what verification looks like when a
5//! must-drop resource is honored vs. silently leaked. `clean_inv()` is the
6//! boundary that breaks on leaks.
7//!
8//! After the per-frame migration there is a single must-drop ledger: the
9//! per-instance `frame_obligations` multiset. Both `Frame<M>` and `Segment<M>`
10//! use it.
11//!
12//! - `Frame<M>`: `ManuallyDrop::new(frame, ..)` mints one entry at
13//!   `frame.key()` (paired with the recovery path); `Frame::drop` /
14//!   `ManuallyDrop::new` redeem one.
15//! - `Segment<M>`: records one entry per frame it holds (minted by
16//!   [`crate::specs::mm::frame::segment::tracked_mint_seg_obligations`],
17//!   drained on `Segment::drop`).
18//!
19//! Leaking either leaves `frame_obligations` non-empty, breaking the
20//! `frame_obligations.len() == 0` conjunct of `clean_inv`.
21//!
22//! # How to use
23//!
24//! - As-shipped, [`demo_honored`] verifies.
25//! - To see the leak case rejected, flip the `demo_leak` cfg gate on
26//!   [`demo_leaked_when_enabled`] and re-run
27//!   `cargo dv verify --targets ostd`. The expected error is documented in
28//!   the comments above that function.
29use vstd::prelude::*;
30
31use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
32
33verus! {
34
35/// Honored: the obligation is minted on the per-frame ledger, then redeemed
36/// before the function returns. Verifies cleanly.
37#[verus_spec(
38    with Tracked(regions): Tracked<&mut MetaRegionOwners>
39    requires
40        old(regions).clean_inv(),
41    ensures
42        final(regions).clean_inv(),
43)]
44pub fn demo_honored(slot_idx: usize) {
45    proof {
46        let tracked obl = regions.tracked_mint_frame_obligation(slot_idx);
47        // ... here a real caller would construct a Frame/Segment, hand it
48        // around, etc. — for the demo we just immediately redeem.
49        regions.tracked_redeem_frame_obligation(obl);
50    }
51}
52
53// =============================================================================
54// LEAK DEMO
55// =============================================================================
56//
57// Body intentionally omits the `redeem` call. Gated behind the `demo_leak`
58// cfg flag so the default build verifies — flip it on to reproduce the
59// failure. The function promises `final(regions).clean_inv()` but the minted
60// obligation never leaves `frame_obligations`, so the
61// `frame_obligations.len() == 0` conjunct of `clean_inv` is unsatisfiable at
62// function exit.
63//
64// Reproduce:
65//
66//     cargo dv verify --targets ostd \
67//         -- --rustc-extra-args='--cfg demo_leak'
68//
69// or temporarily remove the `#[cfg(demo_leak)]` attribute below.
70//
71// Adding `regions.tracked_redeem_frame_obligation(obl)` at the end of the
72// body (rebinding `_obl` → `obl`) makes verification succeed.
73#[cfg(demo_leak)]
74#[verus_spec(
75    with Tracked(regions): Tracked<&mut MetaRegionOwners>
76    requires
77        old(regions).clean_inv(),
78    ensures
79        final(regions).clean_inv(),
80)]
81pub fn demo_leaked_when_enabled(slot_idx: usize) {
82    proof {
83        // Mint a per-frame obligation — analog of `ManuallyDrop::new(frame, ..)`
84        // or a single segment frame. No matching `Drop::drop` /
85        // `ManuallyDrop::new` follows, so the multiset entry persists and
86        // `clean_inv` fails on `frame_obligations.len() == 0` at function exit.
87        let tracked _obl = regions.tracked_mint_frame_obligation(slot_idx);
88    }
89}
90
91} // verus!
ostd/mm/frame/obligation_demo.rs

ostd/mm/frame/
obligation_demo.rs
