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::*;
use vstd_extra::ownership::*;

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_MAX, REF_COUNT_UNUSED},
};
use crate::mm::page_table::*;
use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
use crate::specs::arch::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
use crate::specs::mm::frame::{
    mapping::{frame_to_index, group_page_meta, meta_to_index},
    meta_region_owners::MetaRegionOwners,
};
use crate::specs::mm::page_table::{INC_LEVELS, PageTableOwner};
use crate::specs::task::InAtomicMode;

use core::marker::PhantomData;
use core::ops::Deref;

use crate::{
    mm::{nr_subpage_per_huge, nr_subpage_per_huge_spec, page_prop::PageProperty},
    //    sync::RcuDrop,
    //    task::atomic_mode::InAtomicMode,
};

use super::*;

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>>,
             Tracked(regions): Tracked<&MetaRegionOwners>,
        requires
            owner.inv(),
            self.wf(owner),
            parent_owner.relate_guard(*self.node),
            parent_owner.inv(),
            parent_owner.level == owner.parent_level,
            regions.inv(),
            parent_owner.metaregion_sound_node(*regions),
        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), Tracked(&*regions))]
            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).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), Tracked(&*regions))]
        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_spec(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|
                #![auto]
                op.ensures((p_in,), p_out) ==> C::tracked(C::item_from_raw_spec(pa, level, p_out))
                    == C::tracked(C::item_from_raw_spec(pa, level, p_in)),
            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_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)),
            new_child matches Child::PageTable(node) ==> old(regions).frame_obligations.count(
                meta_to_index(node.ptr.addr()),
            ) > 0,
        ensures
            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|k: int|
                old(regions).slots.contains_key(k) ==> #[trigger] final(regions).slots.contains_key(
                    k,
                ),
            forall|idx: int|
                #![trigger final(regions).slot_owners[idx].ref_count()]
                final(regions).slot_owners[idx].ref_count() == old(
                    regions,
                ).slot_owners[idx].ref_count(),
            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,
            // When both old and new are not nodes: from_pte/into_pte are identity.
            (!old(owner).is_node() && !final(new_owner).is_node()) ==> {
                &&& final(regions).slots == old(regions).slots
                &&& forall|i: int|
                    #![trigger final(regions).slot_owners[i]]
                    final(regions).slot_owners[i] == old(
                        regions,
                    ).slot_owners[i]
                // Canonical model: neither `from_pte` (old non-node) nor
                // `into_pte` (new non-node) touches the per-frame ledger, so
                // it is preserved. Lets the huge-page split loop carry the
                // freshly-allocated node's obligation across the per-child
                // `replace` calls up to its own `into_pte`.
                &&& final(regions).frame_obligations == old(regions).frame_obligations
            },
            // When old child is absent and new child is not a node: slots values unchanged.
            (old(owner).is_absent() && !final(new_owner).is_node()) ==> forall|k: int|
                old(regions).slots.contains_key(k) ==> old(regions).slots[k]
                    == #[trigger] final(regions).slots[k],
            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> {
        // For restoring `count_consistent` (the `nr_children == count_present`
        // invariant) at the end: snapshot the parent's PTE array and counter
        // before the PTE write + counter inc/dec.
        let ghost cp0 = parent_owner.children_perm.value();

        #[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), Tracked(&*regions))]
        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() {
            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
            let tracked meta_slot_owner = regions.slot_owners.tracked_borrow(
                parent_owner.slot_index,
            );
            #[verus_spec(with
                Tracked(meta_points_to),
                Tracked(&meta_slot_owner.metadata_perm),
                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_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() {
            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
            let tracked meta_slot_owner = regions.slot_owners.tracked_borrow(
                parent_owner.slot_index,
            );
            #[verus_spec(with
                Tracked(meta_points_to),
                Tracked(&meta_slot_owner.metadata_perm),
                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), Tracked(regions))]
        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.
            // Nodes: singleton overwrite (tree enforces unique node path).
            // Frames: their path is installed by the caller BEFORE calling replace,
            //   so that `new_child.invariants` — which now requires
            //   `paths_in_pt.contains(new.path)` for the frame arm — is satisfied on
            //   entry. See the huge-page split and `replace_cur_entry` caller sites.
            if new_owner.is_node() {
                let paddr = new_owner.meta_slot_paddr().unwrap();
                regions.lemma_contains_valid_frame_paddr(paddr);

                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();
                regions.lemma_contains_valid_frame_paddr(paddr);
            }
            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<'rcu>>,
        requires
            old(self).invariants(old(owner).value(), *old(regions)),
            old(owner).inv(),
            old(self).node_matching(old(owner).value(), *old(parent_owner), *old(self).node),
            old(owner).level() < INC_LEVELS - 1,
            // The cursor entry's ghost-tree level is its DEPTH
            // (`INC_LEVELS - parent_PT_level`), tying it to the freshly-
            // allocated node's depth (`new_node_owner.level`) so we can prove
            // `final(owner).inv()`'s `child.level == self.level + 1`.
            old(owner).level() + old(parent_owner).level == INC_LEVELS,
            old(parent_owner).metaregion_sound_node(*old(regions)),
        ensures
            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().meta_vaddr())
                &&& final(owner).value().node().relate_guard(res->0)
                &&& 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().meta_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().meta_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![]
                // All children of the newly allocated node are absent (empty PT node).
                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
                    #[trigger] final(owner).children()[i] is Some && final(owner).children()[i]->0.value().is_absent()
                // Children's paths are rebased onto the cursor path. Required by
                // `pt_edge_at` for the freshly-allocated node, since the bare
                // `allocated_empty_node_owner` from `PageTableNode::alloc` uses
                // an empty parent path and `alloc_if_none` rewrites that path to
                // the cursor path; without rebasing the children, their paths
                // would be `[i]` rather than `cursor_path.push_tail(i)`.
                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
                    (#[trigger] final(owner).children()[i])->0.value().path
                        == final(owner).value().path.push_tail(i)
                // Grandchildren are all None (from `PageTableNode::alloc`'s
                // `allocated_empty_node_grandchildren_none` ensures; the path
                // rebasing leaves grandchildren untouched).
                &&& crate::specs::mm::page_table::allocated_empty_node_grandchildren_none(*final(owner))
                // Other child fields preserved from `allocated_empty_node_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)
                // slot_owners unchanged for all indices except the new PT node's index.
                &&& 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]
                // slots keys: the new PT node was removed then re-inserted, so all old keys preserved.
                &&& 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]
                // The new PT node's ref_count is not UNUSED (was set to 1 by get_from_unused).
                &&& final(regions).slot_owner(final(owner).value().meta_slot_paddr()->0)
                    .ref_count() != REF_COUNT_UNUSED
                // The allocated slot had ref_count == UNUSED before allocation (from get_from_unused).
                &&& old(regions).slot_owner(final(owner).value().meta_slot_paddr().unwrap())
                    .ref_count() == REF_COUNT_UNUSED
                // Allocator pool is disjoint from MMIO ranges (from `PageTableNode::alloc`).
                &&& !crate::specs::mm::frame::meta_owners::is_mmio_paddr(
                    final(owner).value().meta_slot_paddr().unwrap())
            },
            !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().meta_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();
        // For restoring `count_consistent` after adding the child below.
        let ghost cp0 = parent_owner.children_perm.value();

        #[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
        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.nr_children_absent_slot_bound(self.idx);
            }

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

            #[verus_spec(with Tracked(parent_owner), Tracked(regions), Tracked(guards), Ghost(self.idx) => 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 by {
                    assert(crate::specs::mm::page_table::allocated_empty_node_owner(
                        new_node_owner,
                        (level - 1) as PagingLevel,
                    ));
                    assert(new_node_owner.has_child(i));
                };
            }

            proof {
                let pte = C::E::new_pt_spec(
                    meta_to_frame(new_node_owner.value().node().meta_vaddr()),
                );
                C::E::lemma_page_table_entry_properties();
            }

            let ghost new_node_slot_idx = new_node_owner.value().node().slot_index;
            let tracked new_node_slot_perm = regions.slots.tracked_borrow(new_node_slot_idx);
            #[verus_spec(with Tracked(new_node_slot_perm))]
            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), Tracked(regions))]
                Child::PageTable(new_page).into_pte()
            };
            self.pte = new_pte;

            let pt_ref = unsafe {
                #[verus_spec(with Tracked(regions))]
                PageTableNodeRef::borrow_paddr(paddr)
            };

            // Lock before writing the PTE, so no one else can operate on it.
            let mut 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)
            };

            // 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 tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
            let tracked meta_slot_owner = regions.slot_owners.tracked_borrow(
                parent_owner.slot_index,
            );
            #[verus_spec(with
                Tracked(meta_points_to),
                Tracked(&meta_slot_owner.metadata_perm),
                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 {
                // For `final(owner).inv()`'s `child.level == self.level + 1`:
                // the grafted children carry `new_node_owner.level + 1`, and
                // `owner.level` is unchanged. The fresh node's depth equals
                // `owner.level` (from `allocated_empty_node_owner` + the
                // `owner.level + parent_owner.level == INC_LEVELS` precond), so
                // the grafted children's levels line up with `owner.level + 1`.
                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;
                // Rebase children's paths from `[i]` (rooted at empty) onto
                // the cursor path `old_path` so `pt_edge_at`'s
                // `child.path == parent.path.push_tail(i)` holds.
                assert(owner.children() == fresh_children);
                assert forall|i: int| 0 <= i < NR_ENTRIES implies (
                #[trigger] owner.children()[i]) is Some by {};
                crate::specs::mm::page_table::rebase_freshly_allocated_children(owner, old_path);

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

                // Restore the parent's `count_consistent`: the slot at `self.idx`
                // went absent → present (the new PT node) and `nr_children` was
                // incremented by 1.
                crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                    cp0,
                    NR_ENTRIES as int,
                    self.idx as int,
                    self.pte,
                );

                // Discharge the region-preservation + fresh-node
                // `subtree_satisfies` conjuncts of the big `is_absent` ensures
                // block.
                broadcast use crate::specs::mm::frame::meta_owners::axiom_mmio_usage_iff_mmio_paddr;
                // `subtree_satisfies` over the fresh node: each predicate
                // holds at the node root and trivially at the absent children
                // (which have `None` grandchildren), via
                // `fresh_node_subtree_satisfies`.

                let ghost new_node_addr = owner.value().node().meta_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);

                crate::specs::mm::page_table::fresh_node_subtree_satisfies(
                    *owner,
                    owner.value().path,
                    f_nu,
                );
                crate::specs::mm::page_table::fresh_node_subtree_satisfies(
                    *owner,
                    owner.value().path,
                    f_ms,
                );
                crate::specs::mm::page_table::fresh_node_subtree_satisfies(
                    *owner,
                    owner.value().path,
                    f_pt,
                );
            }

            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<'rcu>>
        requires
            old(regions).inv(),
            old(owner).inv(),
            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(parent_owner).metaregion_sound_node(*old(regions)),
            // Frame entries being split must have `metaregion_sound` for
            // their slot — provides `regions.slots.contains_key(pa_idx)` and
            // ref_count facts at the parent slot itself (j = 0 case in the
            // split loop's invariant). Without this, those facts can't be
            // re-established after alloc.
            old(owner).value().is_frame() && old(parent_owner).level > 1 ==>
                old(owner).value().metaregion_sound(*old(regions)),
            // Sub-page validity for huge-page split: each 4KB sub-page slot must
            // exist; non-MMIO sub-pages must additionally have `rc != UNUSED`.
            // (MMIO sub-pages keep `usage == MMIO` and `rc == UNUSED`.)
            old(owner).value().is_frame() && old(parent_owner).level > 1 ==>
                forall |j: usize| #![trigger frame_to_index(
                    (old(owner).value().frame().mapped_pa
                        + j * PAGE_SIZE) as usize)]
                    0 < j < page_size(old(parent_owner).level) / PAGE_SIZE ==> {
                    let sub_idx = frame_to_index(
                        (old(owner).value().frame().mapped_pa
                            + j * PAGE_SIZE) as usize);
                    &&& old(regions).slots.contains_key(sub_idx)
                    &&& old(regions).slot_owners[sub_idx].usage !is MMIO ==>
                        old(regions).slot_owners[sub_idx].ref_count()
                            != REF_COUNT_UNUSED
                },
        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().meta_vaddr() == res->0.inner.inner@.ptr.addr()
                &&& final(guards).lock_held(res->0.inner.inner@.ptr.addr())
                // All children of the new node subtree are frames with the same prop (from the split loop).
                &&& 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
                &&& 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(*final(guards)))
                &&& 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(*final(guards)))
                &&& 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(self).node.inner.inner@.ptr.addr() == old(self).node.inner.inner@.ptr.addr(),
            forall |i: usize| old(guards).lock_held(i) ==> final(guards).lock_held(i),
            forall |i: usize| old(guards).unlocked(i) ==> final(guards).unlocked(i),
            // slot_owners unchanged for all indices except the new PT node's index.
            old(owner).value().is_frame() && old(parent_owner).level > 1 ==> {
                &&& forall|i: int| i != meta_to_index(final(owner).value().node().meta_vaddr()) ==>
                    (#[trigger] final(regions).slot_owners[i]) == old(regions).slot_owners[i]
                // slots keys preserved (alloc removes then borrow re-inserts).
                &&& forall|i: int| old(regions).slots.contains_key(i)
                    ==> (#[trigger] final(regions).slots.contains_key(i))
                // The new PT node's ref_count is not UNUSED.
                &&& final(regions).slot_owners[meta_to_index(final(owner).value().node().meta_vaddr())]
                    .ref_count() != REF_COUNT_UNUSED
                // The allocated slot had ref_count == UNUSED before allocation.
                &&& old(regions).slot_owners[meta_to_index(final(owner).value().node().meta_vaddr())]
                    .ref_count() == REF_COUNT_UNUSED
            },
            // 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), Tracked(&*regions))]
        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 {
            EntryOwner::last_pte_implies_frame_match(owner.value(), self.pte, level);
        }

        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(parent_owner), Tracked(regions), Tracked(guards), Ghost(self.idx) => Tracked(new_owner))]
        let new_page = PageTableNode::<C>::alloc(level - 1);
        proof {
            assert forall|i: int| 0 <= i < NR_ENTRIES implies (
            #[trigger] new_owner.children()[i]) is Some by {
                assert(crate::specs::mm::page_table::allocated_empty_node_owner(
                    new_owner,
                    (level - 1) as PagingLevel,
                ));
                assert(new_owner.has_child(i));
            };
        }

        let ghost new_owner_slot_idx = new_owner.value().node().slot_index;
        let tracked new_owner_slot_perm = regions.slots.tracked_borrow(new_owner_slot_idx);
        #[verus_spec(with Tracked(new_owner_slot_perm))]
        let paddr = new_page.start_paddr();

        proof {
            broadcast use group_page_meta;

        }

        let pt_ref = unsafe {
            #[verus_spec(with Tracked(regions))]
            PageTableNodeRef::borrow_paddr(paddr)
        };

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

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

        proof {
            // Carry the huge frame's slot facts (the precondition's
            // `metaregion_sound`/`frame_sub_pages_valid`, stated about
            // `old(regions)`) across `alloc` to post-alloc `regions`,
            // establishing the split loop's j=0 and sub-page invariants.
            //
            // `alloc` (get_node_from_unused_spec + slot_perm_reparked_spec) only
            // mutates the freshly-allocated node's slot `new_idx`; the huge
            // frame's own slot and every sub-page slot is distinct from
            // `new_idx`: non-MMIO slots have `rc != UNUSED` while `new_idx` was
            // UNUSED pre-alloc; MMIO slots are `is_mmio` while the new node is
            // `!is_mmio`.
            broadcast use crate::specs::mm::frame::mapping::lemma_frame_to_index_injective;
            broadcast use crate::specs::mm::frame::meta_owners::axiom_mmio_usage_iff_mmio_paddr;
            broadcast use group_page_meta;

            let new_idx = meta_to_index(new_owner_meta_addr);
            let new_paddr = meta_to_frame(new_owner_meta_addr);
            let nr_pages = page_size(level) / PAGE_SIZE;

            // The huge frame's own slot (j = 0): `usage != PageTable` from the
            // precondition's `metaregion_sound` (frame arm), preserved across
            // `alloc` because `frame_to_index(pa) != new_idx`.
            let pa_idx = frame_to_index(pa);
            assert(pa_idx != new_idx) by {
                if old(regions).slot_owners[pa_idx].usage
                    == crate::specs::mm::frame::meta_owners::PageUsage::MMIO {
                    old(regions).lemma_contains_valid_frame_paddr(pa);
                } else {
                    // metaregion_sound frame arm: non-MMIO ⟹ rc != UNUSED.
                }
            };

            // Sub-pages (j > 0): `frame_sub_pages_valid` facts, preserved.
            assert forall|j: usize|
                #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
                0 < j < nr_pages implies {
                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
                &&& regions.slots.contains_key(sub_idx)
                &&& regions.slot_owners[sub_idx].usage
                    != crate::specs::mm::frame::meta_owners::PageUsage::PageTable
                &&& regions.slot_owners[sub_idx].usage
                    != crate::specs::mm::frame::meta_owners::PageUsage::MMIO ==> {
                    &&& regions.slot_owners[sub_idx].ref_count() != REF_COUNT_UNUSED
                    &&& regions.slot_owners[sub_idx].ref_count() > 0
                    &&& regions.slot_owners[sub_idx].ref_count() <= REF_COUNT_MAX
                }
            } by {
                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
                assert(sub_idx != new_idx) by {
                    if old(regions).slot_owners[sub_idx].usage
                        == crate::specs::mm::frame::meta_owners::PageUsage::MMIO {
                        old(regions).lemma_contains_valid_frame_paddr(
                            (pa + j * PAGE_SIZE) as usize,
                        );
                    } else {
                    }
                };
            };
        }

        proof {
            C::lemma_paging_consts_properties();
            assert(nr_subpage_per_huge_spec::<C>() == NR_ENTRIES);
        }

        for i in 0..nr_subpage_per_huge::<C>()
            invariant
                nr_subpage_per_huge_spec::<C>() == NR_ENTRIES,
                1 < level < NR_LEVELS,
                owner.inv(),
                owner.value().is_frame(),
                owner.value().parent_level == level,
                owner.value().frame().mapped_pa == pa,
                owner.value().frame().prop == prop,
                pa == old(owner).value().frame().mapped_pa,
                level == old(parent_owner).level,
                pa % page_size(level) == 0,
                pa + page_size(level) <= MAX_PADDR,
                regions.inv(),
                // Canonical model: the freshly-allocated node carries its
                // pending-Drop obligation across the per-child `replace`
                // calls (each net-zero on the ledger), discharging the
                // `into_pte` consume after the loop.
                regions.frame_obligations.count(meta_to_index(new_owner_meta_addr)) > 0,
                parent_owner.inv(),
                new_owner.value().is_node(),
                new_owner.inv(),
                new_owner.value().path == new_owner_path,
                new_owner.value().node().meta_vaddr() == new_owner_meta_addr,
                new_owner.value().node().relate_guard(pt_lock_guard),
                guards.lock_held(new_owner_meta_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()
                    },
                // Sub-page slots (4KB-grained, j > 0): slots.contains_key is unconditional;
                // rc constraints apply only to non-MMIO sub-pages (MMIO sub-pages keep
                // `usage == MMIO` and `rc == UNUSED`).
                forall|j: usize|
                    #![trigger frame_to_index(
                    (pa + j * PAGE_SIZE) as usize)]
                    0 < j < page_size(level) / PAGE_SIZE ==> {
                        let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
                        &&& regions.slots.contains_key(sub_idx)
                        &&& regions.slot_owners[sub_idx].usage !is PageTable
                        &&& regions.slot_owners[sub_idx].usage !is MMIO ==> {
                            &&& regions.slot_owners[sub_idx].ref_count() != REF_COUNT_UNUSED
                            &&& regions.slot_owners[sub_idx].ref_count() > 0
                            &&& regions.slot_owners[sub_idx].ref_count() <= REF_COUNT_MAX
                        }
                    },
                regions.slots.contains_key(frame_to_index(pa)),
                regions.slot_owner(pa).usage !is PageTable,
                regions.slot_owner(pa).usage !is MMIO ==> {
                    &&& regions.slot_owner(pa).ref_count() != REF_COUNT_UNUSED
                    &&& 0 < regions.slot_owner(pa).ref_count() <= REF_COUNT_MAX
                },
                new_page.ptr.addr() == new_owner_meta_addr,
                new_owner.value().node().metaregion_sound_node(*regions),
                regions.slot_owners[meta_to_index(new_owner_meta_addr)].ref_count()
                    != REF_COUNT_UNUSED,
                0 < regions.slot_owners[meta_to_index(new_owner_meta_addr)].ref_count()
                    <= REF_COUNT_MAX,
                regions.slot_owners[meta_to_index(new_owner_meta_addr)].paths_in_pt
                    == set![new_owner_path],
        {
            proof {
                C::lemma_page_table_config_constant_properties();
                C::lemma_paging_consts_properties();
                let ghost the_node = new_owner.value().node();

                assert(0 <= i < NR_ENTRIES);
                assert(new_owner.has_child(i as int));
                assert(new_owner.inv_children());
                assert(new_owner.child(i as int).inv());
                assert(new_owner.child(i as int).level() == new_owner.level() + 1);
                EntryOwner::huge_frame_split_child_at(owner.value(), *regions, i as usize);
            }

            let small_pa = pa + i * page_size(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,
            );

            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 {
                let idx = frame_to_index(small_pa);
                if i != 0 {
                    let ghost big_j =
                        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_split_sub_page_big_j(
                    pa, level, i);
                }
                if level - 1 > 1 {
                    let nr_subpages = page_size((level - 1) as PagingLevel) / PAGE_SIZE;
                    crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_div_mul_eq(
                    (level - 1) as PagingLevel);
                    crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_div_mul_eq(
                    level);
                    crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_nr_entries_times_sub_page_size(
                    level);
                    assert forall|j_prime: usize|
                        #![trigger frame_to_index((small_pa + j_prime * PAGE_SIZE) as usize)]
                        0 < j_prime < nr_subpages implies {
                        let sub_idx = frame_to_index((small_pa + j_prime * PAGE_SIZE) as usize);
                        &&& regions.slots.contains_key(sub_idx)
                        &&& regions.slot_owners[sub_idx].usage !is MMIO ==> {
                            &&& regions.slot_owners[sub_idx].ref_count() != REF_COUNT_UNUSED
                            &&& regions.slot_owners[sub_idx].ref_count() > 0
                            &&& regions.slot_owners[sub_idx].ref_count() <= REF_COUNT_MAX
                        }
                    } by {
                        let sub_pages_per_subframe = page_size((level - 1) as PagingLevel)
                            / PAGE_SIZE;
                        let big_j_int: int = i * sub_pages_per_subframe + j_prime;
                        vstd::arithmetic::mul::lemma_mul_nonnegative(
                            i as int,
                            sub_pages_per_subframe as int,
                        );
                        vstd::arithmetic::mul::lemma_mul_inequality(
                            i + 1,
                            NR_ENTRIES as int,
                            sub_pages_per_subframe as int,
                        );
                        vstd::arithmetic::mul::lemma_mul_is_distributive_add_other_way(
                            sub_pages_per_subframe as int,
                            i as int,
                            1int,
                        );
                        vstd::arithmetic::mul::lemma_mul_is_associative(
                            NR_ENTRIES as int,
                            sub_pages_per_subframe as int,
                            PAGE_SIZE as int,
                        );
                        vstd::arithmetic::div_mod::lemma_div_by_multiple(
                            NR_ENTRIES * sub_pages_per_subframe,
                            PAGE_SIZE as int,
                        );
                        let big_j: usize = big_j_int as usize;
                        vstd::arithmetic::mul::lemma_mul_is_distributive_add_other_way(
                            PAGE_SIZE as int,
                            i * sub_pages_per_subframe,
                            j_prime as int,
                        );
                        vstd::arithmetic::mul::lemma_mul_is_associative(
                            i as int,
                            sub_pages_per_subframe as int,
                            PAGE_SIZE as int,
                        );
                        assert((small_pa + j_prime * PAGE_SIZE) as usize == (pa + big_j
                            * PAGE_SIZE) as usize);
                        assert(regions.slots.contains_key(
                            frame_to_index((pa + big_j * PAGE_SIZE) as usize),
                        ));
                    }
                }
                if i == 0 {
                    assert(i * page_size((level - 1) as PagingLevel) == 0) by {
                        vstd::arithmetic::mul::lemma_mul_by_zero_is_zero(
                            page_size((level - 1) as PagingLevel) as int,
                        );
                    }
                } else {
                    let ghost big_j =
                        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_split_sub_page_big_j(
                    pa, level, i);
                    assert(regions.slots.contains_key(
                        frame_to_index((pa + big_j * PAGE_SIZE) as usize),
                    ));
                }

                regions.lemma_contains_valid_frame_paddr(small_pa);
                let tracked mut small_slot = regions.tracked_borrow_mut_slot_owner(small_pa);
                small_slot.paths_in_pt = small_slot.paths_in_pt.insert(child_owner.path);

                if (level - 1) > 1 {
                }
                let ghost target_idx = frame_to_index(small_pa);
                if i != 0 {
                    let ghost _ =
                        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_split_sub_page_big_j(
                    pa, level, i);

                }
                C::lemma_raw_item_well_formed_split(pa, level, prop, small_pa, i);
            }

            // Snapshot the node's own-slot facts while the loop invariant still
            // holds (regions unchanged since loop entry), so we can frame them
            // across the `replace` below.
            let ghost nidx = meta_to_index(new_owner_meta_addr);
            proof {
                // The loop invariant still holds for the current `regions`
                // (unchanged since entry), so pin the node-slot paths_in_pt fact
                // here for the post-`replace` preservation step to carry forward.
            }
            let ghost regions_pre_replace = *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 {
                new_owner_child_before_update.lemma_set_value_observable_fields(child_owner);
                OwnerSubtree::lemma_ext_equal(
                    *new_owner_child,
                    new_owner_child_before_update.set_value(child_owner),
                );
                assert(new_owner_child.inv());

                {
                    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());
                vstd::seq_lib::lemma_update_is_remove_insert(
                    new_owner_before_update.children(),
                    i as int,
                    Some(*new_owner_child),
                );
                assert(new_owner.children() == new_owner_before_update.children().remove(
                    i as int,
                ).insert(i as int, Some(*new_owner_child)));
                assert(owner_with_updated_value.insert(i as int, *new_owner_child).children()
                    == new_owner_before_update.children().update(i as int, Some(*new_owner_child)));
                assert(new_owner.children() =~= owner_with_updated_value.insert(
                    i as int,
                    *new_owner_child,
                ).children());
                assert(new_owner.children() == owner_with_updated_value.insert(
                    i as int,
                    *new_owner_child,
                ).children());
                OwnerSubtree::lemma_ext_equal(
                    new_owner,
                    owner_with_updated_value.insert(i as int, *new_owner_child),
                );
                assert forall|j: int| 0 <= j < NR_ENTRIES implies (
                #[trigger] new_owner.children()[j]) is Some by {
                    if j != i {
                        assert(owner_with_updated_value.insert(
                            i as int,
                            *new_owner_child,
                        ).children()[j] == owner_with_updated_value.children()[j]);
                    }
                };
                assert(new_owner.inv());

            }
        }

        self.pte = {
            let tracked new_owner_value = new_owner.tracked_borrow_mut_value();
            #[verus_spec(with Tracked(new_owner_value), Tracked(regions))]
            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 {
            let tracked owner_value = owner.tracked_borrow_mut_value();
            #[verus_spec(with Tracked(owner_value.tracked_borrow_mut_node()), Tracked(&*regions))]
            self.node.write_pte(self.idx, self.pte)
        };

        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|
                #![auto]
                op.ensures((p_in,), p_out) ==> C::tracked(C::item_from_raw_spec(pa, level, p_out))
                    == C::tracked(C::item_from_raw_spec(pa, level, p_in)),
            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_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,
            );
        }

        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)),
            new_child matches Child::PageTable(node) ==> old(regions).frame_obligations.count(
                meta_to_index(node.ptr.addr()),
            ) > 0,
        ensures
            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|k: int|
                old(regions).slots.contains_key(k) ==> #[trigger] final(regions).slots.contains_key(k),
            forall|slot: int|
                #![trigger final(regions).slot_owners[slot].ref_count()]
                final(regions).slot_owners[slot].ref_count() == old(
                    regions,
                ).slot_owners[slot].ref_count(),
            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,
            (!old(owner).is_node() && !final(new_owner).is_node()) ==> {
                &&& final(regions).slots == old(regions).slots
                &&& forall|i: int|
                    #![trigger final(regions).slot_owners[i]]
                    final(regions).slot_owners[i] == old(
                        regions,
                    ).slot_owners[i]
                &&& final(regions).frame_obligations == old(regions).frame_obligations
            },
            (old(owner).is_absent() && !final(new_owner).is_node()) ==> forall|k: int|
                old(regions).slots.contains_key(k) ==> old(regions).slots[k]
                    == #[trigger] final(regions).slots[k],
            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> {
        #[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), Tracked(&*regions))]
        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() {
            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
            let tracked meta_slot_owner = regions.slot_owners.tracked_borrow(
                parent_owner.slot_index,
            );
            #[verus_spec(with
                Tracked(meta_points_to),
                Tracked(&meta_slot_owner.metadata_perm),
                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_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() {
            let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
            let tracked meta_slot_owner = regions.slot_owners.tracked_borrow(
                parent_owner.slot_index,
            );
            #[verus_spec(with
                Tracked(meta_points_to),
                Tracked(&meta_slot_owner.metadata_perm),
                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), Tracked(regions))]
        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,
            );
        }

        proof {
            if new_owner.is_node() {
                let paddr = new_owner.meta_slot_paddr().unwrap();
                regions.lemma_contains_valid_frame_paddr(paddr);
                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();
                regions.lemma_contains_valid_frame_paddr(paddr);
            }
        }

        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<'rcu>>,
        requires
            old(owner).inv(),
            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(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(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().meta_vaddr() == res.inner.inner@.ptr.addr(),
            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().meta_vaddr()),
            OwnerSubtree::implies(
                CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
                CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value().node().meta_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().meta_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,
            !crate::specs::mm::frame::meta_owners::is_mmio_paddr(
                final(owner).value().meta_slot_paddr().unwrap()),
            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().meta_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), Tracked(&*regions))]
        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.nr_children_absent_slot_bound(idx);
        }
        let ghost regions_pre = *regions;
        // 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(parent_owner), Tracked(regions), Tracked(guards), Ghost(idx) => 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 by {
                assert(crate::specs::mm::page_table::allocated_empty_node_owner(
                    new_node_owner,
                    (level - 1) as PagingLevel,
                ));
                assert(new_node_owner.has_child(i));
            };
        }

        proof {
            let pte = C::E::new_pt_spec(meta_to_frame(new_node_owner.value().node().meta_vaddr()));
            C::E::lemma_page_table_entry_properties();
        }

        let ghost new_node_slot_idx = new_node_owner.value().node().slot_index;
        let tracked new_node_slot_perm = regions.slots.tracked_borrow(new_node_slot_idx);
        #[verus_spec(with Tracked(new_node_slot_perm))]
        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), Tracked(regions))]
            Child::PageTable(new_page).into_pte()
        };

        proof {
            broadcast use group_page_meta;

        }

        let pt_ref = unsafe {
            #[verus_spec(with Tracked(regions))]
            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)
        };

        // `count_consistent` is momentarily broken between `alloc` and the
        // `+ 1` below, but the `nr_children` id-clause that `read`/`write` need
        // is framed from the pre-`alloc` snapshot: `meta_own` is preserved by
        // `set_children_perm`/`write_pte`, and the parent slot perm is untouched
        // (`alloc` allocates a different slot, `write_pte` leaves regions
        // immutable).

        let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
        let tracked meta_slot_owner = regions.slot_owners.tracked_borrow(parent_owner.slot_index);
        #[verus_spec(with
            Tracked(meta_points_to),
            Tracked(&meta_slot_owner.metadata_perm),
            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 {
            // Restore the parent's `count_consistent`: slot `idx` went
            // absent → present (the new PT node) and `nr_children` was
            // incremented by 1, so `count_present(children_perm)` rises by 1
            // in lockstep.
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                cp0,
                NR_ENTRIES as int,
                idx as int,
                new_pte,
            );
        }

        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;
            assert(owner.children() == fresh_children);
            crate::specs::mm::page_table::rebase_freshly_allocated_children(owner, old_path);

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

        proof {
            broadcast use crate::specs::mm::frame::meta_owners::axiom_mmio_usage_iff_mmio_paddr;

            let ghost new_node_addr = owner.value().node().meta_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);

            // Root predicates.

            crate::specs::mm::page_table::fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                f_nu,
            );
            crate::specs::mm::page_table::fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                f_ms,
            );
            crate::specs::mm::page_table::fresh_node_subtree_satisfies(
                *owner,
                owner.value().path,
                f_pt,
            );
        }

        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,
    ) {
        // For restoring `count_consistent` after the absent→frame install.
        let ghost cp0 = parent_owner.children_perm.value();
        let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
        let tracked meta_slot_owner = regions.slot_owners.tracked_borrow(parent_owner.slot_index);
        #[verus_spec(with
            Tracked(meta_points_to),
            Tracked(&meta_slot_owner.metadata_perm),
            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.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), Tracked(regions))]
        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 {
            // Restore the parent's `count_consistent`: slot `idx` went
            // absent → present (the new frame) and `nr_children` was
            // incremented by 1.
            crate::specs::mm::page_table::node::owners::lemma_count_present_upto_update(
                cp0,
                NR_ENTRIES as int,
                idx as int,
                new_pte,
            );
        }
    }
}

} // verus!