ostd/specs/mm/frame/
frame_lifecycle.rs

1use vstd::prelude::*;
2
3use crate::mm::frame::meta::mapping::frame_to_index;
4use crate::mm::frame::meta::AnyFrameMeta;
5use crate::mm::frame::Frame;
6use crate::mm::Paddr;
7use crate::specs::mm::frame::frame_specs::*;
8use crate::specs::mm::frame::mapping::group_page_meta;
9use crate::specs::mm::frame::meta_owners::{MetaSlotOwner, REF_COUNT_UNUSED};
10use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
11
12use vstd_extra::drop_tracking::*;
13use vstd_extra::ownership::*;
14
15verus! {
16
17#[verus_verify]
18impl<'a, M: AnyFrameMeta> Frame<M> {
19
20    pub proof fn lemma_from_raw_manuallydrop_general(
21        raw: Paddr,
22        frame: Self,
23        regions0: MetaRegionOwners,
24        regions1: MetaRegionOwners,
25        tracked debt: BorrowDebt,
26    )
27        requires
28            Self::from_raw_requires_safety(regions0, raw),
29            regions0.slot_owners[frame_to_index(raw)].raw_count <= 1,
30            regions0.slot_owners[frame_to_index(raw)].inner_perms.ref_count.value()
31                != REF_COUNT_UNUSED,
32            Self::from_raw_ensures(regions0, regions1, raw, frame),
33            <Self as TrackDrop>::constructor_requires(frame, regions1),
34            debt.frame_index == frame_to_index(raw),
35            debt.raw_count_at_issue == regions0.slot_owners[frame_to_index(raw)].raw_count,
36
37        ensures
38            forall |regions2: MetaRegionOwners|
39                #![trigger regions2.slot_owners[frame_to_index(raw)]]
40                <Self as TrackDrop>::constructor_ensures(frame, regions1, regions2) ==> {
41                    &&& regions2.slot_owners[frame_to_index(raw)].raw_count == 1
42                    &&& regions2.slot_owners[frame_to_index(raw)].inner_perms
43                        == regions0.slot_owners[frame_to_index(raw)].inner_perms
44                    &&& regions2.slot_owners[frame_to_index(raw)].self_addr
45                        == regions0.slot_owners[frame_to_index(raw)].self_addr
46                    &&& regions2.slot_owners[frame_to_index(raw)].usage
47                        == regions0.slot_owners[frame_to_index(raw)].usage
48                    &&& regions2.slot_owners[frame_to_index(raw)].paths_in_pt
49                        == regions0.slot_owners[frame_to_index(raw)].paths_in_pt
50                    &&& forall |i: usize|
51                        #![trigger regions2.slot_owners[i]]
52                        i != frame_to_index(raw) ==> regions2.slot_owners[i]
53                            == regions0.slot_owners[i]
54                    &&& regions2.slot_owners.dom() =~= regions0.slot_owners.dom()
55                    &&& regions2.slots =~= regions1.slots
56                    &&& regions2.inv()
57                }
58    {
59        broadcast use group_page_meta;
60        debt.discharge_in_lemma(&regions1);
61        let idx = frame_to_index(raw);
62        assert(frame.paddr() == raw);
63        assert(regions0.slot_owners.dom() =~= regions1.slot_owners.dom());
64
65        assert forall |regions2: MetaRegionOwners|
66            <Self as TrackDrop>::constructor_ensures(frame, regions1, regions2)
67        implies
68            regions2.slot_owners[idx].raw_count == 1
69            && regions2.slot_owners[idx].inner_perms
70                == regions0.slot_owners[idx].inner_perms
71            && regions2.slot_owners[idx].self_addr
72                == regions0.slot_owners[idx].self_addr
73            && regions2.slot_owners[idx].usage == regions0.slot_owners[idx].usage
74            && regions2.slot_owners[idx].paths_in_pt
75                == regions0.slot_owners[idx].paths_in_pt
76            && (forall |i: usize|
77                #![trigger regions2.slot_owners[i]]
78                i != idx ==> regions2.slot_owners[i] == regions0.slot_owners[i])
79            && regions2.slot_owners.dom() =~= regions0.slot_owners.dom()
80            && regions2.slots =~= regions1.slots
81            && regions2.inv()
82        by {
83            assert forall |i: usize| i != idx implies
84                #[trigger] regions2.slot_owners[i] == regions0.slot_owners[i]
85            by {
86                assert(regions2.slot_owners[i] == regions1.slot_owners[i]);
87                assert(regions1.slot_owners[i] == regions0.slot_owners[i]);
88            }
89
90            assert forall |i: usize| #[trigger] regions2.slot_owners.contains_key(i)
91                implies regions2.slot_owners[i].inv()
92            by {
93                if i == idx {
94                    assert(regions1.slot_owners[idx].inv());
95                    assert(regions0.slot_owners[idx].inner_perms.ref_count.value()
96                        != REF_COUNT_UNUSED);
97                } else {
98                    assert(regions1.slot_owners[i].inv());
99                }
100            }
101
102            assert forall |i: usize| #[trigger] regions2.slots.contains_key(i)
103                implies {
104                    &&& regions2.slot_owners.contains_key(i)
105                    &&& regions2.slot_owners[i].inv()
106                    &&& regions2.slots[i].is_init()
107                    &&& regions2.slots[i].value().wf(regions2.slot_owners[i])
108                    &&& regions2.slot_owners[i].self_addr == regions2.slots[i].addr()
109                }
110            by {
111                assert(regions1.slots.contains_key(i));
112                if i != idx {
113                    assert(regions2.slot_owners[i] == regions1.slot_owners[i]);
114                }
115            }
116            assert(regions2.inv());
117        }
118    }
119
120}
121
122}
ostd/specs/mm/frame/frame_lifecycle.rs

ostd/specs/mm/frame/
frame_lifecycle.rs
