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::atomic::{PAtomicU8, PAtomicU64, PermissionU64};
use vstd::cell::pcell_maybe_uninit;
use vstd::prelude::*;
use vstd::simple_pptr::{self, PPtr};
use vstd_extra::cast_ptr::*;
use vstd_extra::ownership::*;
use vstd_extra::panic::{may_panic, panic_diverge};
use vstd_extra::prelude::*;

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

verus! {

pub(crate) mod mapping {
    use crate::mm::frame::MetaSlot;
    use crate::mm::frame::meta::meta_slot_size;
    use crate::mm::{PAGE_SIZE, Paddr, Vaddr};
    use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
    use crate::specs::arch::mm::MAX_PADDR;
    pub use crate::specs::mm::frame::mapping::*;
    use vstd::prelude::*;

    #[verifier::inline]
    pub open spec fn frame_to_meta_spec(paddr: Paddr) -> Vaddr {
        (FRAME_METADATA_RANGE.start + (paddr / PAGE_SIZE) * meta_slot_size()) as usize
    }

    #[verifier::inline]
    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.
    #[inline(always)]
    #[verifier::when_used_as_spec(frame_to_meta_spec)]
    pub fn frame_to_meta(paddr: Paddr) -> (res: Vaddr)
        requires
            paddr % PAGE_SIZE == 0,
            paddr < MAX_PADDR,
        ensures
            res == frame_to_meta_spec(paddr),
            res % META_SLOT_SIZE == 0,
    {
        let base = FRAME_METADATA_RANGE.start;
        let offset = paddr / PAGE_SIZE;
        base + offset * META_SLOT_SIZE
    }

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

}

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

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

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

verus! {

#[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.
    ///
    /// # 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.
    pub ref_count: PAtomicU64,
    /// The virtual table that indicates the type of the metadata. 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: 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>;

/// 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,
    /// Verification only: `compare_exchange` returned `Err`, retry
    Retry,
}

pub open spec fn get_slot_spec(paddr: Paddr) -> (res: PPtr<MetaSlot>)
    recommends
        paddr % 4096 == 0,
        paddr < MAX_PADDR,
{
    let slot = frame_to_meta(paddr);
    PPtr(slot, PhantomData::<MetaSlot>)
}

/// Space-holder of the AnyFrameMeta virtual table.
///
/// Dyn-compatible: no `Self`-by-value, no associated types on dispatched
/// methods, no dyn-incompatible supertrait. `vtable_ptr` is `Self: Sized`
/// because it's only used statically (the runtime vtable pointer lives on
/// the slot, not on the instance). Sites that need `Repr<MetaSlotStorage>`
/// must spell it out — it was previously a supertrait.
pub unsafe trait AnyFrameMeta {
    /// 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
    }

    exec 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)),
    {
    }

    exec fn is_untyped(&self) -> bool {
        false
    }

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

global layout MetaSlot is size == 64, align == 8;

pub broadcast axiom fn size_of_meta_slot()
    ensures
        #![trigger size_of::<MetaSlot>()]
        #![trigger align_of::<MetaSlot>()]
        size_of::<MetaSlot>() == 64,
        align_of::<MetaSlot>() == 8,
;

#[inline(always)]
#[verifier::allow_in_spec]
pub const fn meta_slot_size() -> (res: usize)
    returns
        64usize,
{
    size_of::<MetaSlot>()
}

pub open spec fn has_safe_slot(paddr: Paddr) -> bool {
    &&& paddr % PAGE_SIZE == 0
    &&& paddr < MAX_PADDR
}

/// 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 pointer to its metadata slot.
/// ## Safety
/// Verus ensures that the pointer will only be used when we have a permission object, so creating it is safe.
#[verus_spec(res =>
    ensures
        has_safe_slot(paddr) <==> res is Ok,
        res is Ok ==> res.unwrap().addr() == frame_to_meta(paddr),
)]
pub(super) fn get_slot(paddr: Paddr) -> Result<PPtr<MetaSlot>, GetFrameError> {
    if paddr % PAGE_SIZE != 0 {
        return Err(GetFrameError::NotAligned);
    }
    if paddr >= MAX_PADDR {
        return Err(GetFrameError::OutOfBound);
    }
    let vaddr = 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(ptr)
}

