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
158/// Permissions whose initialized contents belong to one installed metadata
159/// value.
160pub tracked struct MetadataPerms {
161    pub storage_perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
162    pub vtable_ptr_perm: vstd::simple_pptr::PointsTo<usize>,
163}
164
165/// Well-formedness of a concrete metadata representation. The outer slot
166/// permission remains permanently in `MetaRegionOwners`; the metadata bundle
167/// describes the permissions tied to the currently installed metadata.
168pub open spec fn typed_meta_wf<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
169    points_to: vstd::simple_pptr::PointsTo<MetaSlot>,
170    metadata_perms: MetadataPerms,
171    repr_perm: M::ReprPerm,
172) -> bool {
173    &&& points_to.is_init()
174    &&& metadata_perms.storage_perm.is_init()
175    &&& metadata_perms.storage_perm.id() == points_to.value().storage.id()
176    &&& M::wf(metadata_perms.storage_perm.value(), repr_perm)
177}
178
179pub open spec fn typed_meta_value<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
180    metadata_perms: MetadataPerms,
181    repr_perm: M::ReprPerm,
182) -> M {
183    M::from_repr_spec(metadata_perms.storage_perm.value(), repr_perm)
184}
185
186pub fn borrow_meta<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
187    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
188    Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
189    Tracked(metadata_perms): Tracked<&'a MetadataPerms>,
190    Tracked(repr_perm): Tracked<&'a M::ReprPerm>,
191) -> (res: &'a M)
192    requires
193        typed_meta_wf::<M>(*points_to, *metadata_perms, *repr_perm),
194        ptr.addr() == points_to.addr(),
195    ensures
196        *res == typed_meta_value::<M>(*metadata_perms, *repr_perm),
197{
198    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(points_to));
199    M::from_borrowed(slot.storage.borrow(Tracked(&metadata_perms.storage_perm)), Tracked(repr_perm))
200}
201
202pub fn borrow_meta_mut<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
203    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
204    Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
205    Tracked(slot_owner): Tracked<&'a mut MetaSlotOwner>,
206    Tracked(repr_perm): Tracked<&'a mut M::ReprPerm>,
207) -> (res: &'a mut M)
208    requires
209        old(slot_owner).inv(),
210        points_to.value().wf(*old(slot_owner)),
211        typed_meta_wf::<M>(*points_to, old(slot_owner).metadata_perm, *old(repr_perm)),
212        ptr.addr() == points_to.addr(),
213    ensures
214        *res == typed_meta_value::<M>(old(slot_owner).metadata_perm, *old(repr_perm)),
215        final(slot_owner).inv(),
216        points_to.value().wf(*final(slot_owner)),
217        final(slot_owner).slot_vaddr == old(slot_owner).slot_vaddr,
218        final(slot_owner).usage == old(slot_owner).usage,
219        final(slot_owner).paths_in_pt == old(slot_owner).paths_in_pt,
220        final(slot_owner).ref_count_perm == old(slot_owner).ref_count_perm,
221        final(slot_owner).vtable_ptr_perm() == old(slot_owner).vtable_ptr_perm(),
222        final(slot_owner).in_list_perm == old(slot_owner).in_list_perm,
223        typed_meta_wf::<M>(*points_to, final(slot_owner).metadata_perm, *final(repr_perm)),
224        *final(res) == typed_meta_value::<M>(final(slot_owner).metadata_perm, *final(repr_perm)),
225{
226    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(points_to));
227    let tracked metadata_perms = slot_owner.tracked_borrow_mut_metadata_perms();
228    M::from_borrowed_mut(
229        slot.storage.borrow_mut(Tracked(&mut metadata_perms.storage_perm)),
230        Tracked(repr_perm),
231    )
232}
233
234/// Permissions that remain under the authority of `MetaRegionOwners`.
235///
236/// `ref_count` and `in_list` exist for the complete lifetime of the
237/// corresponding `MetaSlot` (i.e., `'static`).
238pub tracked struct MetaSlotOwner {
239    pub metadata_perm: MetadataPerms,
240    pub ref_count_perm: PermissionU64,
241    pub in_list_perm: PermissionU64,
242    pub ghost slot_vaddr: Vaddr,
243    pub ghost usage: PageUsage,
244    /// The set of tree paths at which this slot is referenced. For PT-node
245    /// slots this is a singleton. For data-frame slots this tracks every
246    /// location the frame is currently mapped — allowing a single frame to be
247    /// mapped at multiple addresses.
248    pub ghost paths_in_pt: Set<TreePath<NR_ENTRIES>>,
249}
250
251impl Inv for MetaSlotOwner {
252    open spec fn inv(self) -> bool {
253        // A managed slot at `REF_COUNT_UNUSED` is free — it has no live
254        // PTE mapping, since a mapping is itself a reference that would
255        // keep the count above the unused sentinel. Hence `paths_in_pt`
256        // is empty. Maintained by the teardown path: the sole transition
257        // *into* `UNUSED` is `drop_last_in_place`, whose
258        // `drop_last_in_place_safety_cond` requires an empty
259        // `paths_in_pt`. MMIO slots are excluded — they are not
260        // ref-counted as ordinary frames (an MMIO region may sit at the
261        // `UNUSED` sentinel while still mapped), exactly as the embedding
262        // accounting and the huge-page split loop invariant scope out
263        // `usage == MMIO`.
264        &&& self.ref_count() == REF_COUNT_UNUSED ==> {
265            &&& self.storage_perm().is_uninit()
266            &&& self.vtable_ptr_perm().is_uninit()
267            &&& self.in_list_perm.value() == 0
268            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
269        }
270        &&& self.ref_count() == REF_COUNT_UNIQUE ==> {
271            &&& self.vtable_ptr_perm().is_init()
272            &&& self.storage_perm().is_init()
273            // A UNIQUE non-MMIO slot has no live PTE mapping (same rationale as
274            // the UNUSED branch): a mapping would be a reference keeping the
275            // count above the unique sentinel. Lets the list-store embedding
276            // discharge `paths_in_pt.is_empty()` for linked-list frames.
277            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
278        }
279        // A SHARED slot (`0 < rc <= REF_COUNT_MAX`) is genuinely in use:
280        // metadata storage is written, `vtable_ptr` resolves the
281        // dynamic type, and the slot is *not* on the allocator's free
282        // list. `storage.is_init()` and `in_list.value() == 0` were
283        // previously asserted only in the `UNIQUE` branch and via the
284        // `rc == 1 ⟹ ...` guard on `Frame::drop_requires`; they are
285        // universally true of any in-use slot, so they live here. Once
286        // these are invariants, the embedding's `op_pre[FrameDrop]` can
287        // drop its `rc == 1 ⟹ storage.is_init ∧ in_list == 0` residual
288        // (it follows from `regions.inv() ⟹ slot_owners[idx].inv()`).
289        &&& 0 < self.ref_count() <= REF_COUNT_MAX ==> {
290            &&& self.vtable_ptr_perm().is_init()
291            &&& self.storage_perm().is_init()
292            &&& self.in_list_perm.value() == 0
293        }
294        &&& REF_COUNT_MAX < self.ref_count() < REF_COUNT_UNIQUE ==> { false }
295        &&& self.ref_count() == 0 ==> {
296            &&& self.in_list_perm.value() == 0
297        }
298        &&& FRAME_METADATA_RANGE.start <= self.slot_vaddr < FRAME_METADATA_RANGE.end
299        &&& self.slot_vaddr % META_SLOT_SIZE == 0
300    }
301}
302
303pub ghost struct MetaSlotModel {
304    pub status: MetaSlotStatus,
305    pub storage: MemContents<MetaSlotStorage>,
306    pub ref_count: u64,
307    pub vtable_ptr: MemContents<usize>,
308    pub in_list: u64,
309    pub slot_vaddr: Vaddr,
310    pub usage: PageUsage,
311}
312
313impl Inv for MetaSlotModel {
314    open spec fn inv(self) -> bool {
315        match self.ref_count {
316            REF_COUNT_UNUSED => {
317                &&& self.vtable_ptr.is_uninit()
318                &&& self.in_list == 0
319            },
320            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
321            0 => { &&& self.in_list == 0 },
322            _ if self.ref_count <= REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
323            _ => { false },
324        }
325    }
326}
327
328impl View for MetaSlotOwner {
329    type V = MetaSlotModel;
330
331    open spec fn view(&self) -> Self::V {
332        let storage = self.storage_perm().mem_contents();
333        let ref_count = self.ref_count();
334        let vtable_ptr = self.vtable_ptr_perm().mem_contents();
335        let in_list = self.in_list_perm.value();
336        let slot_vaddr = self.slot_vaddr;
337        let usage = self.usage;
338        let status = match ref_count {
339            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
340            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
341            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
342            _ if ref_count <= REF_COUNT_MAX => MetaSlotStatus::SHARED,
343            _ => MetaSlotStatus::OVERFLOW,
344        };
345        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, slot_vaddr, usage }
346    }
347}
348
349impl InvView for MetaSlotOwner {
350    proof fn view_preserves_inv(self) {
351    }
352}
353
354impl OwnerOf for MetaSlot {
355    type Owner = MetaSlotOwner;
356
357    open spec fn wf(self, owner: Self::Owner) -> bool {
358        &&& self.storage.id() == owner.storage_perm().id()
359        &&& self.ref_count.id() == owner.ref_count_perm.id()
360        &&& self.vtable_ptr == owner.vtable_ptr_perm().pptr()
361        &&& self.in_list.id() == owner.in_list_perm.id()
362    }
363}
364
365impl MetaSlotOwner {
366    pub open spec fn same_permissions(self, other: Self) -> bool {
367        &&& self.metadata_perm == other.metadata_perm
368        &&& self.ref_count_perm == other.ref_count_perm
369        &&& self.in_list_perm == other.in_list_perm
370    }
371
372    pub open spec fn ref_count(self) -> u64 {
373        self.ref_count_perm.value()
374    }
375
376    pub open spec fn storage_perm(self) -> pcell_maybe_uninit::PointsTo<MetaSlotStorage> {
377        self.metadata_perm.storage_perm
378    }
379
380    pub open spec fn vtable_ptr_perm(self) -> vstd::simple_pptr::PointsTo<usize> {
381        self.metadata_perm.vtable_ptr_perm
382    }
383
384    pub proof fn tracked_borrow_mut_metadata_perms(tracked &mut self) -> (tracked res:
385        &mut MetadataPerms)
386        ensures
387            *res == old(self).metadata_perm,
388            *final(self) == (Self { metadata_perm: *final(res), ..*old(self) }),
389    {
390        &mut self.metadata_perm
391    }
392}
393
394/// Writes `metadata` into the byte storage and establishes its direct
395/// `Repr<MetaSlotStorage>` interpretation.
396pub exec fn write_metadata_into_storage<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
397    cell: &pcell_maybe_uninit::PCell<MetaSlotStorage>,
398    Tracked(storage): Tracked<&mut pcell_maybe_uninit::PointsTo<MetaSlotStorage>>,
399    Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
400    metadata: M,
401)
402    requires
403        cell.id() == old(storage).id(),
404    ensures
405        final(storage).id() == old(storage).id(),
406        final(storage).is_init(),
407        M::wf(final(storage).value(), *final(repr_perm)),
408        M::from_repr_spec(final(storage).value(), *final(repr_perm)) == metadata,
409{
410    proof {
411        M::from_to_repr(metadata, *repr_perm);
412        M::to_repr_wf(metadata, *repr_perm);
413    }
414    let repr = metadata.to_repr(Tracked(repr_perm));
415    cell.write(Tracked(storage), repr);
416}
417
418} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
