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

ostd/specs/mm/frame/
meta_owners.rs