#[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<&vstd::simple_pptr::PointsTo<MetaSlot>>,
        requires
            self == perm.value(),
        returns
            perm.addr(),
    )]
    fn addr_of(&self) -> Paddr {
        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>
        requires
            old(regions).inv(),
        ensures
            // Helper: on success, `regions.slots` loses the extracted slot
            // (caller is responsible for re-parking it via `sync_slot_perm`
            // to restore `regions.inv()`). On Err, regions is left intact
            // and the inv is preserved.
            res is Err ==> final(regions).inv(),
            // On failure the slot perm/owner are re-parked unchanged: nothing
            // was claimed, so the whole region state is intact.
            res is Err ==> *final(regions) == *old(regions),
            res matches Ok((res, perm)) ==> Self::get_from_unused_perm_spec(paddr, metadata, as_unique_ptr, res, perm@),
            res matches Ok((res, perm)) ==> perm@.value().wf(
                final(regions).slot_owners[frame_to_index(paddr)]),
            // The returned perm is exactly the slot perm that was extracted
            // from `regions.slots`. Lets callers re-park via `sync_slot_perm`
            // and recover `final.slots == old.slots`.
            res matches Ok((_, perm)) ==> perm@ == old(regions).slots[frame_to_index(paddr)],
            res is Ok ==> Self::get_from_unused_spec(paddr, as_unique_ptr, *old(regions), *final(regions)),
            // The extracted slot perm is handed back via the out-param, so it
            // leaves `regions.slots` (caller re-parks it via `sync_slot_perm`).
            res is Ok ==> Self::slot_perm_extracted_spec(paddr, *old(regions), *final(regions)),
            !has_safe_slot(paddr) ==> res is Err,
            // Linear-drop pilot: claiming an unused slot doesn't mint or
            // redeem segment or frame obligations on any path.
            final(regions).frame_obligations =~= old(regions).frame_obligations,
    )]
    pub(super) fn get_from_unused<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>(
        paddr: Paddr,
        metadata: M,
        as_unique_ptr: bool,
    ) -> Result<(PPtr<Self>, Tracked<vstd::simple_pptr::PointsTo<MetaSlot>>), GetFrameError> {
        let slot = get_slot(paddr)?;

        proof {
            assert(has_safe_slot(paddr));
            regions.inv_implies_correct_addr(paddr);
        }

        let tracked mut slot_own = regions.slot_owners.tracked_remove(frame_to_index(paddr));
        let tracked mut slot_perm = regions.slots.tracked_remove(frame_to_index(paddr));

        // `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.borrow(Tracked(&slot_perm)).ref_count.compare_exchange(
            Tracked(&mut slot_own.inner_perms.ref_count),
            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 {
                let idx = frame_to_index(paddr);
                regions.slot_owners.tracked_insert(idx, slot_own);
                regions.slots.tracked_insert(idx, slot_perm);
                // 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].inner_perms.ref_count,
                    old(regions).slot_owners[idx].inner_perms.ref_count,
                );
                assert(regions.slot_owners[idx] == old(regions).slot_owners[idx]);
                assert(regions.slot_owners =~= old(regions).slot_owners);
                assert(regions.slots =~= old(regions).slots);
                assert(*regions == *old(regions));
            }

            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.inner_perms.storage), Tracked(&mut slot_own.inner_perms.vtable_ptr))]
            slot.borrow(Tracked(&slot_perm)).write_meta(metadata)
        };

        if as_unique_ptr {
            slot.borrow(Tracked(&slot_perm)).ref_count.store(
                Tracked(&mut slot_own.inner_perms.ref_count),
                REF_COUNT_UNIQUE,
            );
        } else {
            slot.borrow(Tracked(&slot_perm)).ref_count.store(
                Tracked(&mut slot_own.inner_perms.ref_count),
                1,
            );
        }

        proof {
            slot_own.usage = PageUsage::Frame;
            assert(slot_perm.value().wf(slot_own));
            regions.slot_owners.tracked_insert(frame_to_index(paddr), slot_own);
        }

        Ok((slot, Tracked(slot_perm)))
    }

    /// The inner loop of `Self::get_from_in_use`.
    /// # Verified Properties
    /// ## Preconditions
    /// - The permission must point to the slot.
    /// - The permission must be initialized.
    /// - **Liveness**: The reference count of the inner permissions must not be at the maximum.
    /// ## Postconditions
    /// - The reference count of the inner permissions is increased by one.
    #[verus_spec(res =>
        with Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,
            Tracked(inner_perms): Tracked<&mut MetadataInnerPerms>,
        requires
            perm.pptr() == slot,
            perm.is_init(),
            perm.value().ref_count.id() == old(inner_perms).ref_count.id(),
            old(inner_perms).ref_count.value() >= REF_COUNT_MAX ==> may_panic(),
        ensures
            res is Ok ==> final(inner_perms).ref_count.value() == old(inner_perms).ref_count.value() + 1,
            res is Ok ==> final(inner_perms).ref_count.value() <= REF_COUNT_MAX,
            res is Ok ==> old(inner_perms).ref_count.value() > 0,
            res matches Ok(ptr) ==> ptr == slot,
            res is Err ==> final(inner_perms).ref_count.value() == old(inner_perms).ref_count.value(),
            final(inner_perms).ref_count.id() == old(inner_perms).ref_count.id(),
            final(inner_perms).storage == old(inner_perms).storage,
            final(inner_perms).vtable_ptr == old(inner_perms).vtable_ptr,
            final(inner_perms).in_list == old(inner_perms).in_list,
    )]
    fn get_from_in_use_loop(slot: PPtr<MetaSlot>) -> Result<PPtr<Self>, GetFrameError> {
        match slot.borrow(Tracked(perm)).ref_count.load(Tracked(&mut inner_perms.ref_count)) {
            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.borrow(Tracked(perm)).ref_count.compare_exchange_weak(
                    Tracked(&mut inner_perms.ref_count),
                    last_ref_cnt,
                    last_ref_cnt + 1,
                ).is_ok() {
                    return Ok(slot);
                } else {
                    return Err(GetFrameError::Retry);
                }
            },
        }
    }

    /// Gets another owning pointer to the metadata slot from the given page.
    /// # Verified Properties
    /// ## Verification Design
    /// To simplify the verification, we verify the loop body separately from the outer loop. 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(),
            has_safe_slot(paddr) ==> old(regions).ref_count(frame_to_index(paddr)) >= REF_COUNT_MAX ==> may_panic(),
        ensures
            final(regions).inv(),
            !has_safe_slot(paddr) ==> res is Err,
            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]
    pub(super) fn get_from_in_use(paddr: Paddr) -> Result<PPtr<Self>, GetFrameError> {
        let ghost regions0 = *regions;

        let slot = get_slot(paddr)?;

        proof {
            assert(regions0 == *old(regions));
            assert(has_safe_slot(paddr));
            // `get_slot` succeeded ⟹ `has_safe_slot(paddr)`; with `regions.inv()`
            // that recovers the slot facts the caller used to supply: the slot is
            // present, its address is `frame_to_meta(paddr)`, and its inner-perm
            // ref-count cell matches the slot's (via the per-slot `wf`).
            broadcast use crate::mm::frame::meta::mapping::group_page_meta;

            regions.inv_implies_correct_addr(paddr);
        }

        let tracked mut slot_own = regions.slot_owners.tracked_remove(frame_to_index(paddr));
        let tracked slot_perm = regions.slots.tracked_borrow(frame_to_index(paddr));

        let ghost pre = slot_own.inner_perms.ref_count.value();

        loop
            invariant
                has_safe_slot(paddr),
                slot_perm.addr() == slot.addr(),
                slot_perm.is_init(),
                slot_perm.value().ref_count.id() == slot_own.inner_perms.ref_count.id(),
                slot_own.inner_perms.ref_count.value() == pre,
                slot_own.inner_perms.ref_count.value() >= REF_COUNT_MAX ==> may_panic(),
                regions0.slots.contains_key(frame_to_index(paddr)),
                regions0.slot_owners.contains_key(frame_to_index(paddr)),
                regions0.inv(),
                regions0.slots[frame_to_index(paddr)] == *slot_perm,
                slot_own.self_addr == regions0.slot_owners[frame_to_index(paddr)].self_addr,
                slot_own.usage == regions0.slot_owners[frame_to_index(paddr)].usage,
                slot_own.paths_in_pt == regions0.slot_owners[frame_to_index(paddr)].paths_in_pt,
                FRAME_METADATA_RANGE.start <= slot_own.self_addr < FRAME_METADATA_RANGE.end,
                slot_own.self_addr % META_SLOT_SIZE == 0,
                slot_own.self_addr == slot_perm.addr(),
                slot_perm.value().storage.id() == slot_own.inner_perms.storage.id(),
                slot_perm.value().vtable_ptr == slot_own.inner_perms.vtable_ptr.pptr(),
                slot_perm.value().in_list.id() == slot_own.inner_perms.in_list.id(),
                slot_own.inner_perms.ref_count.id() == regions0.slot_owners[frame_to_index(
                    paddr,
                )].inner_perms.ref_count.id(),
                slot_own.inner_perms.storage == regions0.slot_owners[frame_to_index(
                    paddr,
                )].inner_perms.storage,
                slot_own.inner_perms.vtable_ptr == regions0.slot_owners[frame_to_index(
                    paddr,
                )].inner_perms.vtable_ptr,
                slot_own.inner_perms.in_list == regions0.slot_owners[frame_to_index(
                    paddr,
                )].inner_perms.in_list,
                // pre equals the original ref_count value
                pre == regions0.slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value(),
                // regions0 equals old(regions)
                regions0 == *old(regions),
                // slot pptr matches what postcondition expects
                slot == regions0.slots[frame_to_index(paddr)].pptr(),
                // regions state: slot_owners has idx removed; slots borrowed (unchanged)
                regions.slot_owners == regions0.slot_owners.remove(frame_to_index(paddr)),
                regions.slots == regions0.slots,
                // Linear-drop pilot: this path doesn't mint/redeem segment
                // obligations, so the ledger is invariant.
                regions.frame_obligations =~= regions0.frame_obligations,
        {
            match #[verus_spec(with Tracked(slot_perm), Tracked(&mut slot_own.inner_perms))]
            Self::get_from_in_use_loop(slot) {
                Err(GetFrameError::Retry) => {
                    core::hint::spin_loop();
                },
                res => {
                    proof {
                        let idx = frame_to_index(paddr);

                        assert(slot_own.inner_perms.ref_count.id()
                            == regions0.slot_owners[idx].inner_perms.ref_count.id());

                        let ghost orig = regions0.slot_owners[idx];
                        assert(orig.inv());
                        assert(pre == orig.inner_perms.ref_count.value());

                        assert(slot_own.inner_perms.vtable_ptr == orig.inner_perms.vtable_ptr);

                        if res is Ok {
                            assert(slot_own.inner_perms.ref_count.value() == pre + 1);
                            assert(slot_own.inner_perms.ref_count.value() <= REF_COUNT_MAX);
                            assert(pre > 0);
                            assert(0 < orig.inner_perms.ref_count.value());
                            assert(orig.inner_perms.ref_count.value() <= REF_COUNT_MAX);
                            assert(orig.inner_perms.vtable_ptr.is_init());
                            assert(slot_own.inner_perms.vtable_ptr.is_init());
                        } else {
                            assert(slot_own.inner_perms.ref_count.value() == pre);
                            assert(slot_own.inner_perms.ref_count.value()
                                == orig.inner_perms.ref_count.value());
                            assert(slot_own.inner_perms.ref_count.id()
                                == orig.inner_perms.ref_count.id());
                            assert(slot_own.inner_perms.storage == orig.inner_perms.storage);
                            assert(slot_own.inner_perms.vtable_ptr == orig.inner_perms.vtable_ptr);
                            assert(slot_own.inner_perms.in_list == orig.inner_perms.in_list);
                        }
                        assert(slot_own.inv());
                        assert(slot_perm.value().wf(slot_own));
                        assert(slot_own.self_addr == slot_perm.addr());

                        if res is Err {
                            assert(slot_own.inner_perms.ref_count.value() == pre);
                            assert(slot_own.inner_perms.ref_count.id()
                                == orig.inner_perms.ref_count.id());
                            assert(slot_own.inner_perms.storage == orig.inner_perms.storage);
                            assert(slot_own.inner_perms.vtable_ptr == orig.inner_perms.vtable_ptr);
                            assert(slot_own.inner_perms.in_list == orig.inner_perms.in_list);
                        }
                        regions.slot_owners.tracked_insert(idx, slot_own);

                        assert(regions.slot_owners.dom() =~= regions0.slot_owners.dom());
                        assert(regions.slots =~= regions0.slots);

                        assert forall|i: usize| i != idx implies #[trigger] regions.slot_owners[i]
                            == regions0.slot_owners[i] by {};

                        assert(regions.slot_owners[idx].inner_perms.ref_count.id()
                            == regions0.slot_owners[idx].inner_perms.ref_count.id());
                        assert(regions.slot_owners[idx].inner_perms.storage
                            == regions0.slot_owners[idx].inner_perms.storage);
                        assert(regions.slot_owners[idx].inner_perms.vtable_ptr
                            == regions0.slot_owners[idx].inner_perms.vtable_ptr);
                        assert(regions.slot_owners[idx].inner_perms.in_list
                            == regions0.slot_owners[idx].inner_perms.in_list);
                        assert(regions.slot_owners[idx].self_addr
                            == regions0.slot_owners[idx].self_addr);
                        assert(regions.slot_owners[idx].usage == regions0.slot_owners[idx].usage);

                        // For ptr postcondition: slot_perm.pptr() == old(regions).slots[idx].pptr()
                        assert(*slot_perm == regions0.slots[idx]);

                        // For Err ==> *regions == *old(regions)
                        if res is Err {
                            // On Err, ref_count unchanged so slot_own == orig.
                            // Use extensional equality axiom for PermissionU64.
                            assert(regions.slot_owners[idx].inner_perms.ref_count.value()
                                == regions0.slot_owners[idx].inner_perms.ref_count.value());
                            assert(regions.slot_owners[idx].inner_perms.ref_count.id()
                                == regions0.slot_owners[idx].inner_perms.ref_count.id());
                            vstd_extra::auxiliary::axiom_permission_u64_ext_eq(
                                regions.slot_owners[idx].inner_perms.ref_count,
                                regions0.slot_owners[idx].inner_perms.ref_count,
                            );
                            assert(regions.slot_owners[idx] == regions0.slot_owners[idx]);
                            assert(regions.slot_owners =~= regions0.slot_owners);
                            assert(*regions == *old(regions));
                        }
                    }

                    return res;
                },
            }
        }
    }

    /// 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<&vstd::simple_pptr::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`.
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety**: The caller must provide an existing permission that matches the contents of the metadata slot.
    /// ## Postconditions
    /// - **Correctness**: The function returns a pointer to the stored metadata, of type `M`.
    /// ## Safety
    /// - Calling the method is always safe, but using the returned pointer could
    /// be unsafe. Specifically, the dereferencer should ensure that:
    ///  - the stored metadata is initialized (by [`Self::write_meta`]) and valid;
    ///  - the initialized metadata is of type `M` (`Repr<M>::wf`);
    ///  - the returned pointer should not be dereferenced as mutable unless having exclusive access to the metadata slot.
    #[verus_spec(res =>
        with
            Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,
        requires
            self == perm.value(),
        ensures
            res.ptr.addr() == perm.addr(),
            res.addr() == perm.addr(),
    )]
    pub(super) fn as_meta_ptr<M: AnyFrameMeta + Repr<MetaSlotStorage>>(&self) -> ReprPtr<
        MetaSlot,
        Metadata<M>,
    > {
        proof_with!(Tracked(perm));
        let addr = self.addr_of();

        proof_with!(Tracked(perm));
        self.cast_slot(addr)
    }

    /// Writes the metadata to the slot without reading or dropping the previous value.
    ///
    /// # 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(vtable_perm): Tracked<&mut vstd::simple_pptr::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(),
            Metadata::<M>::metadata_from_inner_perms(*final(meta_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).
        Metadata::<M>::write_metadata_into_storage(&self.storage, Tracked(meta_perm), metadata);
    }

    /// Drops the metadata and deallocates the frame.
    ///
    /// # 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).inner_perms.ref_count.id(),
            Self::drop_last_in_place_safety_cond(*old(owner)),
        ensures
            final(owner).inv(),
            final(owner).inner_perms.ref_count.value() == REF_COUNT_UNUSED,
            final(owner).inner_perms.ref_count.id() == old(owner).inner_perms.ref_count.id(),
            final(owner).inner_perms.storage.id() == old(owner).inner_perms.storage.id(),
            final(owner).inner_perms.storage.is_uninit(),
            final(owner).inner_perms.vtable_ptr.is_uninit(),
            final(owner).inner_perms.vtable_ptr.pptr() == old(owner).inner_perms.vtable_ptr.pptr(),
            final(owner).inner_perms.in_list == old(owner).inner_perms.in_list,
            final(owner).self_addr == old(owner).self_addr,
            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.inner_perms.ref_count), 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).inner_perms.ref_count.value() == 0 || old(slot_own).inner_perms.ref_count.value() == REF_COUNT_UNIQUE,
            old(slot_own).inner_perms.storage.is_init(),
            old(slot_own).inner_perms.in_list.value() == 0,
        ensures
            final(slot_own).inner_perms.ref_count == old(slot_own).inner_perms.ref_count,
            final(slot_own).inner_perms.storage.is_uninit(),
            final(slot_own).inner_perms.storage.id() == old(slot_own).inner_perms.storage.id(),
            final(slot_own).inner_perms.in_list == old(slot_own).inner_perms.in_list,
            final(slot_own).inner_perms.vtable_ptr.is_uninit(),
            final(slot_own).inner_perms.vtable_ptr.pptr() == old(slot_own).inner_perms.vtable_ptr.pptr(),
            final(slot_own).self_addr == old(slot_own).self_addr,
            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) 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!