ostd/specs/mm/frame/
meta_region_owners.rs

1use vstd::atomic::*;
2use vstd::cell;
3use vstd::prelude::*;
4use vstd::simple_pptr::{self, *};
5
6use core::ops::Range;
7
8use vstd_extra::ownership::*;
9
10use super::meta_owners::{MetaSlotModel, MetaSlotOwner};
11use super::*;
12use crate::mm::frame::meta::{
13    mapping::{frame_to_index_spec, frame_to_meta, max_meta_slots, meta_addr, META_SLOT_SIZE},
14    MetaSlot,
15};
16use crate::mm::Paddr;
17use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
18use crate::specs::arch::mm::{MAX_PADDR, PAGE_SIZE};
19
20verus! {
21
22/// Represents the meta-frame memory region. Can be viewed as a collection of
23/// Cell<MetaSlot> at a fixed address range.
24pub struct MetaRegion;
25
26pub tracked struct MetaRegionOwners {
27    pub slots: Map<usize, simple_pptr::PointsTo<MetaSlot>>,
28    pub dropped_slots: Map<usize, simple_pptr::PointsTo<MetaSlot>>,
29    pub slot_owners: Map<usize, MetaSlotOwner>,
30}
31
32pub ghost struct MetaRegionModel {
33    pub slots: Map<usize, MetaSlotModel>,
34}
35
36impl Inv for MetaRegionOwners {
37    open spec fn inv(self) -> bool {
38        &&& self.slots.dom().finite()
39        &&& {
40            // All accessible slots are within the valid address range.
41            forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
42        }
43        &&& { forall|i: usize| #[trigger] self.slots.contains_key(i) ==> i < max_meta_slots() }
44        &&& {
45            forall|i: usize| #[trigger] self.dropped_slots.contains_key(i) ==> i < max_meta_slots()
46        }
47        &&& {
48            // Invariant for each slot holds.
49            forall|i: usize| #[trigger]
50                self.slot_owners.contains_key(i) ==> self.slot_owners[i].inv()
51        }
52        &&& {
53            forall|i: usize| #[trigger]
54                self.slots.contains_key(i) ==> {
55                    &&& self.slots[i].is_init()
56                    &&& self.slots[i].addr() == meta_addr(i)
57                    &&& self.slots[i].value().wf(self.slot_owners[i])
58                    &&& self.slot_owners[i].self_addr == self.slots[i].addr()
59                    &&& !self.dropped_slots.contains_key(i)
60                }
61        }
62        &&& {
63            forall|i: usize| #[trigger]
64                self.dropped_slots.contains_key(i) ==> {
65                    &&& self.dropped_slots[i].is_init()
66                    &&& self.dropped_slots[i].addr() == meta_addr(i)
67                    &&& self.dropped_slots[i].value().wf(self.slot_owners[i])
68                    &&& self.slot_owners[i].self_addr == self.dropped_slots[i].addr()
69                    &&& !self.slots.contains_key(i)
70                }
71        }
72    }
73}
74
75impl Inv for MetaRegionModel {
76    open spec fn inv(self) -> bool {
77        &&& self.slots.dom().finite()
78        &&& forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slots.contains_key(i)
79        &&& forall|i: usize| #[trigger] self.slots.contains_key(i) ==> self.slots[i].inv()
80    }
81}
82
83impl View for MetaRegionOwners {
84    type V = MetaRegionModel;
85
86    open spec fn view(&self) -> <Self as View>::V {
87        let slots = self.slot_owners.map_values(|s: MetaSlotOwner| s@);
88        MetaRegionModel { slots }
89    }
90}
91
92impl InvView for MetaRegionOwners {
93    // XXX: verus `map_values` does not preserves the `finite()` attribute.
94    axiom fn view_preserves_inv(self);
95}
96
97impl OwnerOf for MetaRegion {
98    type Owner = MetaRegionOwners;
99
100    open spec fn wf(self, owner: Self::Owner) -> bool {
101        true
102    }
103}
104
105impl ModelOf for MetaRegion {
106
107}
108
109impl MetaRegionOwners {
110    pub open spec fn ref_count(self, i: usize) -> (res: u64)
111        recommends
112            self.inv(),
113            i < max_meta_slots() as usize,
114    {
115        self.slot_owners[i].ref_count.value()
116    }
117
118    pub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
119        recommends
120            self.inv(),
121            range.start < range.end < MAX_PADDR(),
122    {
123        forall|paddr: Paddr|
124            #![trigger frame_to_index_spec(paddr)]
125            (range.start <= paddr < range.end && paddr % PAGE_SIZE() == 0)
126                ==> self.slots.contains_key(frame_to_index_spec(paddr))
127    }
128
129    pub open spec fn paddr_range_in_dropped_region(self, range: Range<Paddr>) -> bool
130        recommends
131            self.inv(),
132            range.start < range.end < MAX_PADDR(),
133    {
134        forall|paddr: Paddr|
135            #![trigger frame_to_index_spec(paddr)]
136            (range.start <= paddr < range.end && paddr % PAGE_SIZE() == 0)
137                ==> !self.slots.contains_key(frame_to_index_spec(paddr))
138                && self.dropped_slots.contains_key(frame_to_index_spec(paddr))
139    }
140
141    pub open spec fn paddr_range_not_in_region(self, range: Range<Paddr>) -> bool
142        recommends
143            self.inv(),
144            range.start < range.end < MAX_PADDR(),
145    {
146        forall|paddr: Paddr|
147            #![trigger frame_to_index_spec(paddr)]
148            (range.start <= paddr < range.end && paddr % PAGE_SIZE() == 0)
149                ==> !self.slots.contains_key(frame_to_index_spec(paddr))
150                && !self.dropped_slots.contains_key(frame_to_index_spec(paddr))
151    }
152
153    pub proof fn inv_implies_correct_addr(self, paddr: usize)
154        requires
155            paddr < MAX_PADDR(),
156            paddr % PAGE_SIZE() == 0,
157            self.inv(),
158        ensures
159            self.slot_owners.contains_key(frame_to_index_spec(paddr) as usize),
160    {
161        assert((frame_to_index_spec(paddr)) < max_meta_slots() as usize);
162    }
163}
164
165} // verus!
ostd/specs/mm/frame/meta_region_owners.rs

ostd/specs/mm/frame/
meta_region_owners.rs
