ostd/mm/frame/

meta.rs

// SPDX-License-Identifier: MPL-2.0
//! Metadata management of frames.
//!
//! You can picture a globally shared, static, gigantic array of metadata
//! initialized for each frame.
//! Each entry in this array holds the metadata for a single frame.
//! There would be a dedicated small
//! "heap" space in each slot for dynamic metadata. You can store anything as
//! the metadata of a frame as long as it's [`Sync`].
//!
//! # Implementation
//!
//! The slots are placed in the metadata pages mapped to a certain virtual
//! address in the kernel space. So finding the metadata of a frame often
//! comes with no costs since the translation is a simple arithmetic operation.
use vstd::prelude::*;

verus! {

pub(crate) mod mapping {
    //! The metadata of each physical page is linear mapped to fixed virtual addresses
    //! in [`FRAME_METADATA_RANGE`].
    use core::mem::size_of;
    use super::MetaSlot;
    use crate::mm::{kspace::FRAME_METADATA_RANGE, Paddr, PagingConstsTrait, Vaddr};
    use super::META_SLOT_SIZE;
    use crate::specs::arch::*;
    use vstd::prelude::*;

    pub open spec fn frame_to_meta_spec(paddr: Paddr) -> Vaddr {
        (FRAME_METADATA_RANGE.start + (paddr / PAGE_SIZE) * META_SLOT_SIZE) as usize
    }

    pub open spec fn meta_to_frame_spec(vaddr: Vaddr) -> Paddr {
        ((vaddr - FRAME_METADATA_RANGE.start) / META_SLOT_SIZE as int * PAGE_SIZE) as usize
    }

    /// Converts a physical address of a base frame to the virtual address of the metadata slot.
    #[verifier::when_used_as_spec(frame_to_meta_spec)]
    pub const fn frame_to_meta(paddr: Paddr) -> (res: Vaddr)
        requires
            valid_frame_paddr(paddr),
        ensures
            res % META_SLOT_SIZE == 0,
        returns
            frame_to_meta(paddr),
        no_unwind
    {
        proof {
            MetaSlot::lemma_layout();
        }
        let base = FRAME_METADATA_RANGE.start;
        let offset = paddr / PAGE_SIZE;
        base + offset * size_of::<MetaSlot>()
    }

    /// Converts a virtual address of the metadata slot to the physical address of the frame.
    #[verifier::when_used_as_spec(meta_to_frame_spec)]
    pub const fn meta_to_frame(vaddr: Vaddr) -> (res: Paddr)
        requires
            FRAME_METADATA_RANGE.start <= vaddr < FRAME_METADATA_RANGE.end,
            vaddr % META_SLOT_SIZE == 0,
        ensures
            res % PAGE_SIZE == 0,
        returns
            meta_to_frame(vaddr),
    {
        proof {
            MetaSlot::lemma_layout();
        }
        let base = FRAME_METADATA_RANGE.start;
        let offset = (vaddr - base) / size_of::<MetaSlot>();
        offset * PAGE_SIZE
    }

}

} // verus!
use vstd::atomic::{PAtomicU64, PermissionU64};
use vstd::cell::pcell_maybe_uninit;
use vstd::prelude::*;
use vstd::simple_pptr::{PPtr, PointsTo};
use vstd_extra::cast_ptr::{Repr, ReprPtr};
use vstd_extra::ownership::*;
use vstd_extra::panic::{may_panic, panic_diverge};
use vstd_extra::prelude::*;

use core::{
    alloc::Layout,
    any::Any,
    cell::UnsafeCell,
    fmt::Debug,
    marker::PhantomData,
    mem::{ManuallyDrop, MaybeUninit},
    result::Result,
    sync::atomic::{AtomicU64, Ordering},
};

use align_ext::AlignExt;
//use log::info;

use self::mapping::{frame_to_meta, meta_to_frame};
use crate::mm::io::{Infallible, VmReader};
use crate::specs::arch::*;
use crate::specs::mm::frame::{
    mapping::frame_to_index, meta_owners::*, meta_region_owners::MetaRegionOwners,
};

use crate::{
    //    boot::memory_region::MemoryRegionType,
    //    const_assert,
    mm::{
        /*VmReader,*/
        /*Infallible,*/ Paddr,
        PagingLevel,
        //Segment,
        Vaddr,
        kspace::FRAME_METADATA_RANGE,
        //        frame::allocator::{self, EarlyAllocatedFrameMeta},
        paddr_to_vaddr,
        //        page_table::boot_pt,
        page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags},
    },
    //    panic::abort,
    //    util::ops::range_difference,
};

