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

ostd/mm/frame/
unique.rs
