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 Perm = ();
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    proof fn from_to_repr(self, perm: ()) {
142    }
143
144    proof fn to_from_repr(slot: MetaSlotStorage, perm: ()) {
145    }
146
147    proof fn to_repr_wf(self, perm: ()) {
148    }
149}
150
151impl MetaSlotStorage {
152    pub open spec fn get_link_spec(self) -> Option<StoredLink> {
153        match self {
154            MetaSlotStorage::FrameLink(link) => Some(link),
155            _ => None,
156        }
157    }
158
159    #[verifier::when_used_as_spec(get_link_spec)]
160    pub fn get_link(self) -> (res: Option<StoredLink>)
161        ensures
162            res == self.get_link_spec(),
163    {
164        match self {
165            MetaSlotStorage::FrameLink(link) => Some(link),
166            _ => None,
167        }
168    }
169
170    pub open spec fn get_node_spec(self) -> Option<StoredPageTablePageMeta> {
171        match self {
172            MetaSlotStorage::PTNode(node) => Some(node),
173            _ => None,
174        }
175    }
176
177    #[verifier::when_used_as_spec(get_node_spec)]
178    pub fn get_node(self) -> (res: Option<StoredPageTablePageMeta>)
179        ensures
180            res == self.get_node_spec(),
181    {
182        match self {
183            MetaSlotStorage::PTNode(node) => Some(node),
184            _ => None,
185        }
186    }
187}
188
189pub tracked struct MetadataInnerPerms {
190    pub storage: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
191    pub ref_count: PermissionU64,
192    pub vtable_ptr: vstd::simple_pptr::PointsTo<usize>,
193    pub in_list: PermissionU64,
194}
195
196pub tracked struct MetaSlotOwner {
197    pub inner_perms: MetadataInnerPerms,
198    pub ghost slot_vaddr: Vaddr,
199    pub ghost usage: PageUsage,
200    /// The set of tree paths at which this slot is referenced. For PT-node
201    /// slots this is a singleton. For data-frame slots this tracks every
202    /// location the frame is currently mapped — allowing a single frame to be
203    /// mapped at multiple addresses.
204    pub ghost paths_in_pt: Set<TreePath<NR_ENTRIES>>,
205}
206
207impl Inv for MetaSlotOwner {
208    open spec fn inv(self) -> bool {
209        // A managed slot at `REF_COUNT_UNUSED` is free — it has no live
210        // PTE mapping, since a mapping is itself a reference that would
211        // keep the count above the unused sentinel. Hence `paths_in_pt`
212        // is empty. Maintained by the teardown path: the sole transition
213        // *into* `UNUSED` is `drop_last_in_place`, whose
214        // `drop_last_in_place_safety_cond` requires an empty
215        // `paths_in_pt`. MMIO slots are excluded — they are not
216        // ref-counted as ordinary frames (an MMIO region may sit at the
217        // `UNUSED` sentinel while still mapped), exactly as the embedding
218        // accounting and the huge-page split loop invariant scope out
219        // `usage == MMIO`.
220        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNUSED ==> {
221            &&& self.inner_perms.storage.is_uninit()
222            &&& self.inner_perms.vtable_ptr.is_uninit()
223            &&& self.inner_perms.in_list.value() == 0
224            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
225        }
226        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNIQUE ==> {
227            &&& self.inner_perms.vtable_ptr.is_init()
228            &&& self.inner_perms.storage.is_init()
229            // A UNIQUE non-MMIO slot has no live PTE mapping (same rationale as
230            // the UNUSED branch): a mapping would be a reference keeping the
231            // count above the unique sentinel. Lets the list-store embedding
232            // discharge `paths_in_pt.is_empty()` for linked-list frames.
233            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
234        }
235        // A SHARED slot (`0 < rc <= REF_COUNT_MAX`) is genuinely in use:
236        // metadata storage is written, `vtable_ptr` resolves the
237        // dynamic type, and the slot is *not* on the allocator's free
238        // list. `storage.is_init()` and `in_list.value() == 0` were
239        // previously asserted only in the `UNIQUE` branch and via the
240        // `rc == 1 ⟹ ...` guard on `Frame::drop_requires`; they are
241        // universally true of any in-use slot, so they live here. Once
242        // these are invariants, the embedding's `op_pre[FrameDrop]` can
243        // drop its `rc == 1 ⟹ storage.is_init ∧ in_list == 0` residual
244        // (it follows from `regions.inv() ⟹ slot_owners[idx].inv()`).
245        &&& 0 < self.inner_perms.ref_count.value() <= REF_COUNT_MAX ==> {
246            &&& self.inner_perms.vtable_ptr.is_init()
247            &&& self.inner_perms.storage.is_init()
248            &&& self.inner_perms.in_list.value() == 0
249        }
250        &&& REF_COUNT_MAX < self.inner_perms.ref_count.value() < REF_COUNT_UNIQUE ==> { false }
251        &&& self.inner_perms.ref_count.value() == 0 ==> {
252            &&& self.inner_perms.in_list.value() == 0
253        }
254        &&& FRAME_METADATA_RANGE.start <= self.slot_vaddr < FRAME_METADATA_RANGE.end
255        &&& self.slot_vaddr % META_SLOT_SIZE == 0
256    }
257}
258
259pub ghost struct MetaSlotModel {
260    pub status: MetaSlotStatus,
261    pub storage: MemContents<MetaSlotStorage>,
262    pub ref_count: u64,
263    pub vtable_ptr: MemContents<usize>,
264    pub in_list: u64,
265    pub slot_vaddr: Vaddr,
266    pub usage: PageUsage,
267}
268
269impl Inv for MetaSlotModel {
270    open spec fn inv(self) -> bool {
271        match self.ref_count {
272            REF_COUNT_UNUSED => {
273                &&& self.vtable_ptr.is_uninit()
274                &&& self.in_list == 0
275            },
276            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
277            0 => { &&& self.in_list == 0 },
278            _ if self.ref_count <= REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
279            _ => { false },
280        }
281    }
282}
283
284impl View for MetaSlotOwner {
285    type V = MetaSlotModel;
286
287    open spec fn view(&self) -> Self::V {
288        let storage = self.inner_perms.storage.mem_contents();
289        let ref_count = self.inner_perms.ref_count.value();
290        let vtable_ptr = self.inner_perms.vtable_ptr.mem_contents();
291        let in_list = self.inner_perms.in_list.value();
292        let slot_vaddr = self.slot_vaddr;
293        let usage = self.usage;
294        let status = match ref_count {
295            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
296            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
297            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
298            _ if ref_count <= REF_COUNT_MAX => MetaSlotStatus::SHARED,
299            _ => MetaSlotStatus::OVERFLOW,
300        };
301        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, slot_vaddr, usage }
302    }
303}
304
305impl InvView for MetaSlotOwner {
306    proof fn view_preserves_inv(self) {
307    }
308}
309
310impl OwnerOf for MetaSlot {
311    type Owner = MetaSlotOwner;
312
313    open spec fn wf(self, owner: Self::Owner) -> bool {
314        &&& self.storage.id() == owner.inner_perms.storage.id()
315        &&& self.ref_count.id() == owner.inner_perms.ref_count.id()
316        &&& self.vtable_ptr == owner.inner_perms.vtable_ptr.pptr()
317        &&& self.in_list.id() == owner.inner_perms.in_list.id()
318    }
319}
320
321impl MetaSlotOwner {
322    pub proof fn tracked_borrow_mut_inner_perms(tracked &mut self) -> (tracked res:
323        &mut MetadataInnerPerms)
324        ensures
325            *res == old(self).inner_perms,
326            *final(self) == (Self { inner_perms: *final(res), ..*old(self) }),
327    {
328        &mut self.inner_perms
329    }
330}
331
332pub struct Metadata<M: AnyFrameMeta + Repr<MetaSlotStorage>> {
333    pub metadata: M,
334    pub ref_count: u64,
335    pub vtable_ptr: MemContents<usize>,
336    pub in_list: u64,
337}
338
339impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M> {
340    /// The metadata value is an abstract function of the inner permissions,
341    /// since extracting `M` from `MetaSlotStorage` requires `M::Perm` which
342    /// is not stored in `MetadataInnerPerms`.
343    pub uninterp spec fn metadata_from_inner_perms(
344        perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
345    ) -> M;
346
347    /// Inverse of [`metadata_from_inner_perms`]: given an `M` and a base
348    /// storage permission, produce a new permission with the same cell id
349    /// whose `metadata_from_inner_perms` interpretation yields `m`.
350    pub uninterp spec fn inner_perms_from_metadata(
351        m: M,
352        base: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
353    ) -> pcell_maybe_uninit::PointsTo<MetaSlotStorage>;
354
355    /// Axiomatic roundtrip laws for the metadata ↔ storage-perm pair. The
356    /// conversion is a transmute / reinterpret at exec level, so these laws
357    /// live at the `cast_ptr` trust boundary.
358    pub axiom fn metadata_perms_inverse(m: M, base: pcell_maybe_uninit::PointsTo<MetaSlotStorage>)
359        ensures
360            Self::metadata_from_inner_perms(Self::inner_perms_from_metadata(m, base)) == m,
361            Self::inner_perms_from_metadata(m, base).id() == base.id(),
362            Self::inner_perms_from_metadata(m, base).is_init(),
363    ;
364
365    pub axiom fn inner_perms_from_metadata_roundtrip(
366        perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
367    )
368        ensures
369            Self::inner_perms_from_metadata(Self::metadata_from_inner_perms(perm), perm) == perm,
370    ;
371
372    /// Proof-level companion: given a storage perm that has been initialized
373    /// with some (arbitrary) `MetaSlotStorage` value, advance it to the
374    /// spec form `inner_perms_from_metadata(m, *old(perm))`. This is the
375    /// proof-side step for writing `m` into the cell — it bridges the raw
376    /// `PCell::write` of a `MetaSlotStorage` value to the spec encoding.
377    /// Combined with [`Self::metadata_perms_inverse`], it lets a real exec
378    /// write discharge the `metadata_from_inner_perms == m` post.
379    #[verifier::external_body]
380    pub proof fn switch_perm_to_inner_perms_from_metadata(
381        tracked perm: &mut pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
382        m: M,
383    )
384        requires
385            old(perm).is_init(),
386        ensures
387            *final(perm) == Self::inner_perms_from_metadata(m, *old(perm)),
388    {
389    }
390
391    /// Exec-level write primitive: writing `metadata` into the storage cell
392    /// yields a perm whose `metadata_from_inner_perms` interpretation is
393    /// exactly `metadata`.
394    pub exec fn write_metadata_into_storage(
395        cell: &pcell_maybe_uninit::PCell<MetaSlotStorage>,
396        Tracked(perm): Tracked<&mut pcell_maybe_uninit::PointsTo<MetaSlotStorage>>,
397        metadata: M,
398    )
399        requires
400            cell.id() == old(perm).id(),
401        ensures
402            final(perm).id() == old(perm).id(),
403            final(perm).is_init(),
404            Self::metadata_from_inner_perms(*final(perm)) == metadata,
405    {
406        // Raw cell write — any well-formed `MetaSlotStorage` value initialises
407        // the cell. The spec-level decoding is unspecified for this raw value;
408        // the proof step below reinterprets the perm so it decodes to `metadata`.
409        cell.write(Tracked(perm), MetaSlotStorage::Untyped);
410        proof {
411            let ghost base = *perm;
412            Self::switch_perm_to_inner_perms_from_metadata(perm, metadata);
413            Self::metadata_perms_inverse(metadata, base);
414        }
415    }
416}
417
418/// Value-updaters for the opaque tracked permission types inside
419/// [`MetadataInnerPerms`]. Each uninterp operation produces a new permission
420/// with the same id as the input but a specified value; the paired axioms
421/// document the expected behavior. The conversions are implemented in exec
422/// by `external_body` primitives, so the laws are axiomatic.
423pub uninterp spec fn perm_u64_with(p: PermissionU64, v: u64) -> PermissionU64;
424
425pub axiom fn perm_u64_with_value(p: PermissionU64, v: u64)
426    ensures
427        perm_u64_with(p, v).value() == v,
428        perm_u64_with(p, v).id() == p.id(),
429;
430
431/// Setting a `PermissionU64` to its own current value is a no-op.
432pub axiom fn perm_u64_with_identity(p: PermissionU64)
433    ensures
434        perm_u64_with(p, p.value()) == p,
435;
436
437pub uninterp spec fn pptr_usize_with(
438    p: vstd::simple_pptr::PointsTo<usize>,
439    c: MemContents<usize>,
440) -> vstd::simple_pptr::PointsTo<usize>;
441
442pub axiom fn pptr_usize_with_value(p: vstd::simple_pptr::PointsTo<usize>, c: MemContents<usize>)
443    ensures
444        pptr_usize_with(p, c).mem_contents() == c,
445        pptr_usize_with(p, c).pptr() == p.pptr(),
446;
447
448/// Setting a `PointsTo<usize>` to its own contents is a no-op.
449pub axiom fn pptr_usize_with_identity(p: vstd::simple_pptr::PointsTo<usize>)
450    ensures
451        pptr_usize_with(p, p.mem_contents()) == p,
452;
453
454/// Reconstruct a [`MetaSlot`] from its underlying cell ids. The exec
455/// implementation is a cast; the laws pin `.id()` / `.pptr()` equalities.
456pub uninterp spec fn meta_slot_from_perm(perm: MetadataInnerPerms) -> MetaSlot;
457
458pub axiom fn meta_slot_from_perm_ids(perm: MetadataInnerPerms)
459    ensures
460        meta_slot_from_perm(perm).storage.id() == perm.storage.id(),
461        meta_slot_from_perm(perm).ref_count.id() == perm.ref_count.id(),
462        meta_slot_from_perm(perm).vtable_ptr == perm.vtable_ptr.pptr(),
463        meta_slot_from_perm(perm).in_list.id() == perm.in_list.id(),
464;
465
466/// A `MetaSlot` is uniquely determined by its cell ids + vtable_ptr address.
467/// This is a structural fact about the opaque atomic/cell primitives — two
468/// `MetaSlot` values whose ids agree on every field are equal.
469pub axiom fn meta_slot_eq_by_ids(a: MetaSlot, b: MetaSlot)
470    ensures
471        (a.storage.id() == b.storage.id() && a.ref_count.id() == b.ref_count.id() && a.vtable_ptr
472            == b.vtable_ptr && a.in_list.id() == b.in_list.id()) ==> a == b,
473;
474
475impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M> {
476    type Perm = MetadataInnerPerms;
477
478    open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool {
479        &&& perm.storage.id() == r.storage.id()
480        &&& perm.ref_count.id() == r.ref_count.id()
481        &&& perm.vtable_ptr.pptr() == r.vtable_ptr
482        &&& perm.in_list.id() == r.in_list.id()
483    }
484
485    open spec fn to_repr_spec(self, perm: MetadataInnerPerms) -> (MetaSlot, MetadataInnerPerms) {
486        let new_perm = MetadataInnerPerms {
487            storage: Self::inner_perms_from_metadata(self.metadata, perm.storage),
488            ref_count: perm_u64_with(perm.ref_count, self.ref_count),
489            vtable_ptr: pptr_usize_with(perm.vtable_ptr, self.vtable_ptr),
490            in_list: perm_u64_with(perm.in_list, self.in_list),
491        };
492        (meta_slot_from_perm(new_perm), new_perm)
493    }
494
495    #[verifier::external_body]
496    fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot {
497        unimplemented!()
498    }
499
500    open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self {
501        Metadata {
502            metadata: Self::metadata_from_inner_perms(perm.storage),
503            ref_count: perm.ref_count.value(),
504            vtable_ptr: perm.vtable_ptr.mem_contents(),
505            in_list: perm.in_list.value(),
506        }
507    }
508
509    #[verifier::external_body]
510    fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self {
511        unimplemented!()
512    }
513
514    #[verifier::external_body]
515    fn from_borrowed<'a>(
516        r: &'a MetaSlot,
517        Tracked(perm): Tracked<&'a MetadataInnerPerms>,
518    ) -> &'a Self {
519        unimplemented!()
520    }
521
522    proof fn from_to_repr(self, perm: MetadataInnerPerms) {
523        Self::metadata_perms_inverse(self.metadata, perm.storage);
524        perm_u64_with_value(perm.ref_count, self.ref_count);
525        perm_u64_with_value(perm.in_list, self.in_list);
526        pptr_usize_with_value(perm.vtable_ptr, self.vtable_ptr);
527        let (r, np) = self.to_repr_spec(perm);
528    }
529
530    proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms) {
531        // wf(r, perm) gives us: r's ids match perm's ids; r.vtable_ptr == perm.vtable_ptr.pptr().
532        Self::inner_perms_from_metadata_roundtrip(perm.storage);
533        perm_u64_with_identity(perm.ref_count);
534        perm_u64_with_identity(perm.in_list);
535        pptr_usize_with_identity(perm.vtable_ptr);
536        // Each field of np2 equals the corresponding field of perm:
537        //   np2.storage    = inner_perms_from_metadata(metadata_from_inner_perms(perm.storage), perm.storage)
538        //                  = perm.storage                   (inner_perms_from_metadata_roundtrip)
539        //   np2.ref_count  = perm_u64_with(perm.ref_count, perm.ref_count.value())
540        //                  = perm.ref_count                 (perm_u64_with_identity)
541        //   np2.vtable_ptr = pptr_usize_with(perm.vtable_ptr, perm.vtable_ptr.mem_contents())
542        //                  = perm.vtable_ptr                (pptr_usize_with_identity)
543        //   np2.in_list    = perm.in_list                   (perm_u64_with_identity)
544        let md = Self::from_repr_spec(r, perm);
545        let (r2, np2) = md.to_repr_spec(perm);
546        // r2 is produced from np2 == perm; its ids match perm's; perm's ids match r's (by wf).
547        meta_slot_from_perm_ids(np2);
548        meta_slot_eq_by_ids(r2, r);
549    }
550
551    proof fn to_repr_wf(self, perm: MetadataInnerPerms) {
552        let (r, np) = self.to_repr_spec(perm);
553        meta_slot_from_perm_ids(np);
554        Self::metadata_perms_inverse(self.metadata, perm.storage);
555        perm_u64_with_value(perm.ref_count, self.ref_count);
556        perm_u64_with_value(perm.in_list, self.in_list);
557        pptr_usize_with_value(perm.vtable_ptr, self.vtable_ptr);
558        // wf checks id equality between np's perms and r's slot fields.
559    }
560}
561
562/// A permission token for frame metadata.
563///
564/// [`Frame<M>`] the high-level representation of the low-level pointer
565/// to the [`super::meta::MetaSlot`].
566pub type MetaPerm<M  /*: AnyFrameMeta + Repr<MetaSlotStorage>*/ > =
567    cast_ptr::PointsTo<MetaSlot, Metadata<M>>;
568
569} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