verus! {

/* /// The maximum number of bytes of the metadata of a frame.
pub const FRAME_METADATA_MAX_SIZE: usize = META_SLOT_SIZE
    - size_of::<AtomicU64>()
    - size_of::<FrameMetaVtablePtr>()
    - size_of::<AtomicU64>(); */
/// The maximum alignment in bytes of the metadata of a frame.
pub const FRAME_METADATA_MAX_ALIGN: usize = META_SLOT_SIZE;

pub const META_SLOT_SIZE: usize = 64;

#[repr(C)]
pub struct MetaSlot {
    /// The metadata of a frame.
    ///
    /// It is placed at the beginning of a slot because:
    ///  - the implementation can simply cast a `*const MetaSlot`
    ///    to a `*const AnyFrameMeta` for manipulation;
    ///  - if the metadata need special alignment, we can provide
    ///    at most `PAGE_METADATA_ALIGN` bytes of alignment;
    ///  - the subsequent fields can utilize the padding of the
    ///    reference count to save space.
    ///
    /// Don't interpret this field as an array of bytes. It is a
    /// placeholder for the metadata of a frame.
    // storage: UnsafeCell<[u8; FRAME_METADATA_MAX_SIZE]>
    /// # Verification Design
    /// We model the metadata of the slot as a `MetaSlotStorage`, which is a tagged union of the different
    /// types of metadata defined in the development.
    pub storage: pcell_maybe_uninit::PCell<MetaSlotStorage>,
    /// The reference count of the page.
    ///
    /// Specifically, the reference count has the following meaning:
    ///  - `REF_COUNT_UNUSED`: The page is not in use.
    ///  - `REF_COUNT_UNIQUE`: The page is owned by a [`UniqueFrame`].
    ///  - `0`: The page is being constructed ([`Frame::from_unused`])
    ///    or destructured ([`drop_last_in_place`]).
    ///  - `1..REF_COUNT_MAX`: The page is in use.
    ///  - `REF_COUNT_MAX..REF_COUNT_UNIQUE`: Illegal values to
    ///    prevent the reference count from overflowing. Otherwise,
    ///    overflowing the reference count will cause soundness issue.
    ///
    /// [`Frame::from_unused`]: super::Frame::from_unused
    /// [`UniqueFrame`]: super::unique::UniqueFrame
    /// [`drop_last_in_place`]: Self::drop_last_in_place
    //
    // Other than this field the fields should be `MaybeUninit`.
    // See initialization in `alloc_meta_frames`.
    pub ref_count: PAtomicU64,
    /// The virtual table that indicates the type of the metadata.
    /// VERUS LIMITATION: Currently we do not verify this because
    /// of the dependency on the `dyn Trait` pattern. But we can revisit it now that `dyn Trait` is supported by Verus.
    // pub vtable_ptr: UnsafeCell<MaybeUninit<FrameMetaVtablePtr>>,
    pub vtable_ptr: PPtr<usize>,
    /// This is only accessed by [`crate::mm::frame::linked_list`].
    /// It stores 0 if the frame is not in any list, otherwise it stores the
    /// ID of the list.
    ///
    /// It is ugly but allows us to tell if a frame is in a specific list by
    /// one relaxed read. Otherwise, if we store it conditionally in `storage`
    /// we would have to ensure that the type is correct before the read, which
    /// costs a synchronization.
    pub in_list: PAtomicU64,
}

pub const REF_COUNT_UNUSED: u64 = u64::MAX;

pub const REF_COUNT_UNIQUE: u64 = u64::MAX - 1;

pub const REF_COUNT_MAX: u64 = i64::MAX as u64;

type FrameMetaVtablePtr = core::ptr::DynMetadata<dyn AnyFrameMeta>;

/// All frame metadata types must implement this trait.
///
/// If a frame type needs specific drop behavior, it should specify
/// when implementing this trait. When we drop the last handle to
/// this frame, the `on_drop` method will be called. The `on_drop`
/// method is called with the physical address of the frame.
///
/// The implemented structure should have a size less than or equal to
/// [`FRAME_METADATA_MAX_SIZE`] and an alignment less than or equal to
/// [`FRAME_METADATA_MAX_ALIGN`]. Otherwise, the metadata type cannot
/// be used because storing it will fail compile-time assertions.
///
/// # Safety
///
/// If `on_drop` reads the page using the provided `VmReader`, the
/// implementer must ensure that the frame is safe to read.
pub unsafe trait AnyFrameMeta:   /*Any +*/
Send + Sync {
    /// Per-impl precondition for [`Self::on_drop`]. Default is `true`.
    /// Impls that need richer caller-side invariants (e.g. the PT-node's
    /// reader/region invariants) override this; the trait method's
    /// `requires` clause calls it.
    open spec fn on_drop_pre(
        &self,
        reader: VmReader<'_, Infallible>,
        regions: MetaRegionOwners,
        vm_io_owner: crate::specs::mm::io::VmIoOwner,
    ) -> bool {
        true
    }

    fn on_drop(
        &mut self,
        _reader: &mut VmReader<'_, Infallible>,
        Tracked(_regions): Tracked<&mut MetaRegionOwners>,
        Tracked(_vm_io_owner): Tracked<&mut crate::specs::mm::io::VmIoOwner>,
    )
        requires
            old(_regions).inv(),
            old(_reader).inv(),
            old(_vm_io_owner).inv(),
            old(_reader).wf(*old(_vm_io_owner)),
            old(self).on_drop_pre(*old(_reader), *old(_regions), *old(_vm_io_owner)),
        ensures
            final(_regions).inv(),
            final(_reader).inv(),
            final(_vm_io_owner).inv(),
            final(_reader).wf(*final(_vm_io_owner)),
        default_ensures
            *final(_reader) == *old(_reader),
            *final(_regions) == *old(_regions),
            *final(_vm_io_owner) == *old(_vm_io_owner),
    {
    }

    fn is_untyped(&self) -> (res: bool)
        default_ensures
            res == false,
    {
        false
    }

    spec fn vtable_ptr(&self) -> usize where Self: Sized;
}

/*/// Makes a structure usable as a frame metadata.
#[macro_export]
macro_rules! impl_frame_meta_for {
    // Implement without specifying the drop behavior.
    ($t:ty) => {
        // SAFETY: `on_drop` won't read the page.
        unsafe impl $crate::mm::frame::meta::AnyFrameMeta for $t {}

        $crate::const_assert!(
            core::mem::size_of::<$t>() <= $crate::mm::frame::meta::FRAME_METADATA_MAX_SIZE
        );
        $crate::const_assert!(
            $crate::mm::frame::meta::FRAME_METADATA_MAX_ALIGN % core::mem::align_of::<$t>() == 0
        );
    };
}

pub use impl_frame_meta_for;*/

/// The error type for getting the frame from a physical address.
#[derive(Debug)]
pub enum GetFrameError {
    /// The frame is in use.
    InUse,
    /// The frame is not in use.
    Unused,
    /// The frame is being initialized or destructed.
    Busy,
    /// The frame is private to an owner of [`UniqueFrame`].
    ///
    /// [`UniqueFrame`]: super::unique::UniqueFrame
    Unique,
    /// The provided physical address is out of bound.
    OutOfBound,
    /// The provided physical address is not aligned.
    NotAligned,
}

/// Gets the reference to a metadata slot.
/// # Verified Properties
/// ## Preconditions
/// `paddr` is the physical address of a frame, with a valid owner.
/// ## Postconditions
/// If `paddr` is aligned properly and in-bounds, the function returns a static reference to its metadata slot.
/// ## Safety
/// Verus ensures that the pointer is properly dereferenced with a permission object, so creating it is safe.
#[verus_spec(res =>
    with
        Tracked(slot_perm): Tracked<Option<&'static vstd::simple_pptr::PointsTo<MetaSlot>>>
    requires
        valid_frame_paddr(paddr) ==> {
            &&& slot_perm is Some
            &&& slot_perm->0.addr() == frame_to_meta(paddr)
            &&& slot_perm->0.is_init()
        }
    ensures
        valid_frame_paddr(paddr) == res is Ok,
        res is Ok ==> res->Ok_0 == slot_perm->0.value(),
)]
pub(super) fn get_slot(paddr: Paddr) -> Result<&'static MetaSlot, GetFrameError> {
    if paddr % PAGE_SIZE != 0 {
        return Err(GetFrameError::NotAligned);
    }
    if paddr >= super::max_paddr() {
        return Err(GetFrameError::OutOfBound);
    }
    let vaddr = mapping::frame_to_meta(paddr);
    let ptr = PPtr::<MetaSlot>::from_addr(vaddr);

    // SAFETY: `ptr` points to a valid `MetaSlot` that will never be
    // mutably borrowed, so taking an immutable reference to it is safe.
    // Ok(unsafe { &*ptr })
    Ok(ptr.borrow(Tracked(slot_perm.tracked_borrow())))
}

