ostd/mm/page_table/node/

entry.rs

// SPDX-License-Identifier: MPL-2.0
//! This module provides accessors to the page table entries in a node.
use vstd::prelude::*;
use vstd_extra::{ghost_tree::*, ownership::*};

use crate::specs::{
    arch::*,
    mm::{
        frame::{
            mapping::{frame_to_index, meta_to_index},
            meta_region_owners::MetaRegionOwners,
        },
        page_table::{INC_LEVELS, PageTableOwner},
    },
    task::InAtomicMode,
};

use super::*;
use crate::arch::mm::PagingConsts;
use crate::mm::frame::meta::mapping::{frame_to_meta, meta_to_frame};
use crate::mm::frame::{Frame, FrameRef, meta::REF_COUNT_UNUSED};
use crate::mm::page_table::*;
use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
use crate::{
    mm::{nr_subpage_per_huge, nr_subpage_per_huge_spec, page_prop::PageProperty},
    //    sync::RcuDrop,
    //    task::atomic_mode::InAtomicMode,
};
use core::marker::PhantomData;
use core::ops::Deref;

verus! {

broadcast use group_ghost_tree_lemmas;

/// A reference to a page table node.
pub type PageTableNodeRef<'a, C> = FrameRef<'a, PageTablePageMeta<C>>;

/// A guard that holds the lock of a page table node.
pub struct PageTableGuard<'rcu, C: PageTableConfig> {
    pub inner: PageTableNodeRef<'rcu, C>,
}

impl<'rcu, C: PageTableConfig> Deref for PageTableGuard<'rcu, C> {
    type Target = PageTableNodeRef<'rcu, C>;

    #[verus_spec(ensures returns self.inner)]
    fn deref(&self) -> &Self::Target {
        &self.inner
    }
}

pub struct Entry<'a, 'rcu, C: PageTableConfig> {
    /// The page table entry.
    ///
    /// We store the page table entry here to optimize the number of reads from
    /// the node. We cannot hold a `&mut E` reference to the entry because that
    /// other CPUs may modify the memory location for accessed/dirty bits. Such
    /// accesses will violate the aliasing rules of Rust and cause undefined
    /// behaviors.
    ///
    /// # Verification Design
    /// The concrete value of a PTE is specific to the architecture and the page table configuration,
    /// represented by the type `C::E`. We represent its value as an abstract [`EntryOwner`], which is
    /// connected to the concrete value by `match_pte`. The `EntryOwner` is well-formed with respect to
    /// `Entry` if it is related to the concrete value by `match_pte`.
    ///
    /// An `Entry` can be thought of as a mutable handle to the concrete value of the PTE.
    /// The `node` field is a mutable reference to the guard of the node that contains the entry,
    /// `index` provides the offset, and the `pte` is current value. Only one `Entry` can exist for
    /// a given node at any given time.
    pub pte: C::E,
    /// The index of the entry in the node.
    pub idx: usize,
    /// The node that contains the entry.
    pub node: &'a mut PageTableGuard<'rcu, C>,
}

#[verus_verify]
impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
    pub open spec fn new_spec(
        pte: C::E,
        idx: usize,
        node: &'a mut PageTableGuard<'rcu, C>,
    ) -> Self {
        Self { pte, idx, node }
    }

    #[verus_spec(res =>
        ensures
            res.pte == pte,
            res.idx == idx,
            *res.node == *old(node),
            *final(node) == *final(res.node),
    )]
    pub fn new(pte: C::E, idx: usize, node: &'a mut PageTableGuard<'rcu, C>) -> Self {
        Self { pte, idx, node }
    }
}

