ostd/specs/mm/frame/
meta_owners.rs

1//! The model of a metadata slot. It includes:
2//! - The model of the metadata slot: `MetaSlotModel`.
3//! - The invariants for both MetaSlot and MetaSlotModel.
4//! - The primitives for MetaSlot.
5use vstd::atomic::*;
6use vstd::cell::pcell_maybe_uninit;
7use vstd::prelude::*;
8use vstd::simple_pptr::*;
9
10use vstd_extra::cast_ptr::{self, Repr};
11use vstd_extra::ghost_tree::TreePath;
12use vstd_extra::ownership::*;
13
14use super::*;
15use crate::mm::frame::meta::MetaSlot;
16use crate::mm::frame::AnyFrameMeta;
17use crate::mm::PagingLevel;
18use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
19use crate::specs::arch::mm::NR_ENTRIES;
20use crate::specs::mm::frame::linked_list::linked_list_owners::StoredLink;
21use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
22
23verus! {
24
25#[allow(non_camel_case_types)]
26pub enum MetaSlotStatus {
27    UNUSED,
28    UNIQUE,
29    SHARED,
30    OVERFLOW,
31    UNDER_CONSTRUCTION,
32}
33
34pub enum PageState {
35    Unused,
36    Typed,
37    Untyped,
38}
39
40#[repr(u8)]
41#[derive(Debug, PartialEq, Clone, Copy)]
42pub enum PageUsage {
43    // The zero variant is reserved for the unused type. Only an unused page
44    // can be designated for one of the other purposes.
45    #[allow(dead_code)]
46    Unused,
47    /// The page is reserved or unusable. The kernel should not touch it.
48    #[allow(dead_code)]
49    Reserved,
50    /// The page is used as a frame, i.e., a page of untyped memory.
51    Frame,
52    /// The page is used by a page table.
53    PageTable,
54    /// The page stores metadata of other pages.
55    Meta,
56    /// The page stores the kernel such as kernel code, data, etc.
57    Kernel,
58}
59
60impl PageUsage {
61    pub open spec fn as_u8_spec(&self) -> u8 {
62        match self {
63            PageUsage::Unused => 0,
64            PageUsage::Reserved => 1,
65            PageUsage::Frame => 32,
66            PageUsage::PageTable => 64,
67            PageUsage::Meta => 65,
68            PageUsage::Kernel => 66,
69        }
70    }
71
72    #[verifier::external_body]
73    #[verifier::when_used_as_spec(as_u8_spec)]
74    pub fn as_u8(&self) -> (res: u8)
75        ensures
76            res == self.as_u8_spec(),
77    {
78        *self as u8
79    }
80
81    #[vstd::contrib::auto_spec]
82    pub fn as_state(&self) -> (res: PageState) {
83        match &self {
84            PageUsage::Unused => PageState::Unused,
85            PageUsage::Frame => PageState::Untyped,
86            _ => PageState::Typed,
87        }
88    }
89}
90
91pub const REF_COUNT_UNUSED: u64 = u64::MAX;
92
93pub const REF_COUNT_UNIQUE: u64 = u64::MAX - 1;
94
95pub const REF_COUNT_MAX: u64 = i64::MAX as u64;
96
97pub struct StoredPageTablePageMeta {
98    pub nr_children: pcell_maybe_uninit::PCell<u16>,
99    pub stray: pcell_maybe_uninit::PCell<bool>,
100    pub level: PagingLevel,
101    pub lock: PAtomicU8,
102}
103
104pub enum MetaSlotStorage {
105    Empty([u8; 39]),
106    FrameLink(StoredLink),
107    PTNode(StoredPageTablePageMeta),
108}
109
110/// `MetaSlotStorage` is an inductive tagged union of all of the frame meta types that
111/// we work with in this development. So, it should itself implement `AnyFrameMeta`, and
112/// it can then be used to stand in for `dyn AnyFrameMeta`.
113impl AnyFrameMeta for MetaSlotStorage {
114    uninterp spec fn vtable_ptr(&self) -> usize;
115}
116
117impl Repr<MetaSlotStorage> for MetaSlotStorage {
118    type Perm = ();
119
120    open spec fn wf(slot: MetaSlotStorage, perm: ()) -> bool {
121        true
122    }
123
124    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
125        (self, ())
126    }
127
128    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
129        self
130    }
131
132    open spec fn from_repr_spec(slot: MetaSlotStorage, perm: ()) -> Self {
133        slot
134    }
135
136    fn from_repr(slot: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
137        slot
138    }
139
140    fn from_borrowed<'a>(slot: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
141        slot
142    }
143
144    proof fn from_to_repr(self, perm: ()) {
145    }
146
147    proof fn to_from_repr(slot: MetaSlotStorage, perm: ()) {
148    }
149
150    proof fn to_repr_wf(self, perm: ()) {
151    }
152}
153
154impl MetaSlotStorage {
155    pub open spec fn get_link_spec(self) -> Option<StoredLink> {
156        match self {
157            MetaSlotStorage::FrameLink(link) => Some(link),
158            _ => None,
159        }
160    }
161
162    #[verifier::when_used_as_spec(get_link_spec)]
163    pub fn get_link(self) -> (res: Option<StoredLink>)
164        ensures
165            res == self.get_link_spec(),
166    {
167        match self {
168            MetaSlotStorage::FrameLink(link) => Some(link),
169            _ => None,
170        }
171    }
172
173    pub open spec fn get_node_spec(self) -> Option<StoredPageTablePageMeta> {
174        match self {
175            MetaSlotStorage::PTNode(node) => Some(node),
176            _ => None,
177        }
178    }
179
180    #[verifier::when_used_as_spec(get_node_spec)]
181    pub fn get_node(self) -> (res: Option<StoredPageTablePageMeta>)
182        ensures
183            res == self.get_node_spec(),
184    {
185        match self {
186            MetaSlotStorage::PTNode(node) => Some(node),
187            _ => None,
188        }
189    }
190}
191
192pub tracked struct MetadataInnerPerms {
193    pub storage: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
194    pub ref_count: PermissionU64,
195    pub vtable_ptr: vstd::simple_pptr::PointsTo<usize>,
196    pub in_list: PermissionU64,
197}
198
199pub tracked struct MetaSlotOwner {
200    pub inner_perms: MetadataInnerPerms,
201    pub self_addr: usize,
202    pub usage: PageUsage,
203    pub raw_count: usize,
204    pub path_if_in_pt: Option<TreePath<NR_ENTRIES>>,
205}
206
207impl Inv for MetaSlotOwner {
208    open spec fn inv(self) -> bool {
209        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNUSED ==> {
210            &&& self.raw_count == 0
211            &&& self.inner_perms.storage.is_uninit()
212            &&& self.inner_perms.vtable_ptr.is_uninit()
213            &&& self.inner_perms.in_list.value() == 0
214        }
215        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNIQUE ==> {
216            &&& self.inner_perms.vtable_ptr.is_init()
217            &&& self.inner_perms.storage.is_init()
218            &&& self.inner_perms.in_list.value() == 0
219        }
220        &&& 0 < self.inner_perms.ref_count.value() <= REF_COUNT_MAX ==> {
221            &&& self.inner_perms.vtable_ptr.is_init()
222        }
223        &&& REF_COUNT_MAX <= self.inner_perms.ref_count.value() < REF_COUNT_UNIQUE ==> { false }
224        &&& self.inner_perms.ref_count.value() == 0 ==> {
225            &&& self.inner_perms.vtable_ptr.is_uninit()
226            &&& self.inner_perms.in_list.value() == 0
227        }
228        &&& FRAME_METADATA_RANGE.start <= self.self_addr < FRAME_METADATA_RANGE.end
229        &&& self.self_addr % META_SLOT_SIZE == 0
230    }
231}
232
233pub ghost struct MetaSlotModel {
234    pub status: MetaSlotStatus,
235    pub storage: MemContents<MetaSlotStorage>,
236    pub ref_count: u64,
237    pub vtable_ptr: MemContents<usize>,
238    pub in_list: u64,
239    pub self_addr: usize,
240    pub usage: PageUsage,
241}
242
243impl Inv for MetaSlotModel {
244    open spec fn inv(self) -> bool {
245        match self.ref_count {
246            REF_COUNT_UNUSED => {
247                &&& self.vtable_ptr.is_uninit()
248                &&& self.in_list == 0
249            },
250            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
251            0 => {
252                &&& self.vtable_ptr.is_uninit()
253                &&& self.in_list == 0
254            },
255            _ if self.ref_count < REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
256            _ => { false },
257        }
258    }
259}
260
261impl View for MetaSlotOwner {
262    type V = MetaSlotModel;
263
264    open spec fn view(&self) -> Self::V {
265        let storage = self.inner_perms.storage.mem_contents();
266        let ref_count = self.inner_perms.ref_count.value();
267        let vtable_ptr = self.inner_perms.vtable_ptr.mem_contents();
268        let in_list = self.inner_perms.in_list.value();
269        let self_addr = self.self_addr;
270        let usage = self.usage;
271        let status = match ref_count {
272            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
273            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
274            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
275            _ if ref_count < REF_COUNT_MAX => MetaSlotStatus::SHARED,
276            _ => MetaSlotStatus::OVERFLOW,
277        };
278        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, self_addr, usage }
279    }
280}
281
282impl InvView for MetaSlotOwner {
283    proof fn view_preserves_inv(self) {
284    }
285}
286
287impl OwnerOf for MetaSlot {
288    type Owner = MetaSlotOwner;
289
290    open spec fn wf(self, owner: Self::Owner) -> bool {
291        &&& self.storage.id() == owner.inner_perms.storage.id()
292        &&& self.ref_count.id() == owner.inner_perms.ref_count.id()
293        &&& self.vtable_ptr == owner.inner_perms.vtable_ptr.pptr()
294        &&& self.in_list.id() == owner.inner_perms.in_list.id()
295    }
296}
297
298impl ModelOf for MetaSlot {
299
300}
301
302impl MetaSlotOwner {
303    pub axiom fn take_inner_perms(tracked &mut self) -> (tracked res: MetadataInnerPerms)
304        ensures
305            res == old(self).inner_perms,
306            self.self_addr == old(self).self_addr,
307            self.usage == old(self).usage,
308            self.raw_count == old(self).raw_count,
309            self.path_if_in_pt == old(self).path_if_in_pt;
310
311    pub axiom fn sync_inner(tracked &mut self, inner_perms: &MetadataInnerPerms)
312        ensures *self == (Self { inner_perms: *inner_perms, ..*old(self) });
313}
314
315pub struct Metadata<M: AnyFrameMeta> {
316    pub metadata: M,
317    pub ref_count: u64,
318    pub vtable_ptr: MemContents<usize>,
319    pub in_list: u64,
320}
321
322impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M> {
323    /// The metadata value is an abstract function of the inner permissions,
324    /// since extracting `M` from `MetaSlotStorage` requires `M::Perm` which
325    /// is not stored in `MetadataInnerPerms`.
326    pub uninterp spec fn metadata_from_inner_perms(perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>) -> M;
327}
328
329impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M> {
330    type Perm = MetadataInnerPerms;
331
332    open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool {
333        &&& perm.storage.id() == r.storage.id()
334        &&& perm.ref_count.id() == r.ref_count.id()
335        &&& perm.vtable_ptr.pptr() == r.vtable_ptr
336        &&& perm.in_list.id() == r.in_list.id()
337    }
338
339    uninterp spec fn to_repr_spec(self, perm: MetadataInnerPerms) -> (MetaSlot, MetadataInnerPerms);
340
341    #[verifier::external_body]
342    fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot {
343        unimplemented!()
344    }
345
346    open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self {
347        Metadata {
348            metadata: Self::metadata_from_inner_perms(perm.storage),
349            ref_count: perm.ref_count.value(),
350            vtable_ptr: perm.vtable_ptr.mem_contents(),
351            in_list: perm.in_list.value(),
352        }
353    }
354
355    #[verifier::external_body]
356    fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self {
357        unimplemented!()
358    }
359
360    #[verifier::external_body]
361    fn from_borrowed<'a>(r: &'a MetaSlot, Tracked(perm): Tracked<&'a MetadataInnerPerms>) -> &'a Self {
362        unimplemented!()
363    }
364
365    proof fn from_to_repr(self, perm: MetadataInnerPerms) {
366        admit()
367    }
368
369    proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms) {
370        admit()
371    }
372
373    proof fn to_repr_wf(self, perm: MetadataInnerPerms) {
374        admit()
375    }
376}
377
378/// A permission token for frame metadata.
379///
380/// [`Frame<M>`] the high-level representation of the low-level pointer
381/// to the [`super::meta::MetaSlot`].
382pub type MetaPerm<M: AnyFrameMeta + Repr<MetaSlotStorage>> = cast_ptr::PointsTo<MetaSlot, Metadata<M>>;
383
384
385} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