#[verus_verify]
impl MetaSlot {
    /// This is the equivalent of &self as *const as Vaddr, but we need to axiomatize it.
    /// # Safety
    /// It is safe to take the address of a pointer, but it may not be safe to use that
    /// address for all purposes.
    #[verifier::external_body]
    #[verus_spec(
        with
            Tracked(perm): Tracked<&PointsTo<MetaSlot>>,
        requires
            self == perm.value(),
        returns
            perm.addr(),
    )]
    fn addr_of(&self) -> Vaddr {
        unimplemented!()
    }

    /// Initializes the metadata slot of a frame assuming it is unused.
    ///
    /// If successful, the function returns a pointer to the metadata slot.
    /// And the slot is initialized with the given metadata.
    ///
    /// The resulting reference count held by the returned pointer is
    /// [`REF_COUNT_UNIQUE`] if `as_unique_ptr` is `true`, otherwise `1`.
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety Invariant**: Metaslot region invariants must hold.
    /// - **Bookkeeping**: The slot permissions must be available in order to check the reference count.
    /// This precondition is stronger than it needs to be; absent permissions correspond to error cases.
    /// ## Postconditions
    /// - **Safety Invariant**: Metaslot region invariants hold after the call.
    /// - **Safety**: Other slots are not affected by the call.
    /// - **Correctness**: If successful, the function returns a pointer to the metadata slot and a permission to the slot.
    /// - **Correctness**: If successful, the slot is initialized with the given metadata.
    /// ## Safety
    /// - This function returns an error if `paddr` does not correspond to a valid slot or the slot is in use.
    /// - Accesses to the slot itself are gated by atomic checks, avoiding data races.
    #[verus_spec(res =>
        with
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(repr_perm): Tracked<&mut M::ReprPerm>
        requires
            old(regions).inv(),
        ensures
            res is Err ==> *final(regions) == *old(regions),
            res matches Ok(res) ==> {
                &&& res.addr() == frame_to_meta(paddr)
                &&& final(regions).inv()
                &&& Self::get_from_unused_spec(paddr, as_unique_ptr, *old(regions), *final(regions))
                &&& <M as Repr<MetaSlotStorage>>::wf(
                    final(regions).slot_owner(paddr).storage_perm().value(),
                    *final(repr_perm),
                )
                &&& M::from_repr_spec(
                    final(regions).slot_owner(paddr).storage_perm().value(),
                    *final(repr_perm),
                ) == metadata
            },
            res is Ok ==> valid_frame_paddr(paddr),
    )]
    pub(super) fn get_from_unused<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(
        paddr: Paddr,
        metadata: M,
        as_unique_ptr: bool,
    ) -> Result<PPtr<Self>, GetFrameError> {
        proof_decl! {
            let ghost idx = frame_to_index(paddr);
            if valid_frame_paddr(paddr) {
                regions.lemma_contains_valid_frame_paddr(paddr);
            }

            let tracked slot_perm = if valid_frame_paddr(paddr) {
                Some(*regions.slots.tracked_borrow(idx))
            } else {
                None
            };
        }

        let slot = #[verus_spec(with Tracked(slot_perm))]
        get_slot(paddr)?;

        let tracked slot_own = regions.slot_owners.tracked_borrow_mut(idx);
        proof {
            axiom_mmio_usage_iff_mmio_paddr(*slot_own);
        }

        // `Acquire` pairs with the `Release` in `drop_last_in_place` and ensures the metadata
        // initialization won't be reordered before this memory compare-and-exchange.
        let last_ref_cnt = slot.ref_count.compare_exchange(
            Tracked(&mut slot_own.ref_count_perm),
            REF_COUNT_UNUSED,
            0,
        ).map_err(
            |val|
                match val {
                    REF_COUNT_UNIQUE => GetFrameError::Unique,
                    0 => GetFrameError::Busy,
                    _ => GetFrameError::InUse,
                },
        );

        if let Err(err) = last_ref_cnt {
            proof {
                // CAS failure leaves `ref_count` unchanged (value + id), so the
                // re-parked slot is exactly the original — region state intact.
                vstd_extra::auxiliary::axiom_permission_u64_ext_eq(
                    regions.slot_owners[idx].ref_count_perm,
                    old(regions).slot_owners[idx].ref_count_perm,
                );
            }

            return Err(err);
        }
        // SAFETY: The slot now has a reference count of `0`, other threads will
        // not access the metadata slot so it is safe to have a mutable reference.

        unsafe {
            #[verus_spec(with
                Tracked(&mut slot_own.metadata_perm.storage_perm),
                Tracked(repr_perm),
                Tracked(&mut slot_own.metadata_perm.vtable_ptr_perm)
            )]
            slot.write_meta(metadata)
        };

        if as_unique_ptr {
            // No one can create a `Frame` instance directly from the page
            // address, so `Relaxed` is fine here.
            slot.ref_count.store(Tracked(&mut slot_own.ref_count_perm), REF_COUNT_UNIQUE);
        } else {
            // `Release` is used to ensure that the metadata initialization
            // won't be reordered after this memory store.
            slot.ref_count.store(Tracked(&mut slot_own.ref_count_perm), 1);
        }

        proof {
            slot_own.usage = PageUsage::Frame;
            axiom_mmio_usage_iff_mmio_paddr(*slot_own);
        }

        Ok(PPtr::from_addr(frame_to_meta(paddr)))
    }

    /// Gets another owning pointer to the metadata slot from the given page.
    /// # Verified Properties
    /// We do not prove termination.
    /// ## Preconditions
    /// - **Safety Invariant**: Metaslot region invariants must hold.
    /// - **Bookkeeping**: The slot permissions must be available in order to check the reference count.
    /// This precondition is stronger than it needs to be; absent permissions correspond to error cases.
    /// - **Liveness**: The reference count of the inner permissions must not be at the maximum, or the function will panic.
    /// ## Postconditions
    /// - **Safety**: Metaslot region invariants hold after the call.
    /// - **Correctness**: If successful, the slot's reference count is increased by one.
    /// - **Correctness**: If unsuccessful, the metaslot region remains unchanged.
    /// ## Safety
    /// The potential data race is avoided by the spin-lock.
    #[verus_spec(res =>
        with Tracked(regions): Tracked<&mut MetaRegionOwners>
        requires
            old(regions).inv(),
            valid_frame_paddr(paddr) ==> old(regions).ref_count(frame_to_index(paddr)) >= REF_COUNT_MAX ==> may_panic(),
        ensures
            final(regions).inv(),
            res is Ok ==> valid_frame_paddr(paddr),
            res is Ok ==> Self::get_from_in_use_success(paddr, *old(regions), *final(regions)),
            res matches Ok(ptr) ==> ptr == old(regions).slots[frame_to_index(paddr)].pptr(),
            res is Err ==> *final(regions) == *old(regions),
            final(regions).frame_obligations == old(regions).frame_obligations,
    )]
    #[verifier::exec_allows_no_decreases_clause]
    #[verifier::loop_isolation(false)]
    pub(super) fn get_from_in_use(paddr: Paddr) -> Result<PPtr<Self>, GetFrameError> {
        proof_decl! {
            let ghost idx = frame_to_index(paddr);
            if valid_frame_paddr(paddr) {
                regions.lemma_contains_valid_frame_paddr(paddr);
            }
            let tracked slot_perm = if valid_frame_paddr(paddr) {
                Some(*regions.slots.tracked_borrow(idx))
            } else {
                None
            };
        }
        let slot = #[verus_spec(with Tracked(slot_perm))]
        get_slot(paddr)?;

        loop
            invariant
                *regions == *old(regions),
        {
            proof {
                vstd_extra::auxiliary::axiom_permission_u64_ext_eq(
                    regions.slot_owners[idx].ref_count_perm,
                    old(regions).slot_owners[idx].ref_count_perm,
                );
            }

            let tracked slot_own = regions.slot_owners.tracked_borrow_mut(idx);

            match slot.ref_count.load(Tracked(&mut slot_own.ref_count_perm)) {
                REF_COUNT_UNUSED => return Err(GetFrameError::Unused),
                REF_COUNT_UNIQUE => return Err(GetFrameError::Unique),
                0 => return Err(GetFrameError::Busy),
                last_ref_cnt => {
                    if last_ref_cnt >= REF_COUNT_MAX {
                        // See `Self::inc_ref_count` for the explanation.
                        vstd_extra::panic::panic_diverge();
                    }
                    // Using `Acquire` here to pair with `get_from_unused` or
                    // `<Frame<M> as From<UniqueFrame<M>>>::from` (who must be
                    // performed after writing the metadata).
                    //
                    // It ensures that the written metadata will be visible to us.

                    if slot.ref_count.compare_exchange_weak(
                        Tracked(&mut slot_own.ref_count_perm),
                        last_ref_cnt,
                        last_ref_cnt + 1,
                    ).is_ok() {
                        return Ok(PPtr::from_addr(frame_to_meta(paddr)));
                    }
                    proof {
                        vstd_extra::auxiliary::axiom_permission_u64_ext_eq(
                            slot_own.ref_count_perm,
                            old(regions).slot_owners[idx].ref_count_perm,
                        );
                    }

                },
            }
            core::hint::spin_loop();
        }
    }

    /// Increases the frame reference count by one.
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Bookkeeping**: The permission must match the reference count being updated.
    /// - **Liveness**: The function will abort if the reference count is at the maximum.
    /// ## Postconditions
    /// - **Correctness**: The reference count is increased by one.
    /// ## Safety
    /// By requiring the caller to provide a permission for the reference count, we ensure that it already has a reference to the frame.
    #[verus_spec(
        with
            Tracked(rc_perm): Tracked<&mut PermissionU64>,
        requires
            old(rc_perm).is_for(self.ref_count),
            old(rc_perm).value() != REF_COUNT_UNUSED,
            old(rc_perm).value() >= REF_COUNT_MAX ==> may_panic(),
        ensures
            final(rc_perm).value() == old(rc_perm).value() + 1,
            old(rc_perm).value() < REF_COUNT_MAX,
            final(rc_perm).id() == old(rc_perm).id(),
    )]
    pub(super) unsafe fn inc_ref_count(&self) {
        let last_ref_cnt = self.ref_count.fetch_add(Tracked(rc_perm), 1);

        if last_ref_cnt >= REF_COUNT_MAX {
            // This follows the same principle as the `Arc::clone` implementation to prevent the
            // reference count from overflowing. See also
            // <https://doc.rust-lang.org/std/sync/struct.Arc.html#method.clone>.
            panic_diverge();
        }
    }

    /// Gets the corresponding frame's physical address.
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety**: The permission must point to a valid metadata slot.
    /// - **Correctness**: The permission must point to the metadata slot.
    /// ## Postconditions
    /// - **Correctness**: The function returns the physical address of the frame.
    /// ## Safety
    /// The safety precondition requires that the permission points to a valid metadata slot.
    /// This is an internal function, so it is fine to require the caller to verify this.
    #[verus_spec(
        with
            Tracked(perm): Tracked<&PointsTo<MetaSlot>>,
        requires
            perm.value() == self,
            Self::frame_paddr_safety_cond(*perm),
        returns
            meta_to_frame(perm.addr()),
    )]
    pub(super) fn frame_paddr(&self) -> (pa: Paddr) {
        proof_with!(Tracked(perm));
        let addr = self.addr_of();
        meta_to_frame(addr)
    }

    /*
    /// Gets a dynamically typed pointer to the stored metadata.
    ///
    /// # Safety
    ///
    /// The caller should ensure that:
    ///  - the stored metadata is initialized (by [`Self::write_meta`]) and valid.
    ///
    /// The returned pointer should not be dereferenced as mutable unless having
    /// exclusive access to the metadata slot.

    #[verifier::external_body]
    pub(super) unsafe fn dyn_meta_ptr<M: AnyFrameMeta>(&self) -> PPtr<M> {
        unimplemented!()

        // SAFETY: The page metadata is valid to be borrowed immutably, since
        // it will never be borrowed mutably after initialization.
        let vtable_ptr = unsafe { *self.vtable_ptr.get() };

        // SAFETY: The page metadata is initialized and valid.
        let vtable_ptr = *unsafe { vtable_ptr.assume_init_ref() };

        let meta_ptr: *mut dyn AnyFrameMeta =
            core::ptr::from_raw_parts_mut(self as *const MetaSlot as *mut MetaSlot, vtable_ptr);

        meta_ptr
    }

    /// Gets the stored metadata as type `M`.
    ///
    /// Calling the method should be safe, but using the returned pointer would
    /// be unsafe. Specifically, the derefernecer should ensure that:
    ///  - the stored metadata is initialized (by [`Self::write_meta`]) and
    ///    valid;
    ///  - the initialized metadata is of type `M`;
    ///  - the returned pointer should not be dereferenced as mutable unless
    ///    having exclusive access to the metadata slot.
    pub(super) fn as_meta_ptr<M: AnyFrameMeta>(&self) -> *mut M {
        self.storage.get() as *mut M
    }

    */
    /// Writes the metadata to the slot without reading or dropping the previous value.
    ///
    /// # Safety
    ///
    /// The caller should have exclusive access to the metadata slot's fields.
    ///
    /// # Verification Design
    /// This function is axiomatized for now because of trait constraints.
    /// ## Preconditions
    /// - The caller must provide the permission token to the metadata slot's storage.
    /// ## Postconditions
    /// - The permission is initialized to the new metadata.
    /// ## Safety
    /// The caller must have exclusive access to the metadata slot's storage in order to provide the permission token.
    #[verus_spec(
        with
            Tracked(meta_perm): Tracked<&mut vstd::cell::pcell_maybe_uninit::PointsTo<MetaSlotStorage>>,
            Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
            Tracked(vtable_perm): Tracked<&mut PointsTo<usize>>,
        requires
            self.storage.id() == old(meta_perm).id(),
            self.vtable_ptr == old(vtable_perm).pptr(),
            old(vtable_perm).is_uninit(),
        ensures
            final(meta_perm).id() == old(meta_perm).id(),
            final(meta_perm).is_init(),
            final(vtable_perm).pptr() == old(vtable_perm).pptr(),
            final(vtable_perm).is_init(),
            <M as Repr<MetaSlotStorage>>::wf(
                final(meta_perm).value(),
                *final(repr_perm),
            ),
            M::from_repr_spec(
                final(meta_perm).value(),
                *final(repr_perm),
            ) == metadata,
    )]
    pub(super) unsafe fn write_meta<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(
        &self,
        metadata: M,
    ) {
        // SAFETY: Caller ensures that the access to the fields are exclusive.
        //        let vtable_ptr = unsafe { &mut *self.vtable_ptr.get() };
        //        vtable_ptr.write(core::ptr::metadata(&metadata as &dyn AnyFrameMeta));
        self.vtable_ptr.put(Tracked(vtable_perm), 0);

        // SAFETY:
        // 1. `ptr` points to the metadata storage.
        // 2. The size and the alignment of the metadata storage is large enough to hold `M`
        //    (guaranteed by the const assertions above).
        // 3. We have exclusive access to the metadata storage (guaranteed by the caller).
        // unsafe { ptr.cast::<M>().write(metadata) };
        write_metadata_into_storage(
            &self.storage,
            Tracked(meta_perm),
            Tracked(repr_perm),
            metadata,
        );
    }

    /// Drops the metadata and deallocates the frame.
    ///
    /// # Safety
    ///
    /// The caller should ensure that:
    ///  - the reference count is `0` (so we are the sole owner of the frame);
    ///  - the metadata is initialized;
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety Invariant**: The metadata slot must satisfy the safety invariants.
    /// - **Safety**: The caller must provide an owner object for the metadata slot, which must include the permission for the
    /// slot's `ref_count` field.
    /// - **Safety**: The owner must satisfy [`drop_last_in_place_safety_cond`], which ensures that its reference count is 0
    /// and it has no dangling raw pointers.
    /// ## Postconditions
    /// - **Safety**: The metadata slot satisfies the safety invariants after the call.
    /// - **Correctness**: The reference count is set to `REF_COUNT_UNUSED` and the contents of the slot are uninitialized.
    /// ## Safety
    /// - By requiring the caller to provide an owner object, we ensure that it already has a reference to the frame.
    /// - The safety precondition ensures that there are no dangling pointers, including raw pointer, guaranteeing temporal safety.
    #[verus_spec(
        with
            Tracked(owner): Tracked<&mut MetaSlotOwner>,
        requires
            old(owner).inv(),
            self.ref_count.id() == old(owner).ref_count_perm.id(),
            Self::drop_last_in_place_safety_cond(*old(owner)),
        ensures
            final(owner).inv(),
            final(owner).ref_count() == REF_COUNT_UNUSED,
            final(owner).ref_count_perm.id() == old(owner).ref_count_perm.id(),
            final(owner).storage_perm().id() == old(owner).storage_perm().id(),
            final(owner).storage_perm().is_uninit(),
            final(owner).vtable_ptr_perm().is_uninit(),
            final(owner).vtable_ptr_perm().pptr() == old(owner).vtable_ptr_perm().pptr(),
            final(owner).in_list_perm == old(owner).in_list_perm,
            final(owner).slot_vaddr == old(owner).slot_vaddr,
            final(owner).usage == old(owner).usage,
            final(owner).paths_in_pt == old(owner).paths_in_pt,
    )]
    pub(super) unsafe fn drop_last_in_place(&self) {
        // This should be guaranteed as a safety requirement.
        //        debug_assert_eq!(self.ref_count.load(Tracked(&*rc_perm)), 0);
        // SAFETY: The caller ensures safety.
        unsafe {
            #[verus_spec(with Tracked(owner))]
            self.drop_meta_in_place()
        };

        // `Release` pairs with the `Acquire` in `Frame::from_unused` and ensures
        // `drop_meta_in_place` won't be reordered after this memory store.
        self.ref_count.store(Tracked(&mut owner.ref_count_perm), REF_COUNT_UNUSED);
    }

    /// Drops the metadata of a slot in place.
    ///
    /// After this operation, the metadata becomes uninitialized. Any access to the
    /// metadata is undefined behavior unless it is re-initialized by [`Self::write_meta`].
    ///
    /// # Verification Design
    /// This function is axiomatized because of its reliance on dynamic trait methods and `VmReader`.
    /// The latter dependency makes it part of the "bootstrap gap".
    /// Now that Verus better supports the `dyn Trait` pattern and we have verified `VmReader`, we can revisit it.
    /// ## Preconditions
    /// - The caller must provide an owner object for the metadata slot.
    /// - The reference count must be 0
    /// ## Safety
    ///
    /// The caller should ensure that:
    ///  - the reference count is `0` (so we are the sole owner of the frame);
    ///  - the metadata is initialized;
    #[verifier::external_body]
    #[verus_spec(
        with
            Tracked(slot_own): Tracked<&mut MetaSlotOwner>,
        requires
            old(slot_own).ref_count() == 0 || old(slot_own).ref_count() == REF_COUNT_UNIQUE,
            old(slot_own).storage_perm().is_init(),
            old(slot_own).in_list_perm.value() == 0,
        ensures
            final(slot_own).ref_count_perm == old(slot_own).ref_count_perm,
            final(slot_own).storage_perm().is_uninit(),
            final(slot_own).storage_perm().id() == old(slot_own).storage_perm().id(),
            final(slot_own).in_list_perm == old(slot_own).in_list_perm,
            final(slot_own).vtable_ptr_perm().is_uninit(),
            final(slot_own).vtable_ptr_perm().pptr() == old(slot_own).vtable_ptr_perm().pptr(),
            final(slot_own).slot_vaddr == old(slot_own).slot_vaddr,
            final(slot_own).usage == old(slot_own).usage,
            final(slot_own).paths_in_pt == old(slot_own).paths_in_pt,
    )]
    #[verifier::external_body]
    pub(super) unsafe fn drop_meta_in_place(&self) {
        // Smoke test for the dyn-dispatch shape — body kept `external_body`
        // because (a) the args bundle isn't threaded through the call chain
        // yet (Tracked::assume_new forges it here), (b) `VmReader`,
        // `vtable_ptr.assume_init_read`, and `core::ptr::drop_in_place` have
        // no Verus specs. Activates only the type-check; runtime behavior is
        // axiomatic per the verus_spec ensures above.
        let paddr = unimplemented!();
        let _: Paddr = paddr;

        // SAFETY: We have exclusive access to the frame metadata.
        let vtable_ptr: *const core::ptr::DynMetadata<dyn AnyFrameMeta> = unimplemented!();
        // SAFETY: The frame metadata is initialized and valid.
        let vtable_ptr = unsafe { *vtable_ptr };

        let storage_ptr: *mut () = unimplemented!();
        let meta_ptr: *mut dyn AnyFrameMeta = core::ptr::from_raw_parts_mut(
            storage_ptr,
            vtable_ptr,
        );

        // SAFETY: The implementer of the frame metadata decides that if the
        // frame is safe to be read or not.
        let mut reader: VmReader<'_, Infallible> = unimplemented!();

        // SAFETY: `ptr` points to the metadata storage which is valid to be
        // mutably borrowed under `vtable_ptr` because the metadata is valid,
        // the vtable is correct, and we have exclusive access.
        let regions: Tracked<&mut MetaRegionOwners> = Tracked::assume_new();
        let vm_io_owner: Tracked<&mut crate::specs::mm::io::VmIoOwner> = Tracked::assume_new();
        unsafe {
            // Invoke the custom `on_drop` handler.
            (*meta_ptr).on_drop(&mut reader, regions, vm_io_owner);
            // Drop the frame metadata.
            core::ptr::drop_in_place(meta_ptr);
        }
    }
}

