ostd/mm/frame/
unique.rs

1// SPDX-License-Identifier: MPL-2.0
2//! The unique frame pointer that is not shared with others.
3use vstd::{
4    prelude::*,
5    simple_pptr::{self, PPtr},
6};
7use vstd_extra::{auxiliary::OptionExtraFns, cast_ptr::*, ownership::*};
8
9use crate::specs::{
10    arch::*,
11    mm::frame::{
12        mapping::{frame_to_index, group_page_meta, index_to_meta, max_meta_slots, meta_to_index},
13        meta_owners::{MetaSlotStorage, MetadataPerm, borrow_meta, borrow_meta_mut},
14        meta_region_owners::MetaRegionOwners,
15        unique::*,
16    },
17};
18
19use super::{
20    AnyFrameMeta, Frame, MetaSlot,
21    mapping::{frame_to_meta, meta_to_frame},
22    meta::{GetFrameError, META_SLOT_SIZE, REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
23};
24use crate::mm::{Paddr, PagingConsts, PagingLevel};
25use core::{marker::PhantomData, mem::ManuallyDrop, sync::atomic::Ordering};
26
27verus! {
28
29pub struct UniqueFrame<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
30    pub ptr: PPtr<MetaSlot>,
31    pub _marker: PhantomData<M>,
32    /// The permission to access the `MetaSlot` fields.
33    #[cfg(verus_keep_ghost_body)]
34    pub tracked_slot_perm: Tracked<&'static simple_pptr::PointsTo<MetaSlot>>,
35    /// The complete permission for the currently installed metadata.
36    #[cfg(verus_keep_ghost_body)]
37    pub tracked_metadata_perm: Tracked<Option<MetadataPerm>>,
38}
39
40#[verifier::external]
41unsafe impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + Send> Send for UniqueFrame<M> {
42
43}
44
45#[verifier::external]
46unsafe impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + Sync> Sync for UniqueFrame<M> {
47
48}
49
50/*
51impl<M: AnyFrameMeta + ?Sized> core::fmt::Debug for UniqueFrame<M> {
52    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
53        write!(f, "UniqueFrame({:#x})", self.start_paddr())
54    }
55}*/
56
57#[verus_verify]
58impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
59    /// Gets a [`UniqueFrame`] with a specific usage from a raw, unused page.
60    ///
61    /// The caller should provide the initial metadata of the page.
62    /// # Verified Properties
63    /// ## Preconditions
64    /// The page must be unused and the metadata region must be well-formed.
65    /// ## Postconditions
66    /// If the page is valid, the function returns a unique frame.
67    /// ## Safety
68    /// If `paddr` is misaligned or out of bounds, the function will return an error. If it returns a frame,
69    /// it also returns an owner for that frame, indicating that the caller now has exclusive ownership of it.
70    /// See [Safe Encapsulation] for more details.
71    #[verus_spec(res =>
72        with
73            Tracked(regions): Tracked<&mut MetaRegionOwners>,
74            Tracked(meta_own_in): Tracked<M::Owner>,
75            Tracked(repr_perm_in): Tracked<M::ReprPerm>,
76                -> owner: Tracked<Option<UniqueFrameOwner<M>>>,
77        requires
78            old(regions).contains(frame_to_index(paddr)),
79            old(regions).slot_owner(paddr).usage is Unused,
80            old(regions).inv(),
81            <M as OwnerOf>::wf(metadata, meta_own_in),
82        ensures
83            res matches Ok(res) ==> {
84                &&& owner@ is Some
85                &&& res.wf(owner@->0)
86                &&& res.wf_with_region(owner@->0, *final(regions))
87                &&& owner@->0.meta_own == meta_own_in
88                &&& res.meta_value(owner@->0) == metadata
89                &&& res.inv()
90                &&& res.start_paddr_spec() == paddr
91            },
92            res is Err ==> {
93                &&& owner@ is None
94                &&& *final(regions) == *old(regions)
95            },
96            final(regions).inv(),
97    )]
98    pub fn from_unused(paddr: Paddr, metadata: M) -> Result<Self, GetFrameError> {
99        let tracked mut repr_perm = repr_perm_in;
100        #[verus_spec(with
101            Tracked(regions),
102            Tracked(&mut repr_perm) => Tracked(permissions)
103        )]
104        let from_unused = MetaSlot::get_from_unused(paddr, metadata, true);
105
106        if let Err(err) = from_unused {
107            proof_with!(|= Tracked(None));
108            Err(err)
109        } else {
110            proof_decl! {
111                let tracked metadata_perms = permissions.tracked_unwrap().tracked_take_right();
112                let tracked slot_perm = regions.tracked_borrow_slot(paddr);
113                let tracked owner = UniqueFrameOwner::<M>::tracked_from_unused_owner(
114                    meta_own_in,
115                    repr_perm,
116                    frame_to_index(paddr),
117                );
118            }
119
120            let ptr = from_unused.unwrap();
121
122            proof_with!(|= Tracked(Some(owner)));
123            Ok(
124                Self {
125                    ptr,
126                    _marker: PhantomData,
127                    #[cfg(verus_keep_ghost_body)]
128                    tracked_slot_perm: Tracked(slot_perm),
129                    #[cfg(verus_keep_ghost_body)]
130                    tracked_metadata_perm: Tracked(Some(metadata_perms)),
131                },
132            )
133        }
134    }
135
136    // FIXME: This seems to be unsound and has to be corrected until we have better modeling of trait object.
137    pub open spec fn transmute_spec<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(
138        self,
139        transmuted: UniqueFrame<M1>,
140    ) -> bool {
141        &&& transmuted.ptr.addr() == self.ptr.addr()
142        &&& transmuted._marker == PhantomData::<M1>
143        &&& transmuted.tracked_slot_perm@ == self.tracked_slot_perm@
144        &&& transmuted.tracked_metadata_perm@ == self.tracked_metadata_perm@
145    }
146
147    #[verifier::external_body]
148    #[verus_spec(res =>
149        ensures
150            Self::transmute_spec(self, res),
151    )]
152    pub fn transmute<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(self) -> UniqueFrame<M1> {
153        unimplemented!()
154    }
155
156    /// Repurposes the frame with a new metadata.
157    /// # Verified Properties
158    /// ## Preconditions
159    /// - The caller must provide a valid owner for the frame, and the metadata region invariants must hold.
160    /// - The meta slot's reference count must be `REF_COUNT_UNIQUE`.
161    /// ## Postconditions
162    /// The function returns a new owner for the frame with the new metadata,
163    /// and the metadata region invariants are preserved.
164    /// ## Safety
165    /// The existence of a valid owner guarantees that the memory is initialized with metadata of type `M`,
166    /// and represents that the caller has exclusive ownership of the frame.
167    #[verus_spec(res =>
168        with
169            Tracked(owner): Tracked<UniqueFrameOwner<M>>,
170            Tracked(regions): Tracked<&mut MetaRegionOwners>,
171            Tracked(meta_own_in): Tracked<M1::Owner>,
172            Tracked(repr_perm_in): Tracked<M1::ReprPerm>,
173                -> new_owner: Tracked<UniqueFrameOwner<M1>>,
174        requires
175            self.wf_with_region(owner, *old(regions)),
176            old(regions).slot_owners[self.index()].in_list_perm.value() == 0,
177            old(regions).inv(),
178            self.inv(),
179            owner.inv(),
180            <M1 as OwnerOf>::wf(metadata, meta_own_in),
181        ensures
182            res.wf(new_owner@),
183            res.wf_with_region(new_owner@, *final(regions)),
184            new_owner@.meta_own == meta_own_in,
185            res.meta_value(new_owner@) == metadata,
186            final(regions).inv(),
187    )]
188    pub fn repurpose<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(
189        mut self,
190        metadata: M1,
191    ) -> UniqueFrame<M1> {
192        proof_decl! {
193            broadcast use group_page_meta;
194            let tracked mut repr_perm = repr_perm_in;
195            let ghost idx = self.index();
196            let tracked slot_own = regions.slot_owners.tracked_borrow_mut(idx);
197            let tracked metadata_perm = self.tracked_metadata_perm.tracked_take();
198        }
199
200        // SAFETY: We are the sole owner and the metadata is initialized.
201        unsafe {
202            #[verus_spec(with
203                Tracked(&slot_own.ref_count_perm),
204                Tracked(&slot_own.in_list_perm),
205                Tracked(&mut metadata_perm)
206            )]
207            self.slot().drop_meta_in_place()
208        };
209
210        unsafe {
211            #[verus_spec(with
212                Tracked(&mut metadata_perm),
213                Tracked(&mut repr_perm)
214            )]
215            self.slot().write_meta(metadata)
216        };
217
218        proof_decl!{
219        let tracked new_owner = UniqueFrameOwner::<M1>::tracked_from_unused_owner(
220            meta_own_in,
221            repr_perm,
222            meta_to_index(self.ptr.addr()),
223        );
224        }
225
226        #[cfg(verus_keep_ghost_body)]
227        {
228            self.tracked_metadata_perm = Tracked(Some(metadata_perm));
229        }
230
231        // SAFETY: The metadata is initialized with type `M1`.
232        proof_with!(|= Tracked(new_owner));
233        self.transmute()
234    }
235
236    /// Gets the metadata of this page.
237    /// # Verified Properties
238    /// ## Preconditions
239    /// The caller must provide a valid owner for the frame.
240    /// ## Postconditions
241    /// The function returns the metadata of the frame.
242    /// ## Safety
243    /// The existence of a valid owner guarantees that the memory is initialized with metadata of type `M`,
244    /// and represents that the caller has exclusive ownership of the frame.
245    #[verus_spec(l =>
246        with
247            Tracked(owner): Tracked<&'a UniqueFrameOwner<M>>,
248        requires
249            owner.inv(),
250            self.inv(),
251            self.wf(*owner),
252            self.meta_wf(*owner),
253        ensures
254            self.meta_value(*owner) == l,
255    )]
256    pub fn meta<'a>(&'a self) -> &'a M {
257        // SAFETY: The type is tracked by the type system.
258        // unsafe { &*self.slot().as_meta_ptr::<M>() }
259        let tracked points_to = *self.tracked_slot_perm.borrow();
260        let tracked metadata_perms = self.tracked_metadata_perm.borrow().tracked_borrow();
261        borrow_meta(
262            ReprPtr::<MetaSlotStorage, M>::from_pptr(PPtr::from_addr(self.ptr.addr())),
263            Tracked(points_to),
264            Tracked(metadata_perms),
265            Tracked(owner.tracked_borrow_repr_perm()),
266        )
267    }
268
269    /// Gets the mutable metadata of this page.
270    /// Verified Properties
271    /// ## Preconditions
272    /// The caller must provide a valid owner for the frame.
273    /// ## Postconditions
274    /// The function returns the mutable metadata of the frame.
275    /// ## Safety
276    /// The existence of a valid owner guarantees that the memory is initialized with metadata of type `M`,
277    /// and represents that the caller has exclusive ownership of the frame. (See [Safe Encapsulation])
278    #[verus_spec(res =>
279        with
280            Tracked(owner): Tracked<&'a mut UniqueFrameOwner<M>>,
281        requires
282            old(self).inv(),
283            old(self).wf(*owner),
284            old(self).meta_wf(*owner),
285            owner.inv(),
286        ensures
287            *res == old(self).meta_value(*old(owner)),
288            *final(res) == final(self).meta_value(*final(owner)),
289            final(self).inv(),
290            final(self).ptr == old(self).ptr,
291            final(self).tracked_slot_perm@ == old(self).tracked_slot_perm@,
292            final(owner).meta_own == old(owner).meta_own,
293            final(owner).slot_index == old(owner).slot_index,
294            final(owner).inv(),
295            final(self).meta_wf(*final(owner)),
296            (*final(self)).wf(*final(owner)),
297    )]
298    pub fn meta_mut<'a>(&'a mut self) -> &'a mut M {
299        let tracked points_to = *self.tracked_slot_perm.borrow();
300        let tracked metadata_perms = self.tracked_metadata_perm.borrow_mut().tracked_borrow_mut();
301        let tracked repr_perm = owner.tracked_borrow_mut_repr_perm();
302        borrow_meta_mut(
303            ReprPtr::<MetaSlotStorage, M>::from_pptr(PPtr::from_addr(self.ptr.addr())),
304            Tracked(points_to),
305            Tracked(metadata_perms),
306            Tracked(repr_perm),
307        )
308    }
309}
310
311impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + ?Sized> UniqueFrame<M> {
312    /// Gets the size of this page in bytes.
313    pub const fn size(&self) -> usize
314        returns
315            PAGE_SIZE,
316    {
317        PAGE_SIZE
318    }
319
320    /// Gets the paging level of this page.
321    ///
322    /// This is the level of the page table entry that maps the frame,
323    /// which determines the size of the frame.
324    ///
325    /// Currently, the level is always 1, which means the frame is a regular
326    /// page frame.
327    pub const fn level(&self) -> PagingLevel
328        returns
329            1u8,
330    {
331        1
332    }
333}
334
335#[verus_verify]
336impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + ?Sized> UniqueFrame<M> {
337    /// Gets the physical address of the start of the frame.
338    #[verus_spec(
339        requires
340            self.ptr_inv(),
341        returns
342            meta_to_frame(self.ptr.addr()),
343    )]
344    pub fn start_paddr(&self) -> Paddr {
345        let slot = self.slot();
346
347        #[verus_spec(with self.tracked_slot_perm)]
348        slot.frame_paddr()
349    }
350
351    /*    /// Gets the dynamically-typed metadata of this frame.
352    ///
353    /// If the type is known at compile time, use [`Frame::meta`] instead.
354
355    #[verifier::external_body]
356    pub fn dyn_meta(&self) -> &M {
357        // SAFETY: The metadata is initialized and valid.
358        unsafe { &*self.slot().dyn_meta_ptr::<M>() }
359    }
360
361    /// Gets the dynamically-typed metadata of this frame.
362    ///
363    /// If the type is known at compile time, use [`Frame::meta`] instead.
364
365    #[verifier::external_body]
366    pub fn dyn_meta_mut(&mut self) -> &mut FrameMeta {
367        // SAFETY: The metadata is initialized and valid. We have the exclusive
368        // access to the frame.
369        unsafe { &mut *self.slot().dyn_meta_ptr() }
370    }*/
371    /// Resets the frame to unused without up-calling the allocator.
372    ///
373    /// This is solely useful for the allocator implementation/testing and
374    /// is highly experimental. Usage of this function is discouraged.
375    ///
376    /// Usage of this function other than the allocator would actually leak
377    /// the frame since the allocator would not be aware of the frame.
378    //
379    // FIXME: We may have a better `Segment` and `UniqueSegment` design to
380    // allow the allocator hold the ownership of all the frames in a chunk
381    // instead of the head. Then this weird public API can be `#[cfg(ktest)]`.
382    #[verus_spec(
383        with
384            Tracked(owner): Tracked<UniqueFrameOwner<M>>,
385            Tracked(regions): Tracked<&mut MetaRegionOwners>,
386        requires
387            self.inv(),
388            owner.inv(),
389            regions.inv(),
390            self.wf_with_region(owner, *old(regions)),
391            old(regions).slot_owners[owner.slot_index].in_list_perm.value() == 0,
392        ensures
393            final(regions).inv(),
394    )]
395    pub fn reset_as_unused(mut self) {
396        let mut this = self;
397
398        proof_decl! {
399            let tracked mut owner = owner;
400            let tracked slot_own = regions.tracked_borrow_mut_slot_owner(self.start_paddr_spec());
401            let tracked metadata_perms = this.tracked_metadata_perm.tracked_take();
402            slot_own.metadata_perm.put_resource(metadata_perms);
403        }
404
405        this.slot().ref_count.store(Tracked(&mut slot_own.ref_count_perm), 0);
406
407        // SAFETY: We are the sole owner and the reference count is 0.
408        // The slot is initialized.
409        unsafe {
410            #[verus_spec(with Tracked(slot_own))]
411            this.slot().drop_last_in_place()
412        };
413    }
414
415    /// Converts this frame into a raw physical address.
416    #[verus_spec(r =>
417        with
418            Tracked(owner): Tracked<&UniqueFrameOwner<M>>,
419                -> metadata_perms: Tracked<MetadataPerm>,
420        requires
421            self.inv(),
422        ensures
423            metadata_perms@ == self.metadata_perm(),
424            r == meta_to_frame(self.ptr.addr()),
425    )]
426    pub(crate) fn into_raw(mut self) -> Paddr {
427        let tracked metadata_perms = self.tracked_metadata_perm.tracked_take();
428        let this = ManuallyDrop::new(self);
429
430        proof_with!(|= Tracked(metadata_perms));
431        this.start_paddr()
432    }
433
434    /// Restores a raw physical address back into a unique frame.
435    ///
436    /// # Safety
437    ///
438    /// The caller must ensure that the physical address is valid and points to
439    /// a forgotten frame that was previously casted by [`Self::into_raw`].
440    #[verus_spec(res =>
441        with
442            Tracked(slot_perm): Tracked<&'static simple_pptr::PointsTo<MetaSlot>>,
443            Tracked(meta_own): Tracked<M::Owner>,
444            Tracked(repr_perm): Tracked<M::ReprPerm>,
445            Tracked(metadata_perm): Tracked<MetadataPerm>,
446            ->
447                owner: Tracked<UniqueFrameOwner<M>>,
448        requires
449            valid_frame_paddr(paddr),
450            slot_perm.addr() == frame_to_meta(paddr),
451            slot_perm.is_init(),
452            MetaSlot::perms_related(*slot_perm, metadata_perm)
453        ensures
454            res.inv(),
455            res.start_paddr_spec() == paddr,
456            res.tracked_slot_perm@ == slot_perm,
457            res.wf(owner@),
458            owner@.meta_own == meta_own,
459            owner@.repr_perm == Some(repr_perm),
460            res.tracked_metadata_perm@ == Some(metadata_perm),
461            owner@.slot_index == frame_to_index(paddr),
462    )]
463    pub(crate) unsafe fn from_raw(paddr: Paddr) -> Self {
464        let vaddr = frame_to_meta(paddr);
465        let ptr = vstd::simple_pptr::PPtr::<MetaSlot>::from_addr(vaddr);
466
467        let tracked owner = UniqueFrameOwner {
468            meta_own,
469            repr_perm: Some(repr_perm),
470            slot_index: frame_to_index(paddr),
471        };
472
473        proof_with!{ |= Tracked(owner)}
474        Self {
475            ptr,
476            _marker: PhantomData,
477            #[cfg(verus_keep_ghost_body)]
478            tracked_slot_perm: Tracked(slot_perm),
479            #[cfg(verus_keep_ghost_body)]
480            tracked_metadata_perm: Tracked(Some(metadata_perm)),
481        }
482    }
483
484    #[verus_spec(
485        requires
486            self.ptr_inv(),
487        returns
488            self.tracked_slot_perm@.value(),
489    )]
490    pub fn slot<'a>(&self) -> &'a MetaSlot {
491        // SAFETY: `ptr` points to a valid `MetaSlot` that will never be
492        // mutably borrowed, so taking an immutable reference to it is safe.
493        let tracked slot_perm = *self.tracked_slot_perm;
494        self.ptr.borrow(Tracked(slot_perm))
495    }
496}
497
498/*
499impl<M: AnyFrameMeta + ?Sized> Drop for UniqueFrame<M> {
500    fn drop(&mut self) {
501        self.slot().ref_count.store(0, Ordering::Relaxed);
502        // SAFETY: We are the sole owner and the reference count is 0.
503        // The slot is initialized.
504        unsafe { self.slot().drop_last_in_place() };
505
506        super::allocator::get_global_frame_allocator().dealloc(self.start_paddr(), PAGE_SIZE);
507    }
508} */
509
510impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + ?Sized> UniqueFrame<M> {
511    #[verus_spec(
512        with
513            Tracked(owner): Tracked<UniqueFrameOwner<M>>,
514            Tracked(regions): Tracked<&mut MetaRegionOwners>,
515        requires
516            old(self).inv(),
517            owner.inv(),
518            regions.inv(),
519            old(self).wf_with_region(owner, *old(regions)),
520            old(regions).slot_owners[owner.slot_index].in_list_perm.value() == 0,
521        ensures
522            final(regions).inv(),
523            final(regions).slots == old(regions).slots,
524            forall|i: int| #![trigger final(regions).slot_owners[i]]
525                i != owner.slot_index ==> final(regions).slot_owners[i]
526                    == old(regions).slot_owners[i],
527    )]
528    pub(crate) fn drop(&mut self) {
529        let tracked mut owner = owner;
530        let tracked slot_own = regions.tracked_borrow_mut_slot_owner(self.start_paddr_spec());
531        let tracked metadata_perms = self.tracked_metadata_perm.tracked_take();
532        proof {
533            slot_own.metadata_perm.put_resource(metadata_perms);
534        }
535        // SAFETY: We are the sole owner and the reference count is 0.
536        // The slot is initialized.
537        self.slot().ref_count.store(Tracked(&mut slot_own.ref_count_perm), 0);
538
539        unsafe {
540            #[verus_spec(with Tracked(slot_own))]
541            self.slot().drop_last_in_place()
542        };
543
544        // super::allocator::get_global_frame_allocator().dealloc(self.start_paddr(), PAGE_SIZE);
545    }
546}
547
548#[verus_verify]
549impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
550    #[verus_spec(res =>
551        with
552            Tracked(owner): Tracked<UniqueFrameOwner<M>>,
553            Tracked(regions): Tracked<&mut MetaRegionOwners>,
554        requires
555            unique.inv(),
556            owner.inv(),
557            old(regions).inv(),
558            unique.wf_with_region(owner, *old(regions)),
559            old(regions).slot_owners[owner.slot_index].in_list_perm.value() == 0,
560        ensures
561            res.inv(),
562            final(regions).inv(),
563            res.wf_with_region(*final(regions)),
564            final(regions).slots == old(regions).slots,
565            final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
566    )]
567    pub fn from_unique(unique: UniqueFrame<M>) -> Self {
568        let tracked mut owner = owner;
569        let ptr = unique.ptr;
570        let ghost idx = meta_to_index(unique.ptr.addr());
571        proof {
572            broadcast use group_page_meta;
573
574            regions.lemma_contains_valid_frame_paddr(meta_to_frame(unique.ptr.addr()));
575        }
576        let tracked slot_own = regions.slot_owners.tracked_borrow_mut(idx);
577        let slot = unique.slot();
578        let tracked metadata_perms = unique.tracked_metadata_perm.get().tracked_unwrap();
579        proof {
580            slot_own.metadata_perm.put_resource(metadata_perms);
581        }
582        let tracked frame_permission = slot_own.metadata_perm.split_one();
583        let tracked mut inner_perms = &mut slot_own;
584
585        slot.ref_count.store(Tracked(&mut inner_perms.ref_count_perm), 1);
586
587        let res = Frame {
588            ptr,
589            _marker: PhantomData,
590            #[cfg(verus_keep_ghost_body)]
591            tracked_slot_perm: unique.tracked_slot_perm,
592            #[cfg(verus_keep_ghost_body)]
593            tracked_metadata_perm: Tracked(Some(frame_permission)),
594        };
595        res
596    }
597}
598
599#[verus_verify]
600impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
601    /// Tries to convert a shared frame into a unique one by CAS'ing ref_count
602    /// from 1 to `REF_COUNT_UNIQUE`. Inherent sibling of
603    /// `TryFrom<Frame<M>> for UniqueFrame<M>`.
604    #[verus_spec(res =>
605        with
606            Tracked(regions): Tracked<&mut MetaRegionOwners>,
607        requires
608            frame.inv(),
609            old(regions).inv(),
610            frame.wf_with_region(*old(regions)),
611        ensures
612            final(regions).slots == old(regions).slots,
613            final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
614    )]
615    pub fn try_from_shared(mut frame: Frame<M>) -> Result<Self, Frame<M>> {
616        let ghost idx = meta_to_index(frame.ptr.addr());
617        proof {
618            broadcast use group_page_meta;
619
620            regions.lemma_contains_valid_frame_paddr(frame.start_paddr_spec());
621        }
622        let tracked mut slot_own = regions.slot_owners.tracked_borrow_mut(idx);
623        let tracked inner_perms = &mut slot_own;
624        let res = frame.slot().ref_count.compare_exchange(
625            Tracked(&mut inner_perms.ref_count_perm),
626            1,
627            REF_COUNT_UNIQUE,
628        );
629
630        match res {
631            Ok(_) => {
632                let tracked frame_permission = frame.tracked_metadata_perm.tracked_take();
633                proof {
634                    slot_own.metadata_perm.combine(frame_permission);
635                }
636                let tracked metadata_perms = slot_own.metadata_perm.take_resource();
637                Ok(
638                    UniqueFrame {
639                        ptr: frame.ptr,
640                        _marker: PhantomData,
641                        #[cfg(verus_keep_ghost_body)]
642                        tracked_slot_perm: frame.tracked_slot_perm,
643                        #[cfg(verus_keep_ghost_body)]
644                        tracked_metadata_perm: Tracked(Some(metadata_perms)),
645                    },
646                )
647            },
648            Err(_) => Err(frame),
649        }
650    }
651}
652
653impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> From<UniqueFrame<M>> for Frame<M> {
654    #[verifier::external_body]
655    fn from(unique: UniqueFrame<M>) -> Self {
656        Frame::from_unique(unique)
657    }
658}
659
660impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TryFrom<Frame<M>> for UniqueFrame<M> {
661    type Error = Frame<M>;
662
663    /// Tries to get a unique frame from a shared frame.
664    ///
665    /// If the reference count is not 1, the frame is returned back.
666    #[verifier::external_body]
667    fn try_from(frame: Frame<M>) -> Result<Self, Self::Error> {
668        UniqueFrame::try_from_shared(frame)
669    }
670}
671
672} // verus!
ostd/mm/frame/unique.rs

ostd/mm/frame/
unique.rs
