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

ostd/mm/frame/
unique.rs