/// The metadata of frames that holds metadata of frames.
#[derive(Debug, Default)]
pub struct MetaPageMeta {}

//impl_frame_meta_for!(MetaPageMeta);
/*
/// Initializes the metadata of all physical frames.
///
/// The function returns a list of `Frame`s containing the metadata.
///
/// # Safety
///
/// This function should be called only once and only on the BSP,
/// before any APs are started.
pub(crate) unsafe fn init() -> Segment<MetaPageMeta> {
    let max_paddr = {
        let regions = &crate::boot::EARLY_INFO.get().unwrap().memory_regions;
        regions
            .iter()
            .filter(|r| r.typ() == MemoryRegionType::Usable)
            .map(|r| r.base() + r.len())
            .max()
            .unwrap()
    };

    info!(
        "Initializing frame metadata for physical memory up to {:x}",
        max_paddr
    );

    // In RISC-V, the boot page table has mapped the 512GB memory,
    // so we don't need to add temporary linear mapping.
    // In LoongArch, the DWM0 has mapped the whole memory,
    // so we don't need to add temporary linear mapping.
    #[cfg(target_arch = "x86_64")]
    add_temp_linear_mapping(max_paddr);

    let tot_nr_frames = max_paddr / page_size::<PagingConsts>(1);
    let (nr_meta_pages, meta_pages) = alloc_meta_frames(tot_nr_frames);

    // Map the metadata frames.
    boot_pt::with_borrow(|boot_pt| {
        for i in 0..nr_meta_pages {
            let frame_paddr = meta_pages + i * PAGE_SIZE;
            let vaddr = frame_to_meta::<PagingConsts>(0) + i * PAGE_SIZE;
            let prop = PageProperty {
                flags: PageFlags::RW,
                cache: CachePolicy::Writeback,
                priv_flags: PrivilegedPageFlags::GLOBAL,
            };
            // SAFETY: we are doing the metadata mappings for the kernel.
            unsafe { boot_pt.map_base_page(vaddr, frame_paddr / PAGE_SIZE, prop) };
        }
    })
    .unwrap();

    // Now the metadata frames are mapped, we can initialize the metadata.
    super::MAX_PADDR.store(max_paddr, Ordering::Relaxed);

    let meta_page_range = meta_pages..meta_pages + nr_meta_pages * PAGE_SIZE;

    let (range_1, range_2) = allocator::EARLY_ALLOCATOR
        .lock()
        .as_ref()
        .unwrap()
        .allocated_regions();
    for r in range_difference(&range_1, &meta_page_range) {
        let early_seg = Segment::from_unused(r, |_| EarlyAllocatedFrameMeta).unwrap();
        let _ = ManuallyDrop::new(early_seg);
    }
    for r in range_difference(&range_2, &meta_page_range) {
        let early_seg = Segment::from_unused(r, |_| EarlyAllocatedFrameMeta).unwrap();
        let _ = ManuallyDrop::new(early_seg);
    }

    mark_unusable_ranges();

    Segment::from_unused(meta_page_range, |_| MetaPageMeta {}).unwrap()
}

/// Returns whether the global frame allocator is initialized.
pub(in crate::mm) fn is_initialized() -> bool {
    // `init` sets it with relaxed ordering somewhere in the middle. But due
    // to the safety requirement of the `init` function, we can assume that
    // there is no race conditions.
    super::MAX_PADDR.load(Ordering::Relaxed) != 0
}

fn alloc_meta_frames(tot_nr_frames: usize) -> (usize, Paddr) {
    let nr_meta_pages = tot_nr_frames
        .checked_mul(size_of::<MetaSlot>())
        .unwrap()
        .div_ceil(PAGE_SIZE);
    let start_paddr = allocator::early_alloc(
        Layout::from_size_align(nr_meta_pages * PAGE_SIZE, PAGE_SIZE).unwrap(),
    )
    .unwrap();

    let slots = paddr_to_vaddr(start_paddr) as *mut MetaSlot;

    // Initialize the metadata slots.
    for i in 0..tot_nr_frames {
        // SAFETY: The memory is successfully allocated with `tot_nr_frames`
        // slots so the index must be within the range.
        let slot = unsafe { slots.add(i) };
        // SAFETY: The memory is just allocated so we have exclusive access and
        // it's valid for writing.
        unsafe {
            slot.write(MetaSlot {
                storage: UnsafeCell::new(MetaSlotStorage::Empty([0; FRAME_METADATA_MAX_SIZE - 1])),
                ref_count: AtomicU64::new(REF_COUNT_UNUSED),
                vtable_ptr: UnsafeCell::new(MaybeUninit::uninit()),
                in_list: AtomicU64::new(0),
            })
        };
    }

    (nr_meta_pages, start_paddr)
}

/// Unusable memory metadata. Cannot be used for any purposes.
#[derive(Debug)]
pub struct UnusableMemoryMeta;
impl_frame_meta_for!(UnusableMemoryMeta);

/// Reserved memory metadata. Maybe later used as I/O memory.
#[derive(Debug)]
pub struct ReservedMemoryMeta;
impl_frame_meta_for!(ReservedMemoryMeta);

/// The metadata of physical pages that contains the kernel itself.
#[derive(Debug, Default)]
pub struct KernelMeta;
impl_frame_meta_for!(KernelMeta);

macro_rules! mark_ranges {
    ($region: expr, $typ: expr) => {{
        debug_assert!($region.base() % PAGE_SIZE == 0);
        debug_assert!($region.len() % PAGE_SIZE == 0);

        let seg = Segment::from_unused($region.base()..$region.end(), |_| $typ).unwrap();
        let _ = ManuallyDrop::new(seg);
    }};
}

fn mark_unusable_ranges() {
    let regions = &crate::boot::EARLY_INFO.get().unwrap().memory_regions;

    for region in regions
        .iter()
        .rev()
        .skip_while(|r| r.typ() != MemoryRegionType::Usable)
    {
        match region.typ() {
            MemoryRegionType::BadMemory => mark_ranges!(region, UnusableMemoryMeta),
            MemoryRegionType::Unknown => mark_ranges!(region, ReservedMemoryMeta),
            MemoryRegionType::NonVolatileSleep => mark_ranges!(region, UnusableMemoryMeta),
            MemoryRegionType::Reserved => mark_ranges!(region, ReservedMemoryMeta),
            MemoryRegionType::Kernel => mark_ranges!(region, KernelMeta),
            MemoryRegionType::Module => mark_ranges!(region, UnusableMemoryMeta),
            MemoryRegionType::Framebuffer => mark_ranges!(region, ReservedMemoryMeta),
            MemoryRegionType::Reclaimable => mark_ranges!(region, UnusableMemoryMeta),
            MemoryRegionType::Usable => {} // By default it is initialized as usable.
        }
    }
}

/// Adds a temporary linear mapping for the metadata frames.
///
/// We only assume boot page table to contain 4G linear mapping. Thus if the
/// physical memory is huge we end up depleted of linear virtual memory for
/// initializing metadata.
#[cfg(target_arch = "x86_64")]
fn add_temp_linear_mapping(max_paddr: Paddr) {
    const PADDR4G: Paddr = 0x1_0000_0000;

    if max_paddr <= PADDR4G {
        return;
    }

    // TODO: We don't know if the allocator would allocate from low to high or
    // not. So we prepare all linear mappings in the boot page table. Hope it
    // won't drag the boot performance much.
    let end_paddr = max_paddr.align_up(PAGE_SIZE);
    let prange = PADDR4G..end_paddr;
    let prop = PageProperty {
        flags: PageFlags::RW,
        cache: CachePolicy::Writeback,
        priv_flags: PrivilegedPageFlags::GLOBAL,
    };

    // SAFETY: we are doing the linear mapping for the kernel.
    unsafe {
        boot_pt::with_borrow(|boot_pt| {
            for paddr in prange.step_by(PAGE_SIZE) {
                let vaddr = LINEAR_MAPPING_BASE_VADDR + paddr;
                boot_pt.map_base_page(vaddr, paddr / PAGE_SIZE, prop);
            }
        })
        .unwrap();
    }
}
*/
} // verus!