ostd/specs/mm/frame/
frame_lifecycle.rs

1use vstd::prelude::*;
2
3use crate::mm::frame::meta::AnyFrameMeta;
4use crate::mm::frame::Frame;
5use crate::mm::Paddr;
6use crate::specs::mm::frame::frame_specs::*;
7use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
8
9use vstd_extra::drop_tracking::*;
10
11verus! {
12
13#[verus_verify]
14impl<'a, M: AnyFrameMeta> Frame<M> {
15
16    pub proof fn lemma_from_raw_manuallydrop_inverse(
17        raw: Paddr,
18        frame: Self,
19        regions0: MetaRegionOwners,
20        regions1: MetaRegionOwners
21    )
22        requires
23            Self::from_raw_requires(regions0, raw),
24            Self::from_raw_ensures(regions0, regions1, raw, frame),
25            <Self as TrackDrop>::constructor_requires(frame, regions1),
26
27        ensures
28            forall |regions2: MetaRegionOwners|
29                <Self as TrackDrop>::constructor_ensures(frame, regions1, regions2) ==>
30                regions2 == regions0
31    {
32        admit()
33    }
34
35}
36
37}