ostd/specs/mm/frame/
frame_lifecycle.rs

1use vstd::prelude::*;
2
3use crate::mm::frame::meta::AnyFrameMeta;
4use crate::mm::frame::meta::mapping::frame_to_index;
5use crate::mm::frame::Frame;
6use crate::mm::Paddr;
7use crate::specs::mm::frame::frame_specs::*;
8use crate::specs::mm::frame::meta_owners::MetaSlotOwner;
9use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
10
11use vstd_extra::drop_tracking::*;
12use vstd_extra::ownership::*;
13
14verus! {
15
16#[verus_verify]
17impl<'a, M: AnyFrameMeta> Frame<M> {
18
19    /// Original lemma: when `raw_count == 1` before `from_raw`, the
20    /// `from_raw` + `ManuallyDrop::new` pair is a no-op on `regions`.
21    pub proof fn lemma_from_raw_manuallydrop_inverse(
22        raw: Paddr,
23        frame: Self,
24        regions0: MetaRegionOwners,
25        regions1: MetaRegionOwners
26    )
27        requires
28            Self::from_raw_requires(regions0, raw),
29            Self::from_raw_ensures(regions0, regions1, raw, frame),
30            <Self as TrackDrop>::constructor_requires(frame, regions1),
31
32        ensures
33            forall |regions2: MetaRegionOwners|
34                <Self as TrackDrop>::constructor_ensures(frame, regions1, regions2) ==>
35                regions2 == regions0
36    {
37        admit()
38    }
39
40    /// Generalized lemma: for any starting `raw_count <= 1`, the
41    /// `from_raw` + `ManuallyDrop::new` pair leaves `raw_count == 1`
42    /// and preserves all other slot fields.  Consumes the `BorrowDebt`
43    /// issued by `from_raw`.
44    pub proof fn lemma_from_raw_manuallydrop_general(
45        raw: Paddr,
46        frame: Self,
47        regions0: MetaRegionOwners,
48        regions1: MetaRegionOwners,
49        tracked debt: BorrowDebt,
50    )
51        requires
52            Self::from_raw_requires_safety(regions0, raw),
53            regions0.slot_owners[frame_to_index(raw)].raw_count <= 1,
54            Self::from_raw_ensures(regions0, regions1, raw, frame),
55            <Self as TrackDrop>::constructor_requires(frame, regions1),
56            debt.frame_index == frame_to_index(raw),
57            debt.raw_count_at_issue == regions0.slot_owners[frame_to_index(raw)].raw_count,
58
59        ensures
60            forall |regions2: MetaRegionOwners|
61                #![trigger regions2.slot_owners[frame_to_index(raw)]]
62                <Self as TrackDrop>::constructor_ensures(frame, regions1, regions2) ==> {
63                    // raw_count is always 1 after from_raw (→0) + ManuallyDrop::new (→1)
64                    &&& regions2.slot_owners[frame_to_index(raw)].raw_count == 1
65                    // All other fields of this slot are preserved from regions0
66                    &&& regions2.slot_owners[frame_to_index(raw)].inner_perms
67                        == regions0.slot_owners[frame_to_index(raw)].inner_perms
68                    &&& regions2.slot_owners[frame_to_index(raw)].self_addr
69                        == regions0.slot_owners[frame_to_index(raw)].self_addr
70                    &&& regions2.slot_owners[frame_to_index(raw)].usage
71                        == regions0.slot_owners[frame_to_index(raw)].usage
72                    &&& regions2.slot_owners[frame_to_index(raw)].path_if_in_pt
73                        == regions0.slot_owners[frame_to_index(raw)].path_if_in_pt
74                    // Other slots are unchanged
75                    &&& forall |i: usize|
76                        #![trigger regions2.slot_owners[i]]
77                        i != frame_to_index(raw) ==> regions2.slot_owners[i]
78                            == regions0.slot_owners[i]
79                    &&& regions2.slot_owners.dom() =~= regions0.slot_owners.dom()
80                    &&& regions2.slots =~= regions1.slots
81                    &&& regions2.inv()
82                }
83    {
84        admit()
85    }
86
87}
88
89}
ostd/specs/mm/frame/frame_lifecycle.rs

ostd/specs/mm/frame/
frame_lifecycle.rs
