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    Untyped,
107    FrameLink(StoredLink),
108    PTNode(StoredPageTablePageMeta),
109}
110
111/// `MetaSlotStorage` is an inductive tagged union of all of the frame meta types that
112/// we work with in this development. So, it should itself implement `AnyFrameMeta`, and
113/// it can then be used to stand in for `dyn AnyFrameMeta`.
114impl AnyFrameMeta for MetaSlotStorage {
115    uninterp spec fn vtable_ptr(&self) -> usize;
116}
117
118impl Repr<MetaSlotStorage> for MetaSlotStorage {
119    type Perm = ();
120
121    open spec fn wf(slot: MetaSlotStorage, perm: ()) -> bool {
122        true
123    }
124
125    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
126        (self, ())
127    }
128
129    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
130        self
131    }
132
133    open spec fn from_repr_spec(slot: MetaSlotStorage, perm: ()) -> Self {
134        slot
135    }
136
137    fn from_repr(slot: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
138        slot
139    }
140
141    fn from_borrowed<'a>(slot: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
142        slot
143    }
144
145    proof fn from_to_repr(self, perm: ()) {
146    }
147
148    proof fn to_from_repr(slot: MetaSlotStorage, perm: ()) {
149    }
150
151    proof fn to_repr_wf(self, perm: ()) {
152    }
153}
154
155impl MetaSlotStorage {
156    pub open spec fn get_link_spec(self) -> Option<StoredLink> {
157        match self {
158            MetaSlotStorage::FrameLink(link) => Some(link),
159            _ => None,
160        }
161    }
162
163    #[verifier::when_used_as_spec(get_link_spec)]
164    pub fn get_link(self) -> (res: Option<StoredLink>)
165        ensures
166            res == self.get_link_spec(),
167    {
168        match self {
169            MetaSlotStorage::FrameLink(link) => Some(link),
170            _ => None,
171        }
172    }
173
174    pub open spec fn get_node_spec(self) -> Option<StoredPageTablePageMeta> {
175        match self {
176            MetaSlotStorage::PTNode(node) => Some(node),
177            _ => None,
178        }
179    }
180
181    #[verifier::when_used_as_spec(get_node_spec)]
182    pub fn get_node(self) -> (res: Option<StoredPageTablePageMeta>)
183        ensures
184            res == self.get_node_spec(),
185    {
186        match self {
187            MetaSlotStorage::PTNode(node) => Some(node),
188            _ => None,
189        }
190    }
191}
192
193pub tracked struct MetadataInnerPerms {
194    pub storage: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
195    pub ref_count: PermissionU64,
196    pub vtable_ptr: vstd::simple_pptr::PointsTo<usize>,
197    pub in_list: PermissionU64,
198}
199
200pub tracked struct MetaSlotOwner {
201    pub inner_perms: MetadataInnerPerms,
202    pub self_addr: usize,
203    pub usage: PageUsage,
204    pub raw_count: usize,
205    pub path_if_in_pt: Option<TreePath<NR_ENTRIES>>,
206}
207
208impl Inv for MetaSlotOwner {
209    open spec fn inv(self) -> bool {
210        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNUSED ==> {
211            &&& self.raw_count == 0
212            &&& self.inner_perms.storage.is_uninit()
213            &&& self.inner_perms.vtable_ptr.is_uninit()
214            &&& self.inner_perms.in_list.value() == 0
215        }
216        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNIQUE ==> {
217            &&& self.inner_perms.vtable_ptr.is_init()
218            &&& self.inner_perms.storage.is_init()
219            &&& self.inner_perms.in_list.value() == 0
220        }
221        &&& 0 < self.inner_perms.ref_count.value() <= REF_COUNT_MAX ==> {
222            &&& self.inner_perms.vtable_ptr.is_init()
223        }
224        &&& REF_COUNT_MAX <= self.inner_perms.ref_count.value() < REF_COUNT_UNIQUE ==> { false }
225        &&& self.inner_perms.ref_count.value() == 0 ==> {
226            &&& self.inner_perms.vtable_ptr.is_uninit()
227            &&& self.inner_perms.in_list.value() == 0
228        }
229        &&& FRAME_METADATA_RANGE.start <= self.self_addr < FRAME_METADATA_RANGE.end
230        &&& self.self_addr % META_SLOT_SIZE == 0
231    }
232}
233
234pub ghost struct MetaSlotModel {
235    pub status: MetaSlotStatus,
236    pub storage: MemContents<MetaSlotStorage>,
237    pub ref_count: u64,
238    pub vtable_ptr: MemContents<usize>,
239    pub in_list: u64,
240    pub self_addr: usize,
241    pub usage: PageUsage,
242}
243
244impl Inv for MetaSlotModel {
245    open spec fn inv(self) -> bool {
246        match self.ref_count {
247            REF_COUNT_UNUSED => {
248                &&& self.vtable_ptr.is_uninit()
249                &&& self.in_list == 0
250            },
251            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
252            0 => {
253                &&& self.vtable_ptr.is_uninit()
254                &&& self.in_list == 0
255            },
256            _ if self.ref_count < REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
257            _ => { false },
258        }
259    }
260}
261
262impl View for MetaSlotOwner {
263    type V = MetaSlotModel;
264
265    open spec fn view(&self) -> Self::V {
266        let storage = self.inner_perms.storage.mem_contents();
267        let ref_count = self.inner_perms.ref_count.value();
268        let vtable_ptr = self.inner_perms.vtable_ptr.mem_contents();
269        let in_list = self.inner_perms.in_list.value();
270        let self_addr = self.self_addr;
271        let usage = self.usage;
272        let status = match ref_count {
273            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
274            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
275            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
276            _ if ref_count < REF_COUNT_MAX => MetaSlotStatus::SHARED,
277            _ => MetaSlotStatus::OVERFLOW,
278        };
279        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, self_addr, usage }
280    }
281}
282
283impl InvView for MetaSlotOwner {
284    proof fn view_preserves_inv(self) {
285    }
286}
287
288impl OwnerOf for MetaSlot {
289    type Owner = MetaSlotOwner;
290
291    open spec fn wf(self, owner: Self::Owner) -> bool {
292        &&& self.storage.id() == owner.inner_perms.storage.id()
293        &&& self.ref_count.id() == owner.inner_perms.ref_count.id()
294        &&& self.vtable_ptr == owner.inner_perms.vtable_ptr.pptr()
295        &&& self.in_list.id() == owner.inner_perms.in_list.id()
296    }
297}
298
299impl ModelOf for MetaSlot {
300
301}
302
303impl MetaSlotOwner {
304    pub axiom fn take_inner_perms(tracked &mut self) -> (tracked res: MetadataInnerPerms)
305        ensures
306            res == old(self).inner_perms,
307            self.self_addr == old(self).self_addr,
308            self.usage == old(self).usage,
309            self.raw_count == old(self).raw_count,
310            self.path_if_in_pt == old(self).path_if_in_pt;
311
312    pub axiom fn sync_inner(tracked &mut self, inner_perms: &MetadataInnerPerms)
313        ensures *self == (Self { inner_perms: *inner_perms, ..*old(self) });
314}
315
316pub struct Metadata<M: AnyFrameMeta> {
317    pub metadata: M,
318    pub ref_count: u64,
319    pub vtable_ptr: MemContents<usize>,
320    pub in_list: u64,
321}
322
323impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M> {
324    /// The metadata value is an abstract function of the inner permissions,
325    /// since extracting `M` from `MetaSlotStorage` requires `M::Perm` which
326    /// is not stored in `MetadataInnerPerms`.
327    pub uninterp spec fn metadata_from_inner_perms(perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>) -> M;
328}
329
330impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M> {
331    type Perm = MetadataInnerPerms;
332
333    open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool {
334        &&& perm.storage.id() == r.storage.id()
335        &&& perm.ref_count.id() == r.ref_count.id()
336        &&& perm.vtable_ptr.pptr() == r.vtable_ptr
337        &&& perm.in_list.id() == r.in_list.id()
338    }
339
340    uninterp spec fn to_repr_spec(self, perm: MetadataInnerPerms) -> (MetaSlot, MetadataInnerPerms);
341
342    #[verifier::external_body]
343    fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot {
344        unimplemented!()
345    }
346
347    open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self {
348        Metadata {
349            metadata: Self::metadata_from_inner_perms(perm.storage),
350            ref_count: perm.ref_count.value(),
351            vtable_ptr: perm.vtable_ptr.mem_contents(),
352            in_list: perm.in_list.value(),
353        }
354    }
355
356    #[verifier::external_body]
357    fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self {
358        unimplemented!()
359    }
360
361    #[verifier::external_body]
362    fn from_borrowed<'a>(r: &'a MetaSlot, Tracked(perm): Tracked<&'a MetadataInnerPerms>) -> &'a Self {
363        unimplemented!()
364    }
365
366    proof fn from_to_repr(self, perm: MetadataInnerPerms) {
367        admit()
368    }
369
370    proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms) {
371        admit()
372    }
373
374    proof fn to_repr_wf(self, perm: MetadataInnerPerms) {
375        admit()
376    }
377}
378
379/// A permission token for frame metadata.
380///
381/// [`Frame<M>`] the high-level representation of the low-level pointer
382/// to the [`super::meta::MetaSlot`].
383pub type MetaPerm<M: AnyFrameMeta + Repr<MetaSlotStorage>> = cast_ptr::PointsTo<MetaSlot, Metadata<M>>;
384
385} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