#[verus_verify]
impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
    /// Returns if the entry does not map to anything.
    #[verus_spec(r =>
        with Tracked(owner): Tracked<&EntryOwner<C>>,
        requires
            self.wf(*owner),
            owner.inv(),
        returns owner.is_absent(),
    )]
    pub(in crate::mm) fn is_none(&self) -> bool {
        !self.pte.is_present()
    }

    /// Returns if the entry maps to a page table node.
    #[verus_spec(
        with Tracked(owner): Tracked<EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&NodeOwner<C>>,
        requires
            owner.inv(),
            self.wf(owner),
            parent_owner.relate_guard(*self.node),
            parent_owner.inv(),
            parent_owner.level() == owner.parent_level,
        returns
            owner.is_node(),
    )]
    pub(in crate::mm) fn is_node(&self) -> bool {
        self.pte.is_present() && !self.pte.is_last(
            #[verus_spec(with Tracked(&*parent_owner))]
            self.node.level(),
        )
    }

    /// Gets a reference to the child.
    #[verus_spec(res =>
        with Tracked(owner): Tracked<&EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&NodeOwner<C>>,
             Tracked(regions): Tracked<&mut MetaRegionOwners>,
        requires
            self.invariants(*owner, *old(regions)),
            self.node_matching(*owner, *parent_owner, *self.node),
            parent_owner.metaregion_sound_node(*old(regions)),
        ensures
            res.invariants(*owner, *final(regions)),
            final(regions).slots == old(regions).slots,
            final(regions).slot_owners == old(regions).slot_owners,
            forall|k: int|
                old(regions).slots.contains_key(k) ==> #[trigger] final(regions).slots.contains_key(
                    k,
                ),
            forall|k: int|
                old(regions).slots.contains_key(k) ==> old(regions).slots[k]
                    == #[trigger] final(regions).slots[k],
            final(regions).inv(),
    )]
    pub(in crate::mm) fn to_ref(&self) -> ChildRef<'rcu, C> {
        #[verus_spec(with Tracked(&*parent_owner))]
        let level = self.node.level();

        // SAFETY:
        //  - The PTE outlives the reference (since we have `&self`).
        //  - The level matches the current node.
        let res = unsafe {
            #[verus_spec(with Tracked(regions), Tracked(owner))]
            ChildRef::from_pte(&self.pte, level)
        };

        res
    }

    /// Operates on the mapping properties of the entry.
    ///
    /// It only modifies the properties if the entry is present.
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety Invariants**: The entry must satisfy the relevant safety invariants.
    /// - **Safety**: The entry must be a frame.
    /// ## Postconditions
    /// - **Safety Invariants**: The entry continues to satisfy the relevant safety invariants.
    /// - **Safety**: The guard permission is preserved.
    /// - **Correctness**: The entry's permissions are updated by `op`
    /// ## Safety
    /// - The entry is updated in place, only changing its properties.
    /// `regions` is passed read-only to source the parent node's slot perm
    /// via the borrow-model bridge (used by `write_pte`'s `start_paddr` call).
    #[verus_spec(
        with Tracked(owner) : Tracked<&mut EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
             Tracked(regions): Tracked<&MetaRegionOwners>,
        requires
            old(owner).inv(),
            old(self).wf(*old(owner)),
            old(self).node_matching(*old(owner), *old(parent_owner), *old(self).node),
            op.requires((old(self).pte.prop(),)),
            old(owner).is_frame(),
            regions.inv(),
            regions.slots.contains_key(old(parent_owner).slot_index),
            old(parent_owner).metaregion_sound_node(*regions),
            // `op` must preserve the trackedness of `item_from_raw(pa, level, _)`
            // across the prop change so frame-accounting guarantees remain unchanged.
            // For `KernelPtConfig`, `C::tracked(item)` reads `prop.flags.AVAIL1`, so this
            // precondition reduces to "op preserves AVAIL1". For `UserPtConfig`,
            // `C::tracked` is constant `true`, so this is trivial.
            forall|pa: Paddr, level: PagingLevel, p_in: PageProperty, p_out: PageProperty,
                perm: Tracked<Option<C::Perm>>|
                #![auto]
                op.ensures((p_in,), p_out) ==> (
                    C::item_into_raw(C::item_from_raw(pa, level, p_out, perm)).3@
                        is Some
                ) == (perm@ is Some),
            forall|pa: Paddr, level: PagingLevel, p_in: PageProperty, p_out: PageProperty|
                #![auto]
                op.ensures((p_in,), p_out) && C::E::new_page_req(pa, level, p_in)
                    ==> C::E::new_page_req(pa, level, p_out),
        ensures
            final(owner).inv(),
            final(self).wf(*final(owner)),
            final(self).node_matching(*final(owner), *final(parent_owner), *final(self).node),
            final(self).parent_perms_preserved(*old(parent_owner), *final(parent_owner)),
            final(owner).is_frame(),
            final(owner).frame().mapped_pa == old(owner).frame().mapped_pa,
            final(owner).frame_permission() == old(owner).frame_permission(),
            final(owner).frame_is_tracked() == old(owner).frame_is_tracked(),
            final(owner).path == old(owner).path,
            final(owner).parent_level == old(owner).parent_level,
            final(self).idx == old(self).idx,
            *final(self).node == *old(self).node,
            old(self).pte.is_present() ==> op.ensures(
                (old(owner).frame().prop,),
                final(owner).frame().prop,
            ),
            // `protect` only changes a present PTE's `prop` (never its
            // present-status) and never touches `nr_children`, so the present
            // count and the counter are both unchanged — keeping the parent's
            // `count_consistent` invariant intact for the caller.
            crate::specs::mm::page_table::node::owners::count_present(
                final(parent_owner).children_perm.value(),
            ) == crate::specs::mm::page_table::node::owners::count_present(
                old(parent_owner).children_perm.value(),
            ),
            final(parent_owner).meta_own.nr_children.value() == old(
                parent_owner,
            ).meta_own.nr_children.value(),
    )]
    pub(in crate::mm) fn protect(&mut self, op: impl FnOnce(PageProperty) -> PageProperty) {
        #[verus_spec(with Tracked(owner), Tracked(parent_owner), Tracked(regions))]
        let pte = self.node.protect_child(self.idx, op);
        self.pte = pte;
    }

    /// Replaces the entry with a new child.
    ///
    /// The old child is returned.
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety Invariants**: Both old and new owners must satisfy the respective safety invariants for an [Entry](Entry::invariants)
    /// and a [Child](Child::invariants).
    /// - **Safety**: The caller must provide valid owners for all objects, and for the parent node where the entry
    /// is being replaced. The parent node must have a valid guard permission.
    /// - **Correctness**: The new child must be compatible with the old, for instance by having the same level.
    /// ## Postconditions
    /// - **Safety Invariants**: The old and new owners will satisfy the safety invariants for an [Entry](Entry::invariants)
    /// and a [Child](Child::invariants), but they have changed positions.
    /// - **Safety**: Safety properties that hold across the page table's tree structure are preserved
    /// everywhere except for the entry being replaced.
    /// - **Correctness**: The entry will match the argument, and the returned child will match the entry that was replaced.
    /// ## Safety
    /// - The invariants ensure that the entry is appropriately aligned and its index is within bounds.
    /// - The transformation from child to entry ensures that the tree now owns the updated entry.
    #[verus_spec(res =>
        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
             Tracked(owner): Tracked<&mut EntryOwner<C>>,
             Tracked(new_owner): Tracked<&mut EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
        requires
            old(self).invariants(*old(owner), *old(regions)),
            new_child.invariants(*old(new_owner), *old(regions)),
            old(self).node_matching(*old(owner), *old(parent_owner), *old(self).node),
            old(self).new_owner_compatible(new_child, *old(owner), *old(new_owner), *old(regions)),
            old(parent_owner).metaregion_sound_node(*old(regions)),
        ensures
            res matches Child::PageTable(node) ==> {
                &&& node.tracked_slot_perm@ == final(regions).slots[final(owner).node().slot_index]
                &&& node.tracked_metadata_perm@ is None
            },
            final(self).invariants(*final(new_owner), *final(regions)),
            res.invariants(*final(owner), *final(regions)),
            final(self).node_matching(*final(new_owner), *final(parent_owner), *final(self).node),
            final(self).idx == old(self).idx,
            *final(self).node == *old(self).node,
            *final(owner) == old(owner).from_pte_owner_spec(),
            *final(new_owner) == old(new_owner).into_pte_owner_spec(),
            Self::metaregion_sound_neq_preserved(
                *old(owner),
                *final(new_owner),
                *old(regions),
                *final(regions),
            ),
            !final(new_owner).is_node() ==> Self::metaregion_sound_neq_old_preserved(
                *old(owner),
                *old(regions),
                *final(regions),
            ),
            (!old(owner).is_node() && !final(new_owner).is_node())
                ==> Self::metaregion_sound_preserved(*old(regions), *final(regions)),
            final(new_owner).is_node() && !final(new_owner).is_absent() ==> PageTableOwner::<
                C,
            >::path_tracked_pred(*final(regions))(*final(new_owner), final(new_owner).path),
            final(self).parent_perms_preserved(*old(parent_owner), *final(parent_owner)),
            final(parent_owner).metaregion_sound_node(*final(regions)),
            forall|idx: int|
                #![trigger final(regions).slot_owners[idx].paths_in_pt]
                (!final(new_owner).is_node() || final(new_owner).is_absent() || idx
                    != frame_to_index(final(new_owner).meta_slot_paddr()->0))
                    ==> final(regions).slot_owners[idx].paths_in_pt == old(
                    regions,
                ).slot_owners[idx].paths_in_pt,
            forall|idx: int|
                #![trigger final(regions).slot_owners[idx].ref_count()]
                final(regions).ref_count(idx) == old(
                    regions,
                ).ref_count(idx),
            forall|idx: int|
                #![trigger final(regions).slot_owners[idx]]
                final(regions).slot_owners[idx].same_permissions(
                    old(regions).slot_owners[idx],
                ),
            final(regions).slots == old(regions).slots,
            forall|idx: int| #![trigger final(regions).slot_owners[idx].usage]
                old(regions).contains(idx) ==>
                    final(regions).slot_owners[idx].usage == old(regions).slot_owners[idx].usage,
            // When both old and new are not nodes: from_pte/into_pte are identity.
            (!old(owner).is_node() && !final(new_owner).is_node()) ==> {
                &&& forall|i: int|
                    #![trigger final(regions).slot_owners[i]]
                    final(regions).slot_owners[i] == old(
                        regions,
                    ).slot_owners[i]
            },
            Self::replace_nonpanic_condition(*old(parent_owner), *old(new_owner)),
    )]
    #[verifier::spinoff_prover]
    pub(in crate::mm) fn replace(&mut self, new_child: Child<C>) -> Child<C> {
        let ghost cp0 = parent_owner.children_perm.value();
        let ghost initial_regions = *regions;
        let ghost initial_owner = *owner;

        #[cfg(feature = "allow_panic")]
        {
            let guard_level = self.node.level();
            match &new_child {
                Child::PageTable(node) => {
                    assert!(node.level() == guard_level - 1);
                },
                Child::Frame(_, level, _) => {
                    assert!(*level == guard_level);
                },
                Child::None => {},
            }
        }

        // SAFETY:
        //  - The PTE is not referenced by other `ChildRef`s (since we have `&mut self`).
        //  - The level matches the current node.
        #[verus_spec(with Tracked(&*parent_owner))]
        let level = self.node.level();

        let old_child = unsafe {
            #[verus_spec(with Tracked(regions), Tracked(owner))]
            Child::from_pte(self.pte, level)
        };

        if old_child.is_none() && !new_child.is_none() {
            #[verus_spec(with
                Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                    &parent_owner.frame_permission,
                )),
                Ghost(parent_owner.meta_own.nr_children.id())
            )]
            let nr_children = self.node.nr_children_mut();
            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
            proof {
                parent_owner.lemma_nr_children_absent_slot_bound(self.idx);
            }
            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
        } else if !old_child.is_none() && new_child.is_none() {
            #[verus_spec(with
                Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                    &parent_owner.frame_permission,
                )),
                Ghost(parent_owner.meta_own.nr_children.id())
            )]
            let nr_children = self.node.nr_children_mut();
            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
            proof {
                parent_owner.nr_children_present_slot_bound(self.idx);
            }
            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp - 1);
        }
        #[verus_spec(with Tracked(new_owner))]
        let new_pte = new_child.into_pte();

        // SAFETY:
        //  1. The index is within the bounds.
        //  2. The new PTE is a valid child whose level matches the current page table node.
        //  3. The ownership of the child is passed to the page table node.
        unsafe {
            #[verus_spec(with Tracked(parent_owner), Tracked(&*regions))]
            self.node.write_pte(self.idx, new_pte)
        };

        self.pte = new_pte;

        proof {
            // Install new entry's path into its slot's paths_in_pt.
            if new_owner.is_node() {
                let paddr = new_owner.meta_slot_paddr().unwrap();

                let tracked mut new_meta_slot = regions.tracked_borrow_mut_slot_owner(paddr);
                new_meta_slot.paths_in_pt = set![new_owner.path];
            }
        }

        proof {
            if new_owner.is_node() || new_owner.is_frame() {
                let paddr = new_owner.meta_slot_paddr().unwrap();
            }
            if owner.is_frame() {
                let paddr = owner.frame().mapped_pa;
                let slot = frame_to_index(paddr);
                C::lemma_perm_well_formed_with_region_preserved(
                    paddr,
                    Tracked(owner.frame_permission()),
                    initial_regions,
                    *regions,
                );
            }
            if new_owner.is_frame() {
                let paddr = new_owner.frame().mapped_pa;
                let slot = frame_to_index(paddr);
            }
            assert(Self::metaregion_sound_neq_preserved(
                initial_owner,
                *new_owner,
                initial_regions,
                *regions,
            )) by {
                let f = |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
                    entry.meta_slot_paddr_neq(initial_owner) && entry.meta_slot_paddr_neq(
                        *new_owner,
                    ) && entry.metaregion_sound(initial_regions);
                let g = |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
                    entry.metaregion_sound(*regions);
                assert forall|entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
                    entry.inv() && f(entry, path) implies #[trigger] g(entry, path) by {
                    if entry.is_frame() {
                        let paddr = entry.frame().mapped_pa;
                        C::lemma_perm_well_formed_with_region_preserved(
                            paddr,
                            Tracked(entry.frame_permission()),
                            initial_regions,
                            *regions,
                        );
                    }
                };
            };
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                cp0,
                NR_ENTRIES as int,
                self.idx as int,
                new_pte,
            );
        }

        old_child
    }

    /// Allocates a new child page table node and replaces the entry with it.
    ///
    /// If the old entry is not none, the operation will fail and return `None`.
    /// Otherwise, the lock guard of the new child page table node is returned.
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety Invariants**: The old node's root must satisfy the safety invariants for an [Entry](Entry::invariants)
    /// and the caller must provide its parent node owner.
    /// ## Postconditions
    /// - **Safety Invariants**: If a new node is allocated, it will satisfy the safety invariants.
    /// - **Safety**: If a new node is allocated, all other nodes have their invariants preserved.
    /// - **Correctness**: A new node is allocated if and only if the old node is absent.
    /// - **Correctness**: If the old node is present, the function retuns `None` and the state is unchanged.
    /// ## Safety
    /// - The invariants ensure that the entry is appropriately aligned and its index is within bounds.
    /// - The invariants of the entire page table are preserved in both cases.
    #[verus_spec(res =>
        with Tracked(owner): Tracked<&mut OwnerSubtree<C>>,
            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(guards): Tracked<&mut Guards>,
        requires
            old(self).invariants(old(owner).value(), *old(regions)),
            old(owner).inv(),
            old(owner).value().path.len() == old(owner).level(),
            old(self).node_matching(old(owner).value(), *old(parent_owner), *old(self).node),
            old(owner).level() < INC_LEVELS - 1,
            old(owner).level() + old(parent_owner).level() == INC_LEVELS,
            old(parent_owner).metaregion_sound_node(*old(regions)),
        ensures
            final(regions).slots == old(regions).slots,
            final(self).invariants(final(owner).value(), *final(regions)),
            final(self).parent_perms_preserved(*old(parent_owner), *final(parent_owner)),
            final(self).idx == old(self).idx,
            final(parent_owner).count_consistent(),
            *final(self).node == *old(self).node,
            old(owner).value().is_absent() && old(parent_owner).level() > 1 ==> {
                &&& final(self).node_matching(final(owner).value(), *final(parent_owner), *final(self).node)
                &&& final(owner).inv()
            },
            old(owner).value().is_absent() && old(parent_owner).level() > 1 ==> {
                &&& res is Some
                &&& final(owner).value().is_node()
                &&& final(owner).level() == old(owner).level()
                &&& final(owner).value().parent_level == old(owner).value().parent_level
                &&& final(guards).lock_held(final(owner).value().node().slot_vaddr())
                &&& final(owner).value().node().relate_guard(res->0)
                &&& final(owner).value().path == old(owner).value().path
                &&& final(owner).value().metaregion_sound(*final(regions))
                &&& MetaSlot::claim_unused_slot_region_spec(
                    final(owner).value().meta_slot_paddr()->0,
                    false, *old(regions), *final(regions))
                &&& OwnerSubtree::implies(
                    CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
                    CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value().node().slot_vaddr()))
                &&& Self::metaregion_sound_neq_preserved(old(owner).value(), final(owner).value(), *old(regions), *final(regions))
                &&& Self::path_tracked_pred_preserved(*old(regions), *final(regions))
                &&& old(regions).slots.contains_key(frame_to_index(final(owner).value().meta_slot_paddr()->0))
                &&& final(owner).subtree_satisfies(final(owner).value().path,
                    CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value().node().slot_vaddr()))
                &&& final(owner).subtree_satisfies(final(owner).value().path, PageTableOwner::<C>::metaregion_sound_pred(*final(regions)))
                &&& final(owner).subtree_satisfies(final(owner).value().path, PageTableOwner::<C>::path_tracked_pred(*final(regions)))
                &&& PageTableOwner(*final(owner)).view_rec(final(owner).value().path) == set![]
                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
                    #[trigger] final(owner).children()[i] is Some && final(owner).children()[i]->0.value().is_absent()
                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
                    (#[trigger] final(owner).children()[i])->0.value().path
                        == final(owner).value().path.push_tail(i)
                &&& crate::specs::mm::page_table::allocated_empty_node_grandchildren_none(*final(owner))
                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
                    (#[trigger] final(owner).child(i)).value().parent_level
                        == final(owner).value().node().level()
                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
                    (#[trigger] final(owner).child(i)).value().match_pte(
                        final(owner).value().node().children_perm.value()[i],
                        final(owner).child(i).value().parent_level)
            },
            !old(owner).value().is_absent() ==> {
                &&& res is None
                &&& *final(owner) == *old(owner)
            },
            forall |i: usize| old(guards).lock_held(i) ==> final(guards).lock_held(i),
            forall |i: usize| old(guards).unlocked(i) && i != final(owner).value().node().slot_vaddr() ==> final(guards).unlocked(i),
    )]
    #[verifier::spinoff_prover]
    pub(in crate::mm) fn alloc_if_none<A: InAtomicMode>(&mut self, guard: &'rcu A) -> Option<
        PageTableGuard<'rcu, C>,
    > {
        let entry_is_present = self.pte.is_present();
        let ghost cp0 = parent_owner.children_perm.value();

        #[verus_spec(with Tracked(&*parent_owner))]
        let level = self.node.level();

        if entry_is_present || level <= 1 {
            None
        } else {
            let ghost old_path = owner.value().path;
            let ghost old_owner_val = owner.value();

            proof {
                parent_owner.lemma_nr_children_absent_slot_bound(self.idx);
            }

            proof_decl! {
                let tracked mut new_node_owner: Tracked<OwnerSubtree<C>>;
            }

            #[verus_spec(with Tracked(regions), Tracked(guards) => Tracked(new_node_owner))]
            let new_page = PageTableNode::<C>::alloc(level - 1);
            let ghost fresh_children = new_node_owner.children();
            proof {
                assert forall|i: int| 0 <= i < NR_ENTRIES implies {
                    &&& (#[trigger] fresh_children[i]) is Some
                    &&& fresh_children[i]->0.value().is_absent()
                    &&& fresh_children[i]->0.value().parent_level == (level - 1) as PagingLevel
                } by {
                    assert(new_node_owner.has_child(i));
                };
                assert forall|i: int, j: int|
                    0 <= i < NR_ENTRIES && 0 <= j
                        < NR_ENTRIES implies !#[trigger] fresh_children[i]->0.has_child(j) by {
                    assert(!new_node_owner.child(i).has_child(j));
                };
            }

            let paddr = new_page.start_paddr();

            let new_pte = {
                let tracked new_node_value = new_node_owner.tracked_borrow_mut_value();
                #[verus_spec(with Tracked(new_node_value))]
                Child::PageTable(new_page).into_pte()
            };
            self.pte = new_pte;

            let tracked new_node = new_node_owner.tracked_borrow_value().tracked_borrow_node();
            let tracked slot_perm = *regions.slots.tracked_borrow(new_node.slot_index);
            let pt_ref = unsafe {
                #[verus_spec(with Tracked(slot_perm), Tracked(&new_node.frame_permission))]
                PageTableNodeRef::borrow_paddr(paddr)
            };

            // Lock before writing the PTE, so no one else can operate on it.
            let mut pt_lock_guard = {
                #[verus_spec(with Tracked(new_node_owner.tracked_borrow_value().tracked_borrow_node()), Tracked(guards))]
                pt_ref.lock(guard)
            };

            // SAFETY:
            //  1. The index is within the bounds.
            //  2. The new PTE is a child in `C` and at the correct paging level.
            //  3. The ownership of the child is passed to the page table node.
            unsafe {
                #[verus_spec(with Tracked(parent_owner), Tracked(&*regions))]
                self.node.write_pte(self.idx, self.pte)
            };

            #[verus_spec(with
                Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                    &parent_owner.frame_permission,
                )),
                Ghost(parent_owner.meta_own.nr_children.id())
            )]
            let nr_children = self.node.nr_children_mut();
            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);

            proof {
                let tracked new_node_value = new_node_owner.tracked_borrow_mut_value();
                new_node_value.parent_level = level as PagingLevel;
                new_node_value.path = old_path;
                *owner = new_node_owner;
                crate::specs::mm::page_table::tracked_rebase_freshly_allocated_children(
                    owner,
                    old_path,
                );
                let new_paddr = owner.value().meta_slot_paddr().unwrap();
                let tracked new_meta_slot = regions.tracked_borrow_mut_slot_owner(new_paddr);
                new_meta_slot.paths_in_pt = set![owner.value().path];

                crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                    cp0,
                    NR_ENTRIES as int,
                    self.idx as int,
                    self.pte,
                );

                let f_nu = CursorOwner::<'rcu, C>::node_unlocked_except(
                    *guards,
                    owner.value().node().slot_vaddr(),
                );
                let f_ms = PageTableOwner::<C>::metaregion_sound_pred(*regions);
                let f_pt = PageTableOwner::<C>::path_tracked_pred(*regions);
                Entry::<C>::lemma_allocated_node_preserves_disjoint_entries(
                    old_owner_val,
                    owner.value(),
                    *old(regions),
                    *regions,
                );

                crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                    *owner,
                    owner.value().path,
                    f_nu,
                );
                crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                    *owner,
                    owner.value().path,
                    f_ms,
                );
                crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                    *owner,
                    owner.value().path,
                    f_pt,
                );
                let pt = PageTableOwner(*owner);
                pt.lemma_view_rec_contains(old_path);
            }
            Some(pt_lock_guard)
        }
    }

    /// Splits the entry to smaller pages if it maps to a huge page.
    ///
    /// If the entry does map to a huge page, it is split into smaller pages
    /// mapped by a child page table node. The new child page table node
    /// is returned.
    ///
    /// If the entry does not map to a untracked huge page, the method returns
    /// `None`.
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety Invariants**: The old node's root must satisfy the safety invariants for an [Entry](Entry::invariants)
    /// and the caller must provide its parent node owner.
    /// ## Postconditions
    /// - **Safety Invariants**: The node allocated in place of the split page satisfies the safety invariants.
    /// - **Safety**: All other nodes have their invariants preserved.
    #[verifier::spinoff_prover]
    #[verifier::rlimit(200)]
    #[verus_spec(res =>
        with Tracked(owner) : Tracked<&mut OwnerSubtree<C>>,
             Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
             Tracked(regions): Tracked<&mut MetaRegionOwners>,
             Tracked(guards): Tracked<&mut Guards>
        requires
            old(regions).inv(),
            old(owner).inv(),
            old(owner).value().path.len() == old(owner).level(),
            old(self).wf(old(owner).value()),
            old(parent_owner).relate_guard(*old(self).node),
            old(parent_owner).inv(),
            old(parent_owner).level() == old(owner).value().parent_level,
            old(parent_owner).level() < NR_LEVELS,
            old(owner).level() + old(parent_owner).level() == INC_LEVELS,
            old(self).node_matching(old(owner).value(), *old(parent_owner), *old(self).node),
            old(parent_owner).metaregion_sound_node(*old(regions)),
            old(owner).value().is_frame() && old(parent_owner).level() > 1 ==>
                old(owner).value().metaregion_sound(*old(regions)),
        ensures
            old(owner).value().is_frame() && old(parent_owner).level() > 1 ==> {
                &&& res is Some
                &&& final(owner).value().is_node()
                &&& final(owner).level() == old(owner).level()
                &&& final(parent_owner).relate_guard(*final(self).node)
                &&& final(owner).value().node().relate_guard(res->0)
                &&& final(owner).value().node().slot_vaddr() == res->0.inner.inner@.slot_vaddr()
                &&& PageTableOwner(*final(owner)).pt_inv()
                &&& PageTableOwner(*final(owner)).view_rec(final(owner).value().path)
                    == Set::<int>::range(0, NR_ENTRIES as int).map(|i: int|
                        CursorView::<C>::split_index(
                            PageTableOwner(*old(owner)).view_rec(old(owner).value().path).choose(),
                            page_size::<PagingConsts>((old(parent_owner).level() - 1) as PagingLevel),
                            i as usize))
                &&& final(guards).lock_held(res->0.inner.inner@.slot_vaddr())
                &&& forall |j: int| 0 <= j < NR_ENTRIES ==>
                    (#[trigger] final(owner).children()[j])->0.value().is_frame()
                &&& forall |j: int| 0 <= j < NR_ENTRIES ==>
                    (#[trigger] final(owner).children()[j])->0.value().frame().prop
                        == old(owner).value().frame().prop
                &&& forall |j: int| 0 <= j < NR_ENTRIES ==>
                    (#[trigger] final(owner).children()[j])->0.value().frame().mapped_pa
                        == old(owner).value().frame().mapped_pa
                            + j * page_size::<PagingConsts>((old(parent_owner).level() - 1) as PagingLevel)
                &&& final(owner).value().path == old(owner).value().path
                &&& final(owner).value().metaregion_sound(*final(regions))
                &&& OwnerSubtree::implies(
                    CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
                    CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value().node().slot_vaddr()))
                &&& OwnerSubtree::implies(
                    PageTableOwner::<C>::metaregion_sound_pred(*old(regions)),
                    PageTableOwner::<C>::metaregion_sound_pred(*final(regions)))
                &&& final(owner).subtree_satisfies(final(owner).value().path,
                    CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value().node().slot_vaddr()))
                &&& final(owner).subtree_satisfies(final(owner).value().path,
                    PageTableOwner::<C>::metaregion_sound_pred(*final(regions)))
            },
            !old(owner).value().is_frame() || old(parent_owner).level() <= 1 ==> {
                &&& res is None
                &&& *final(owner) == *old(owner)
            },
            final(owner).inv(),
            final(owner).value().parent_level == old(owner).value().parent_level,
            final(self).idx == old(self).idx,
            old(owner).value().is_frame() && old(parent_owner).level() > 1 ==>
                final(self).node_matching(final(owner).value(), *final(parent_owner), *final(self).node),
            final(regions).inv(),
            final(parent_owner).inv(),
            final(parent_owner).level() == old(parent_owner).level(),
            final(parent_owner).tree_level == old(parent_owner).tree_level,
            *final(self).node == *old(self).node,
            *final(final(self).node) == *final(old(self).node),
            final(parent_owner).metaregion_sound_node(*final(regions)),
            final(parent_owner).slot_index == old(parent_owner).slot_index,
            final(parent_owner).meta_own == old(parent_owner).meta_own,
            final(parent_owner).frame_permission == old(parent_owner).frame_permission,
            final(regions).slots == old(regions).slots,
            final(self).node.inner.inner@.slot_vaddr() == old(self).node.inner.inner@.slot_vaddr(),
            forall |i: usize| old(guards).lock_held(i) ==> final(guards).lock_held(i),
            forall |i: usize| old(guards).unlocked(i)
                && i != final(owner).value().node().slot_vaddr() ==> final(guards).unlocked(i),
            old(owner).value().is_frame() && old(parent_owner).level() > 1 ==>
                MetaSlot::claim_unused_slot_region_spec(
                    final(owner).value().meta_slot_paddr()->0,
                    false, *old(regions), *final(regions)),
            // Parent's other PTEs are preserved: only the entry at self.idx
            // is overwritten (with the new PT pointer). Lets callers re-derive
            // `inv_children_rel` for the unchanged children when restoring the
            // parent NodeOwner into the cursor's continuation.
            old(owner).value().is_frame() && old(parent_owner).level() > 1 ==>
                forall|j: int| 0 <= j < NR_ENTRIES && j != old(self).idx ==>
                    #[trigger] final(parent_owner).children_perm.value()[j]
                        == old(parent_owner).children_perm.value()[j],
    )]
    pub(in crate::mm) fn split_if_mapped_huge<A: InAtomicMode>(&mut self, guard: &'rcu A) -> Option<
        PageTableGuard<'rcu, C>,
    > {
        #[verus_spec(with Tracked(&*parent_owner))]
        let level = self.node.level();

        if !(self.pte.is_last(level) && level > 1) {
            return None;
        }
        let pa = self.pte.paddr();
        let prop = self.pte.prop();

        proof {
            C::lemma_huge_raw_item_untracked(
                pa,
                level,
                prop,
                Tracked(owner.value().frame_permission()),
            );
        }

        proof_decl!{
            let tracked mut new_owner: OwnerSubtree<C>;
        }

        // alloc takes the NEW NODE level (level - 1, one below the cursor's
        // level which is `level`). Convention: alloc(M) produces node.level=M.
        #[verus_spec(with Tracked(regions), Tracked(guards) => Tracked(new_owner))]
        let new_page = PageTableNode::<C>::alloc(level - 1);
        let ghost fresh_children = new_owner.children();
        proof {
            assert forall|i: int, j: int|
                0 <= i < NR_ENTRIES && 0 <= j
                    < NR_ENTRIES implies !#[trigger] fresh_children[i]->0.has_child(j) by {
                assert(!new_owner.child(i).has_child(j));
            };
            assert forall|i: int| 0 <= i < NR_ENTRIES implies {
                &&& (#[trigger] fresh_children[i]) is Some
                &&& fresh_children[i]->0.value().is_absent()
                &&& fresh_children[i]->0.value().parent_level == (level - 1) as PagingLevel
            } by {
                assert(new_owner.has_child(i));
            };
        }
        proof {
            let tracked new_value = new_owner.tracked_borrow_mut_value();
            new_value.path = owner.value().path;
            crate::specs::mm::page_table::tracked_rebase_freshly_allocated_children(
                &mut new_owner,
                owner.value().path,
            );
        }
        let paddr = new_page.start_paddr();

        let tracked new_node = new_owner.tracked_borrow_value().tracked_borrow_node();
        let tracked slot_perm = *regions.slots.tracked_borrow(new_node.slot_index);
        let pt_ref = unsafe {
            #[verus_spec(with Tracked(slot_perm), Tracked(&new_node.frame_permission))]
            PageTableNodeRef::borrow_paddr(paddr)
        };

        // Lock before writing the PTE, so no one else can operate on it.
        let mut pt_lock_guard = {
            #[verus_spec(with Tracked(new_owner.tracked_borrow_value().tracked_borrow_node()), Tracked(guards))]
            pt_ref.lock(guard)
        };

        let ghost new_owner_path = new_owner.value().path;
        let ghost new_owner_meta_addr = new_owner.value().node().slot_vaddr();

        proof {
            C::lemma_paging_consts_properties();
            C::axiom_current_paging_consts_hardcoded();
        }

        for i in 0..nr_subpage_per_huge::<C>()
            invariant
                nr_subpage_per_huge_spec::<C>() == NR_ENTRIES,
                1 < level < NR_LEVELS,
                *self == *old(self),
                // Keep the original guard loan tied to the guard stored in Entry.
                *final(self.node) == *final(old(self).node),
                owner.inv(),
                *owner == *old(owner),
                new_owner.level() == old(owner).level(),
                new_owner.value().parent_level == level,
                new_owner.value().path == old(owner).value().path,
                forall|j: int|
                    0 <= j < i ==> #[trigger] new_owner.child(j).value().frame().prop == prop,
                forall|j: int|
                    0 <= j < i ==> #[trigger] new_owner.child(j).value().frame().mapped_pa == pa + j
                        * page_size::<PagingConsts>((level - 1) as PagingLevel),
                owner.value().is_frame(),
                owner.value().parent_level == level,
                owner.value().frame().mapped_pa == pa,
                owner.value().frame().prop == prop,
                !owner.value().frame_is_tracked(),
                owner.value().frame_permission() is None,
                pa == old(owner).value().frame().mapped_pa,
                level == old(parent_owner).level(),
                pa % page_size::<PagingConsts>(level) == 0,
                pa + page_size::<PagingConsts>(level) <= MAX_PADDR,
                regions.inv(),
                MetaSlot::claim_unused_slot_region_spec(
                    meta_to_frame(new_owner_meta_addr),
                    false,
                    *old(regions),
                    *regions,
                ),
                crate::specs::mm::page_table::allocated_empty_node_grandchildren_none(new_owner),
                forall|j: int|
                    0 <= j < i ==> #[trigger] new_owner.child(j).value().metaregion_sound(*regions),
                parent_owner.inv(),
                parent_owner.metaregion_sound_node(*regions),
                *parent_owner == *old(parent_owner),
                new_owner.value().is_node(),
                new_owner.inv(),
                new_owner.value().path == new_owner_path,
                new_owner.value().node().slot_vaddr() == new_owner_meta_addr,
                new_owner.value().node().relate_guard(pt_lock_guard),
                guards.lock_held(new_owner_meta_addr),
                forall|addr: usize| #[trigger]
                    old(guards).lock_held(addr) ==> guards.lock_held(addr),
                forall|addr: usize| #[trigger]
                    old(guards).unlocked(addr) && addr != new_owner_meta_addr ==> guards.unlocked(
                        addr,
                    ),
                new_owner.value().node().level() == (level - 1) as PagingLevel,
                forall|j: int| 0 <= j < NR_ENTRIES ==> (#[trigger] new_owner.children()[j]) is Some,
                forall|j: int|
                    0 <= j < NR_ENTRIES ==> {
                        &&& (#[trigger] new_owner.children()[j]) is Some
                        &&& new_owner.children()[j].unwrap().value().match_pte(
                            new_owner.value().node().children_perm.value()[j],
                            new_owner.value().node().level(),
                        )
                        &&& new_owner.children()[j].unwrap().value().parent_level
                            == new_owner.value().node().level()
                        &&& new_owner.children()[j].unwrap().value().inv()
                        &&& new_owner.children()[j].unwrap().value().path
                            == new_owner_path.push_tail(j)
                    },
                forall|j: int|
                    i <= j < NR_ENTRIES ==> {
                        &&& (#[trigger] new_owner.children()[j]) is Some
                        &&& new_owner.children()[j].unwrap().value().is_absent()
                        &&& new_owner.value().node().children_perm.value()[j]
                            == C::E::new_absent_spec()
                    },
                // Children [0, i) have been replaced with frames.
                forall|j: int|
                    0 <= j < i ==> {
                        &&& (#[trigger] new_owner.children()[j]) is Some
                        &&& new_owner.children()[j].unwrap().value().is_frame()
                    },
                new_page.slot_vaddr() == new_owner_meta_addr,
                new_owner.value().node().metaregion_sound_node(*regions),
                regions.slot_owners[meta_to_index(new_owner_meta_addr)].paths_in_pt.is_empty(),
        {
            proof {
                C::lemma_page_table_config_constant_properties();
                C::axiom_current_paging_consts_hardcoded();

                assert(new_owner.child(i as int).inv());
                EntryOwner::huge_frame_split_child_at(owner.value(), *regions, i as usize);
            }

            let small_pa = pa + i * page_size::<C>(level - 1);

            let tracked mut child_owner = EntryOwner::tracked_new_frame(
                small_pa,
                new_owner.value().path.push_tail(i as int),
                (level - 1) as PagingLevel,
                prop,
                None,
            );

            let ghost new_owner_before_update = new_owner;
            let tracked mut new_owner_node = {
                let tracked new_owner_value = new_owner.tracked_borrow_mut_value();
                new_owner_value.tracked_take_node()
            };
            let tracked mut new_owner_child = new_owner.tracked_borrow_mut_child(i as int);
            let ghost new_owner_child_before_update = *new_owner_child;

            proof {
                C::lemma_raw_item_well_formed_split(
                    pa,
                    level,
                    prop,
                    small_pa,
                    i,
                    Tracked(owner.value().frame_permission()),
                );
                child_owner.lemma_untracked_frame_metaregion_sound(*regions);
            }

            {
                let tracked new_owner_child_value = new_owner_child.tracked_borrow_mut_value();
                #[verus_spec(with Tracked(regions),
                    Tracked(new_owner_child_value),
                    Tracked(&mut child_owner),
                    Tracked(&mut new_owner_node))]
                pt_lock_guard.replace_absent_with_frame(i, small_pa, level - 1, prop);

                proof {
                    *new_owner_child_value = child_owner;
                }
            }

            proof {
                OwnerSubtree::lemma_ext_equal(
                    *new_owner_child,
                    new_owner_child_before_update.set_value(child_owner),
                );
                {
                    let tracked new_owner_value = new_owner.tracked_borrow_mut_value();
                    new_owner_value.tracked_put_node(new_owner_node);
                }

                let owner_with_updated_value = new_owner_before_update.set_value(new_owner.value());
                OwnerSubtree::lemma_ext_equal(
                    new_owner,
                    owner_with_updated_value.insert(i as int, *new_owner_child),
                );
                assert forall|j: int, k: int|
                    0 <= j < NR_ENTRIES && 0 <= k < NR_ENTRIES implies !#[trigger] new_owner.child(
                    j,
                ).has_child(k) by {
                    assert(!new_owner_before_update.child(j).has_child(k));
                };
                assert forall|j: int| 0 <= j <= i implies #[trigger] new_owner.child(
                    j,
                ).value().frame().prop == prop by {
                    if j != i {
                        assert(new_owner.child(j) == new_owner_before_update.child(j));
                    }
                };
                assert forall|j: int| 0 <= j <= i implies #[trigger] new_owner.child(
                    j,
                ).value().frame().mapped_pa == pa + j * page_size::<PagingConsts>(
                    (level - 1) as PagingLevel,
                ) by {
                    if j != i {
                        assert(new_owner.child(j) == new_owner_before_update.child(j));
                    }
                };
                assert forall|j: int| 0 <= j <= i implies #[trigger] new_owner.child(
                    j,
                ).value().metaregion_sound(*regions) by {
                    if j != i {
                        assert(new_owner.child(j) == new_owner_before_update.child(j));
                    }
                };
            }
        }

        self.pte = {
            let tracked new_owner_value = new_owner.tracked_borrow_mut_value();
            #[verus_spec(with Tracked(new_owner_value))]
            Child::PageTable(new_page).into_pte()
        };

        proof {
            *owner = new_owner;
        }

        // SAFETY:
        //  1. The index is within the bounds.
        //  2. The new PTE is a child in `C` and at the correct paging level.
        //  3. The ownership of the child is passed to the page table node.
        unsafe {
            #[verus_spec(with Tracked(parent_owner), Tracked(&*regions))]
            self.node.write_pte(self.idx, self.pte)
        };

        let ghost regions_before_registration = *regions;
        proof {
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                old(parent_owner).children_perm.value(),
                NR_ENTRIES as int,
                self.idx as int,
                self.pte,
            );
            let tracked new_slot = regions.tracked_borrow_mut_slot_owner(
                owner.value().meta_slot_paddr().unwrap(),
            );
            new_slot.paths_in_pt = set![owner.value().path];
            assert forall|j: int| 0 <= j < NR_ENTRIES implies #[trigger] owner.child(
                j,
            ).value().metaregion_sound(*regions) by {
                assert(owner.child(j).value().metaregion_sound(regions_before_registration));
                owner.child(j).value().lemma_metaregion_sound_one_slot_changed(
                    regions_before_registration,
                    *regions,
                    frame_to_index(owner.value().meta_slot_paddr()->0),
                );
            };
            PageTableOwner::<C>::lemma_fresh_node_pt_inv(*owner);
            PageTableOwner(*owner).lemma_split_node_view(PageTableOwner(*old(owner)));
            let absent = EntryOwner::<C>::new_absent(
                owner.value().path,
                owner.value().parent_level,
            );
            Entry::<C>::lemma_allocated_node_preserves_disjoint_entries(
                absent,
                owner.value(),
                *old(regions),
                *regions,
            );
            crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                CursorOwner::<'rcu, C>::node_unlocked_except(
                    *guards,
                    owner.value().node().slot_vaddr(),
                ),
            );
            crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                PageTableOwner::<C>::metaregion_sound_pred(*regions),
            );
            assert forall|j: int| 0 <= j < NR_ENTRIES implies (
            #[trigger] owner.children()[j])->0.value().frame().mapped_pa == old(
                owner,
            ).value().frame().mapped_pa + j * page_size::<PagingConsts>(
                (old(parent_owner).level() - 1) as PagingLevel,
            ) by {
                assert(owner.child(j).value().frame().mapped_pa == pa + j * page_size::<
                    PagingConsts,
                >((level - 1) as PagingLevel));
            };
            assert forall|j: int| 0 <= j < NR_ENTRIES implies (
            #[trigger] owner.children()[j])->0.value().frame().prop == old(
                owner,
            ).value().frame().prop by {
                assert(owner.child(j).value().frame().prop == prop);
            };
        }
        Some(pt_lock_guard)
    }

    /// Create a new entry at the node with guard.
    ///
    /// # Verified Properties
    /// ## Preconditions
    /// - **Safety**: The caller must provide the owner of the entry and the parent node, and the entry
    /// must match the parent node's PTE at the given index.
    /// - **Safety**: The caller must provide a valid guard permission matching `guard`, and it must be guarding the
    /// correct parent.
    /// ## Postconditions
    /// - **Correctness**: The resulting entry matches the owner.
    /// ## Safety
    /// - The precondition ensures that the index is within the bounds of the node.
    /// - This function does not modify the actual entry or any other relevant structure, so it is safe to call.
    /// Because we also require the guard to be correct, it will be safe to use the resulting `Entry` as a handle to the
    /// underlying `PTE`.
    #[verus_spec(res =>
        with Tracked(owner): Tracked<&EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&NodeOwner<C>>,
             Tracked(regions): Tracked<&MetaRegionOwners>,
        requires
            owner.inv(),
            parent_owner.inv(),
            parent_owner.relate_guard(*guard),
            idx < NR_ENTRIES,
            owner.match_pte(parent_owner.children_perm.value()[idx as int], owner.parent_level),
            regions.inv(),
            regions.slots.contains_key(parent_owner.slot_index),
        ensures
            res.wf(*owner),
            res.idx == idx,
            parent_owner.relate_guard(*res.node),
            // Pinpoint the reborrow: the Entry's node is exactly the guard
            // we were handed in, so callers get `*res.node == *old(guard)`.
            *res.node == *old(guard),
            *final(guard) == *final(res.node),
    )]
    pub(in crate::mm) unsafe fn new_at(guard: &'a mut PageTableGuard<'rcu, C>, idx: usize) -> Self {
        // SAFETY: The index is within the bound.
        let pte = unsafe {
            #[verus_spec(with Tracked(parent_owner), Tracked(regions))]
            guard.read_pte(idx)
        };
        Self::new(pte, idx, guard)
    }
}

