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    /// The set of tree paths at which this slot is referenced. For PT-node
206    /// slots this is a singleton. For data-frame slots this tracks every
207    /// location the frame is currently mapped — allowing a single frame to be
208    /// mapped at multiple addresses.
209    pub ghost paths_in_pt: Set<TreePath<NR_ENTRIES>>,
210}
211
212impl Inv for MetaSlotOwner {
213    open spec fn inv(self) -> bool {
214        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNUSED ==> {
215            &&& self.raw_count == 0
216            &&& self.inner_perms.storage.is_uninit()
217            &&& self.inner_perms.vtable_ptr.is_uninit()
218            &&& self.inner_perms.in_list.value() == 0
219        }
220        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNIQUE ==> {
221            &&& self.inner_perms.vtable_ptr.is_init()
222            &&& self.inner_perms.storage.is_init()
223            &&& self.inner_perms.in_list.value() == 0
224        }
225        &&& 0 < self.inner_perms.ref_count.value() <= REF_COUNT_MAX ==> {
226            &&& self.inner_perms.vtable_ptr.is_init()
227        }
228        &&& REF_COUNT_MAX <= self.inner_perms.ref_count.value() < REF_COUNT_UNIQUE ==> { false }
229        &&& self.inner_perms.ref_count.value() == 0 ==> {
230            &&& self.inner_perms.in_list.value() == 0
231        }
232        &&& FRAME_METADATA_RANGE.start <= self.self_addr < FRAME_METADATA_RANGE.end
233        &&& self.self_addr % META_SLOT_SIZE == 0
234    }
235}
236
237pub ghost struct MetaSlotModel {
238    pub status: MetaSlotStatus,
239    pub storage: MemContents<MetaSlotStorage>,
240    pub ref_count: u64,
241    pub vtable_ptr: MemContents<usize>,
242    pub in_list: u64,
243    pub self_addr: usize,
244    pub usage: PageUsage,
245}
246
247impl Inv for MetaSlotModel {
248    open spec fn inv(self) -> bool {
249        match self.ref_count {
250            REF_COUNT_UNUSED => {
251                &&& self.vtable_ptr.is_uninit()
252                &&& self.in_list == 0
253            },
254            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
255            0 => {
256                &&& self.in_list == 0
257            },
258            _ if self.ref_count < REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
259            _ => { false },
260        }
261    }
262}
263
264impl View for MetaSlotOwner {
265    type V = MetaSlotModel;
266
267    open spec fn view(&self) -> Self::V {
268        let storage = self.inner_perms.storage.mem_contents();
269        let ref_count = self.inner_perms.ref_count.value();
270        let vtable_ptr = self.inner_perms.vtable_ptr.mem_contents();
271        let in_list = self.inner_perms.in_list.value();
272        let self_addr = self.self_addr;
273        let usage = self.usage;
274        let status = match ref_count {
275            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
276            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
277            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
278            _ if ref_count < REF_COUNT_MAX => MetaSlotStatus::SHARED,
279            _ => MetaSlotStatus::OVERFLOW,
280        };
281        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, self_addr, usage }
282    }
283}
284
285impl InvView for MetaSlotOwner {
286    proof fn view_preserves_inv(self) { }
287}
288
289impl OwnerOf for MetaSlot {
290    type Owner = MetaSlotOwner;
291
292    open spec fn wf(self, owner: Self::Owner) -> bool {
293        &&& self.storage.id() == owner.inner_perms.storage.id()
294        &&& self.ref_count.id() == owner.inner_perms.ref_count.id()
295        &&& self.vtable_ptr == owner.inner_perms.vtable_ptr.pptr()
296        &&& self.in_list.id() == owner.inner_perms.in_list.id()
297    }
298}
299
300impl ModelOf for MetaSlot {
301
302}
303
304impl MetaSlotOwner {
305    pub axiom fn take_inner_perms(tracked &mut self) -> (tracked res: MetadataInnerPerms)
306        ensures
307            res == old(self).inner_perms,
308            final(self).self_addr == old(self).self_addr,
309            final(self).usage == old(self).usage,
310            final(self).raw_count == old(self).raw_count,
311            final(self).paths_in_pt == old(self).paths_in_pt;
312
313    pub axiom fn sync_inner(tracked &mut self, inner_perms: &MetadataInnerPerms)
314        ensures *final(self) == (Self { inner_perms: *inner_perms, ..*old(self) });
315}
316
317pub struct Metadata<M: AnyFrameMeta> {
318    pub metadata: M,
319    pub ref_count: u64,
320    pub vtable_ptr: MemContents<usize>,
321    pub in_list: u64,
322}
323
324impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M> {
325    /// The metadata value is an abstract function of the inner permissions,
326    /// since extracting `M` from `MetaSlotStorage` requires `M::Perm` which
327    /// is not stored in `MetadataInnerPerms`.
328    pub uninterp spec fn metadata_from_inner_perms(perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>) -> M;
329
330    /// Inverse of [`metadata_from_inner_perms`]: given an `M` and a base
331    /// storage permission, produce a new permission with the same cell id
332    /// whose `metadata_from_inner_perms` interpretation yields `m`.
333    pub uninterp spec fn inner_perms_from_metadata(
334        m: M,
335        base: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
336    ) -> pcell_maybe_uninit::PointsTo<MetaSlotStorage>;
337
338    /// Axiomatic roundtrip laws for the metadata ↔ storage-perm pair. The
339    /// conversion is a transmute / reinterpret at exec level, so these laws
340    /// live at the `cast_ptr` trust boundary.
341    pub axiom fn metadata_perms_inverse(
342        m: M,
343        base: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
344    )
345        ensures
346            Self::metadata_from_inner_perms(Self::inner_perms_from_metadata(m, base)) == m,
347            Self::inner_perms_from_metadata(m, base).id() == base.id();
348
349    pub axiom fn inner_perms_from_metadata_roundtrip(
350        perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
351    )
352        ensures
353            Self::inner_perms_from_metadata(Self::metadata_from_inner_perms(perm), perm) == perm;
354}
355
356/// Value-updaters for the opaque tracked permission types inside
357/// [`MetadataInnerPerms`]. Each uninterp operation produces a new permission
358/// with the same id as the input but a specified value; the paired axioms
359/// document the expected behavior. The conversions are implemented in exec
360/// by `external_body` primitives, so the laws are axiomatic.
361pub uninterp spec fn perm_u64_with(p: PermissionU64, v: u64) -> PermissionU64;
362
363pub axiom fn perm_u64_with_value(p: PermissionU64, v: u64)
364    ensures
365        perm_u64_with(p, v).value() == v,
366        perm_u64_with(p, v).id() == p.id();
367
368/// Setting a `PermissionU64` to its own current value is a no-op.
369pub axiom fn perm_u64_with_identity(p: PermissionU64)
370    ensures perm_u64_with(p, p.value()) == p;
371
372pub uninterp spec fn pptr_usize_with(
373    p: vstd::simple_pptr::PointsTo<usize>,
374    c: MemContents<usize>,
375) -> vstd::simple_pptr::PointsTo<usize>;
376
377pub axiom fn pptr_usize_with_value(
378    p: vstd::simple_pptr::PointsTo<usize>,
379    c: MemContents<usize>,
380)
381    ensures
382        pptr_usize_with(p, c).mem_contents() == c,
383        pptr_usize_with(p, c).pptr() == p.pptr();
384
385/// Setting a `PointsTo<usize>` to its own contents is a no-op.
386pub axiom fn pptr_usize_with_identity(p: vstd::simple_pptr::PointsTo<usize>)
387    ensures pptr_usize_with(p, p.mem_contents()) == p;
388
389/// Reconstruct a [`MetaSlot`] from its underlying cell ids. The exec
390/// implementation is a cast; the laws pin `.id()` / `.pptr()` equalities.
391pub uninterp spec fn meta_slot_from_perm(perm: MetadataInnerPerms) -> MetaSlot;
392
393pub axiom fn meta_slot_from_perm_ids(perm: MetadataInnerPerms)
394    ensures
395        meta_slot_from_perm(perm).storage.id() == perm.storage.id(),
396        meta_slot_from_perm(perm).ref_count.id() == perm.ref_count.id(),
397        meta_slot_from_perm(perm).vtable_ptr == perm.vtable_ptr.pptr(),
398        meta_slot_from_perm(perm).in_list.id() == perm.in_list.id();
399
400/// A `MetaSlot` is uniquely determined by its cell ids + vtable_ptr address.
401/// This is a structural fact about the opaque atomic/cell primitives — two
402/// `MetaSlot` values whose ids agree on every field are equal.
403pub axiom fn meta_slot_eq_by_ids(a: MetaSlot, b: MetaSlot)
404    ensures
405        (a.storage.id() == b.storage.id()
406         && a.ref_count.id() == b.ref_count.id()
407         && a.vtable_ptr == b.vtable_ptr
408         && a.in_list.id() == b.in_list.id())
409        ==> a == b;
410
411impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M> {
412    type Perm = MetadataInnerPerms;
413
414    open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool {
415        &&& perm.storage.id() == r.storage.id()
416        &&& perm.ref_count.id() == r.ref_count.id()
417        &&& perm.vtable_ptr.pptr() == r.vtable_ptr
418        &&& perm.in_list.id() == r.in_list.id()
419    }
420
421    open spec fn to_repr_spec(self, perm: MetadataInnerPerms) -> (MetaSlot, MetadataInnerPerms) {
422        let new_perm = MetadataInnerPerms {
423            storage: Self::inner_perms_from_metadata(self.metadata, perm.storage),
424            ref_count: perm_u64_with(perm.ref_count, self.ref_count),
425            vtable_ptr: pptr_usize_with(perm.vtable_ptr, self.vtable_ptr),
426            in_list: perm_u64_with(perm.in_list, self.in_list),
427        };
428        (meta_slot_from_perm(new_perm), new_perm)
429    }
430
431    #[verifier::external_body]
432    fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot {
433        unimplemented!()
434    }
435
436    open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self {
437        Metadata {
438            metadata: Self::metadata_from_inner_perms(perm.storage),
439            ref_count: perm.ref_count.value(),
440            vtable_ptr: perm.vtable_ptr.mem_contents(),
441            in_list: perm.in_list.value(),
442        }
443    }
444
445    #[verifier::external_body]
446    fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self {
447        unimplemented!()
448    }
449
450    #[verifier::external_body]
451    fn from_borrowed<'a>(r: &'a MetaSlot, Tracked(perm): Tracked<&'a MetadataInnerPerms>) -> &'a Self {
452        unimplemented!()
453    }
454
455    proof fn from_to_repr(self, perm: MetadataInnerPerms) {
456        Self::metadata_perms_inverse(self.metadata, perm.storage);
457        perm_u64_with_value(perm.ref_count, self.ref_count);
458        perm_u64_with_value(perm.in_list, self.in_list);
459        pptr_usize_with_value(perm.vtable_ptr, self.vtable_ptr);
460        let (r, np) = self.to_repr_spec(perm);
461        assert(Self::from_repr_spec(r, np) =~= self);
462    }
463
464    proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms) {
465        // wf(r, perm) gives us: r's ids match perm's ids; r.vtable_ptr == perm.vtable_ptr.pptr().
466        Self::inner_perms_from_metadata_roundtrip(perm.storage);
467        perm_u64_with_identity(perm.ref_count);
468        perm_u64_with_identity(perm.in_list);
469        pptr_usize_with_identity(perm.vtable_ptr);
470        // Each field of np2 equals the corresponding field of perm:
471        //   np2.storage    = inner_perms_from_metadata(metadata_from_inner_perms(perm.storage), perm.storage)
472        //                  = perm.storage                   (inner_perms_from_metadata_roundtrip)
473        //   np2.ref_count  = perm_u64_with(perm.ref_count, perm.ref_count.value())
474        //                  = perm.ref_count                 (perm_u64_with_identity)
475        //   np2.vtable_ptr = pptr_usize_with(perm.vtable_ptr, perm.vtable_ptr.mem_contents())
476        //                  = perm.vtable_ptr                (pptr_usize_with_identity)
477        //   np2.in_list    = perm.in_list                   (perm_u64_with_identity)
478        let md = Self::from_repr_spec(r, perm);
479        let (r2, np2) = md.to_repr_spec(perm);
480        assert(np2 =~= perm);
481        // r2 is produced from np2 == perm; its ids match perm's; perm's ids match r's (by wf).
482        meta_slot_from_perm_ids(np2);
483        meta_slot_eq_by_ids(r2, r);
484        assert(r2 == r);
485    }
486
487    proof fn to_repr_wf(self, perm: MetadataInnerPerms) {
488        let (r, np) = self.to_repr_spec(perm);
489        meta_slot_from_perm_ids(np);
490        Self::metadata_perms_inverse(self.metadata, perm.storage);
491        perm_u64_with_value(perm.ref_count, self.ref_count);
492        perm_u64_with_value(perm.in_list, self.in_list);
493        pptr_usize_with_value(perm.vtable_ptr, self.vtable_ptr);
494        // wf checks id equality between np's perms and r's slot fields.
495    }
496}
497
498/// A permission token for frame metadata.
499///
500/// [`Frame<M>`] the high-level representation of the low-level pointer
501/// to the [`super::meta::MetaSlot`].
502pub type MetaPerm<M: AnyFrameMeta + Repr<MetaSlotStorage>> = cast_ptr::PointsTo<MetaSlot, Metadata<M>>;
503
504} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
