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::AnyFrameMeta;
16use crate::mm::frame::meta::{
17    META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
18    mapping::meta_to_frame,
19};
20use crate::mm::kspace::FRAME_METADATA_RANGE;
21use crate::mm::{Paddr, PagingLevel, Vaddr};
22use crate::specs::arch::NR_ENTRIES;
23use crate::specs::mm::frame::linked_list::linked_list_owners::StoredLink;
24
25verus! {
26
27#[allow(non_camel_case_types)]
28pub ghost enum MetaSlotStatus {
29    UNUSED,
30    UNIQUE,
31    SHARED,
32    OVERFLOW,
33    UNDER_CONSTRUCTION,
34}
35
36pub ghost enum PageUsage {
37    // The zero variant is reserved for the unused type. Only an unused page
38    // can be designated for one of the other purposes.
39    Unused,
40    /// The page is reserved or unusable. The kernel should not touch it.
41    Reserved,
42    /// The page is used as a frame, i.e., a page of untyped memory.
43    Frame,
44    /// The page is used by a page table.
45    PageTable,
46    /// The page stores metadata of other pages.
47    Meta,
48    /// The page stores the kernel such as kernel code, data, etc.
49    Kernel,
50    /// The page maps memory-mapped I/O (MMIO). Untracked: no refcount, slot
51    /// stays in the free pool, but distinguishable from `Unused` so the
52    /// kernel allocator never collides with an MMIO mapping.
53    MMIO,
54}
55
56/// Whether `pa` falls in an MMIO physical-address range. Uninterpreted at the
57/// spec level — concrete arch- and machine-specific MMIO range layouts are
58/// outside the verification surface, but the kernel allocator (which picks
59/// slots with `PageUsage::Unused`) is guaranteed disjoint from MMIO mappings.
60pub uninterp spec fn is_mmio_paddr(pa: Paddr) -> bool;
61
62/// Connects a slot's `PageUsage::MMIO` discriminant to its paddr's range
63/// membership. Used to derive disjointness between MMIO mappings and the
64/// regular allocator pool: a slot can be `MMIO` iff its paddr is in MMIO
65/// range, so a slot with `usage != MMIO` (e.g. `Unused`) cannot share an idx
66/// with any MMIO mapping.
67pub broadcast axiom fn axiom_mmio_usage_iff_mmio_paddr(slot: MetaSlotOwner)
68    ensures
69        (#[trigger] slot.usage == PageUsage::MMIO) <==> is_mmio_paddr(
70            meta_to_frame(slot.slot_vaddr),
71        ),
72;
73
74/// MMIO ranges are aligned to (and closed under) huge-page granularities:
75/// every sub-paddr within a huge frame inherits the huge frame's MMIO-ness.
76/// This is a hardware-layout convention — MMIO BARs are mapped at huge-page
77/// boundaries, and the verified `split_if_mapped_huge` relies on it to
78/// transfer MMIO-ness from a huge frame to its 4KB sub-pages. Non-broadcast:
79/// callers invoke this explicitly with the relevant `page_size`.
80pub axiom fn axiom_mmio_paddr_huge_page_closed(pa: Paddr, page_size: usize, offset: usize)
81    requires
82        pa % page_size == 0,
83        offset < page_size,
84    ensures
85        is_mmio_paddr((pa + offset) as Paddr) == is_mmio_paddr(pa),
86;
87
88pub struct StoredPageTablePageMeta {
89    pub nr_children: pcell_maybe_uninit::PCell<u16>,
90    pub stray: pcell_maybe_uninit::PCell<bool>,
91    pub level: PagingLevel,
92    pub lock: PAtomicU8,
93}
94
95pub enum MetaSlotStorage {
96    Empty([u8; 39]),
97    Untyped,
98    FrameLink(StoredLink),
99    PTNode(StoredPageTablePageMeta),
100}
101
102/// `MetaSlotStorage` is an inductive tagged union of all of the frame meta types that
103/// we work with in this development. So, it should itself implement `AnyFrameMeta`, and
104/// it can then be used to stand in for `dyn AnyFrameMeta`.
105unsafe impl AnyFrameMeta for MetaSlotStorage {
106    uninterp spec fn vtable_ptr(&self) -> usize;
107}
108
109impl Repr<MetaSlotStorage> for MetaSlotStorage {
110    type Perm = ();
111
112    open spec fn wf(slot: MetaSlotStorage, perm: ()) -> bool {
113        true
114    }
115
116    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
117        (self, ())
118    }
119
120    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
121        self
122    }
123
124    open spec fn from_repr_spec(slot: MetaSlotStorage, perm: ()) -> Self {
125        slot
126    }
127
128    fn from_repr(slot: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
129        slot
130    }
131
132    fn from_borrowed<'a>(slot: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
133        slot
134    }
135
136    proof fn from_to_repr(self, perm: ()) {
137    }
138
139    proof fn to_from_repr(slot: MetaSlotStorage, perm: ()) {
140    }
141
142    proof fn to_repr_wf(self, perm: ()) {
143    }
144}
145
146impl MetaSlotStorage {
147    pub open spec fn get_link_spec(self) -> Option<StoredLink> {
148        match self {
149            MetaSlotStorage::FrameLink(link) => Some(link),
150            _ => None,
151        }
152    }
153
154    #[verifier::when_used_as_spec(get_link_spec)]
155    pub fn get_link(self) -> (res: Option<StoredLink>)
156        ensures
157            res == self.get_link_spec(),
158    {
159        match self {
160            MetaSlotStorage::FrameLink(link) => Some(link),
161            _ => None,
162        }
163    }
164
165    pub open spec fn get_node_spec(self) -> Option<StoredPageTablePageMeta> {
166        match self {
167            MetaSlotStorage::PTNode(node) => Some(node),
168            _ => None,
169        }
170    }
171
172    #[verifier::when_used_as_spec(get_node_spec)]
173    pub fn get_node(self) -> (res: Option<StoredPageTablePageMeta>)
174        ensures
175            res == self.get_node_spec(),
176    {
177        match self {
178            MetaSlotStorage::PTNode(node) => Some(node),
179            _ => None,
180        }
181    }
182}
183
184pub tracked struct MetadataInnerPerms {
185    pub storage: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
186    pub ref_count: PermissionU64,
187    pub vtable_ptr: vstd::simple_pptr::PointsTo<usize>,
188    pub in_list: PermissionU64,
189}
190
191pub tracked struct MetaSlotOwner {
192    pub inner_perms: MetadataInnerPerms,
193    pub ghost slot_vaddr: Vaddr,
194    pub ghost usage: PageUsage,
195    /// The set of tree paths at which this slot is referenced. For PT-node
196    /// slots this is a singleton. For data-frame slots this tracks every
197    /// location the frame is currently mapped — allowing a single frame to be
198    /// mapped at multiple addresses.
199    pub ghost paths_in_pt: Set<TreePath<NR_ENTRIES>>,
200}
201
202impl Inv for MetaSlotOwner {
203    open spec fn inv(self) -> bool {
204        // A managed slot at `REF_COUNT_UNUSED` is free — it has no live
205        // PTE mapping, since a mapping is itself a reference that would
206        // keep the count above the unused sentinel. Hence `paths_in_pt`
207        // is empty. Maintained by the teardown path: the sole transition
208        // *into* `UNUSED` is `drop_last_in_place`, whose
209        // `drop_last_in_place_safety_cond` requires an empty
210        // `paths_in_pt`. MMIO slots are excluded — they are not
211        // ref-counted as ordinary frames (an MMIO region may sit at the
212        // `UNUSED` sentinel while still mapped), exactly as the embedding
213        // accounting and the huge-page split loop invariant scope out
214        // `usage == MMIO`.
215        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNUSED ==> {
216            &&& self.inner_perms.storage.is_uninit()
217            &&& self.inner_perms.vtable_ptr.is_uninit()
218            &&& self.inner_perms.in_list.value() == 0
219            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
220        }
221        &&& self.inner_perms.ref_count.value() == REF_COUNT_UNIQUE ==> {
222            &&& self.inner_perms.vtable_ptr.is_init()
223            &&& self.inner_perms.storage.is_init()
224            // A UNIQUE non-MMIO slot has no live PTE mapping (same rationale as
225            // the UNUSED branch): a mapping would be a reference keeping the
226            // count above the unique sentinel. Lets the list-store embedding
227            // discharge `paths_in_pt.is_empty()` for linked-list frames.
228            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
229        }
230        // A SHARED slot (`0 < rc <= REF_COUNT_MAX`) is genuinely in use:
231        // metadata storage is written, `vtable_ptr` resolves the
232        // dynamic type, and the slot is *not* on the allocator's free
233        // list. `storage.is_init()` and `in_list.value() == 0` were
234        // previously asserted only in the `UNIQUE` branch and via the
235        // `rc == 1 ⟹ ...` guard on `Frame::drop_requires`; they are
236        // universally true of any in-use slot, so they live here. Once
237        // these are invariants, the embedding's `op_pre[FrameDrop]` can
238        // drop its `rc == 1 ⟹ storage.is_init ∧ in_list == 0` residual
239        // (it follows from `regions.inv() ⟹ slot_owners[idx].inv()`).
240        &&& 0 < self.inner_perms.ref_count.value() <= REF_COUNT_MAX ==> {
241            &&& self.inner_perms.vtable_ptr.is_init()
242            &&& self.inner_perms.storage.is_init()
243            &&& self.inner_perms.in_list.value() == 0
244        }
245        &&& REF_COUNT_MAX < self.inner_perms.ref_count.value() < REF_COUNT_UNIQUE ==> { false }
246        &&& self.inner_perms.ref_count.value() == 0 ==> {
247            &&& self.inner_perms.in_list.value() == 0
248        }
249        &&& FRAME_METADATA_RANGE.start <= self.slot_vaddr < FRAME_METADATA_RANGE.end
250        &&& self.slot_vaddr % META_SLOT_SIZE == 0
251    }
252}
253
254pub ghost struct MetaSlotModel {
255    pub status: MetaSlotStatus,
256    pub storage: MemContents<MetaSlotStorage>,
257    pub ref_count: u64,
258    pub vtable_ptr: MemContents<usize>,
259    pub in_list: u64,
260    pub slot_vaddr: Vaddr,
261    pub usage: PageUsage,
262}
263
264impl Inv for MetaSlotModel {
265    open spec fn inv(self) -> bool {
266        match self.ref_count {
267            REF_COUNT_UNUSED => {
268                &&& self.vtable_ptr.is_uninit()
269                &&& self.in_list == 0
270            },
271            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
272            0 => { &&& self.in_list == 0 },
273            _ if self.ref_count <= REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
274            _ => { false },
275        }
276    }
277}
278
279impl View for MetaSlotOwner {
280    type V = MetaSlotModel;
281
282    open spec fn view(&self) -> Self::V {
283        let storage = self.inner_perms.storage.mem_contents();
284        let ref_count = self.inner_perms.ref_count.value();
285        let vtable_ptr = self.inner_perms.vtable_ptr.mem_contents();
286        let in_list = self.inner_perms.in_list.value();
287        let slot_vaddr = self.slot_vaddr;
288        let usage = self.usage;
289        let status = match ref_count {
290            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
291            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
292            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
293            _ if ref_count <= REF_COUNT_MAX => MetaSlotStatus::SHARED,
294            _ => MetaSlotStatus::OVERFLOW,
295        };
296        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, slot_vaddr, usage }
297    }
298}
299
300impl InvView for MetaSlotOwner {
301    proof fn view_preserves_inv(self) {
302    }
303}
304
305impl OwnerOf for MetaSlot {
306    type Owner = MetaSlotOwner;
307
308    open spec fn wf(self, owner: Self::Owner) -> bool {
309        &&& self.storage.id() == owner.inner_perms.storage.id()
310        &&& self.ref_count.id() == owner.inner_perms.ref_count.id()
311        &&& self.vtable_ptr == owner.inner_perms.vtable_ptr.pptr()
312        &&& self.in_list.id() == owner.inner_perms.in_list.id()
313    }
314}
315
316impl MetaSlotOwner {
317    pub proof fn tracked_borrow_mut_inner_perms(tracked &mut self) -> (tracked res:
318        &mut MetadataInnerPerms)
319        ensures
320            *res == old(self).inner_perms,
321            *final(self) == (Self { inner_perms: *final(res), ..*old(self) }),
322    {
323        &mut self.inner_perms
324    }
325}
326
327pub struct Metadata<M: AnyFrameMeta + Repr<MetaSlotStorage>> {
328    pub metadata: M,
329    pub ref_count: u64,
330    pub vtable_ptr: MemContents<usize>,
331    pub in_list: u64,
332}
333
334impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M> {
335    /// The metadata value is an abstract function of the inner permissions,
336    /// since extracting `M` from `MetaSlotStorage` requires `M::Perm` which
337    /// is not stored in `MetadataInnerPerms`.
338    pub uninterp spec fn metadata_from_inner_perms(
339        perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
340    ) -> M;
341
342    /// Inverse of [`metadata_from_inner_perms`]: given an `M` and a base
343    /// storage permission, produce a new permission with the same cell id
344    /// whose `metadata_from_inner_perms` interpretation yields `m`.
345    pub uninterp spec fn inner_perms_from_metadata(
346        m: M,
347        base: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
348    ) -> pcell_maybe_uninit::PointsTo<MetaSlotStorage>;
349
350    /// Axiomatic roundtrip laws for the metadata ↔ storage-perm pair. The
351    /// conversion is a transmute / reinterpret at exec level, so these laws
352    /// live at the `cast_ptr` trust boundary.
353    pub axiom fn metadata_perms_inverse(m: M, base: pcell_maybe_uninit::PointsTo<MetaSlotStorage>)
354        ensures
355            Self::metadata_from_inner_perms(Self::inner_perms_from_metadata(m, base)) == m,
356            Self::inner_perms_from_metadata(m, base).id() == base.id(),
357            Self::inner_perms_from_metadata(m, base).is_init(),
358    ;
359
360    pub axiom fn inner_perms_from_metadata_roundtrip(
361        perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
362    )
363        ensures
364            Self::inner_perms_from_metadata(Self::metadata_from_inner_perms(perm), perm) == perm,
365    ;
366
367    /// Proof-level companion: given a storage perm that has been initialized
368    /// with some (arbitrary) `MetaSlotStorage` value, advance it to the
369    /// spec form `inner_perms_from_metadata(m, *old(perm))`. This is the
370    /// proof-side step for writing `m` into the cell — it bridges the raw
371    /// `PCell::write` of a `MetaSlotStorage` value to the spec encoding.
372    /// Combined with [`Self::metadata_perms_inverse`], it lets a real exec
373    /// write discharge the `metadata_from_inner_perms == m` post.
374    #[verifier::external_body]
375    pub proof fn switch_perm_to_inner_perms_from_metadata(
376        tracked perm: &mut pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
377        m: M,
378    )
379        requires
380            old(perm).is_init(),
381        ensures
382            *final(perm) == Self::inner_perms_from_metadata(m, *old(perm)),
383    {
384    }
385
386    /// Exec-level write primitive: writing `metadata` into the storage cell
387    /// yields a perm whose `metadata_from_inner_perms` interpretation is
388    /// exactly `metadata`.
389    pub exec fn write_metadata_into_storage(
390        cell: &pcell_maybe_uninit::PCell<MetaSlotStorage>,
391        Tracked(perm): Tracked<&mut pcell_maybe_uninit::PointsTo<MetaSlotStorage>>,
392        metadata: M,
393    )
394        requires
395            cell.id() == old(perm).id(),
396        ensures
397            final(perm).id() == old(perm).id(),
398            final(perm).is_init(),
399            Self::metadata_from_inner_perms(*final(perm)) == metadata,
400    {
401        // Raw cell write — any well-formed `MetaSlotStorage` value initialises
402        // the cell. The spec-level decoding is unspecified for this raw value;
403        // the proof step below reinterprets the perm so it decodes to `metadata`.
404        cell.write(Tracked(perm), MetaSlotStorage::Untyped);
405        proof {
406            let ghost base = *perm;
407            Self::switch_perm_to_inner_perms_from_metadata(perm, metadata);
408            Self::metadata_perms_inverse(metadata, base);
409        }
410    }
411}
412
413/// Value-updaters for the opaque tracked permission types inside
414/// [`MetadataInnerPerms`]. Each uninterp operation produces a new permission
415/// with the same id as the input but a specified value; the paired axioms
416/// document the expected behavior. The conversions are implemented in exec
417/// by `external_body` primitives, so the laws are axiomatic.
418pub uninterp spec fn perm_u64_with(p: PermissionU64, v: u64) -> PermissionU64;
419
420pub axiom fn perm_u64_with_value(p: PermissionU64, v: u64)
421    ensures
422        perm_u64_with(p, v).value() == v,
423        perm_u64_with(p, v).id() == p.id(),
424;
425
426/// Setting a `PermissionU64` to its own current value is a no-op.
427pub axiom fn perm_u64_with_identity(p: PermissionU64)
428    ensures
429        perm_u64_with(p, p.value()) == p,
430;
431
432pub uninterp spec fn pptr_usize_with(
433    p: vstd::simple_pptr::PointsTo<usize>,
434    c: MemContents<usize>,
435) -> vstd::simple_pptr::PointsTo<usize>;
436
437pub axiom fn pptr_usize_with_value(p: vstd::simple_pptr::PointsTo<usize>, c: MemContents<usize>)
438    ensures
439        pptr_usize_with(p, c).mem_contents() == c,
440        pptr_usize_with(p, c).pptr() == p.pptr(),
441;
442
443/// Setting a `PointsTo<usize>` to its own contents is a no-op.
444pub axiom fn pptr_usize_with_identity(p: vstd::simple_pptr::PointsTo<usize>)
445    ensures
446        pptr_usize_with(p, p.mem_contents()) == p,
447;
448
449/// Reconstruct a [`MetaSlot`] from its underlying cell ids. The exec
450/// implementation is a cast; the laws pin `.id()` / `.pptr()` equalities.
451pub uninterp spec fn meta_slot_from_perm(perm: MetadataInnerPerms) -> MetaSlot;
452
453pub axiom fn meta_slot_from_perm_ids(perm: MetadataInnerPerms)
454    ensures
455        meta_slot_from_perm(perm).storage.id() == perm.storage.id(),
456        meta_slot_from_perm(perm).ref_count.id() == perm.ref_count.id(),
457        meta_slot_from_perm(perm).vtable_ptr == perm.vtable_ptr.pptr(),
458        meta_slot_from_perm(perm).in_list.id() == perm.in_list.id(),
459;
460
461/// A `MetaSlot` is uniquely determined by its cell ids + vtable_ptr address.
462/// This is a structural fact about the opaque atomic/cell primitives — two
463/// `MetaSlot` values whose ids agree on every field are equal.
464pub axiom fn meta_slot_eq_by_ids(a: MetaSlot, b: MetaSlot)
465    ensures
466        (a.storage.id() == b.storage.id() && a.ref_count.id() == b.ref_count.id() && a.vtable_ptr
467            == b.vtable_ptr && a.in_list.id() == b.in_list.id()) ==> a == b,
468;
469
470impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M> {
471    type Perm = MetadataInnerPerms;
472
473    open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool {
474        &&& perm.storage.id() == r.storage.id()
475        &&& perm.ref_count.id() == r.ref_count.id()
476        &&& perm.vtable_ptr.pptr() == r.vtable_ptr
477        &&& perm.in_list.id() == r.in_list.id()
478    }
479
480    open spec fn to_repr_spec(self, perm: MetadataInnerPerms) -> (MetaSlot, MetadataInnerPerms) {
481        let new_perm = MetadataInnerPerms {
482            storage: Self::inner_perms_from_metadata(self.metadata, perm.storage),
483            ref_count: perm_u64_with(perm.ref_count, self.ref_count),
484            vtable_ptr: pptr_usize_with(perm.vtable_ptr, self.vtable_ptr),
485            in_list: perm_u64_with(perm.in_list, self.in_list),
486        };
487        (meta_slot_from_perm(new_perm), new_perm)
488    }
489
490    #[verifier::external_body]
491    fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot {
492        unimplemented!()
493    }
494
495    open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self {
496        Metadata {
497            metadata: Self::metadata_from_inner_perms(perm.storage),
498            ref_count: perm.ref_count.value(),
499            vtable_ptr: perm.vtable_ptr.mem_contents(),
500            in_list: perm.in_list.value(),
501        }
502    }
503
504    #[verifier::external_body]
505    fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self {
506        unimplemented!()
507    }
508
509    #[verifier::external_body]
510    fn from_borrowed<'a>(
511        r: &'a MetaSlot,
512        Tracked(perm): Tracked<&'a MetadataInnerPerms>,
513    ) -> &'a Self {
514        unimplemented!()
515    }
516
517    proof fn from_to_repr(self, perm: MetadataInnerPerms) {
518        Self::metadata_perms_inverse(self.metadata, perm.storage);
519        perm_u64_with_value(perm.ref_count, self.ref_count);
520        perm_u64_with_value(perm.in_list, self.in_list);
521        pptr_usize_with_value(perm.vtable_ptr, self.vtable_ptr);
522        let (r, np) = self.to_repr_spec(perm);
523    }
524
525    proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms) {
526        // wf(r, perm) gives us: r's ids match perm's ids; r.vtable_ptr == perm.vtable_ptr.pptr().
527        Self::inner_perms_from_metadata_roundtrip(perm.storage);
528        perm_u64_with_identity(perm.ref_count);
529        perm_u64_with_identity(perm.in_list);
530        pptr_usize_with_identity(perm.vtable_ptr);
531        // Each field of np2 equals the corresponding field of perm:
532        //   np2.storage    = inner_perms_from_metadata(metadata_from_inner_perms(perm.storage), perm.storage)
533        //                  = perm.storage                   (inner_perms_from_metadata_roundtrip)
534        //   np2.ref_count  = perm_u64_with(perm.ref_count, perm.ref_count.value())
535        //                  = perm.ref_count                 (perm_u64_with_identity)
536        //   np2.vtable_ptr = pptr_usize_with(perm.vtable_ptr, perm.vtable_ptr.mem_contents())
537        //                  = perm.vtable_ptr                (pptr_usize_with_identity)
538        //   np2.in_list    = perm.in_list                   (perm_u64_with_identity)
539        let md = Self::from_repr_spec(r, perm);
540        let (r2, np2) = md.to_repr_spec(perm);
541        // r2 is produced from np2 == perm; its ids match perm's; perm's ids match r's (by wf).
542        meta_slot_from_perm_ids(np2);
543        meta_slot_eq_by_ids(r2, r);
544    }
545
546    proof fn to_repr_wf(self, perm: MetadataInnerPerms) {
547        let (r, np) = self.to_repr_spec(perm);
548        meta_slot_from_perm_ids(np);
549        Self::metadata_perms_inverse(self.metadata, perm.storage);
550        perm_u64_with_value(perm.ref_count, self.ref_count);
551        perm_u64_with_value(perm.in_list, self.in_list);
552        pptr_usize_with_value(perm.vtable_ptr, self.vtable_ptr);
553        // wf checks id equality between np's perms and r's slot fields.
554    }
555}
556
557/// A permission token for frame metadata.
558///
559/// [`Frame<M>`] the high-level representation of the low-level pointer
560/// to the [`super::meta::MetaSlot`].
561pub type MetaPerm<M  /*: AnyFrameMeta + Repr<MetaSlotStorage>*/ > =
562    cast_ptr::PointsTo<MetaSlot, Metadata<M>>;
563
564} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
