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::prelude::*;
6
7use vstd::{atomic::*, cell::pcell_maybe_uninit, simple_pptr::*};
8use vstd_extra::{
9    cast_ptr::{self, Repr},
10    ghost_tree::TreePath,
11    ownership::*,
12};
13
14use crate::specs::{arch::NR_ENTRIES, mm::frame::linked_list::linked_list_owners::StoredLink};
15
16use crate::mm::{
17    Paddr, PagingLevel, Vaddr,
18    frame::{
19        AnyFrameMeta,
20        meta::{
21            META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
22            mapping::meta_to_frame,
23        },
24    },
25    kspace::FRAME_METADATA_RANGE,
26};
27
28use super::*;
29
30verus! {
31
32#[allow(non_camel_case_types)]
33pub ghost enum MetaSlotStatus {
34    UNUSED,
35    UNIQUE,
36    SHARED,
37    OVERFLOW,
38    UNDER_CONSTRUCTION,
39}
40
41pub ghost enum PageUsage {
42    // The zero variant is reserved for the unused type. Only an unused page
43    // can be designated for one of the other purposes.
44    Unused,
45    /// The page is reserved or unusable. The kernel should not touch it.
46    Reserved,
47    /// The page is used as a frame, i.e., a page of untyped memory.
48    Frame,
49    /// The page is used by a page table.
50    PageTable,
51    /// The page stores metadata of other pages.
52    Meta,
53    /// The page stores the kernel such as kernel code, data, etc.
54    Kernel,
55    /// The page maps memory-mapped I/O (MMIO). Untracked: no refcount, slot
56    /// stays in the free pool, but distinguishable from `Unused` so the
57    /// kernel allocator never collides with an MMIO mapping.
58    MMIO,
59}
60
61/// Whether `pa` falls in an MMIO physical-address range. Uninterpreted at the
62/// spec level — concrete arch- and machine-specific MMIO range layouts are
63/// outside the verification surface, but the kernel allocator (which picks
64/// slots with `PageUsage::Unused`) is guaranteed disjoint from MMIO mappings.
65pub uninterp spec fn is_mmio_paddr(pa: Paddr) -> bool;
66
67/// Connects a slot's `PageUsage::MMIO` discriminant to its paddr's range
68/// membership. Used to derive disjointness between MMIO mappings and the
69/// regular allocator pool: a slot can be `MMIO` iff its paddr is in MMIO
70/// range, so a slot with `usage != MMIO` (e.g. `Unused`) cannot share an idx
71/// with any MMIO mapping.
72pub broadcast axiom fn axiom_mmio_usage_iff_mmio_paddr(slot: MetaSlotOwner)
73    ensures
74        (#[trigger] slot.usage == PageUsage::MMIO) <==> is_mmio_paddr(
75            meta_to_frame(slot.slot_vaddr),
76        ),
77;
78
79/// MMIO ranges are aligned to (and closed under) huge-page granularities:
80/// every sub-paddr within a huge frame inherits the huge frame's MMIO-ness.
81/// This is a hardware-layout convention — MMIO BARs are mapped at huge-page
82/// boundaries, and the verified `split_if_mapped_huge` relies on it to
83/// transfer MMIO-ness from a huge frame to its 4KB sub-pages. Non-broadcast:
84/// callers invoke this explicitly with the relevant `page_size`.
85pub axiom fn axiom_mmio_paddr_huge_page_closed(pa: Paddr, page_size: usize, offset: usize)
86    requires
87        pa % page_size == 0,
88        offset < page_size,
89    ensures
90        is_mmio_paddr((pa + offset) as Paddr) == is_mmio_paddr(pa),
91;
92
93pub struct StoredPageTablePageMeta {
94    pub nr_children: pcell_maybe_uninit::PCell<u16>,
95    pub stray: pcell_maybe_uninit::PCell<bool>,
96    pub level: PagingLevel,
97    pub lock: PAtomicU8,
98}
99
100pub enum MetaSlotStorage {
101    Empty([u8; 39]),
102    Untyped,
103    FrameLink(StoredLink),
104    PTNode(StoredPageTablePageMeta),
105}
106
107/// `MetaSlotStorage` is an inductive tagged union of all of the frame meta types that
108/// we work with in this development. So, it should itself implement `AnyFrameMeta`, and
109/// it can then be used to stand in for `dyn AnyFrameMeta`.
110unsafe impl AnyFrameMeta for MetaSlotStorage {
111    uninterp spec fn vtable_ptr(&self) -> usize;
112}
113
114impl Repr<MetaSlotStorage> for MetaSlotStorage {
115    type ReprPerm = ();
116
117    open spec fn wf(slot: MetaSlotStorage, perm: ()) -> bool {
118        true
119    }
120
121    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
122        (self, ())
123    }
124
125    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
126        self
127    }
128
129    open spec fn from_repr_spec(slot: MetaSlotStorage, perm: ()) -> Self {
130        slot
131    }
132
133    fn from_repr(slot: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
134        slot
135    }
136
137    fn from_borrowed<'a>(slot: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
138        slot
139    }
140
141    fn from_borrowed_mut<'a>(
142        slot: &'a mut MetaSlotStorage,
143        Tracked(perm): Tracked<&'a mut ()>,
144    ) -> &'a mut Self {
145        slot
146    }
147
148    proof fn from_to_repr(self, perm: ()) {
149    }
150
151    proof fn to_from_repr(slot: MetaSlotStorage, perm: ()) {
152    }
153
154    proof fn to_repr_wf(self, perm: ()) {
155    }
156}
157
158impl MetaSlotStorage {
159    pub open spec fn get_link_spec(self) -> Option<StoredLink> {
160        match self {
161            MetaSlotStorage::FrameLink(link) => Some(link),
162            _ => None,
163        }
164    }
165
166    #[verifier::when_used_as_spec(get_link_spec)]
167    pub fn get_link(self) -> (res: Option<StoredLink>)
168        ensures
169            res == self.get_link_spec(),
170    {
171        match self {
172            MetaSlotStorage::FrameLink(link) => Some(link),
173            _ => None,
174        }
175    }
176
177    pub open spec fn get_node_spec(self) -> Option<StoredPageTablePageMeta> {
178        match self {
179            MetaSlotStorage::PTNode(node) => Some(node),
180            _ => None,
181        }
182    }
183
184    #[verifier::when_used_as_spec(get_node_spec)]
185    pub fn get_node(self) -> (res: Option<StoredPageTablePageMeta>)
186        ensures
187            res == self.get_node_spec(),
188    {
189        match self {
190            MetaSlotStorage::PTNode(node) => Some(node),
191            _ => None,
192        }
193    }
194}
195
196/// Permissions whose initialized contents belong to one installed metadata
197/// value.
198pub tracked struct MetadataPerms {
199    pub storage_perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
200    pub vtable_ptr_perm: vstd::simple_pptr::PointsTo<usize>,
201}
202
203/// Well-formedness of a concrete metadata representation. The outer slot
204/// permission remains permanently in `MetaRegionOwners`; the metadata bundle
205/// describes the permissions tied to the currently installed metadata.
206pub open spec fn typed_meta_wf<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
207    points_to: vstd::simple_pptr::PointsTo<MetaSlot>,
208    metadata_perms: MetadataPerms,
209    repr_perm: M::ReprPerm,
210) -> bool {
211    &&& points_to.is_init()
212    &&& metadata_perms.storage_perm.is_init()
213    &&& metadata_perms.storage_perm.id() == points_to.value().storage.id()
214    &&& M::wf(metadata_perms.storage_perm.value(), repr_perm)
215}
216
217pub open spec fn typed_meta_value<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
218    metadata_perms: MetadataPerms,
219    repr_perm: M::ReprPerm,
220) -> M {
221    M::from_repr_spec(metadata_perms.storage_perm.value(), repr_perm)
222}
223
224pub fn borrow_meta<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
225    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
226    Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
227    Tracked(metadata_perms): Tracked<&'a MetadataPerms>,
228    Tracked(repr_perm): Tracked<&'a M::ReprPerm>,
229) -> (res: &'a M)
230    requires
231        typed_meta_wf::<M>(*points_to, *metadata_perms, *repr_perm),
232        ptr.addr() == points_to.addr(),
233    ensures
234        *res == typed_meta_value::<M>(*metadata_perms, *repr_perm),
235{
236    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(points_to));
237    M::from_borrowed(slot.storage.borrow(Tracked(&metadata_perms.storage_perm)), Tracked(repr_perm))
238}
239
240pub fn borrow_meta_mut<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
241    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
242    Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
243    Tracked(slot_owner): Tracked<&'a mut MetaSlotOwner>,
244    Tracked(repr_perm): Tracked<&'a mut M::ReprPerm>,
245) -> (res: &'a mut M)
246    requires
247        old(slot_owner).inv(),
248        points_to.value().wf(*old(slot_owner)),
249        typed_meta_wf::<M>(*points_to, old(slot_owner).metadata_perm, *old(repr_perm)),
250        ptr.addr() == points_to.addr(),
251    ensures
252        *res == typed_meta_value::<M>(old(slot_owner).metadata_perm, *old(repr_perm)),
253        final(slot_owner).inv(),
254        points_to.value().wf(*final(slot_owner)),
255        final(slot_owner).slot_vaddr == old(slot_owner).slot_vaddr,
256        final(slot_owner).usage == old(slot_owner).usage,
257        final(slot_owner).paths_in_pt == old(slot_owner).paths_in_pt,
258        final(slot_owner).ref_count_perm == old(slot_owner).ref_count_perm,
259        final(slot_owner).vtable_ptr_perm() == old(slot_owner).vtable_ptr_perm(),
260        final(slot_owner).in_list_perm == old(slot_owner).in_list_perm,
261        typed_meta_wf::<M>(*points_to, final(slot_owner).metadata_perm, *final(repr_perm)),
262        *final(res) == typed_meta_value::<M>(final(slot_owner).metadata_perm, *final(repr_perm)),
263{
264    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(points_to));
265    let tracked metadata_perms = slot_owner.tracked_borrow_mut_metadata_perms();
266    M::from_borrowed_mut(
267        slot.storage.borrow_mut(Tracked(&mut metadata_perms.storage_perm)),
268        Tracked(repr_perm),
269    )
270}
271
272/// Permissions that remain under the authority of `MetaRegionOwners`.
273///
274/// `ref_count` and `in_list` exist for the complete lifetime of the
275/// corresponding `MetaSlot` (i.e., `'static`).
276pub tracked struct MetaSlotOwner {
277    pub metadata_perm: MetadataPerms,
278    pub ref_count_perm: PermissionU64,
279    pub in_list_perm: PermissionU64,
280    pub ghost slot_vaddr: Vaddr,
281    pub ghost usage: PageUsage,
282    /// The set of tree paths at which this slot is referenced. For PT-node
283    /// slots this is a singleton. For data-frame slots this tracks every
284    /// location the frame is currently mapped — allowing a single frame to be
285    /// mapped at multiple addresses.
286    pub ghost paths_in_pt: Set<TreePath<NR_ENTRIES>>,
287}
288
289impl Inv for MetaSlotOwner {
290    open spec fn inv(self) -> bool {
291        // A managed slot at `REF_COUNT_UNUSED` is free — it has no live
292        // PTE mapping, since a mapping is itself a reference that would
293        // keep the count above the unused sentinel. Hence `paths_in_pt`
294        // is empty. Maintained by the teardown path: the sole transition
295        // *into* `UNUSED` is `drop_last_in_place`, whose
296        // `drop_last_in_place_safety_cond` requires an empty
297        // `paths_in_pt`. MMIO slots are excluded — they are not
298        // ref-counted as ordinary frames (an MMIO region may sit at the
299        // `UNUSED` sentinel while still mapped), exactly as the embedding
300        // accounting and the huge-page split loop invariant scope out
301        // `usage == MMIO`.
302        &&& self.ref_count() == REF_COUNT_UNUSED ==> {
303            &&& self.storage_perm().is_uninit()
304            &&& self.vtable_ptr_perm().is_uninit()
305            &&& self.in_list_perm.value() == 0
306            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
307        }
308        &&& self.ref_count() == REF_COUNT_UNIQUE ==> {
309            &&& self.vtable_ptr_perm().is_init()
310            &&& self.storage_perm().is_init()
311            // A UNIQUE non-MMIO slot has no live PTE mapping (same rationale as
312            // the UNUSED branch): a mapping would be a reference keeping the
313            // count above the unique sentinel. Lets the list-store embedding
314            // discharge `paths_in_pt.is_empty()` for linked-list frames.
315            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
316        }
317        // A SHARED slot (`0 < rc <= REF_COUNT_MAX`) is genuinely in use:
318        // metadata storage is written, `vtable_ptr` resolves the
319        // dynamic type, and the slot is *not* on the allocator's free
320        // list. `storage.is_init()` and `in_list.value() == 0` were
321        // previously asserted only in the `UNIQUE` branch and via the
322        // `rc == 1 ⟹ ...` guard on `Frame::drop_requires`; they are
323        // universally true of any in-use slot, so they live here. Once
324        // these are invariants, the embedding's `op_pre[FrameDrop]` can
325        // drop its `rc == 1 ⟹ storage.is_init ∧ in_list == 0` residual
326        // (it follows from `regions.inv() ⟹ slot_owners[idx].inv()`).
327        &&& 0 < self.ref_count() <= REF_COUNT_MAX ==> {
328            &&& self.vtable_ptr_perm().is_init()
329            &&& self.storage_perm().is_init()
330            &&& self.in_list_perm.value() == 0
331        }
332        &&& REF_COUNT_MAX < self.ref_count() < REF_COUNT_UNIQUE ==> { false }
333        &&& self.ref_count() == 0 ==> {
334            &&& self.in_list_perm.value() == 0
335        }
336        &&& FRAME_METADATA_RANGE.start <= self.slot_vaddr < FRAME_METADATA_RANGE.end
337        &&& self.slot_vaddr % META_SLOT_SIZE == 0
338    }
339}
340
341pub ghost struct MetaSlotModel {
342    pub status: MetaSlotStatus,
343    pub storage: MemContents<MetaSlotStorage>,
344    pub ref_count: u64,
345    pub vtable_ptr: MemContents<usize>,
346    pub in_list: u64,
347    pub slot_vaddr: Vaddr,
348    pub usage: PageUsage,
349}
350
351impl Inv for MetaSlotModel {
352    open spec fn inv(self) -> bool {
353        match self.ref_count {
354            REF_COUNT_UNUSED => {
355                &&& self.vtable_ptr.is_uninit()
356                &&& self.in_list == 0
357            },
358            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
359            0 => { &&& self.in_list == 0 },
360            _ if self.ref_count <= REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
361            _ => { false },
362        }
363    }
364}
365
366impl View for MetaSlotOwner {
367    type V = MetaSlotModel;
368
369    open spec fn view(&self) -> Self::V {
370        let storage = self.storage_perm().mem_contents();
371        let ref_count = self.ref_count();
372        let vtable_ptr = self.vtable_ptr_perm().mem_contents();
373        let in_list = self.in_list_perm.value();
374        let slot_vaddr = self.slot_vaddr;
375        let usage = self.usage;
376        let status = match ref_count {
377            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
378            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
379            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
380            _ if ref_count <= REF_COUNT_MAX => MetaSlotStatus::SHARED,
381            _ => MetaSlotStatus::OVERFLOW,
382        };
383        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, slot_vaddr, usage }
384    }
385}
386
387impl InvView for MetaSlotOwner {
388    proof fn view_preserves_inv(self) {
389    }
390}
391
392impl OwnerOf for MetaSlot {
393    type Owner = MetaSlotOwner;
394
395    open spec fn wf(self, owner: Self::Owner) -> bool {
396        &&& self.storage.id() == owner.storage_perm().id()
397        &&& self.ref_count.id() == owner.ref_count_perm.id()
398        &&& self.vtable_ptr == owner.vtable_ptr_perm().pptr()
399        &&& self.in_list.id() == owner.in_list_perm.id()
400    }
401}
402
403impl MetaSlotOwner {
404    pub open spec fn same_permissions(self, other: Self) -> bool {
405        &&& self.metadata_perm == other.metadata_perm
406        &&& self.ref_count_perm == other.ref_count_perm
407        &&& self.in_list_perm == other.in_list_perm
408    }
409
410    pub open spec fn ref_count(self) -> u64 {
411        self.ref_count_perm.value()
412    }
413
414    pub open spec fn storage_perm(self) -> pcell_maybe_uninit::PointsTo<MetaSlotStorage> {
415        self.metadata_perm.storage_perm
416    }
417
418    pub open spec fn vtable_ptr_perm(self) -> vstd::simple_pptr::PointsTo<usize> {
419        self.metadata_perm.vtable_ptr_perm
420    }
421
422    pub proof fn tracked_borrow_mut_metadata_perms(tracked &mut self) -> (tracked res:
423        &mut MetadataPerms)
424        ensures
425            *res == old(self).metadata_perm,
426            *final(self) == (Self { metadata_perm: *final(res), ..*old(self) }),
427    {
428        &mut self.metadata_perm
429    }
430}
431
432/// Writes `metadata` into the byte storage and establishes its direct
433/// `Repr<MetaSlotStorage>` interpretation.
434pub exec fn write_metadata_into_storage<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
435    cell: &pcell_maybe_uninit::PCell<MetaSlotStorage>,
436    Tracked(storage): Tracked<&mut pcell_maybe_uninit::PointsTo<MetaSlotStorage>>,
437    Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
438    metadata: M,
439)
440    requires
441        cell.id() == old(storage).id(),
442    ensures
443        final(storage).id() == old(storage).id(),
444        final(storage).is_init(),
445        M::wf(final(storage).value(), *final(repr_perm)),
446        M::from_repr_spec(final(storage).value(), *final(repr_perm)) == metadata,
447{
448    proof {
449        M::from_to_repr(metadata, *repr_perm);
450        M::to_repr_wf(metadata, *repr_perm);
451    }
452    let repr = metadata.to_repr(Tracked(repr_perm));
453    cell.write(Tracked(storage), repr);
454}
455
456} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