#[verus_verify]
impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
    #[verus_spec(res =>
        with Tracked(owner): Tracked<&mut EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
             Tracked(regions): Tracked<&MetaRegionOwners>,
        requires
            old(owner).inv(),
            old(owner).is_frame(),
            old(owner).match_pte(
                old(parent_owner).children_perm.value()[idx as int],
                old(owner).parent_level,
            ),
            old(parent_owner).inv(),
            old(parent_owner).relate_guard(*old(self)),
            old(parent_owner).level() == old(owner).parent_level,
            old(parent_owner).metaregion_sound_node(*regions),
            idx < NR_ENTRIES,
            op.requires((old(owner).frame().prop,)),
            regions.inv(),
            regions.slots.contains_key(old(parent_owner).slot_index),
            forall|pa: Paddr, level: PagingLevel, p_in: PageProperty, p_out: PageProperty,
                perm: Tracked<Option<C::Perm>>|
                #![auto]
                op.ensures((p_in,), p_out) ==> (
                    C::item_into_raw(C::item_from_raw(pa, level, p_out, perm)).3@
                        is Some
                ) == (perm@ is Some),
            forall|pa: Paddr, level: PagingLevel, p_in: PageProperty, p_out: PageProperty|
                #![auto]
                op.ensures((p_in,), p_out) && C::E::new_page_req(pa, level, p_in)
                    ==> C::E::new_page_req(pa, level, p_out),
        ensures
            final(owner).inv(),
            final(owner).is_frame(),
            final(owner).match_pte(res, final(parent_owner).level()),
            final(owner).match_pte(
                final(parent_owner).children_perm.value()[idx as int],
                final(parent_owner).level(),
            ),
            res == final(parent_owner).children_perm.value()[idx as int],
            final(parent_owner).inv(),
            final(parent_owner).slot_index == old(parent_owner).slot_index,
            final(parent_owner).level() == old(parent_owner).level(),
            final(parent_owner).tree_level == old(parent_owner).tree_level,
            final(parent_owner).meta_own.nr_children.id() == old(parent_owner).meta_own.nr_children.id(),
            final(parent_owner).meta_own.stray == old(parent_owner).meta_own.stray,
            final(parent_owner).relate_guard(*final(self)),
            final(parent_owner).metaregion_sound_node(*regions),
            final(owner).frame().mapped_pa == old(owner).frame().mapped_pa,
            final(owner).frame_permission() == old(owner).frame_permission(),
            final(owner).frame_is_tracked() == old(owner).frame_is_tracked(),
            final(owner).path == old(owner).path,
            final(owner).parent_level == old(owner).parent_level,
            forall|j: int| 0 <= j < NR_ENTRIES && j != idx ==>
                #[trigger] final(parent_owner).children_perm.value()[j]
                    == old(parent_owner).children_perm.value()[j],
            crate::specs::mm::page_table::node::owners::count_present(
                final(parent_owner).children_perm.value(),
            ) == crate::specs::mm::page_table::node::owners::count_present(
                old(parent_owner).children_perm.value(),
            ),
            op.ensures((old(owner).frame().prop,), final(owner).frame().prop),
            *final(self) == *old(self),
    )]
    pub(in crate::mm) fn protect_child(
        &mut self,
        idx: usize,
        op: impl FnOnce(PageProperty) -> PageProperty,
    ) -> C::E {
        let ghost cp_old = parent_owner.children_perm.value();
        let mut pte = unsafe {
            #[verus_spec(with Tracked(&*parent_owner), Tracked(regions))]
            self.read_pte(idx)
        };

        let prop = pte.prop();
        let new_prop = op(prop);

        proof {
            assert(owner.frame().prop == prop);
            assert(op.ensures((prop,), new_prop));
            C::lemma_raw_item_well_formed_preserved(
                owner.frame().mapped_pa,
                owner.parent_level,
                prop,
                new_prop,
                Tracked(owner.frame_permission()),
            );
        }

        assume(pte.set_prop_req(new_prop));
        pte.set_prop(new_prop);

        unsafe {
            #[verus_spec(with Tracked(parent_owner), Tracked(regions))]
            self.write_pte(idx, pte)
        };

        proof {
            owner.tracked_set_frame_prop(new_prop);
            // The PTE at `idx` stayed present (only `prop` changed), so the
            // present-count is unchanged by the `write_pte` update — preserving
            // `count_consistent` for the caller.
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                cp_old,
                NR_ENTRIES as int,
                idx as int,
                pte,
            );
        }

        pte
    }

    #[verifier::spinoff_prover]
    #[verus_spec(res =>
        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
             Tracked(owner): Tracked<&mut EntryOwner<C>>,
             Tracked(new_owner): Tracked<&mut EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
        requires
            old(owner).inv(),
            old(owner).metaregion_sound(*old(regions)),
            old(owner).match_pte(
                old(parent_owner).children_perm.value()[idx as int],
                old(owner).parent_level,
            ),
            old(parent_owner).inv(),
            old(parent_owner).relate_guard(*old(self)),
            old(parent_owner).level() == old(owner).parent_level,
            idx < NR_ENTRIES,
            old(regions).inv(),
            old(regions).slots.contains_key(old(parent_owner).slot_index),
            new_child.invariants(*old(new_owner), *old(regions)),
            old(owner).path == old(new_owner).path,
            old(owner).parent_level == old(new_owner).parent_level,
            old(new_owner).is_node() ==> {
                &&& old(regions).slots.contains_key(frame_to_index(old(new_owner).meta_slot_paddr()->0))
                &&& old(regions).slot_owner(old(new_owner).meta_slot_paddr()->0).ref_count() != REF_COUNT_UNUSED
            },
            old(parent_owner).metaregion_sound_node(*old(regions)),
        ensures
            res matches Child::PageTable(node) ==> {
                &&& node.tracked_slot_perm@ == final(regions).slots[final(owner).node().slot_index]
                &&& node.tracked_metadata_perm@ is None
            },
            res.invariants(*final(owner), *final(regions)),
            final(new_owner).inv(),
            final(new_owner).metaregion_sound(*final(regions)),
            final(new_owner).match_pte(
                final(parent_owner).children_perm.value()[idx as int],
                final(parent_owner).level(),
            ),
            final(new_owner).path == old(new_owner).path,
            final(new_owner).parent_level == old(new_owner).parent_level,
            *final(owner) == old(owner).from_pte_owner_spec(),
            *final(new_owner) == old(new_owner).into_pte_owner_spec(),
            Entry::<C>::metaregion_sound_neq_preserved(
                *old(owner),
                *final(new_owner),
                *old(regions),
                *final(regions),
            ),
            !final(new_owner).is_node() ==> Entry::<C>::metaregion_sound_neq_old_preserved(
                *old(owner),
                *old(regions),
                *final(regions),
            ),
            (!old(owner).is_node() && !final(new_owner).is_node())
                ==> Entry::<C>::metaregion_sound_preserved(*old(regions), *final(regions)),
            final(new_owner).is_node() && !final(new_owner).is_absent() ==> PageTableOwner::<
                C,
            >::path_tracked_pred(*final(regions))(*final(new_owner), final(new_owner).path),
            final(parent_owner).inv(),
            final(parent_owner).level() == old(parent_owner).level(),
            final(parent_owner).relate_guard(*final(self)),
            final(parent_owner).metaregion_sound_node(*final(regions)),
            forall|j: int| 0 <= j < NR_ENTRIES && j != idx ==>
                #[trigger] final(parent_owner).children_perm.value()[j]
                    == old(parent_owner).children_perm.value()[j],
            forall|slot: int|
                #![trigger final(regions).slot_owners[slot].paths_in_pt]
                (!final(new_owner).is_node() || final(new_owner).is_absent() || slot
                    != frame_to_index(final(new_owner).meta_slot_paddr()->0))
                    ==> final(regions).slot_owners[slot].paths_in_pt == old(
                    regions,
                ).slot_owners[slot].paths_in_pt,
            forall|slot: int|
                #![trigger final(regions).slot_owners[slot].ref_count()]
                final(regions).ref_count(slot) == old(
                    regions,
                ).ref_count(slot),
            forall|slot: int|
                #![trigger final(regions).slot_owners[slot]]
                final(regions).slot_owners[slot].same_permissions(
                    old(regions).slot_owners[slot],
                ),
            final(regions).slots == old(regions).slots,
            forall|slot: int| #![trigger final(regions).slot_owners[slot].usage]
                old(regions).contains(slot) ==>
                    final(regions).slot_owners[slot].usage == old(regions).slot_owners[slot].usage,
            (!old(owner).is_node() && !final(new_owner).is_node()) ==> {
                &&& forall|i: int|
                    #![trigger final(regions).slot_owners[i]]
                    final(regions).slot_owners[i] == old(
                        regions,
                    ).slot_owners[i]
            },
            Entry::<C>::replace_nonpanic_condition(*old(parent_owner), *old(new_owner)),
            *final(self) == *old(self),
    )]
    #[verifier::spinoff_prover]
    pub(in crate::mm) fn replace_child(&mut self, idx: usize, new_child: Child<C>) -> Child<C> {
        let ghost initial_regions = *regions;
        let ghost initial_owner = *owner;
        #[cfg(feature = "allow_panic")]
        {
            let guard_level = self.level();
            match &new_child {
                Child::PageTable(node) => {
                    assert!(node.level() == guard_level - 1);
                },
                Child::Frame(_, level, _) => {
                    assert!(*level == guard_level);
                },
                Child::None => {},
            }
        }

        let pte = unsafe {
            #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
            self.read_pte(idx)
        };

        #[verus_spec(with Tracked(&*parent_owner))]
        let level = self.level();

        let old_child = unsafe {
            #[verus_spec(with Tracked(regions), Tracked(owner))]
            Child::from_pte(pte, level)
        };

        // For restoring `count_consistent` after the PTE swap below.
        let ghost cp0 = parent_owner.children_perm.value();

        if old_child.is_none() && !new_child.is_none() {
            #[verus_spec(with
                Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                    &parent_owner.frame_permission,
                )),
                Ghost(parent_owner.meta_own.nr_children.id())
            )]
            let nr_children = self.nr_children_mut();
            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
            proof {
                parent_owner.lemma_nr_children_absent_slot_bound(idx);
            }
            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
        } else if !old_child.is_none() && new_child.is_none() {
            #[verus_spec(with
                Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                    &parent_owner.frame_permission,
                )),
                Ghost(parent_owner.meta_own.nr_children.id())
            )]
            let nr_children = self.nr_children_mut();
            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
            proof {
                parent_owner.nr_children_present_slot_bound(idx);
            }
            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp - 1);
        }
        #[verus_spec(with Tracked(new_owner))]
        let new_pte = new_child.into_pte();

        unsafe {
            #[verus_spec(with Tracked(parent_owner), Tracked(&*regions))]
            self.write_pte(idx, new_pte)
        };

        proof {
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                cp0,
                NR_ENTRIES as int,
                idx as int,
                new_pte,
            );
            if new_owner.is_node() {
                let paddr = new_owner.meta_slot_paddr().unwrap();
                let tracked mut new_meta_slot = regions.tracked_borrow_mut_slot_owner(paddr);
                new_meta_slot.paths_in_pt = set![new_owner.path];
            }
            if owner.is_frame() {
                let paddr = owner.frame().mapped_pa;
                let slot = frame_to_index(paddr);
                C::lemma_perm_well_formed_with_region_preserved(
                    paddr,
                    Tracked(owner.frame_permission()),
                    initial_regions,
                    *regions,
                );
            }
            assert(Entry::<C>::metaregion_sound_neq_preserved(
                initial_owner,
                *new_owner,
                initial_regions,
                *regions,
            )) by {
                let f = |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
                    entry.meta_slot_paddr_neq(initial_owner) && entry.meta_slot_paddr_neq(
                        *new_owner,
                    ) && entry.metaregion_sound(initial_regions);
                let g = |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
                    entry.metaregion_sound(*regions);
                assert forall|entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
                    entry.inv() && f(entry, path) implies #[trigger] g(entry, path) by {
                    if entry.is_frame() {
                        let paddr = entry.frame().mapped_pa;
                        let slot = frame_to_index(paddr);
                        C::lemma_perm_well_formed_with_region_preserved(
                            paddr,
                            Tracked(entry.frame_permission()),
                            initial_regions,
                            *regions,
                        );
                    }
                };
            };
        }

        old_child
    }

    #[verifier::spinoff_prover]
    #[verus_spec(res =>
        with Tracked(owner): Tracked<&mut OwnerSubtree<C>>,
             Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
             Tracked(regions): Tracked<&mut MetaRegionOwners>,
             Tracked(guards): Tracked<&mut Guards>,
        requires
            old(owner).inv(),
            old(owner).value().path.len() == old(owner).level(),
            old(owner).value().is_absent(),
            old(owner).level() < INC_LEVELS - 1,
            old(owner).value().metaregion_sound(*old(regions)),
            old(parent_owner).inv(),
            old(parent_owner).relate_guard(*old(self)),
            old(parent_owner).level() == old(owner).value().parent_level,
            old(parent_owner).level() > 1,
            old(owner).level() + old(parent_owner).level() == INC_LEVELS,
            old(parent_owner).metaregion_sound_node(*old(regions)),
            idx < NR_ENTRIES,
            old(owner).value().match_pte(
                old(parent_owner).children_perm.value()[idx as int],
                old(owner).value().parent_level,
            ),
            old(regions).inv(),
            old(regions).slots.contains_key(old(parent_owner).slot_index),
        ensures
            final(regions).slots == old(regions).slots,
            final(owner).inv(),
            final(owner).value().is_node(),
            final(owner).level() == old(owner).level(),
            final(owner).value().parent_level == old(owner).value().parent_level,
            final(owner).value().path == old(owner).value().path,
            final(owner).value().metaregion_sound(*final(regions)),
            final(owner).value().node().relate_guard(res),
            final(owner).value().node().slot_vaddr() == res.inner.inner@.slot_vaddr(),
            final(owner).value().match_pte(
                final(parent_owner).children_perm.value()[idx as int],
                final(parent_owner).level(),
            ),
            final(guards).lock_held(final(owner).value().node().slot_vaddr()),
            OwnerSubtree::implies(
                CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
                CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value().node().slot_vaddr())),
            Entry::<C>::metaregion_sound_neq_preserved(
                old(owner).value(),
                final(owner).value(),
                *old(regions),
                *final(regions),
            ),
            Entry::<C>::path_tracked_pred_preserved(*old(regions), *final(regions)),
            old(regions).slots.contains_key(frame_to_index(final(owner).value().meta_slot_paddr()->0)),
            final(owner).subtree_satisfies(final(owner).value().path,
                CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value().node().slot_vaddr())),
            final(owner).subtree_satisfies(final(owner).value().path, PageTableOwner::<C>::metaregion_sound_pred(*final(regions))),
            final(owner).subtree_satisfies(final(owner).value().path, PageTableOwner::<C>::path_tracked_pred(*final(regions))),
            PageTableOwner(*final(owner)).view_rec(final(owner).value().path) == set![],
            forall|i: int| 0 <= i < NR_ENTRIES ==>
                #[trigger] final(owner).children()[i] is Some && final(owner).children()[i]->0.value().is_absent(),
            forall|i: int| 0 <= i < NR_ENTRIES ==>
                (#[trigger] final(owner).children()[i])->0.value().path
                    == final(owner).value().path.push_tail(i),
            crate::specs::mm::page_table::allocated_empty_node_grandchildren_none(*final(owner)),
            forall|i: int| 0 <= i < NR_ENTRIES ==>
                (#[trigger] final(owner).children()[i])->0.value().parent_level
                    == final(owner).value().node().level(),
            forall|i: int| 0 <= i < NR_ENTRIES ==>
                (#[trigger] final(owner).children()[i])->0.value().match_pte(
                    final(owner).value().node().children_perm.value()[i],
                    final(owner).children()[i]->0.value().parent_level),
            forall|i: int| i != frame_to_index(final(owner).value().meta_slot_paddr()->0) ==>
                (#[trigger] final(regions).slot_owners[i]) == old(regions).slot_owners[i],
            forall|i: int| old(regions).slots.contains_key(i)
                ==> (#[trigger] final(regions).slots.contains_key(i)),
            forall|i: int| #![trigger final(regions).slots[i]]
                i != frame_to_index(final(owner).value().meta_slot_paddr()->0)
                    && old(regions).slots.contains_key(i)
                ==> final(regions).slots[i] == old(regions).slots[i],
            final(regions).slot_owner(final(owner).value().meta_slot_paddr()->0)
                .ref_count() != REF_COUNT_UNUSED,
            old(regions).slot_owner(final(owner).value().meta_slot_paddr().unwrap())
                .ref_count() == REF_COUNT_UNUSED,
            final(regions).inv(),
            final(parent_owner).inv(),
            final(parent_owner).level() == old(parent_owner).level(),
            final(parent_owner).relate_guard(*final(self)),
            final(parent_owner).metaregion_sound_node(*final(regions)),
            forall|j: int| 0 <= j < NR_ENTRIES && j != idx ==>
                #[trigger] final(parent_owner).children_perm.value()[j]
                    == old(parent_owner).children_perm.value()[j],
            *final(self) == *old(self),
            forall |i: usize| old(guards).lock_held(i) ==> final(guards).lock_held(i),
            forall |i: usize| old(guards).unlocked(i) && i != final(owner).value().node().slot_vaddr() ==> final(guards).unlocked(i),
    )]
    pub(in crate::mm) fn alloc_absent_child<A: InAtomicMode>(
        &mut self,
        idx: usize,
        guard: &'rcu A,
    ) -> PageTableGuard<'rcu, C> {
        #[verus_spec(with Tracked(&*parent_owner))]
        let level = self.level();

        let ghost old_path = owner.value().path;

        // Discharge `nr_children < NR_ENTRIES` PRE-`alloc`, while the parent
        // slot at `idx` is still absent and `count_consistent` holds (from
        // `metaregion_sound_node`). Snapshot the parent meta perm so the
        // `nr_children` id-clause can be framed across `alloc`/`write_pte`,
        // which momentarily break `count_consistent`.
        proof {
            parent_owner.lemma_nr_children_absent_slot_bound(idx);
        }
        // Snapshot the parent's PTE array for restoring `count_consistent`
        // after the absent→present (`new_pte`) install below.
        let ghost cp0 = parent_owner.children_perm.value();
        // The original (absent) entry value, for the fresh-node region/
        // tree-predicate discharge after `owner` is rebuilt as the new node.
        let ghost old_owner_val = owner.value();

        proof_decl! {
            let tracked mut new_node_owner: Tracked<OwnerSubtree<C>>;
        }

        #[verus_spec(with Tracked(regions), Tracked(guards) => Tracked(new_node_owner))]
        let new_page = PageTableNode::<C>::alloc(level - 1);
        let ghost fresh_children = new_node_owner.children();

        proof {
            assert forall|i: int| 0 <= i < NR_ENTRIES implies {
                &&& (#[trigger] fresh_children[i]) is Some
                &&& fresh_children[i]->0.value().is_absent()
                &&& fresh_children[i]->0.value().parent_level == (level - 1) as PagingLevel
            } by {
                assert(new_node_owner.has_child(i));
            };
            assert forall|i: int, j: int|
                0 <= i < NR_ENTRIES && 0 <= j
                    < NR_ENTRIES implies !#[trigger] fresh_children[i]->0.has_child(j) by {
                assert(!new_node_owner.child(i).has_child(j));
            };
        }

        let paddr = new_page.start_paddr();

        let new_pte = {
            let tracked new_node_value = new_node_owner.tracked_borrow_mut_value();
            #[verus_spec(with Tracked(new_node_value))]
            Child::PageTable(new_page).into_pte()
        };

        let tracked new_node_value = new_node_owner.tracked_borrow_value();
        let tracked new_node = new_node_value.tracked_borrow_node();
        let tracked slot_perm = *regions.slots.tracked_borrow(new_node.slot_index);
        let pt_ref = unsafe {
            #[verus_spec(with Tracked(slot_perm), Tracked(&new_node.frame_permission))]
            PageTableNodeRef::borrow_paddr(paddr)
        };

        let pt_lock_guard = {
            let tracked new_node_value = new_node_owner.tracked_borrow_value();
            #[verus_spec(with Tracked(new_node_value.tracked_borrow_node()), Tracked(guards))]
            pt_ref.lock(guard)
        };

        unsafe {
            #[verus_spec(with Tracked(parent_owner), Tracked(&*regions))]
            self.write_pte(idx, new_pte)
        };

        #[verus_spec(with
            Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                &parent_owner.frame_permission,
            )),
            Ghost(parent_owner.meta_own.nr_children.id())
        )]
        let nr_children = self.nr_children_mut();
        let old_nr_children = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
        nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), old_nr_children + 1);

        proof {
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                cp0,
                NR_ENTRIES as int,
                idx as int,
                new_pte,
            );
            {
                let tracked new_node_value = new_node_owner.tracked_borrow_mut_value();
                new_node_value.parent_level = level as PagingLevel;
                new_node_value.path = old_path;
            }
            *owner = new_node_owner;
            crate::specs::mm::page_table::tracked_rebase_freshly_allocated_children(
                owner,
                old_path,
            );

            let new_paddr = owner.value().meta_slot_paddr().unwrap();
            let tracked new_meta_slot = regions.tracked_borrow_mut_slot_owner(new_paddr);
            new_meta_slot.paths_in_pt = set![owner.value().path];

            let ghost new_node_addr = owner.value().node().slot_vaddr();
            let f_nu = CursorOwner::<'rcu, C>::node_unlocked_except(*guards, new_node_addr);
            let f_ms = PageTableOwner::<C>::metaregion_sound_pred(*regions);
            let f_pt = PageTableOwner::<C>::path_tracked_pred(*regions);
            Entry::<C>::lemma_allocated_node_preserves_disjoint_entries(
                old_owner_val,
                owner.value(),
                *old(regions),
                *regions,
            );

            crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                f_nu,
            );
            crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                f_ms,
            );
            crate::specs::mm::page_table::lemma_fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                f_pt,
            );
            let pt = PageTableOwner(*owner);
            assert forall|m: crate::specs::mm::page_table::Mapping|
                pt.view_rec(old_path).contains(m) implies false by {
                let i = pt.view_rec_contains_choose(old_path, m);
            };
        }

        pt_lock_guard
    }

    #[verifier::spinoff_prover]
    #[verus_spec(
        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
             Tracked(owner): Tracked<&mut EntryOwner<C>>,
             Tracked(new_owner): Tracked<&mut EntryOwner<C>>,
             Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
        requires
            old(owner).inv(),
            old(owner).is_absent(),
            old(owner).metaregion_sound(*old(regions)),
            old(parent_owner).inv(),
            old(parent_owner).relate_guard(*old(self)),
            old(parent_owner).level() == old(owner).parent_level,
            idx < NR_ENTRIES,
            old(owner).match_pte(
                old(parent_owner).children_perm.value()[idx as int],
                old(owner).parent_level,
            ),
            old(regions).inv(),
            old(regions).slots.contains_key(old(parent_owner).slot_index),
            old(parent_owner).metaregion_sound_node(*old(regions)),
            Child::<C>::Frame(paddr, level, prop).invariants(*old(new_owner), *old(regions)),
            old(owner).path == old(new_owner).path,
            old(owner).parent_level == old(new_owner).parent_level,
        ensures
            final(new_owner).inv(),
            final(parent_owner).inv(),
            *final(owner) == old(owner).from_pte_owner_spec(),
            *final(new_owner) == old(new_owner).into_pte_owner_spec(),
            final(new_owner).pte_invariants(
                final(parent_owner).children_perm.value()[idx as int],
                *final(regions),
            ),
            forall|i: int|
                0 <= i < NR_ENTRIES && i != idx ==> #[trigger] old(parent_owner).children_perm.value()[i]
                    == final(parent_owner).children_perm.value()[i],
            final(parent_owner).slot_index == old(parent_owner).slot_index,
            final(parent_owner).level() == old(parent_owner).level(),
            final(parent_owner).tree_level == old(parent_owner).tree_level,
            final(parent_owner).meta_own.nr_children.id() == old(parent_owner).meta_own.nr_children.id(),
            final(parent_owner).meta_own.stray == old(parent_owner).meta_own.stray,
            final(parent_owner).relate_guard(*final(self)),
            final(parent_owner).metaregion_sound_node(*final(regions)),
            *final(regions) == *old(regions),
            *final(self) == *old(self),
    )]
    pub(in crate::mm) fn replace_absent_with_frame(
        &mut self,
        idx: usize,
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) {
        let ghost cp0 = parent_owner.children_perm.value();
        #[verus_spec(with
            Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
                &parent_owner.frame_permission,
            )),
            Ghost(parent_owner.meta_own.nr_children.id())
        )]
        let nr_children = self.nr_children_mut();
        let old_nr_children = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
        proof {
            parent_owner.lemma_nr_children_absent_slot_bound(idx);
        }
        nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), old_nr_children + 1);

        #[verus_spec(with Tracked(new_owner))]
        let new_pte = Child::<C>::Frame(paddr, level, prop).into_pte();

        unsafe {
            #[verus_spec(with Tracked(parent_owner), Tracked(&*regions))]
            self.write_pte(idx, new_pte)
        };

        proof {
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                cp0,
                NR_ENTRIES as int,
                idx as int,
                new_pte,
            );
        }
    }
}

} // verus!