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

ostd/mm/frame/
unique.rs
