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, max_meta_slots, meta_addr},
13    meta_owners::{MetaSlotStorage, Metadata},
14    meta_region_owners::MetaRegionOwners,
15    meta_specs::lemma_meta_addr_to_index,
16    unique::UniqueFrameOwner,
17};
18
19use core::{marker::PhantomData, sync::atomic::Ordering};
20
21use super::{
22    AnyFrameMeta, Frame, MetaSlot,
23    mapping::{frame_to_meta, meta_to_frame},
24    meta::{GetFrameError, META_SLOT_SIZE, REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
25};
26use crate::mm::{Paddr, PagingConsts, PagingLevel};
27
28verus! {
29
30pub struct UniqueFrame<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
31    pub ptr: PPtr<MetaSlot>,
32    pub _marker: PhantomData<M>,
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                -> owner: Tracked<Option<UniqueFrameOwner<M>>>,
70        requires
71            old(regions).slot_owners.contains_key(frame_to_index(paddr)),
72            old(regions).slot_owners[frame_to_index(paddr)].usage is Unused,
73            old(regions).inv(),
74        ensures
75            !has_safe_slot(paddr) ==> res is Err,
76            res is Ok ==> {
77                &&& res.unwrap().wf(owner@->0)
78                &&& final(regions).frame_obligations == old(regions).frame_obligations.insert(frame_to_index(paddr))
79            },
80            res is Err ==> final(regions).frame_obligations == old(regions).frame_obligations,
81            final(regions).inv(),
82    )]
83    pub fn from_unused(paddr: Paddr, metadata: M) -> Result<Self, GetFrameError> {
84        #[verus_spec(with Tracked(regions))]
85        let from_unused = MetaSlot::get_from_unused(paddr, metadata, true);
86
87        if let Err(err) = from_unused {
88            proof_with!(|= Tracked(None));
89            Err(err)
90        } else {
91            let (ptr, Tracked(slot_perm)) = from_unused.unwrap();
92            let ghost idx = frame_to_index(paddr);
93
94            proof_decl! {
95                regions.slots.tracked_insert(idx, slot_perm);
96                let tracked owner = UniqueFrameOwner::<M>::tracked_from_unused_owner(regions, paddr);
97            }
98            proof {
99                // The freshly-created live value owes a Drop: mint it.
100                let tracked _ = regions.tracked_mint_frame_obligation(idx);
101            }
102
103            proof_with!(|= Tracked(Some(owner)));
104            Ok(Self { ptr, _marker: PhantomData })
105        }
106    }
107
108    pub open spec fn transmute_spec<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(
109        self,
110        transmuted: UniqueFrame<M1>,
111    ) -> bool {
112        &&& transmuted.ptr.addr() == self.ptr.addr()
113        &&& transmuted._marker == PhantomData::<M1>
114    }
115
116    #[verifier::external_body]
117    #[verus_spec(res =>
118        ensures
119            Self::transmute_spec(self, res),
120    )]
121    pub fn transmute<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(self) -> UniqueFrame<M1> {
122        unimplemented!()
123    }
124
125    /// Repurposes the frame with a new metadata.
126    /// # Verified Properties
127    /// ## Preconditions
128    /// - The caller must provide a valid owner for the frame, and the metadata region invariants must hold.
129    /// - The meta slot's reference count must be `REF_COUNT_UNIQUE`.
130    /// ## Postconditions
131    /// The function returns a new owner for the frame with the new metadata,
132    /// and the metadata region invariants are preserved.
133    /// ## Safety
134    /// The existence of a valid owner guarantees that the memory is initialized with metadata of type `M`,
135    /// and represents that the caller has exclusive ownership of the frame.
136    #[verus_spec(res =>
137        with
138            Tracked(owner): Tracked<UniqueFrameOwner<M>>,
139            Tracked(regions): Tracked<&mut MetaRegionOwners>,
140                -> new_owner: Tracked<UniqueFrameOwner<M1>>,
141        requires
142            self.wf(owner),
143            owner.inv(),
144            owner.global_inv(*old(regions)),
145            old(regions).slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].inner_perms.in_list.value() == 0,
146            old(regions).inv(),
147        ensures
148            res.wf(new_owner@),
149            new_owner@.meta_perm_of(*final(regions)).value().metadata == metadata,
150            final(regions).inv(),
151    )]
152    pub fn repurpose<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(
153        self,
154        metadata: M1,
155    ) -> UniqueFrame<M1> {
156        let ghost idx = frame_to_index(meta_to_frame(self.ptr.addr()));
157        proof {
158            lemma_meta_addr_to_index(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            frame_to_index(meta_to_frame(self.ptr.addr())),
398        )
399        // `self` is a live value with a pending Drop; forgetting it (`MD::new`)
400        // discharges that obligation.
401        &&& regions.frame_obligations.count(frame_to_index(meta_to_frame(self.ptr.addr()))) > 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(
416            frame_to_index(meta_to_frame(self.ptr.addr())),
417        )
418    }
419
420    /// Converts this frame into a raw physical address.
421    #[verus_spec(r =>
422        with
423            Tracked(owner): Tracked<&UniqueFrameOwner<M>>,
424            Tracked(regions): Tracked<&mut MetaRegionOwners>,
425        requires
426            Self::into_raw_requires(self, *old(regions)),
427            self.wf(*owner),
428            owner.inv(),
429            old(regions).inv(),
430            old(regions).slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].inner_perms.ref_count.value() != REF_COUNT_UNUSED,
431        ensures
432            Self::into_raw_ensures(self, *old(regions), *final(regions), r),
433            final(regions).inv(),
434    )]
435    pub(crate) fn into_raw(self) -> Paddr {
436        #[verus_spec(with Tracked(owner), Tracked(&*regions))]
437        let paddr = self.start_paddr();
438
439        // `ManuallyDrop::new` consumes `self`'s pending-Drop obligation; the
440        // caller's `count > 0` precondition guarantees it is outstanding.
441        let _ = ManuallyDrop::new(self, Tracked(regions));
442
443        paddr
444    }
445
446    /// Restores a raw physical address back into a unique frame.
447    ///
448    /// # Safety
449    ///
450    /// The caller must ensure that the physical address is valid and points to
451    /// a forgotten frame that was previously casted by [`Self::into_raw`].
452    #[verus_spec(res =>
453        with
454            Tracked(regions): Tracked<&mut MetaRegionOwners>,
455            Tracked(meta_own): Tracked<M::Owner>,
456        requires
457            paddr < MAX_PADDR,
458            paddr % PAGE_SIZE == 0,
459            old(regions).inv(),
460            old(regions).slot_owners.contains_key(frame_to_index(paddr)),
461            old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == REF_COUNT_UNIQUE,
462        ensures
463            res.0.ptr.addr() == frame_to_meta(paddr),
464            res.0.wf(res.1@),
465            res.1@.meta_own == meta_own,
466            res.1@.slot_index == frame_to_index(paddr),
467            final(regions).inv(),
468            final(regions).slots == old(regions).slots,
469            // `from_raw` reconstitutes a live value (`slot_owners` unchanged,
470            // `raw_count` dormant) and MINTS its pending-Drop obligation.
471            final(regions).slot_owners == old(regions).slot_owners,
472            final(regions).frame_obligations == old(regions).frame_obligations.insert(
473                frame_to_index(paddr),
474            ),
475    )]
476    pub(crate) unsafe fn from_raw(paddr: Paddr) -> (Self, Tracked<UniqueFrameOwner<M>>) {
477        let vaddr = frame_to_meta(paddr);
478        let ptr = vstd::simple_pptr::PPtr::<MetaSlot>::from_addr(vaddr);
479
480        proof {
481            // The reconstituted value owes a Drop: mint its obligation.
482            let tracked _ = regions.tracked_mint_frame_obligation(frame_to_index(paddr));
483        }
484
485        let tracked owner = UniqueFrameOwner { meta_own, slot_index: frame_to_index(paddr) };
486
487        (Self { ptr, _marker: PhantomData }, Tracked(owner))
488    }
489
490    #[verus_spec(
491        with
492            Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
493        requires
494            slot_perm.pptr() == self.ptr,
495            slot_perm.is_init(),
496        returns
497            slot_perm.value(),
498    )]
499    pub fn slot<'a>(&self) -> &'a MetaSlot {
500        // SAFETY: `ptr` points to a valid `MetaSlot` that will never be
501        // mutably borrowed, so taking an immutable reference to it is safe.
502        self.ptr.borrow(Tracked(slot_perm))
503    }
504}
505
506/*
507impl<M: AnyFrameMeta + ?Sized> Drop for UniqueFrame<M> {
508    fn drop(&mut self) {
509        self.slot().ref_count.store(0, Ordering::Relaxed);
510        // SAFETY: We are the sole owner and the reference count is 0.
511        // The slot is initialized.
512        unsafe { self.slot().drop_last_in_place() };
513
514        super::allocator::get_global_frame_allocator().dealloc(self.start_paddr(), PAGE_SIZE);
515    }
516} */
517
518impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + ?Sized> UniqueFrame<M> {
519    #[verus_spec(
520        with
521            Tracked(owner): Tracked<UniqueFrameOwner<M>>,
522            Tracked(regions): Tracked<&mut MetaRegionOwners>,
523        requires
524            old(self).wf_with_region(owner, *old(regions)),
525            old(regions).frame_obligations.count(owner.slot_index) > 0,
526        ensures
527            final(regions).inv(),
528            final(regions).slots == old(regions).slots,
529            forall|i: usize| #![trigger final(regions).slot_owners[i]]
530                i != owner.slot_index ==> final(regions).slot_owners[i]
531                    == old(regions).slot_owners[i],
532            final(regions).frame_obligations == old(regions).frame_obligations.remove(
533                owner.slot_index,
534            ),
535    )]
536    pub(crate) fn drop(&mut self) {
537        let ghost idx = owner.slot_index;
538
539        proof {
540            // Unfold `wf_with_region` to recover the per-slot facts.
541            // `owner.inv()` gives `idx < max_meta_slots`, so `regions.inv()`
542            // delivers `contains_key(idx)`, the `slot_vaddr` shape, and
543            // `slot_owners[idx].inv()`; the latter's UNIQUE branch (under
544            // `rc == REF_COUNT_UNIQUE`) gives the storage/vtable init.
545            assert(regions.slot_owners.contains_key(idx));
546            assert(regions.slot_owners[idx].slot_vaddr == meta_addr(idx));
547            assert(regions.slot_owners[idx].inner_perms.storage.is_init());
548            assert(regions.slot_owners[idx].inner_perms.vtable_ptr.is_init());
549
550            // Running `Drop` discharges the value's pending-Drop obligation.
551            let tracked redeem_tok = vstd_extra::drop_tracking::DropObligation::tracked_mint(idx);
552            regions.tracked_redeem_frame_obligation(redeem_tok);
553        }
554
555        let tracked mut slot_own = regions.slot_owners.tracked_remove(idx);
556        let tracked perm_ref = regions.slots.tracked_borrow(idx);
557
558        // SAFETY: We are the sole owner and the reference count is 0.
559        // The slot is initialized.
560        #[verus_spec(with Tracked(perm_ref))]
561        let slot = self.slot();
562
563        unsafe {
564            #[verus_spec(with Tracked(&mut slot_own))]
565            slot.drop_last_in_place()
566        };
567
568        proof {
569            regions.slot_owners.tracked_insert(idx, slot_own);
570        }
571
572        //        super::allocator::get_global_frame_allocator().dealloc(self.start_paddr(), PAGE_SIZE);
573    }
574}
575
576#[verus_verify]
577impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
578    /// Converts a unique frame into a shared one by setting ref_count = 1.
579    /// Inherent sibling of `From<UniqueFrame<M>> for Frame<M>`: freed from
580    /// the trait-signature straitjacket, this version can thread the tracked
581    /// `MetaRegionOwners` via `verus_spec`.
582    #[verus_spec(res =>
583        with
584            Tracked(owner): Tracked<UniqueFrameOwner<M>>,
585            Tracked(regions): Tracked<&mut MetaRegionOwners>,
586        requires
587            unique.wf(owner),
588            owner.inv(),
589            old(regions).inv(),
590        ensures
591            final(regions).slots == old(regions).slots,
592            final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
593    )]
594    pub fn from_unique(unique: UniqueFrame<M>) -> Self {
595        let ghost idx = frame_to_index(meta_to_frame(unique.ptr.addr()));
596        proof {
597            broadcast use group_page_meta;
598
599            lemma_meta_addr_to_index(owner.slot_index);
600            regions.inv_implies_correct_addr(meta_to_frame(unique.ptr.addr()));
601            assert(idx == owner.slot_index);
602            assert(regions.slots[idx].addr() == unique.ptr.addr());
603            assert(regions.slots[idx].pptr() == unique.ptr);
604        }
605        let tracked mut slot_own = regions.slot_owners.tracked_remove(idx);
606        let tracked slot_perm = regions.slots.tracked_borrow(idx);
607        let tracked mut inner_perms = slot_own.tracked_borrow_mut_inner_perms();
608
609        #[verus_spec(with Tracked(&slot_perm))]
610        let slot = unique.slot();
611        slot.ref_count.store(Tracked(&mut inner_perms.ref_count), 1);
612
613        proof {
614            regions.slot_owners.tracked_insert(idx, slot_own);
615        }
616
617        // UniqueFrame and Frame have identical layout (ptr + PhantomData),
618        // so reconstructing Frame from unique's ptr preserves the handle.
619        Frame { ptr: unique.ptr, _marker: PhantomData }
620    }
621}
622
623#[verus_verify]
624impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
625    /// Tries to convert a shared frame into a unique one by CAS'ing ref_count
626    /// from 1 to `REF_COUNT_UNIQUE`. Inherent sibling of
627    /// `TryFrom<Frame<M>> for UniqueFrame<M>`.
628    #[verus_spec(res =>
629        with
630            Tracked(regions): Tracked<&mut MetaRegionOwners>,
631        requires
632            frame.inv(),
633            old(regions).inv(),
634        ensures
635            final(regions).slots == old(regions).slots,
636            final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
637    )]
638    pub fn try_from_shared(frame: Frame<M>) -> Result<Self, Frame<M>> {
639        let ghost idx = frame_to_index(meta_to_frame(frame.ptr.addr()));
640        proof {
641            broadcast use group_page_meta;
642
643            regions.inv_implies_correct_addr(meta_to_frame(frame.ptr.addr()));
644        }
645        let tracked mut slot_own = regions.slot_owners.tracked_borrow_mut(idx);
646        let tracked slot_perm = regions.slots.tracked_borrow(idx);
647        let tracked inner_perms = slot_own.tracked_borrow_mut_inner_perms();
648
649        #[verus_spec(with Tracked(&slot_perm))]
650        let slot = frame.slot();
651        let res = slot.ref_count.compare_exchange(
652            Tracked(&mut inner_perms.ref_count),
653            1,
654            REF_COUNT_UNIQUE,
655        );
656
657        match res {
658            // Frame and UniqueFrame share layout; construct directly.
659            Ok(_) => Ok(UniqueFrame { ptr: frame.ptr, _marker: PhantomData }),
660            Err(_) => Err(frame),
661        }
662    }
663}
664
665impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> From<UniqueFrame<M>> for Frame<M> {
666    #[verifier::external_body]
667    fn from(unique: UniqueFrame<M>) -> Self {
668        Frame::from_unique(unique)
669    }
670}
671
672impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TryFrom<Frame<M>> for UniqueFrame<M> {
673    type Error = Frame<M>;
674
675    /// Tries to get a unique frame from a shared frame.
676    ///
677    /// If the reference count is not 1, the frame is returned back.
678    #[verifier::external_body]
679    fn try_from(frame: Frame<M>) -> Result<Self, Self::Error> {
680        UniqueFrame::try_from_shared(frame)
681    }
682}
683
684} // verus!
ostd/mm/frame/unique.rs

ostd/mm/frame/
unique.rs
