ostd/specs/mm/page_table/

owners.rs

use vstd::prelude::*;

use core::ops::Range;

use vstd::arithmetic::power2::pow2;
use vstd::seq::*;
use vstd::seq_lib::*;
use vstd::set_lib::*;

use vstd_extra::drop_tracking::*;
use vstd_extra::ghost_tree::*;
use vstd_extra::ownership::*;
use vstd_extra::prelude::TreeNodeValue;

use crate::mm::{
    Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_size,
    page_table::{EntryOwner, EntryOwnerKind},
};

use crate::mm::frame::meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED};
use crate::mm::page_table::{PageTableEntryTrait, PageTableGuard};

use crate::specs::arch::*;
use crate::specs::mm::frame::{mapping::frame_to_index, meta_region_owners::MetaRegionOwners};
use crate::specs::mm::page_table::cursor::page_size_lemmas::{
    lemma_page_size_divides, lemma_page_size_ge_page_size, lemma_page_size_spec_values,
};
use crate::specs::mm::page_table::*;

use core::ops::Deref;

verus! {

#[verifier::inline]
pub open spec fn vaddr_shift_bits<const L: usize>(idx: int) -> nat
    recommends
        0 < L,
        idx < L,
{
    (12 + 9 * (L - 1 - idx)) as nat
}

#[verifier::inline]
pub open spec fn vaddr_shift<const L: usize>(idx: int) -> usize
    recommends
        0 < L,
        idx < L,
{
    pow2(vaddr_shift_bits::<L>(idx)) as usize
}

#[verifier::inline]
pub open spec fn vaddr_make<const L: usize>(idx: int, offset: usize) -> usize
    recommends
        0 < L,
        idx < L,
        0 <= offset < 512,
{
    (vaddr_shift::<L>(idx) * offset) as usize
}

pub open spec fn rec_vaddr(
    path: TreePath<NR_ENTRIES>,
    idx: int,
) -> usize/*        recommends
        0 < NR_LEVELS,
        path.len() <= NR_LEVELS,
        0 <= idx <= path.len(),*/

    decreases path.len() - idx,
    when 0 <= idx <= path.len()
{
    if idx == path.len() {
        0
    } else {
        let offset: usize = path.index(idx);
        (vaddr_make::<NR_LEVELS>(idx, offset) + rec_vaddr(path, idx + 1)) as usize
    }
}

pub open spec fn vaddr(path: TreePath<NR_ENTRIES>) -> usize {
    rec_vaddr(path, 0)
}

/// Virtual address of `path` with `leading_bits` placed in bits `[48, 64)`.
///
/// Matches `AbstractVaddr { offset: 0, index: <from path>, leading_bits }
/// .to_vaddr()` modulo the offset. For `leading_bits == 0` this reduces to
/// `vaddr(path)`; for `leading_bits == 0xffff` and a kernel path this yields
/// the canonical sign-extended high-half address.
pub open spec fn vaddr_at(path: TreePath<NR_ENTRIES>, leading_bits: int) -> usize {
    (vaddr(path) + leading_bits * 0x1_0000_0000_0000int) as usize
}

/// Config-aware `vaddr`: reads `leading_bits` from `C::LEADING_BITS_spec()`.
///
/// Every `Mapping` produced by a cursor on `PageTable<C>` should be built
/// with this — not the bare `vaddr(path)` — so the VA lives in the range
/// advertised by `C::VADDR_RANGE_spec()`.
pub open spec fn vaddr_of<C: PageTableConfig>(path: TreePath<NR_ENTRIES>) -> usize {
    vaddr_at(path, C::LEADING_BITS_spec() as int)
}

/// `vaddr(path) < 2^48` for every valid path: each term in the positional
/// sum is `i_k * 2^(12 + 9·k)` with `i_k < 512 = 2^9`, so the sum is
/// strictly less than `2^48`.
#[verifier::rlimit(400)]
pub proof fn lemma_vaddr_strict_bound(path: TreePath<NR_ENTRIES>)
    requires
        path.inv(),
        path.len() <= INC_LEVELS - 1,
    ensures
        vaddr(path) < 0x1_0000_0000_0000int,
{
    broadcast use TreePath::index_satisfies_elem_inv;
    broadcast use TreePath::push_tail_property;

    lemma_page_size_spec_values();
    vstd::arithmetic::power2::lemma2_to64();
    vstd::arithmetic::power2::lemma2_to64_rest();
    if path.len() == 0 {
        assert(rec_vaddr(path, 0) == 0);
    } else if path.len() == 1 {
        let i0 = path.index(0);
        assert(rec_vaddr(path, 1) == 0);
        assert(rec_vaddr(path, 0) == vaddr_make::<NR_LEVELS>(0, i0) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(0x80_0000_0000usize * i0 < 0x1_0000_0000_0000int) by (nonlinear_arith)
            requires
                i0 < 512,
        ;
    } else if path.len() == 2 {
        let i0 = path.index(0);
        let i1 = path.index(1);
        assert(rec_vaddr(path, 2) == 0);
        assert(rec_vaddr(path, 1) == vaddr_make::<NR_LEVELS>(1, i1) as usize);
        assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
            1,
            i1,
        )) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
        assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 < 0x1_0000_0000_0000int)
            by (nonlinear_arith)
            requires
                i0 < 512,
                i1 < 512,
        ;
    } else if path.len() == 3 {
        let i0 = path.index(0);
        let i1 = path.index(1);
        let i2 = path.index(2);
        assert(rec_vaddr(path, 3) == 0);
        assert(rec_vaddr(path, 2) == vaddr_make::<NR_LEVELS>(2, i2) as usize);
        assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + vaddr_make::<NR_LEVELS>(
            2,
            i2,
        )) as usize);
        assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
            1,
            i1,
        ) + vaddr_make::<NR_LEVELS>(2, i2)) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
        assert(vaddr_make::<NR_LEVELS>(2, i2) == 0x20_0000usize * i2) by (compute);
        assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2
            < 0x1_0000_0000_0000int) by (nonlinear_arith)
            requires
                i0 < 512,
                i1 < 512,
                i2 < 512,
        ;
    } else {
        assert(path.len() == 4);
        let i0 = path.index(0);
        let i1 = path.index(1);
        let i2 = path.index(2);
        let i3 = path.index(3);
        assert(rec_vaddr(path, 4) == 0);
        assert(rec_vaddr(path, 3) == vaddr_make::<NR_LEVELS>(3, i3) as usize);
        assert(rec_vaddr(path, 2) == (vaddr_make::<NR_LEVELS>(2, i2) + vaddr_make::<NR_LEVELS>(
            3,
            i3,
        )) as usize);
        assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + vaddr_make::<NR_LEVELS>(
            2,
            i2,
        ) + vaddr_make::<NR_LEVELS>(3, i3)) as usize);
        assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
            1,
            i1,
        ) + vaddr_make::<NR_LEVELS>(2, i2) + vaddr_make::<NR_LEVELS>(3, i3)) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
        assert(vaddr_make::<NR_LEVELS>(2, i2) == 0x20_0000usize * i2) by (compute);
        assert(vaddr_make::<NR_LEVELS>(3, i3) == 0x1000usize * i3) by (compute);
        assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2 + 0x1000usize
            * i3 < 0x1_0000_0000_0000int) by (nonlinear_arith)
            requires
                i0 < 512,
                i1 < 512,
                i2 < 512,
                i3 < 512,
        ;
    }
}

/// The VA of any path is within the `2^39`-sized cell of its top-level index:
/// `path[0] * 2^39 <= vaddr(path)` and `vaddr(path) + page_size <= (path[0]+1) * 2^39`.
/// Pure VA arithmetic (x86 4-level paging). Used by `view_rec_top_index_va_bound`.
pub proof fn lemma_vaddr_top_index_cell(path: TreePath<NR_ENTRIES>)
    requires
        path.inv(),
        1 <= path.len() <= INC_LEVELS - 1,
    ensures
        (path.index(0)) * 0x80_0000_0000int <= vaddr(path),
        vaddr(path) + page_size((INC_LEVELS - path.len()) as PagingLevel) <= (path.index(0) + 1)
            * 0x80_0000_0000int,
{
    broadcast use TreePath::index_satisfies_elem_inv;

    lemma_page_size_spec_values();
    vstd::arithmetic::power2::lemma2_to64();
    vstd::arithmetic::power2::lemma2_to64_rest();
    let i0 = path.index(0);
    if path.len() == 1 {
        assert(rec_vaddr(path, 1) == 0);
        assert(rec_vaddr(path, 0) == vaddr_make::<NR_LEVELS>(0, i0) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(page_size(4) == 0x80_0000_0000usize);
        assert((0x80_0000_0000int * i0) + 0x80_0000_0000int == (i0 + 1) * 0x80_0000_0000int)
            by (nonlinear_arith);
    } else if path.len() == 2 {
        let i1 = path.index(1);
        assert(rec_vaddr(path, 2) == 0);
        assert(rec_vaddr(path, 1) == vaddr_make::<NR_LEVELS>(1, i1) as usize);
        assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
            1,
            i1,
        )) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
        assert(page_size(3) == 0x4000_0000usize);
        assert(0x80_0000_0000int * i0 <= 0x80_0000_0000int * i0 + 0x4000_0000int * i1)
            by (nonlinear_arith);
        assert(0x80_0000_0000int * i0 + 0x4000_0000int * i1 + 0x4000_0000int <= (i0 + 1)
            * 0x80_0000_0000int) by (nonlinear_arith)
            requires
                i1 < 512,
        ;
    } else if path.len() == 3 {
        let i1 = path.index(1);
        let i2 = path.index(2);
        assert(rec_vaddr(path, 3) == 0);
        assert(rec_vaddr(path, 2) == vaddr_make::<NR_LEVELS>(2, i2) as usize);
        assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + vaddr_make::<NR_LEVELS>(
            2,
            i2,
        )) as usize);
        assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
            1,
            i1,
        ) + vaddr_make::<NR_LEVELS>(2, i2)) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
        assert(vaddr_make::<NR_LEVELS>(2, i2) == 0x20_0000usize * i2) by (compute);
        assert(page_size(2) == 0x20_0000usize);
        assert(0x80_0000_0000int * i0 <= 0x80_0000_0000int * i0 + 0x4000_0000int * i1 + 0x20_0000int
            * i2) by (nonlinear_arith);
        assert(0x80_0000_0000int * i0 + 0x4000_0000int * i1 + 0x20_0000int * i2 + 0x20_0000int <= (
        i0 + 1) * 0x80_0000_0000int) by (nonlinear_arith)
            requires
                i1 < 512,
                i2 < 512,
        ;
    } else {
        assert(path.len() == 4);
        let i1 = path.index(1);
        let i2 = path.index(2);
        let i3 = path.index(3);
        assert(rec_vaddr(path, 4) == 0);
        assert(rec_vaddr(path, 3) == vaddr_make::<NR_LEVELS>(3, i3) as usize);
        assert(rec_vaddr(path, 2) == (vaddr_make::<NR_LEVELS>(2, i2) + vaddr_make::<NR_LEVELS>(
            3,
            i3,
        )) as usize);
        assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + vaddr_make::<NR_LEVELS>(
            2,
            i2,
        ) + vaddr_make::<NR_LEVELS>(3, i3)) as usize);
        assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
            1,
            i1,
        ) + vaddr_make::<NR_LEVELS>(2, i2) + vaddr_make::<NR_LEVELS>(3, i3)) as usize);
        assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
        assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
        assert(vaddr_make::<NR_LEVELS>(2, i2) == 0x20_0000usize * i2) by (compute);
        assert(vaddr_make::<NR_LEVELS>(3, i3) == 0x1000usize * i3) by (compute);
        assert(page_size(1) == 0x1000usize);
        assert(0x80_0000_0000int * i0 <= 0x80_0000_0000int * i0 + 0x4000_0000int * i1 + 0x20_0000int
            * i2 + 0x1000int * i3) by (nonlinear_arith);
        assert(0x80_0000_0000int * i0 + 0x4000_0000int * i1 + 0x20_0000int * i2 + 0x1000int * i3
            + 0x1000int <= (i0 + 1) * 0x80_0000_0000int) by (nonlinear_arith)
            requires
                i1 < 512,
                i2 < 512,
                i3 < 512,
        ;
    }
}

/// `vaddr_of::<C>(path)` in `int` equals the unconditional sum — no usize
/// wrap. Holds because `vaddr(path) < 2^48` (any valid path) and
/// `LEADING_BITS < 2^16`, so the sum is `< 2^64 = usize::MAX + 1`.
pub proof fn lemma_vaddr_of_eq_int<C: PageTableConfig>(path: TreePath<NR_ENTRIES>)
    requires
        path.inv(),
        path.len() <= INC_LEVELS - 1,
    ensures
        vaddr_of::<C>(path) == vaddr(path) + C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int,
{
    C::lemma_page_table_config_constant_properties();
    lemma_vaddr_strict_bound(path);
    let lb = C::LEADING_BITS_spec() as int;
    let v = vaddr(path) as int;
    // `0 <= v + lb * 2^48 < 2^64`: sum fits in usize, cast is lossless.
    assert(lb * 0x1_0000_0000_0000int <= 0xffff_int * 0x1_0000_0000_0000int) by (nonlinear_arith)
        requires
            lb < 0x1_0000int,
            lb >= 0,
    ;
    assert(v + lb * 0x1_0000_0000_0000int < 0x1_0000_0000_0000_0000int) by (nonlinear_arith)
        requires
            v < 0x1_0000_0000_0000int,
            lb < 0x1_0000int,
            lb >= 0,
    ;
}

/// page_size is monotonically increasing in its argument.
pub proof fn page_size_monotonic(a: PagingLevel, b: PagingLevel)
    requires
        1 <= a <= b <= NR_LEVELS + 1,
    ensures
        page_size(a) <= page_size(b),
{
    if a == b {
    } else {
        let ps_a = page_size(a);
        let ps_b = page_size(b);

        lemma_page_size_ge_page_size(a);
        lemma_page_size_ge_page_size(b);

        lemma_page_size_divides(a, b);
        assert(ps_b % ps_a == 0);

        assert(ps_a <= ps_b) by {
            if ps_b < ps_a {
                vstd::arithmetic::div_mod::lemma_small_mod(ps_b as nat, ps_a as nat);
                assert(ps_b % ps_a == ps_b);
                assert(ps_b % ps_a == 0);
                assert(false);
            }
        }
    }
}

/// Sibling paths (same prefix, different last index) have disjoint VA ranges,
/// separated by at least the child page size.
///
/// Generic in `C` only so the proof can reach
/// `PageTableOwner<C>::lemma_vaddr_push_tail_eq`; the body does not depend
/// on `C`.
pub proof fn sibling_paths_disjoint<C: PageTableConfig>(
    prefix: TreePath<NR_ENTRIES>,
    j: usize,
    k: usize,
    size: usize,
)
    requires
        prefix.inv(),
        prefix.len() < INC_LEVELS - 1,
        j < NR_ENTRIES,
        k < NR_ENTRIES,
        j != k,
        size == page_size((INC_LEVELS - prefix.len() - 1) as PagingLevel),
    ensures
        vaddr(prefix.push_tail(j)) + size <= vaddr(prefix.push_tail(k)) || vaddr(
            prefix.push_tail(k),
        ) + size <= vaddr(prefix.push_tail(j)),
{
    PageTableOwner::<C>::lemma_vaddr_push_tail_eq(prefix, j);
    PageTableOwner::<C>::lemma_vaddr_push_tail_eq(prefix, k);
    let s = size as int;
    let vp = vaddr(prefix) as int;
    let vj = vaddr(prefix.push_tail(j)) as int;
    let vk = vaddr(prefix.push_tail(k)) as int;
    if j < k {
        assert(vj + s <= vk) by (nonlinear_arith)
            requires
                vj == vp + j * s,
                vk == vp + k * s,
                j < k,
                s >= 0,
        ;
    } else {
        assert(vk + s <= vj) by (nonlinear_arith)
            requires
                vj == vp + j * s,
                vk == vp + k * s,
                k < j,
                s >= 0,
        ;
    }
}

impl<C: PageTableConfig, const L: usize> TreeNodeValue<L> for EntryOwner<C> {
    open spec fn default(lv: nat) -> Self {
        Self {
            kind: EntryOwnerKind::Absent,
            path: TreePath::new(Seq::empty()),
            parent_level: (INC_LEVELS - lv) as PagingLevel,
        }
    }

    proof fn default_preserves_inv() {
    }

    open spec fn la_inv(self, lv: nat) -> bool {
        self.is_node() ==> lv < L - 1
    }

    proof fn default_preserves_la_inv() {
    }

    // PT-specific per-edge facts now live in `PageTableOwner::pt_inv` /
    // `CursorContinuation::pt_inv_children`.
    open spec fn rel_children(self, i: int, child: Option<Self>) -> bool {
        true
    }

    proof fn default_preserves_rel_children(self, lv: nat) {
    }
}

pub const INC_LEVELS: usize = NR_LEVELS + 1;

/// `OwnerSubtree` is a tree `Node` (from `vstd_extra::ghost_tree`) containing `EntryOwner`s.
/// It lives in a tree of maximum depth 5. Page table nodes can be at levels 0-3, and their entries are their children at the next
/// level down. This means that level 4, the lowest level, can only contain frame entries as it consists of the entries of level 1 page tables.
///
/// Level correspondences: tree level 0 ==> path length 0 ==> level 4 page table
///                        tree level 1 ==> path length 1 ==> level 3 page table (the level 4 page table does not map frames directly)
///                        tree level 2 ==> path length 2 ==> level 2 page table or frame mapped by level 3 table
///                        tree level 3 ==> path length 3 ==> level 1 page table or frame mapped by level 2 table
///                        tree level 4 ==> path length 4 ==> frame mapped by level 1 table
pub type OwnerSubtree<C> = Node<EntryOwner<C>, NR_ENTRIES, INC_LEVELS>;

/// Specifies that `owner` is the ghost owner of a newly allocated empty page table node.
/// Captures the structural post-conditions of `PageTableNode::alloc`.
///
/// The `level` parameter is the **NODE level** (i.e., the PT level of the
/// freshly-allocated PT itself). The entry-side `parent_level` is one above
/// (`level + 1`). This convention is internally consistent with `NodeOwner::inv`
/// (which requires `1 <= level <= NR_LEVELS`) for any `level` in `[1, NR_LEVELS-1]`,
/// unlike the prior convention where `alloc(1)` was unsatisfiable.
pub open spec fn allocated_empty_node_owner<C: PageTableConfig>(
    owner: OwnerSubtree<C>,
    level: PagingLevel,
) -> bool {
    &&& owner.inv()
    &&& owner.value.is_node()
    &&& owner.value.path == TreePath::<NR_ENTRIES>::new(Seq::empty())
    &&& owner.value.parent_level == (level + 1) as PagingLevel
    &&& owner.value.node().level
        == level
    // The fresh subtree's ghost-tree depth. Lets `alloc_if_none` discharge
    // `final(owner).inv()`'s `child.level == self.level + 1`: the grafted
    // children sit at `new_node.level + 1`, which must match the cursor entry's
    // depth + 1.
    &&& owner.level == (INC_LEVELS - level - 1) as nat
    &&& owner.value.node().inv()
    &&& !owner.value.node().children_perm.value().all(|child: C::E| child.is_present())
    &&& forall|i: int|
        #![auto]
        0 <= i < NR_ENTRIES ==> {
            &&& owner.children[i] is Some
            &&& owner.children[i]->0.value.is_absent()
            &&& owner.children[i]->0.value.inv()
            &&& owner.children[i]->0.value.path == owner.value.path.push_tail(i as usize)
        }
    &&& forall|i: int|
        #![auto]
        0 <= i < NR_ENTRIES ==> owner.children[i]->0.value.match_pte(
            owner.value.node().children_perm.value()[i],
            owner.children[i]->0.value.parent_level,
        )
    &&& forall|i: int|
        #![auto]
        0 <= i < NR_ENTRIES ==> owner.children[i]->0.value.parent_level
            == owner.value.node().level
    // The freshly-allocated PT node is zero-filled, so every PTE in
    // `children_perm` is the absent PTE. (Stronger than the existing
    // "not all are present" clause; needed by `split_if_mapped_huge`'s
    // loop invariant which inspects each slot's PTE.)
    &&& forall|j: int|
        0 <= j < NR_ENTRIES ==> #[trigger] owner.value.node().children_perm.value()[j]
            == C::E::new_absent_spec()
}

/// Grandchildren of a freshly-allocated PT node are all `None`. The absent
/// children come from `OwnerSubtree::new_val_tracked` (see
/// `vstd_extra::ghost_tree`), which initializes `children = Seq::new(N, |_| None)`.
/// Kept as a separate predicate (rather than folded into
/// `allocated_empty_node_owner`) to avoid SMT trigger pressure at every
/// `allocated_empty_node_owner` reference; threaded through
/// `PageTableNode::alloc` and `alloc_if_none` only where it's actually needed.
pub open spec fn allocated_empty_node_grandchildren_none<C: PageTableConfig>(
    owner: OwnerSubtree<C>,
) -> bool {
    forall|i: int, j: int|
        0 <= i < NR_ENTRIES && 0 <= j < NR_ENTRIES
            ==> #[trigger] owner.children[i]->0.children[j] is None
}

/// Recursive worker for `rebase_freshly_allocated_children`. Rebases
/// `owner.children[i..NR_ENTRIES]` and leaves `owner.children[0..i]`
/// untouched. Verus disallows `while` in proof code, so the loop is
/// expressed as tail recursion on `i`.
pub proof fn rebase_freshly_allocated_children_at<C: PageTableConfig>(
    tracked owner: &mut OwnerSubtree<C>,
    new_path: TreePath<NR_ENTRIES>,
    i: usize,
)
    requires
        i <= NR_ENTRIES,
        old(owner).children.len() == NR_ENTRIES,
        new_path.inv(),
        forall|j: int| i <= j < NR_ENTRIES ==> (#[trigger] old(owner).children[j]) is Some,
    ensures
        final(owner).value == old(owner).value,
        final(owner).level == old(owner).level,
        final(owner).children.len() == NR_ENTRIES,
        forall|j: int|
            0 <= j < i ==> (#[trigger] final(owner).children[j]) == old(owner).children[j],
        forall|j: int|
            i <= j < NR_ENTRIES ==> {
                let c_old = old(owner).children[j]->0;
                let c_new = (#[trigger] final(owner).children[j])->0;
                &&& final(owner).children[j] is Some
                &&& c_new.value == EntryOwner {
                    path: new_path.push_tail(j as usize),
                    ..c_old.value
                }
                &&& c_new.level == c_old.level
                &&& c_new.children == c_old.children
            },
    decreases NR_ENTRIES - i,
{
    if i < NR_ENTRIES {
        let tracked mut child_opt = owner.children.tracked_remove(i as int);
        let tracked mut child = child_opt.tracked_unwrap();
        child.value.path = new_path.push_tail(i);
        owner.children.tracked_insert(i as int, Some(child));
        rebase_freshly_allocated_children_at(owner, new_path, (i + 1) as usize);
    }
}

/// Rebases the children of a freshly-allocated PT node onto a new path.
///
/// `PageTableNode::alloc` produces an `allocated_empty_node_owner` whose
/// `value.path == empty`, so its children's paths are `empty.push_tail(i)
/// == [i]`. When `alloc_if_none` plugs that subtree into the cursor at a
/// non-empty path, it rewrites the parent's path but leaves children with
/// stale `[i]` paths. This helper walks the children seq and rewrites each
/// child's `value.path` to `new_path.push_tail(i)`, producing a subtree
/// whose `pt_edge_at(_, i)` clauses can be discharged.
pub proof fn rebase_freshly_allocated_children<C: PageTableConfig>(
    tracked owner: &mut OwnerSubtree<C>,
    new_path: TreePath<NR_ENTRIES>,
)
    requires
        old(owner).children.len() == NR_ENTRIES,
        new_path.inv(),
        forall|i: int| 0 <= i < NR_ENTRIES ==> (#[trigger] old(owner).children[i]) is Some,
    ensures
        final(owner).value == old(owner).value,
        final(owner).level == old(owner).level,
        final(owner).children.len() == NR_ENTRIES,
        forall|i: int|
            0 <= i < NR_ENTRIES ==> {
                let c_old = old(owner).children[i]->0;
                let c_new = (#[trigger] final(owner).children[i])->0;
                &&& final(owner).children[i] is Some
                &&& c_new.value == EntryOwner {
                    path: new_path.push_tail(i as usize),
                    ..c_old.value
                }
                &&& c_new.level == c_old.level
                &&& c_new.children == c_old.children
            },
{
    rebase_freshly_allocated_children_at(owner, new_path, 0);
}

/// `tree_predicate_map` for a freshly-allocated node grafted into the cursor:
/// every child is a `new_val`-shaped node (all grandchildren `None`), so each
/// child's `tree_predicate_map` reduces to `f` at that child
/// (`new_val_tree_predicate_map`). Combined with `f` at the root node, this
/// discharges the whole one-level subtree. Used by `alloc_if_none` for the
/// `node_unlocked_except` / `metaregion_sound_pred` / `path_tracked_pred`
/// predicates over the fresh node (all of which hold trivially at the absent
/// children).
pub proof fn fresh_node_tree_predicate_map<C: PageTableConfig>(
    node: OwnerSubtree<C>,
    path: TreePath<NR_ENTRIES>,
    f: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
)
    requires
        node.inv(),
        node.level < INC_LEVELS - 1,
        f(node.value, path),
        forall|i: int| 0 <= i < NR_ENTRIES ==> #[trigger] node.children[i] is Some,
        forall|i: int, j: int|
            0 <= i < NR_ENTRIES && 0 <= j < NR_ENTRIES
                ==> #[trigger] node.children[i].unwrap().children[j] is None,
        forall|i: int|
            0 <= i < NR_ENTRIES ==> #[trigger] f(
                node.children[i].unwrap().value,
                path.push_tail(i as usize),
            ),
    ensures
        node.tree_predicate_map(path, f),
{
    assert forall|i: int|
        0 <= i < node.children.len()
            && #[trigger] node.children[i] is Some implies node.children[i]->0.tree_predicate_map(
        path.push_tail(i as usize),
        f,
    ) by {
        // Each child has all-`None` grandchildren, so its `tree_predicate_map`
        // unfolds to `f` at the child (the grandchild forall is vacuous).
        node.child_some_properties(i as usize);
        let child = node.children[i]->0;
        assert(child.children.len() == NR_ENTRIES);
        assert(forall|j: int|
            0 <= j < child.children.len() ==> #[trigger] child.children[j] is None);
    };
}

/// # Verification Design
/// `PageTableOwner` is a wrapper around [`OwnerSubtree`], which is a [`vstd_extra::ghost_tree::Node`]
/// in a tree of [`EntryOwner`]s. In turn, `EntryOwner` carries a enum that may be a
/// [`FrameEntryOwner`] if the entry is a leaf node that maps a frame, or a [`NodeOwner`] if
/// the entry is a sub-table. The root of the top-level page table owner should always be
/// a `NodeOwner`.
pub tracked struct PageTableOwner<C: PageTableConfig>(pub OwnerSubtree<C>);

impl<C: PageTableConfig> PageTableOwner<C> {
    /// Per-edge constraint between a node-parent and its child at index `i`.
    pub open spec fn pt_edge_at(parent: OwnerSubtree<C>, i: int) -> bool {
        &&& parent.children[i] is Some
        &&& parent.children[i]->0.value.path.len() == parent.value.node().tree_level
            + 1
        // The child either matches its PTE as an owned node/frame/absent
        // entry, OR — only at the top level (`level == NR_LEVELS`, e.g. a user
        // PT's shared kernel-half slots) — is a `borrowed` (translation-only)
        // entry whose PTE is a present non-leaf node-PTE pointing at a sub-tree
        // owned by another config. Borrowed children contribute nothing to
        // `view_rec`. The top-level guard keeps deeper consumers on pure
        // `match_pte`, so borrowing never appears below the root.
        &&& (parent.children[i]->0.value.match_pte(
            parent.value.node().children_perm.value()[i],
            parent.value.node().level,
        ) || (parent.value.node().level == NR_LEVELS && C::LEADING_BITS_spec() == 0
            && parent.children[i]->0.value.borrowed_match_pte(
            parent.value.node().children_perm.value()[i],
            parent.value.node().level,
        )))
        &&& parent.children[i]->0.value.path == parent.value.path.push_tail(i as usize)
        &&& parent.children[i]->0.value.parent_level == parent.value.node().level
    }

    /// Depth-indexed PT-specific per-edge invariant. `depth` is a manifest
    /// fuel counter that decreases at each recursive call, so termination
    /// doesn't depend on tree structure.
    pub open spec fn pt_inv_at_depth(self, depth: nat) -> bool
        decreases depth,
    {
        if depth == 0 {
            true
        } else if self.0.value.is_node() {
            forall|i: int|
                #![trigger self.0.children[i]]
                0 <= i < NR_ENTRIES ==> Self::pt_edge_at(self.0, i) && PageTableOwner(
                    self.0.children[i]->0,
                ).pt_inv_at_depth((depth - 1) as nat)
        } else {
            forall|i: int|
                #![trigger self.0.children[i]]
                0 <= i < NR_ENTRIES ==> self.0.children[i] is None
        }
    }

    /// PT-specific tree invariant. Wraps `self.0.inv()` (the ghost
    /// tree's structural invariants) and adds path identity, `match_pte`,
    /// `parent_level`, "nodes have all children Some", and "non-nodes
    /// have all children None" recursively via `pt_inv_at_depth`.
    pub open spec fn pt_inv(self) -> bool {
        &&& self.0.inv()
        &&& self.pt_inv_at_depth((INC_LEVELS - self.0.level) as nat)
    }

    pub proof fn pt_inv_unroll(self, i: int)
        requires
            self.pt_inv(),
            self.0.value.is_node(),
            0 <= i < NR_ENTRIES,
        ensures
            Self::pt_edge_at(self.0, i),
            PageTableOwner(self.0.children[i]->0).pt_inv(),
    {
        // la_inv + is_node() gives tree_level < L-1, so depth > 0 and the
        // node branch of pt_inv_at_depth fires.
        let depth = (INC_LEVELS - self.0.level) as nat;
        assert(<EntryOwner<C> as TreeNodeValue<INC_LEVELS>>::la_inv(self.0.value, self.0.level));
    }

    pub proof fn pt_inv_non_node(self, i: int)
        requires
            self.pt_inv(),
            !self.0.value.is_node(),
            0 <= i < NR_ENTRIES,
        ensures
            self.0.children[i] is None,
    {
        let depth = (INC_LEVELS - self.0.level) as nat;
        if depth == 0 {
            assert(self.0.level >= INC_LEVELS);
        }
    }

    /// `pt_inv_at_depth(depth)` for a non-node subtree whose grandchildren are
    /// all `None`. Used by `allocated_empty_node_pt_inv` for the absent
    /// children of a freshly-allocated PT node.
    pub proof fn non_node_pt_inv_at_depth(self, depth: nat)
        requires
            !self.0.value.is_node(),
            forall|j: int| 0 <= j < NR_ENTRIES ==> #[trigger] self.0.children[j] is None,
        ensures
            self.pt_inv_at_depth(depth),
        decreases depth,
    {
    }

    /// `pt_inv` for a freshly-allocated PT node after `alloc_if_none`'s rebase.
    ///
    /// Discharges the long-standing `assume` that blocked closing
    /// `continuation_inv_holds_after_child_restore`: combines the per-edge
    /// facts threaded through `alloc_if_none`'s ensures (paths rebased,
    /// `match_pte`, `parent_level`) with `allocated_empty_node_grandchildren_none`
    /// to drive `pt_inv_at_depth` to its non-node base case at every absent
    /// child.
    #[verifier::spinoff_prover]
    pub proof fn allocated_empty_node_pt_inv(owner: OwnerSubtree<C>)
        requires
            owner.inv(),
            owner.value.is_node(),
            owner.children.len() == NR_ENTRIES,
            forall|i: int|
                0 <= i < NR_ENTRIES ==> {
                    let c = #[trigger] owner.children[i];
                    &&& c is Some
                    &&& c->0.value.is_absent()
                    &&& c->0.value.path.len() == owner.value.node().tree_level + 1
                    &&& c->0.value.match_pte(
                        owner.value.node().children_perm.value()[i],
                        owner.value.node().level,
                    )
                    &&& c->0.value.path == owner.value.path.push_tail(i as usize)
                    &&& c->0.value.parent_level == owner.value.node().level
                },
            allocated_empty_node_grandchildren_none(owner),
        ensures
            PageTableOwner(owner).pt_inv(),
    {
        let depth = (INC_LEVELS - owner.level) as nat;
        // `is_node` + `la_inv` forces `owner.level < INC_LEVELS - 1`, so depth >= 2.
        assert(<EntryOwner<C> as TreeNodeValue<INC_LEVELS>>::la_inv(owner.value, owner.level));
        // Drive `pt_inv_at_depth(depth)` via the `is_node` branch: prove
        // `pt_edge_at` and the recursive `pt_inv_at_depth(depth-1)` for each child.
        assert forall|i: int| 0 <= i < NR_ENTRIES implies #[trigger] Self::pt_edge_at(owner, i)
            && PageTableOwner(owner.children[i].unwrap()).pt_inv_at_depth((depth - 1) as nat) by {
            let child = owner.children[i].unwrap();
            // pt_edge_at follows from the per-edge facts in the precondition.
            assert(Self::pt_edge_at(owner, i));
            // owner.inv() ⇒ child.inv() (Node::inv recurses since
            // INC_LEVELS - owner.level > 1) ⇒ child.value.inv() ⇒ inv_base
            // ⇒ (node is Some ⇒ !absent), so is_absent ⇒ !is_node.
            assert(child.inv());
            assert(child.value.inv());
            assert(child.value.inv_base());
            assert(!child.value.is_node());
            // Each child is non-node with all grandchildren None — the
            // non-node branch of pt_inv_at_depth fires.
            PageTableOwner(child).non_node_pt_inv_at_depth((depth - 1) as nat);
        };
    }

    /// For a top-level (root) page table, entries at indices outside of
    /// `C::TOP_LEVEL_INDEX_RANGE_spec()` are absent. This ensures that
    /// UserPtConfig and KernelPtConfig page tables manage disjoint portions
    /// of the virtual address space.
    pub open spec fn top_level_indices_absent(self) -> bool {
        let range = C::TOP_LEVEL_INDEX_RANGE_spec();
        self.0.value.is_node() ==> forall|i: int|
            #![trigger self.0.children[i]]
            0 <= i < NR_ENTRIES && !(range.start <= i < range.end) ==> self.0.children[i] is Some
                && self.0.children[i]->0.value.is_absent()
    }

    pub open spec fn view_rec_node_children(self, path: TreePath<NR_ENTRIES>) -> Seq<Set<Mapping>>
        decreases INC_LEVELS - path.len(), 0nat,
        when self.0.inv() && path.len() < INC_LEVELS - 1
    {
        self.0.children.map(
            |i, child: Option<OwnerSubtree<C>>|
                if child is Some {
                    PageTableOwner(child->0).view_rec(path.push_tail(i as usize))
                } else {
                    Set::empty()
                },
        )
    }

    pub open spec fn view_rec(self, path: TreePath<NR_ENTRIES>) -> Set<Mapping>
        decreases INC_LEVELS - path.len(), 1nat,
        when self.0.inv() && path.len() <= INC_LEVELS - 1
    {
        if self.0.value.is_frame() {
            let va = vaddr_of::<C>(path);
            let pt_level = INC_LEVELS - path.len();
            let page_size = page_size(pt_level as PagingLevel);

            set![Mapping {
                va_range: Range { start: va as int, end: va + page_size },
                pa_range: Range {
                    start: self.0.value.frame().mapped_pa,
                    end: (self.0.value.frame().mapped_pa + page_size) as Paddr,
                },
                page_size: page_size,
                property: self.0.value.frame().prop,
            }]
        } else if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
            self.view_rec_node_children(path).to_set().flatten()
        } else {
            set![]
        }
    }

    pub broadcast proof fn lemma_view_rec_contains_intro(
        self,
        path: TreePath<NR_ENTRIES>,
        m: Mapping,
        i: int,
    )
        requires
            self.0.inv(),
            path.len() < INC_LEVELS - 1,
            self.0.value.is_node(),
            0 <= i < self.0.children.len(),
            self.0.children[i] is Some,
            #[trigger] PageTableOwner(self.0.children[i]->0).view_rec(
                path.push_tail(i as usize),
            ).contains(m),
        ensures
            self.view_rec(path).contains(m),
    {
        broadcast use vstd::seq_lib::group_seq_properties;

        let mapped = self.view_rec_node_children(path);
        assert(self.0.value.kind is Node);
        assert(!self.0.value.is_frame());
        assert(mapped[i].contains(m));
        mapped.to_set_ensures();
        assert(mapped.to_set().contains(mapped[i]));
        mapped.to_set().lemma_flatten_contains(m);
    }

    pub broadcast proof fn lemma_view_rec_contains(self, path: TreePath<NR_ENTRIES>)
        requires
            self.0.inv(),
            path.len() < INC_LEVELS - 1,
            self.0.value.is_node(),
        ensures
            #![trigger self.view_rec(path)]
            forall|m: Mapping|
                #![trigger self.view_rec(path).contains(m)]
                self.view_rec(path).contains(m) ==> exists|i: int|
                    #![trigger self.0.children[i]]
                    0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                        self.0.children[i]->0,
                    ).view_rec(path.push_tail(i as usize)).contains(m),
    {
        broadcast use vstd::seq_lib::group_seq_properties;

        assert forall|m: Mapping| #[trigger] self.view_rec(path).contains(m) implies exists|i: int|
            #![trigger self.0.children[i]]
            0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                self.0.children[i]->0,
            ).view_rec(path.push_tail(i as usize)).contains(m) by {
            let mapped = self.view_rec_node_children(path);
            assert(self.0.value.kind is Node);
            assert(!self.0.value.is_frame());
            mapped.to_set().lemma_flatten_contains(m);
            let elem_s = choose|elem_s: Set<Mapping>| #[trigger]
                mapped.to_set().contains(elem_s) && elem_s.contains(m);
            mapped.to_set_ensures();
            assert(mapped.contains(elem_s));
            let i = mapped.lemma_contains_to_index(elem_s);
            if self.0.children[i] is Some {
                assert(mapped[i] == PageTableOwner(self.0.children[i]->0).view_rec(
                    path.push_tail(i as usize),
                ));
            } else {
                assert(mapped[i] == Set::<Mapping>::empty());
                assert(false);
            }
        }
    }

    pub proof fn view_rec_contains_choose(self, path: TreePath<NR_ENTRIES>, m: Mapping) -> (i: int)
        requires
            self.0.inv(),
            path.len() < INC_LEVELS - 1,
            self.view_rec(path).contains(m),
            self.0.value.is_node(),
        ensures
            0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                self.0.children[i]->0,
            ).view_rec(path.push_tail(i as usize)).contains(m),
    {
        broadcast use PageTableOwner::group_lemmas;

        choose|i: int|
            #![auto]
            0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                self.0.children[i].unwrap(),
            ).view_rec(path.push_tail(i as usize)).contains(m)
    }

    /// Closed-form for `vaddr(path.push_tail(i))` by case-split on `path.len() ∈ {0,1,2,3}`.
    #[verifier::rlimit(400)]
    pub proof fn lemma_vaddr_push_tail_eq(path: TreePath<NR_ENTRIES>, i: usize)
        requires
            path.inv(),
            path.len() < INC_LEVELS - 1,
            i < NR_ENTRIES,
        ensures
            vaddr(path.push_tail(i)) == vaddr(path) + i * page_size(
                (INC_LEVELS - path.len() - 1) as PagingLevel,
            ),
            vaddr(path) + (i + 1) * page_size((INC_LEVELS - path.len() - 1) as PagingLevel)
                <= usize::MAX,
    {
        broadcast use TreePath::push_tail_property;
        broadcast use TreePath::index_satisfies_elem_inv;

        lemma_page_size_spec_values();
        vstd::arithmetic::power2::lemma2_to64();
        vstd::arithmetic::power2::lemma2_to64_rest();
        let pt = path.push_tail(i);
        if path.len() >= 1 {
            Self::lemma_vaddr_path_alignment_and_bound(path);
        }
        if path.len() == 0 {
            assert(rec_vaddr(path, 0) == 0);
            assert(pt.len() == 1);
            assert(rec_vaddr(pt, 1) == 0);
            assert(rec_vaddr(pt, 0) == (vaddr_make::<NR_LEVELS>(0, i) + 0) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i) == 0x80_0000_0000usize * i) by (compute);
            assert(page_size(4) == 0x80_0000_0000usize);
            assert(0x80_0000_0000usize * (i + 1) <= usize::MAX) by (nonlinear_arith)
                requires
                    i < 512,
            ;
        } else if path.len() == 1 {
            let i0 = path.index(0);
            assert(rec_vaddr(path, 1) == 0);
            assert(rec_vaddr(path, 0) == vaddr_make::<NR_LEVELS>(0, i0) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
            assert(rec_vaddr(path, 0) == 0x80_0000_0000usize * i0);
            assert(pt.len() == 2);
            assert(pt.index(0) == i0);
            assert(pt.index(1) == i);
            assert(rec_vaddr(pt, 2) == 0);
            assert(rec_vaddr(pt, 1) == vaddr_make::<NR_LEVELS>(1, i) as usize);
            assert(vaddr_make::<NR_LEVELS>(1, i) == 0x4000_0000usize * i) by (compute);
            assert(rec_vaddr(pt, 0) == (0x80_0000_0000usize * i0) + 0x4000_0000usize * i);
            assert(page_size(3) == 0x4000_0000usize);
            assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * (i + 1) <= usize::MAX)
                by (nonlinear_arith)
                requires
                    i0 < 512,
                    i < 512,
            ;
        } else if path.len() == 2 {
            let i0 = path.index(0);
            let i1 = path.index(1);
            assert(rec_vaddr(path, 2) == 0);
            assert(rec_vaddr(path, 1) == vaddr_make::<NR_LEVELS>(1, i1) as usize);
            assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
                1,
                i1,
            )) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
            assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
            assert(pt.len() == 3);
            assert(pt.index(0) == i0);
            assert(pt.index(1) == i1);
            assert(pt.index(2) == i);
            assert(rec_vaddr(pt, 3) == 0);
            assert(rec_vaddr(pt, 2) == vaddr_make::<NR_LEVELS>(2, i) as usize);
            assert(rec_vaddr(pt, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + vaddr_make::<NR_LEVELS>(
                2,
                i,
            )) as usize);
            assert(rec_vaddr(pt, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
                1,
                i1,
            ) + vaddr_make::<NR_LEVELS>(2, i)) as usize);
            assert(vaddr_make::<NR_LEVELS>(2, i) == 0x20_0000usize * i) by (compute);
            assert(page_size(2) == 0x20_0000usize);
            assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * (i + 1)
                <= usize::MAX) by (nonlinear_arith)
                requires
                    i0 < 512,
                    i1 < 512,
                    i < 512,
            ;
        } else {
            assert(path.len() == 3);
            let i0 = path.index(0);
            let i1 = path.index(1);
            let i2 = path.index(2);
            assert(rec_vaddr(path, 3) == 0);
            assert(rec_vaddr(path, 2) == vaddr_make::<NR_LEVELS>(2, i2) as usize);
            assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + vaddr_make::<NR_LEVELS>(
                2,
                i2,
            )) as usize);
            assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
                1,
                i1,
            ) + vaddr_make::<NR_LEVELS>(2, i2)) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
            assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
            assert(vaddr_make::<NR_LEVELS>(2, i2) == 0x20_0000usize * i2) by (compute);
            assert(pt.len() == 4);
            assert(pt.index(0) == i0);
            assert(pt.index(1) == i1);
            assert(pt.index(2) == i2);
            assert(pt.index(3) == i);
            assert(rec_vaddr(pt, 4) == 0);
            assert(rec_vaddr(pt, 3) == vaddr_make::<NR_LEVELS>(3, i) as usize);
            assert(rec_vaddr(pt, 2) == (vaddr_make::<NR_LEVELS>(2, i2) + vaddr_make::<NR_LEVELS>(
                3,
                i,
            )) as usize);
            assert(rec_vaddr(pt, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + vaddr_make::<NR_LEVELS>(
                2,
                i2,
            ) + vaddr_make::<NR_LEVELS>(3, i)) as usize);
            assert(rec_vaddr(pt, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + vaddr_make::<NR_LEVELS>(
                1,
                i1,
            ) + vaddr_make::<NR_LEVELS>(2, i2) + vaddr_make::<NR_LEVELS>(3, i)) as usize);
            assert(vaddr_make::<NR_LEVELS>(3, i) == 0x1000usize * i) by (compute);
            assert(page_size(1) == 0x1000usize);
            assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2
                + 0x1000usize * (i + 1) <= usize::MAX) by (nonlinear_arith)
                requires
                    i0 < 512,
                    i1 < 512,
                    i2 < 512,
                    i < 512,
            ;
        }
    }

    pub proof fn view_rec_vaddr_range(self, path: TreePath<NR_ENTRIES>, m: Mapping)
        requires
            self.pt_inv(),
            path.inv(),
            path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
            self.0.value.parent_level == (INC_LEVELS - self.0.level) as PagingLevel,
            self.view_rec(path).contains(m),
        ensures
            vaddr_of::<C>(path) <= m.va_range.start,
            m.va_range.start < m.va_range.end,
            m.va_range.end <= vaddr_of::<C>(path) + page_size(
                (INC_LEVELS - path.len()) as PagingLevel,
            ),
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;

        lemma_page_size_spec_values();
        if self.0.value.is_frame() {
            Self::lemma_vaddr_path_alignment_and_bound(path);
            let frame = self.0.value.frame();
            let pt_level = (INC_LEVELS - path.len()) as PagingLevel;
            let expected = Mapping {
                va_range: Range {
                    start: vaddr_of::<C>(path) as int,
                    end: vaddr_of::<C>(path) + page_size(pt_level),
                },
                pa_range: Range {
                    start: frame.mapped_pa,
                    end: (frame.mapped_pa + page_size(pt_level)) as Paddr,
                },
                page_size: page_size(pt_level),
                property: frame.prop,
            };
            assert(self.view_rec(path) == set![expected]);
            assert(m == expected);
            assert(page_size(pt_level) > 0);
        } else if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
            let i = choose|i: int|
                #![trigger self.0.children[i]]
                0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                    self.0.children[i].unwrap(),
                ).view_rec(path.push_tail(i as usize)).contains(m);
            self.pt_inv_unroll(i);
            let child = PageTableOwner(self.0.children[i].unwrap());
            path.push_tail_preserves_inv(i as usize);
            path.push_tail_property_len(i as usize);
            child.view_rec_vaddr_range(path.push_tail(i as usize), m);
            Self::lemma_vaddr_push_tail_eq(path, i as usize);

            let parent_ps = page_size((INC_LEVELS - path.len()) as PagingLevel) as int;
            let child_ps = page_size((INC_LEVELS - path.len() - 1) as PagingLevel) as int;
            vstd::arithmetic::power2::lemma2_to64();
            vstd::arithmetic::power2::lemma2_to64_rest();
            if path.len() == 0 {
                assert(parent_ps == 0x1_0000_0000_0000);
                assert(child_ps == 0x80_0000_0000);
            } else if path.len() == 1 {
                assert(parent_ps == 0x80_0000_0000);
                assert(child_ps == 0x4000_0000);
            } else if path.len() == 2 {
                assert(parent_ps == 0x4000_0000);
                assert(child_ps == 0x20_0000);
            } else {
                assert(path.len() == 3);
                assert(parent_ps == 0x20_0000);
                assert(child_ps == 0x1000);
            }
            assert(parent_ps == 512 * child_ps) by (nonlinear_arith)
                requires
                    (parent_ps == 0x1_0000_0000_0000 && child_ps == 0x80_0000_0000) || (parent_ps
                        == 0x80_0000_0000 && child_ps == 0x4000_0000) || (parent_ps == 0x4000_0000
                        && child_ps == 0x20_0000) || (parent_ps == 0x20_0000 && child_ps == 0x1000),
            ;
            assert((i + 1) * child_ps <= 512 * child_ps) by (nonlinear_arith)
                requires
                    0 <= i < 512,
                    child_ps >= 0,
            ;
            assert(m.va_range.end <= vaddr_of::<C>(path.push_tail(i as usize)) + child_ps);
            assert(vaddr(path.push_tail(i as usize)) == vaddr(path) + i * child_ps);
            // Bridge `vaddr_of(push_tail(i)) == vaddr_of(path) + i * child_ps`
            // via the no-wrap helper: both `vaddr_of` terms equal their `int`
            // counterparts, and the `vaddr` identity above lifts directly.
            lemma_vaddr_of_eq_int::<C>(path);
            lemma_vaddr_of_eq_int::<C>(path.push_tail(i as usize));
            assert(vaddr_of::<C>(path.push_tail(i as usize)) == vaddr_of::<C>(path) + i * child_ps);
            assert(i * child_ps + child_ps == (i + 1) * child_ps) by (nonlinear_arith);
            assert(m.va_range.end <= vaddr_of::<C>(path) + (i + 1) * child_ps);
            assert(m.va_range.end <= vaddr_of::<C>(path) + parent_ps);
        }
    }

    /// Any mapping in a subtree's `view_rec` has its VA range within the
    /// `2^39`-sized cell of the subtree's top-level index `path[0]`, shifted by
    /// the config's `LEADING_BITS` high-half base. With `path[0] < t`, the range
    /// end is `<= t * 2^39 + LEADING_BITS * 2^48` — the per-config VA bound that
    /// discharges the user/kernel isolation theorems.
    pub proof fn view_rec_top_index_va_bound(self, path: TreePath<NR_ENTRIES>, m: Mapping, t: int)
        requires
            self.pt_inv(),
            path.inv(),
            1 <= path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
            self.0.value.parent_level == (INC_LEVELS - self.0.level) as PagingLevel,
            path.index(0) < t,
            self.view_rec(path).contains(m),
        ensures
            (path.index(0)) * 0x80_0000_0000int + C::LEADING_BITS_spec() * 0x1_0000_0000_0000int
                <= m.va_range.start,
            m.va_range.start < m.va_range.end,
            m.va_range.end <= t * 0x80_0000_0000int + C::LEADING_BITS_spec()
                * 0x1_0000_0000_0000int,
    {
        self.view_rec_vaddr_range(path, m);
        lemma_vaddr_of_eq_int::<C>(path);
        lemma_vaddr_top_index_cell(path);
        // `vaddr_of(path) == vaddr(path) + LEADING_BITS*2^48` (lemma_vaddr_of_eq_int);
        // the positional `vaddr(path)` lies in the top-index cell
        // `[index(0)*2^39, (index(0)+1)*2^39)` (lemma_vaddr_top_index_cell), and
        // `(index(0)+1) <= t`. Adding the `LEADING_BITS*2^48` base shifts both
        // ends — giving the user (LB=0) low half and the kernel (LB=0xffff)
        // high half.
        assert((path.index(0) + 1) * 0x80_0000_0000int <= t * 0x80_0000_0000int)
            by (nonlinear_arith)
            requires
                path.index(0) < t,
        ;
    }

    /// `pt_inv` (plus the root's recorded path) lifts to a full
    /// `path_correct_pred` tree predicate: every entry's `.path` field
    /// equals its structural position.  `PageTableOwner::inv()` already
    /// bundles this (see the `Inv` impl below) but only for *node*-rooted
    /// trees; callers that need it for an arbitrary `pt_inv` subtree
    /// (including the leaf/frame-rooted child subtrees of a cursor
    /// continuation) need a standalone form not gated on `value.is_node()`.
    pub proof fn pt_inv_implies_path_correct(subtree: OwnerSubtree<C>, path: TreePath<NR_ENTRIES>)
        requires
            PageTableOwner(subtree).pt_inv(),
            subtree.value.path == path,
        ensures
            subtree.tree_predicate_map(path, Self::path_correct_pred()),
        decreases INC_LEVELS - subtree.level,
    {
        assert(subtree.children.len() == NR_ENTRIES);
        // Root: path_correct_pred(value, path) == (value.path == path).
        assert(Self::path_correct_pred()(subtree.value, path));
        if subtree.level < INC_LEVELS - 1 {
            assert forall|i: int|
                0 <= i < subtree.children.len() && (
                #[trigger] subtree.children[i]) is Some implies subtree.children[i].unwrap().tree_predicate_map(
            path.push_tail(i as usize), Self::path_correct_pred()) by {
                if subtree.value.is_node() {
                    PageTableOwner(subtree).pt_inv_unroll(i);
                    // pt_edge_at: child.value.path == subtree.value.path.push_tail(i)
                    assert(subtree.children[i].unwrap().value.path == path.push_tail(i as usize));
                    Self::pt_inv_implies_path_correct(
                        subtree.children[i].unwrap(),
                        path.push_tail(i as usize),
                    );
                } else {
                    // Non-node ⟹ children all None, contradicts `is Some`.
                    PageTableOwner(subtree).pt_inv_non_node(i);
                }
            };
        }
    }

    /// Forward dual of [`Self::view_rec_vaddr_range`]: in a `pt_inv`,
    /// path-correct subtree whose mappings are all contained in
    /// `ambient`, if no mapping in `ambient` starts at
    /// `vaddr_of(removed_path)`, then no *frame* entry anywhere in the
    /// subtree carries `removed_path` as its path.  A frame entry at
    /// structural position `pos` contributes exactly one mapping starting
    /// at `vaddr_of(pos)`; path-correctness makes `pos == entry.path`, so
    /// a frame with `.path == removed_path` would force a mapping starting
    /// at `vaddr_of(removed_path)` into `ambient` — a contradiction.
    pub proof fn no_frame_with_path_rec(
        self,
        path: TreePath<NR_ENTRIES>,
        removed_path: TreePath<NR_ENTRIES>,
        ambient: Set<Mapping>,
    )
        requires
            self.pt_inv(),
            path.inv(),
            path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
            self.0.value.parent_level == (INC_LEVELS - self.0.level) as PagingLevel,
            self.0.value.path == path,
            self.0.tree_predicate_map(path, Self::path_correct_pred()),
            forall|mm: Mapping|
                #![trigger self.view_rec(path).contains(mm)]
                self.view_rec(path).contains(mm) ==> ambient.contains(mm),
            forall|mm: Mapping|
                #![trigger ambient.contains(mm)]
                ambient.contains(mm) ==> mm.va_range.start != vaddr_of::<C>(removed_path),
        ensures
            self.0.tree_predicate_map(
                path,
                |e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>|
                    e.is_frame() ==> e.path != removed_path,
            ),
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;

        let g = |e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>|
            e.is_frame() ==> e.path != removed_path;

        // Path-correctness at the root: value.path == path.
        assert(Self::path_correct_pred()(self.0.value, path));
        assert(self.0.value.path == path);

        // Root entry satisfies `g`.
        if self.0.value.is_frame() {
            let frame = self.0.value.frame();
            let pt_level = (INC_LEVELS - path.len()) as PagingLevel;
            let expected = Mapping {
                va_range: Range {
                    start: vaddr_of::<C>(path) as int,
                    end: vaddr_of::<C>(path) + page_size(pt_level),
                },
                pa_range: Range {
                    start: frame.mapped_pa,
                    end: (frame.mapped_pa + page_size(pt_level)) as Paddr,
                },
                page_size: page_size(pt_level),
                property: frame.prop,
            };
            assert(self.view_rec(path) == set![expected]);
            assert(self.view_rec(path).contains(expected));
            assert(ambient.contains(expected));
            assert(vaddr_of::<C>(path) != vaddr_of::<C>(removed_path));
            assert(self.0.value.path != removed_path);
        }
        assert(g(self.0.value, path));

        if self.0.level < INC_LEVELS - 1 {
            assert forall|i: int|
                0 <= i < self.0.children.len() && (
                #[trigger] self.0.children[i]) is Some implies self.0.children[i].unwrap().tree_predicate_map(
            path.push_tail(i as usize), g) by {
                if self.0.value.is_node() {
                    self.pt_inv_unroll(i);
                    let child = PageTableOwner(self.0.children[i].unwrap());
                    path.push_tail_preserves_inv(i as usize);
                    path.push_tail_property_len(i as usize);
                    // child.view_rec ⊆ self.view_rec(path) ⊆ ambient
                    // path-correctness passes to the child.
                    self.0.map_unroll_once(path, Self::path_correct_pred(), i);
                    child.no_frame_with_path_rec(path.push_tail(i as usize), removed_path, ambient);
                } else {
                    PageTableOwner(self.0).pt_inv_non_node(i);
                }
            };
        }
        assert(self.0.tree_predicate_map(path, g));
    }

    pub proof fn view_rec_disjoint_vaddrs(
        self,
        path: TreePath<NR_ENTRIES>,
        m1: Mapping,
        m2: Mapping,
    )
        requires
            self.pt_inv(),
            path.inv(),
            path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
            self.0.value.parent_level == (INC_LEVELS - self.0.level) as PagingLevel,
            self.view_rec(path).contains(m1),
            self.view_rec(path).contains(m2),
            m1 != m2,
        ensures
            m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start,
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;
        broadcast use group_set_properties;

        if self.0.value.is_frame() {
            assert(self.view_rec(path).is_singleton());
        } else if self.0.value.is_node() {
            let i1 = self.view_rec_contains_choose(path, m1);
            let i2 = self.view_rec_contains_choose(path, m2);

            path.push_tail_preserves_inv(i1 as usize);
            path.push_tail_preserves_inv(i2 as usize);
            path.push_tail_property_len(i1 as usize);
            path.push_tail_property_len(i2 as usize);

            if i1 == i2 {
                self.pt_inv_unroll(i1);
                PageTableOwner(self.0.children[i1].unwrap()).view_rec_disjoint_vaddrs(
                    path.push_tail(i1 as usize),
                    m1,
                    m2,
                );
            } else {
                self.pt_inv_unroll(i1);
                self.pt_inv_unroll(i2);
                let child_ps = page_size((INC_LEVELS - path.len() - 1) as PagingLevel);
                PageTableOwner(self.0.children[i1].unwrap()).view_rec_vaddr_range(
                    path.push_tail(i1 as usize),
                    m1,
                );
                PageTableOwner(self.0.children[i2].unwrap()).view_rec_vaddr_range(
                    path.push_tail(i2 as usize),
                    m2,
                );
                if i1 < i2 {
                    sibling_paths_disjoint::<C>(path, i1 as usize, i2 as usize, child_ps);
                } else {
                    sibling_paths_disjoint::<C>(path, i2 as usize, i1 as usize, child_ps);
                }
                // Bridge `vaddr_of == vaddr + LEADING_BITS * 2^48` for both
                // children, then the int-arithmetic shift cancels across
                // the disjointness inequality.
                lemma_vaddr_of_eq_int::<C>(path.push_tail(i1 as usize));
                lemma_vaddr_of_eq_int::<C>(path.push_tail(i2 as usize));
            }
        }
    }

    /// Every mapping in `view_rec` has `page_size ∈ {4K, 2M, 1G}`.
    ///
    /// Structural induction using the invariant that `parent_level` of each
    /// subtree equals `INC_LEVELS - tree_level`, chained through `rel_children`.
    /// At a leaf frame, `parent_level < NR_LEVELS` (from the tightened
    /// `inv_base`) ensures the page size is one of the allowed values.
    pub proof fn view_rec_mapping_page_size(self, path: TreePath<NR_ENTRIES>)
        requires
            self.pt_inv(),
            path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
            self.0.value.parent_level == (INC_LEVELS - self.0.level) as PagingLevel,
        ensures
            forall|m: Mapping| #[trigger]
                self.view_rec(path).contains(m)
                    ==> set![4096usize, 2097152usize, 1073741824usize].contains(m.page_size),
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;

        if self.0.value.is_frame() {
            lemma_page_size_spec_values();
        } else if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
            assert forall|m: Mapping| #[trigger]
                self.view_rec(path).contains(
                    m,
                ) implies set![4096usize, 2097152usize, 1073741824usize].contains(m.page_size) by {
                let i = choose|i: int|
                    #![trigger self.0.children[i]]
                    0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                        self.0.children[i].unwrap(),
                    ).view_rec(path.push_tail(i as usize)).contains(m);
                self.pt_inv_unroll(i);
                let child = self.0.children[i].unwrap();
                PageTableOwner(child).view_rec_mapping_page_size(path.push_tail(i as usize));
            };
        }
    }

    /// Path-level arithmetic facts consumed by `view_rec_mapping_inv`:
    /// every `vaddr(path)` is aligned to `page_size(INC_LEVELS - path.len())`
    /// and `vaddr(path) + page_size(...)` cannot overflow usize.
    ///
    /// Proved by case analysis on `path.len() ∈ {0, 1, 2, 3, 4}`, unrolling
    /// `rec_vaddr` and using concrete `pow2` values.
    #[verifier::rlimit(400)]
    proof fn lemma_vaddr_path_alignment_and_bound(path: TreePath<NR_ENTRIES>)
        requires
            path.inv(),
            path.len() <= INC_LEVELS - 1,
            1 <= INC_LEVELS - path.len() <= NR_LEVELS,
        ensures
            vaddr(path) % page_size((INC_LEVELS - path.len()) as PagingLevel) == 0,
            vaddr(path) + page_size((INC_LEVELS - path.len()) as PagingLevel) <= usize::MAX,
    {
        lemma_page_size_spec_values();
        vstd::arithmetic::power2::lemma2_to64();
        vstd::arithmetic::power2::lemma2_to64_rest();
        broadcast use TreePath::index_satisfies_elem_inv;
        // NR_LEVELS = 4; each index is < 512.
        // rec_vaddr values per path.len():
        //   0: 0
        //   1: i0 * 2^39
        //   2: i0 * 2^39 + i1 * 2^30
        //   3: i0 * 2^39 + i1 * 2^30 + i2 * 2^21
        //   4: i0 * 2^39 + i1 * 2^30 + i2 * 2^21 + i3 * 2^12
        // page_size(INC_LEVELS - path.len()) per path.len():
        //   1: 2^39, 2: 2^30, 3: 2^21, 4: 2^12
        // In each case every term is a multiple of the smallest (= page_size).

        if path.len() == 0 {
            assert(rec_vaddr(path, 0) == 0);
        } else if path.len() == 1 {
            let i0 = path.index(0);
            assert(rec_vaddr(path, 1) == 0);
            assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + rec_vaddr(
                path,
                1,
            )) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
            assert(rec_vaddr(path, 0) == 0x80_0000_0000usize * i0);
            assert(page_size(4) == 0x80_0000_0000usize);
            assert((0x80_0000_0000usize * i0) % 0x80_0000_0000 == 0) by (nonlinear_arith);
            assert(0x80_0000_0000usize * i0 + 0x80_0000_0000 <= usize::MAX) by (nonlinear_arith)
                requires
                    i0 < 512,
            ;
        } else if path.len() == 2 {
            let i0 = path.index(0);
            let i1 = path.index(1);
            assert(rec_vaddr(path, 2) == 0);
            assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + rec_vaddr(
                path,
                2,
            )) as usize);
            assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + rec_vaddr(
                path,
                1,
            )) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
            assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
            let s = 0x80_0000_0000usize * i0 + 0x4000_0000usize * i1;
            assert(rec_vaddr(path, 0) == s);
            assert(page_size(3) == 0x4000_0000usize);
            assert(s % 0x4000_0000 == 0) by (nonlinear_arith)
                requires
                    s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1,
            ;
            assert(s + 0x4000_0000 <= usize::MAX) by (nonlinear_arith)
                requires
                    s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1,
                    i0 < 512,
                    i1 < 512,
            ;
        } else if path.len() == 3 {
            let i0 = path.index(0);
            let i1 = path.index(1);
            let i2 = path.index(2);
            assert(rec_vaddr(path, 3) == 0);
            assert(rec_vaddr(path, 2) == (vaddr_make::<NR_LEVELS>(2, i2) + rec_vaddr(
                path,
                3,
            )) as usize);
            assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + rec_vaddr(
                path,
                2,
            )) as usize);
            assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + rec_vaddr(
                path,
                1,
            )) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
            assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
            assert(vaddr_make::<NR_LEVELS>(2, i2) == 0x20_0000usize * i2) by (compute);
            let s = 0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2;
            assert(rec_vaddr(path, 0) == s);
            assert(page_size(2) == 0x20_0000usize);
            assert(s % 0x20_0000 == 0) by (nonlinear_arith)
                requires
                    s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1 + 0x20_0000 * i2,
            ;
            assert(s + 0x20_0000 <= usize::MAX) by (nonlinear_arith)
                requires
                    s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1 + 0x20_0000 * i2,
                    i0 < 512,
                    i1 < 512,
                    i2 < 512,
            ;
        } else {
            assert(path.len() == 4);
            let i0 = path.index(0);
            let i1 = path.index(1);
            let i2 = path.index(2);
            let i3 = path.index(3);
            assert(rec_vaddr(path, 4) == 0);
            assert(rec_vaddr(path, 3) == (vaddr_make::<NR_LEVELS>(3, i3) + rec_vaddr(
                path,
                4,
            )) as usize);
            assert(rec_vaddr(path, 2) == (vaddr_make::<NR_LEVELS>(2, i2) + rec_vaddr(
                path,
                3,
            )) as usize);
            assert(rec_vaddr(path, 1) == (vaddr_make::<NR_LEVELS>(1, i1) + rec_vaddr(
                path,
                2,
            )) as usize);
            assert(rec_vaddr(path, 0) == (vaddr_make::<NR_LEVELS>(0, i0) + rec_vaddr(
                path,
                1,
            )) as usize);
            assert(vaddr_make::<NR_LEVELS>(0, i0) == 0x80_0000_0000usize * i0) by (compute);
            assert(vaddr_make::<NR_LEVELS>(1, i1) == 0x4000_0000usize * i1) by (compute);
            assert(vaddr_make::<NR_LEVELS>(2, i2) == 0x20_0000usize * i2) by (compute);
            assert(vaddr_make::<NR_LEVELS>(3, i3) == 0x1000usize * i3) by (compute);
            let s = (0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2
                + 0x1000usize * i3) as int;
            assert(rec_vaddr(path, 0) == s);
            assert(page_size(1) == 0x1000usize);
            assert(s % 0x1000 == 0) by (nonlinear_arith)
                requires
                    s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1 + 0x20_0000 * i2 + 0x1000 * i3,
            ;
            assert(s + 0x1000 <= usize::MAX) by (nonlinear_arith)
                requires
                    s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1 + 0x20_0000 * i2 + 0x1000 * i3,
                    i0 < 512,
                    i1 < 512,
                    i2 < 512,
                    i3 < 512,
            ;
        }
    }

    /// Every mapping in `view_rec` satisfies `Mapping::inv()`.
    ///
    /// Structural induction on the subtree. At a leaf frame, the PA-side
    /// clauses follow from `FrameEntryOwner::inv_base`, the VA-size clause
    /// by construction, the page-size clause from the tightened
    /// `parent_level < NR_LEVELS` constraint plus the arithmetic identity
    /// `page_size(k) ∈ {4K, 2M, 1G}` for `k ∈ {1, 2, 3}`, and VA alignment
    /// + no-overflow via `lemma_vaddr_path_alignment_and_bound`.
    pub proof fn view_rec_mapping_inv(self, path: TreePath<NR_ENTRIES>)
        requires
            self.pt_inv(),
            path.inv(),
            path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
            self.0.value.parent_level == (INC_LEVELS - self.0.level) as PagingLevel,
        ensures
            forall|m: Mapping| #[trigger] self.view_rec(path).contains(m) ==> m.inv(),
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;

        if self.0.value.is_frame() {
            lemma_page_size_spec_values();
            let frame = self.0.value.frame();
            let pt_level = (INC_LEVELS - path.len()) as PagingLevel;
            Self::lemma_vaddr_path_alignment_and_bound(path);
            let m = Mapping {
                va_range: Range {
                    start: vaddr_of::<C>(path) as int,
                    end: vaddr_of::<C>(path) + page_size(pt_level),
                },
                pa_range: Range {
                    start: frame.mapped_pa,
                    end: (frame.mapped_pa + page_size(pt_level)) as Paddr,
                },
                page_size: page_size(pt_level),
                property: frame.prop,
            };
            assert(self.view_rec(path) == set![m]);
            assert(set![4096usize, 2097152usize, 1073741824usize].contains(m.page_size));
            let ps = page_size(pt_level) as int;
            assert((frame.mapped_pa + ps) % ps == 0) by (nonlinear_arith)
                requires
                    (frame.mapped_pa as int) % ps == 0,
                    ps > 0,
            ;
            // Bridge `vaddr_of(path) == vaddr(path) + LB * 2^48`.
            lemma_vaddr_of_eq_int::<C>(path);
            C::lemma_page_table_config_constant_properties();
            lemma_vaddr_strict_bound(path);
            let lb = C::LEADING_BITS_spec() as int;
            vstd::arithmetic::power2::lemma2_to64();
            vstd::arithmetic::power2::lemma2_to64_rest();
            // (A) Alignment. For `ps ∈ {2^12, 2^21, 2^30}`, `ps | 2^48`, so
            //     `lb * 2^48 % ps == 0` and `vaddr(path) % ps == 0` gives
            //     `vaddr_of(path) % ps == 0` via `lemma_mod_adds`.
            assert(vaddr(path) as int % ps == 0);
            assert(lb * 0x1_0000_0000_0000int % ps == 0) by (nonlinear_arith)
                requires
                    lb >= 0,
                    (ps == 0x1000int || ps == 0x20_0000int || ps == 0x4000_0000int),
            ;
            vstd::arithmetic::div_mod::lemma_mod_adds(
                vaddr(path) as int,
                lb * 0x1_0000_0000_0000int,
                ps,
            );
            assert((vaddr_of::<C>(path) as int) % ps == 0);
            assert((vaddr_of::<C>(path) + ps) % ps == 0) by (nonlinear_arith)
                requires
                    (vaddr_of::<C>(path) as int) % ps == 0,
                    ps > 0,
            ;
            // (B) Overflow: `vaddr_of(path) + ps <= 2^64`.
            //     `vaddr(path) + ps <= 2^48`: from strict bound plus alignment.
            let v = vaddr(path) as int;
            assert((v % ps) == 0);
            assert(v + ps <= 0x1_0000_0000_0000int) by (nonlinear_arith)
                requires
                    v % ps == 0,
                    v < 0x1_0000_0000_0000int,
                    (ps == 0x1000int || ps == 0x20_0000int || ps == 0x4000_0000int),
                    (0x1_0000_0000_0000int % ps == 0),
            ;
            assert(vaddr_of::<C>(path) + ps <= pow2(64)) by (nonlinear_arith)
                requires
                    vaddr_of::<C>(path) == v + lb * 0x1_0000_0000_0000int,
                    v + ps <= 0x1_0000_0000_0000int,
                    lb < 0x1_0000int,
                    lb >= 0,
                    pow2(64) == 0x1_0000_0000_0000_0000int,
            ;
            assert(m.inv());
        } else if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
            assert forall|m: Mapping| #[trigger]
                self.view_rec(path).contains(m) implies m.inv() by {
                let i = choose|i: int|
                    #![trigger self.0.children[i]]
                    0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                        self.0.children[i].unwrap(),
                    ).view_rec(path.push_tail(i as usize)).contains(m);
                self.pt_inv_unroll(i);
                let child = self.0.children[i].unwrap();
                path.push_tail_preserves_inv(i as usize);
                PageTableOwner(child).view_rec_mapping_inv(path.push_tail(i as usize));
            };
        }
    }

    /// An absent entry contributes no mappings - view_rec returns the empty set.
    pub proof fn view_rec_absent_empty(self, path: TreePath<NR_ENTRIES>)
        requires
            self.0.inv(),
            self.0.value.is_absent(),
            path.len() <= INC_LEVELS - 1,
        ensures
            self.view_rec(path) == set![],
    {
    }

    /// A node with `nr_children == 0` has no present PTEs, so all children are
    /// absent and the subtree contributes no mappings.
    ///
    /// `count_consistent` ties `nr_children` to `count_present(children_perm)`,
    /// so `nr_children == 0` forces every PTE absent. `pt_edge_at` (from
    /// `pt_inv`) then forces each ghost child `is_absent` — its `view_rec` is
    /// `∅` — and `lemma_view_rec_contains` lifts that to the whole node's
    /// `view_rec`. (At the top level the `borrowed` edge disjunct is ruled out:
    /// `borrowed_match_pte` needs a *present* PTE, which `count_present == 0`
    /// denies.)
    pub proof fn view_rec_nr_children_zero_empty(self, path: TreePath<NR_ENTRIES>)
        requires
            self.pt_inv(),
            self.0.value.is_node(),
            self.0.value.node().meta_own.nr_children.value() == 0,
            self.0.value.node().count_consistent(),
            path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
        ensures
            self.view_rec(path) == set![],
    {
        if path.len() < INC_LEVELS - 1 {
            let cp = self.0.value.node().children_perm.value();
            // `count_consistent` + `nr_children == 0` ⟹ no present PTEs.
            assert(crate::specs::mm::page_table::node::owners::count_present(cp) == 0);
            self.lemma_view_rec_contains(path);
            assert forall|m: Mapping| self.view_rec(path).contains(m) implies false by {
                let i = choose|i: int|
                    #![trigger self.0.children[i]]
                    0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                        self.0.children[i]->0,
                    ).view_rec(path.push_tail(i as usize)).contains(m);
                self.pt_inv_unroll(i);
                // PTE `i` is absent — else `count_present(cp) >= 1`.
                if cp[i].is_present() {
                    crate::specs::mm::page_table::node::owners::lemma_count_present_upto_present(
                        cp,
                        cp.len() as int,
                        i,
                    );
                }
                assert(!cp[i].is_present());
                // `pt_edge_at`'s borrowed disjunct needs a present PTE, so it is
                // false here; the `match_pte` disjunct holds, and `match_pte`
                // with an absent PTE forces the child `is_absent`.
                assert(self.0.children[i]->0.value.is_absent());
                // An absent entry is neither frame nor node ⟹ empty `view_rec`.
                assert(PageTableOwner(self.0.children[i]->0).view_rec(path.push_tail(i as usize))
                    =~= set![]);
            };
            assert(self.view_rec(path) =~= set![]);
        }
    }

    pub open spec fn metaregion_sound_pred(regions: MetaRegionOwners) -> (spec_fn(
        EntryOwner<C>,
        TreePath<NR_ENTRIES>,
    ) -> bool) {
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions)
    }

    pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool
        decreases INC_LEVELS - self.0.level,
        when self.0.inv()
    {
        self.0.tree_predicate_map(self.0.value.path, Self::metaregion_sound_pred(regions))
    }

    /// `PageTableOwner::metaregion_sound` is preserved across regions changes
    /// that (a) keep `slot_owners` exactly equal and (b) only grow the `slots`
    /// map (existing keys preserved with the same values). Both conditions are
    /// satisfied by `Entry::to_ref` and similar `borrow_paddr` operations.
    pub proof fn metaregion_sound_preserved_slot_owners_eq(
        self,
        r0: MetaRegionOwners,
        r1: MetaRegionOwners,
    )
        requires
            self.inv(),
            self.metaregion_sound(r0),
            r0.slot_owners == r1.slot_owners,
            forall|k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
            forall|k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
        ensures
            self.metaregion_sound(r1),
    {
        Self::metaregion_sound_preserved_slot_owners_eq_subtree(self.0, self.0.value.path, r0, r1);
    }

    /// Recursive helper: same preservation property, applied to an arbitrary subtree.
    pub proof fn metaregion_sound_preserved_slot_owners_eq_subtree(
        subtree: OwnerSubtree<C>,
        path: TreePath<NR_ENTRIES>,
        r0: MetaRegionOwners,
        r1: MetaRegionOwners,
    )
        requires
            subtree.inv(),
            subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r0)),
            r0.slot_owners == r1.slot_owners,
            forall|k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
            forall|k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
        ensures
            subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r1)),
        decreases INC_LEVELS - subtree.level,
    {
        // The root entry: its metaregion_sound transfers via the per-entry lemma.
        subtree.value.metaregion_sound_slot_owners_only(r0, r1);
        // Recursively for each Some child.
        if subtree.level < INC_LEVELS - 1 {
            assert forall|i: int|
                #![trigger subtree.children[i]]
                0 <= i < NR_ENTRIES
                    && subtree.children[i] is Some implies subtree.children[i].unwrap().tree_predicate_map(
            path.push_tail(i as usize), Self::metaregion_sound_pred(r1)) by {
                Self::metaregion_sound_preserved_slot_owners_eq_subtree(
                    subtree.children[i].unwrap(),
                    path.push_tail(i as usize),
                    r0,
                    r1,
                );
            }
        }
    }

    /// `PageTableOwner::metaregion_sound` is preserved across a single
    /// `slot_owner` change at index `changed_idx`, provided no entry in the
    /// tree references `changed_idx` (neither as its primary slot nor as a
    /// huge-frame sub-page slot). This is the right shape for `borrow`-style
    /// operations that bump `raw_count` at one slot.
    pub proof fn metaregion_sound_preserved_one_slot_changed(
        self,
        r0: MetaRegionOwners,
        r1: MetaRegionOwners,
        changed_idx: usize,
    )
        requires
            self.inv(),
            self.metaregion_sound(r0),
            forall|i: usize|
                #![trigger r1.slot_owners[i]]
                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
            r0.slot_owners.dom() == r1.slot_owners.dom(),
            forall|k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
            forall|k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
            // No tree entry's primary slot is at changed_idx.
            self.0.tree_predicate_map(
                self.0.value.path,
                |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>|
                    e.meta_slot_paddr() is Some ==> frame_to_index(e.meta_slot_paddr()->0)
                        != changed_idx,
            ),
            // For huge-frame entries, none of their sub-page slots is at changed_idx
            // either; provided as a separate condition because the per-entry lemma
            // requires it.
            self.0.tree_predicate_map(
                self.0.value.path,
                |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>|
                    e.is_frame() && e.parent_level > 1 ==> {
                        let pa = e.frame().mapped_pa;
                        let nr_pages = page_size(e.parent_level) / PAGE_SIZE;
                        forall|j: usize|
                            0 < j < nr_pages ==> {
                                let sub_idx = #[trigger] frame_to_index(
                                    (pa + j * PAGE_SIZE) as usize,
                                );
                                sub_idx != changed_idx || (r1.slots.contains_key(sub_idx)
                                    && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                    != REF_COUNT_UNUSED
                                    && r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
                                    && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                    <= REF_COUNT_MAX)
                            }
                    },
            ),
        ensures
            self.metaregion_sound(r1),
    {
        Self::metaregion_sound_preserved_one_slot_changed_subtree(
            self.0,
            self.0.value.path,
            r0,
            r1,
            changed_idx,
        );
    }

    pub proof fn metaregion_sound_preserved_one_slot_changed_subtree(
        subtree: OwnerSubtree<C>,
        path: TreePath<NR_ENTRIES>,
        r0: MetaRegionOwners,
        r1: MetaRegionOwners,
        changed_idx: usize,
    )
        requires
            subtree.inv(),
            subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r0)),
            forall|i: usize|
                #![trigger r1.slot_owners[i]]
                i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
            r0.slot_owners.dom() == r1.slot_owners.dom(),
            forall|k: usize| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),
            forall|k: usize| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],
            subtree.tree_predicate_map(
                path,
                |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>|
                    e.meta_slot_paddr() is Some ==> frame_to_index(e.meta_slot_paddr()->0)
                        != changed_idx,
            ),
            subtree.tree_predicate_map(
                path,
                |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>|
                    e.is_frame() && e.parent_level > 1 ==> {
                        let pa = e.frame().mapped_pa;
                        let nr_pages = page_size(e.parent_level) / PAGE_SIZE;
                        forall|j: usize|
                            0 < j < nr_pages ==> {
                                let sub_idx = #[trigger] frame_to_index(
                                    (pa + j * PAGE_SIZE) as usize,
                                );
                                sub_idx != changed_idx || (r1.slots.contains_key(sub_idx)
                                    && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                    != REF_COUNT_UNUSED
                                    && r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
                                    && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                    <= REF_COUNT_MAX)
                            }
                    },
            ),
        ensures
            subtree.tree_predicate_map(path, Self::metaregion_sound_pred(r1)),
        decreases INC_LEVELS - subtree.level,
    {
        subtree.value.metaregion_sound_one_slot_changed(r0, r1, changed_idx);
        if subtree.level < INC_LEVELS - 1 {
            assert forall|i: int|
                #![trigger subtree.children[i]]
                0 <= i < NR_ENTRIES
                    && subtree.children[i] is Some implies subtree.children[i].unwrap().tree_predicate_map(
            path.push_tail(i as usize), Self::metaregion_sound_pred(r1)) by {
                Self::metaregion_sound_preserved_one_slot_changed_subtree(
                    subtree.children[i].unwrap(),
                    path.push_tail(i as usize),
                    r0,
                    r1,
                    changed_idx,
                );
            }
        }
    }

    /// Predicate: all entries in the tree have their paths correctly tracked in regions.
    /// Strengthened form: `paths_in_pt == set![entry.path]` (not just non-empty).
    pub open spec fn path_tracked_pred(regions: MetaRegionOwners) -> spec_fn(
        EntryOwner<C>,
        TreePath<NR_ENTRIES>,
    ) -> bool {
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
            {
                // Only nodes track paths_in_pt as a singleton (frames can be shared).
                entry.is_node() && entry.meta_slot_paddr() is Some ==> {
                    &&& regions.slot_owners.contains_key(frame_to_index(entry.meta_slot_paddr()->0))
                    &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr()->0)].paths_in_pt
                        == set![entry.path]
                }
            }
    }

    pub open spec fn relate_region_tracked_pred(regions: MetaRegionOwners) -> spec_fn(
        EntryOwner<C>,
        TreePath<NR_ENTRIES>,
    ) -> bool {
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
            {
                &&& entry.meta_slot_paddr() is Some
                &&& regions.slot_owners.contains_key(frame_to_index(entry.meta_slot_paddr()->0))
                &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr()->0)].paths_in_pt
                    == set![path]
            }
    }

    pub open spec fn path_correct_pred() -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool {
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| { entry.path == path }
    }

    pub open spec fn not_in_scope_pred() -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool {
        |entry: EntryOwner<C>, _path: TreePath<NR_ENTRIES>| true
    }

    /// `tree_predicate_map` for the trivial `not_in_scope_pred`.
    pub proof fn tree_not_in_scope(subtree: OwnerSubtree<C>, path: TreePath<NR_ENTRIES>)
        requires
            subtree.inv(),
        ensures
            subtree.tree_predicate_map(path, Self::not_in_scope_pred()),
        decreases INC_LEVELS - subtree.level,
    {
        // `not_in_scope_pred` is trivially `true`; recurse to discharge it.
        if subtree.level < INC_LEVELS - 1 {
            assert forall|i: int|
                0 <= i < subtree.children.len() && (
                #[trigger] subtree.children[i]) is Some implies subtree.children[i].unwrap().tree_predicate_map(
            path.push_tail(i as usize), Self::not_in_scope_pred()) by {
                Self::tree_not_in_scope(subtree.children[i].unwrap(), path.push_tail(i as usize));
            };
        }
    }

    /// All mappings in a subtree's `view_rec` have
    /// `page_size <= page_size(INC_LEVELS - path.len())`.
    pub proof fn view_rec_page_size_bound(self, path: TreePath<NR_ENTRIES>, m: Mapping)
        requires
            self.0.inv(),
            path.len() <= INC_LEVELS - 1,
            self.view_rec(path).contains(m),
        ensures
            m.page_size <= page_size((INC_LEVELS - path.len()) as PagingLevel),
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;

        if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
            let i = choose|i: int|
                #![trigger self.0.children[i]]
                0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                    self.0.children[i].unwrap(),
                ).view_rec(path.push_tail(i as usize)).contains(m);
            PageTableOwner(self.0.children[i].unwrap()).view_rec_page_size_bound(
                path.push_tail(i as usize),
                m,
            );
            page_size_monotonic(
                (INC_LEVELS - path.len() - 1) as PagingLevel,
                (INC_LEVELS - path.len()) as PagingLevel,
            );
        }
    }

    /// For a node subtree, all mappings have
    /// `page_size <= page_size(INC_LEVELS - path.len() - 1)`.
    pub proof fn view_rec_node_page_size_bound(self, path: TreePath<NR_ENTRIES>, m: Mapping)
        requires
            self.0.inv(),
            self.0.value.is_node(),
            path.len() < INC_LEVELS - 1,
            self.view_rec(path).contains(m),
        ensures
            m.page_size <= page_size(((INC_LEVELS - path.len()) - 1) as PagingLevel),
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;

        let i = choose|i: int|
            #![trigger self.0.children[i]]
            0 <= i < self.0.children.len() && self.0.children[i] is Some && PageTableOwner(
                self.0.children[i].unwrap(),
            ).view_rec(path.push_tail(i as usize)).contains(m);
        PageTableOwner(self.0.children[i].unwrap()).view_rec_page_size_bound(
            path.push_tail(i as usize),
            m,
        );
    }

    /// Spec function: path1 is a prefix of path2
    pub open spec fn is_prefix_of<const N: usize>(prefix: TreePath<N>, path: TreePath<N>) -> bool {
        &&& prefix.len() <= path.len()
        &&& forall|i: int| 0 <= i < prefix.len() ==> prefix.index(i) == path.index(i)
    }

    /// Transitivity of is_prefix_of
    pub proof fn prefix_transitive<const N: usize>(
        p1: TreePath<N>,
        p2: TreePath<N>,
        p3: TreePath<N>,
    )
        requires
            Self::is_prefix_of(p1, p2),
            Self::is_prefix_of(p2, p3),
        ensures
            Self::is_prefix_of(p1, p3),
    {
        assert(p1.len() <= p3.len());
        assert forall|i: int| 0 <= i < p1.len() implies p1.index(i) == p3.index(i) by {
            assert(p1.index(i) == p2.index(i));
            assert(p2.index(i) == p3.index(i));
        };
    }

    pub proof fn prefix_push_different_indices(
        prefix: TreePath<NR_ENTRIES>,
        path: TreePath<NR_ENTRIES>,
        i: usize,
        j: usize,
    )
        requires
            prefix.inv(),
            path.inv(),
            i != j,
            Self::is_prefix_of(prefix.push_tail(i), path),
        ensures
            !Self::is_prefix_of(prefix.push_tail(j), path),
    {
        assert(path.index(prefix.len() as int) == i);
    }

    pub proof fn prefix_push_tail_implies_prefix<const N: usize>(
        prefix: TreePath<N>,
        path: TreePath<N>,
        i: usize,
    )
        requires
            prefix.inv(),
            path.inv(),
            0 <= i < N,
            Self::is_prefix_of(prefix.push_tail(i), path),
        ensures
            Self::is_prefix_of(prefix, path),
    {
        prefix.push_tail_property(i);
        assert(prefix.len() <= path.len());
        assert forall|j: int| 0 <= j < prefix.len() implies prefix.index(j) == path.index(j) by {
            assert(prefix.push_tail(i).index(j) == prefix.index(j));
            assert(prefix.push_tail(i).index(j) == path.index(j));
        };
    }

    pub open spec fn is_at_pred(entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>) -> spec_fn(
        EntryOwner<C>,
        TreePath<NR_ENTRIES>,
    ) -> bool {
        |entry0: EntryOwner<C>, path0: TreePath<NR_ENTRIES>| { path0 == path ==> entry0 == entry }
    }

    pub open spec fn path_in_tree_pred(path: TreePath<NR_ENTRIES>) -> spec_fn(
        EntryOwner<C>,
        TreePath<NR_ENTRIES>,
    ) -> bool {
        |entry: EntryOwner<C>, path0: TreePath<NR_ENTRIES>|
            Self::is_prefix_of(path0, path) ==> !entry.is_node() ==> path == path0
    }

    pub proof fn is_at_pred_eq(
        path: TreePath<NR_ENTRIES>,
        entry1: EntryOwner<C>,
        entry2: EntryOwner<C>,
    )
        requires
            entry1.inv(),
            OwnerSubtree::implies(Self::is_at_pred(entry1, path), Self::is_at_pred(entry2, path)),
        ensures
            entry1 == entry2,
    {
        assert(Self::is_at_pred(entry1, path)(entry1, path) ==> Self::is_at_pred(entry2, path)(
            entry1,
            path,
        ));
    }

    pub proof fn is_at_holds_when_on_wrong_path(
        subtree: OwnerSubtree<C>,
        root_path: TreePath<NR_ENTRIES>,
        dest_path: TreePath<NR_ENTRIES>,
        entry: EntryOwner<C>,
    )
        requires
            subtree.inv(),
            PageTableOwner(subtree).pt_inv(),
            dest_path.inv(),
            !Self::is_prefix_of(root_path, dest_path),
            root_path.len() <= INC_LEVELS - 1,
            root_path.len() == subtree.level,
        ensures
            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry, dest_path)),
        decreases INC_LEVELS - root_path.len(),
    {
        if subtree.level < INC_LEVELS - 1 {
            if subtree.value.is_node() {
                assert forall|i: int| 0 <= i < NR_ENTRIES implies (
                #[trigger] subtree.children[i as int]).unwrap().tree_predicate_map(
                    root_path.push_tail(i as usize),
                    Self::is_at_pred(entry, dest_path),
                ) by {
                    PageTableOwner(subtree).pt_inv_unroll(i);
                    Self::is_at_holds_when_on_wrong_path(
                        subtree.children[i as int].unwrap(),
                        root_path.push_tail(i as usize),
                        dest_path,
                        entry,
                    );
                };
            } else {
                assert forall|i: int| 0 <= i < NR_ENTRIES implies (
                #[trigger] subtree.children[i as int]) is None by {
                    PageTableOwner(subtree).pt_inv_non_node(i);
                };
            }
        }
    }

    /// Counterintuitive: the predicate is vacuously true when the path is not a prefix of the target path,
    /// because it is actually a liveness property: if we keep following the path, we will eventually reach it.
    /// This covers when we are not following it.
    pub proof fn path_in_tree_holds_when_on_wrong_path(
        subtree: OwnerSubtree<C>,
        root_path: TreePath<NR_ENTRIES>,
        dest_path: TreePath<NR_ENTRIES>,
    )
        requires
            subtree.inv(),
            PageTableOwner(subtree).pt_inv(),
            dest_path.inv(),
            !Self::is_prefix_of(root_path, dest_path),
            root_path.len() <= INC_LEVELS - 1,
            root_path.len() == subtree.level,
        ensures
            subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),
        decreases INC_LEVELS - root_path.len(),
    {
        if subtree.level < INC_LEVELS - 1 {
            if subtree.value.is_node() {
                assert forall|i: int| 0 <= i < NR_ENTRIES implies (
                #[trigger] subtree.children[i as int]).unwrap().tree_predicate_map(
                    root_path.push_tail(i as usize),
                    Self::path_in_tree_pred(dest_path),
                ) by {
                    PageTableOwner(subtree).pt_inv_unroll(i);
                    Self::path_in_tree_holds_when_on_wrong_path(
                        subtree.children[i as int].unwrap(),
                        root_path.push_tail(i as usize),
                        dest_path,
                    );
                };
            } else {
                assert forall|i: int| 0 <= i < NR_ENTRIES implies (
                #[trigger] subtree.children[i as int]) is None by {
                    PageTableOwner(subtree).pt_inv_non_node(i);
                };
            }
        }
    }

    /// Entries in a subtree whose structural path is disjoint from `old_entry.path`
    /// have different physical addresses from `old_entry`.
    pub proof fn neq_old_from_path_disjoint(
        subtree: OwnerSubtree<C>,
        path_j: TreePath<NR_ENTRIES>,
        old_entry: EntryOwner<C>,
        regions: MetaRegionOwners,
    )
        requires
            subtree.inv(),
            subtree.value.path == path_j,
            path_j.len() == subtree.level,
            path_j.inv(),
            path_j.len() <= INC_LEVELS - 1,
            subtree.tree_predicate_map(path_j, Self::metaregion_sound_pred(regions)),
            subtree.tree_predicate_map(path_j, Self::path_correct_pred()),
            old_entry.is_node(),
            old_entry.meta_slot_paddr() is Some,
            regions.slot_owners[frame_to_index(old_entry.meta_slot_paddr()->0)].paths_in_pt
                == set![old_entry.path],
            !Self::is_prefix_of(path_j, old_entry.path),
        ensures
            subtree.tree_predicate_map(
                path_j,
                |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| e.meta_slot_paddr_neq(old_entry),
            ),
        decreases INC_LEVELS - subtree.level,
    {
        let f_sound = Self::metaregion_sound_pred(regions);
        let f_path = Self::path_correct_pred();
        let g = |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| e.meta_slot_paddr_neq(old_entry);

        assert(g(subtree.value, path_j)) by {
            assert(f_sound(subtree.value, path_j));
            assert(f_path(subtree.value, path_j));
            assert(subtree.value.path == path_j);
            if subtree.value.meta_slot_paddr() is Some {
                let old_paddr = old_entry.meta_slot_paddr()->0;
                let entry_paddr = subtree.value.meta_slot_paddr()->0;
                if entry_paddr == old_paddr {
                    let idx = frame_to_index(entry_paddr);
                    let old_idx = frame_to_index(old_paddr);
                    assert(idx == old_idx);
                    if subtree.value.is_node() {
                        assert(regions.slot_owners[idx].paths_in_pt == set![subtree.value.path]);
                    } else if subtree.value.is_frame() {
                        assert(regions.slot_owners[idx].paths_in_pt.contains(subtree.value.path));
                    }
                    assert(regions.slot_owners[idx].paths_in_pt == set![old_entry.path]);
                    assert(set![old_entry.path].contains(subtree.value.path));
                    assert(subtree.value.path == old_entry.path);
                    assert(Self::is_prefix_of(path_j, old_entry.path));
                }
            }
        };

        if subtree.level < INC_LEVELS - 1 {
            assert forall|i: int|
                0 <= i < subtree.children.len() && (
                #[trigger] subtree.children[i]) is Some implies subtree.children[i].unwrap().tree_predicate_map(
            path_j.push_tail(i as usize), g) by {
                let child = subtree.children[i].unwrap();
                let child_path = path_j.push_tail(i as usize);
                subtree.map_unroll_once(path_j, f_sound, i);
                subtree.map_unroll_once(path_j, f_path, i);
                path_j.push_tail_property(i as usize);
                assert(child_path.inv());
                assert(child_path.len() == child.level);
                assert(child.value.path == child_path);
                assert(!Self::is_prefix_of(child_path, old_entry.path)) by {
                    if Self::is_prefix_of(child_path, old_entry.path) {
                        Self::prefix_push_tail_implies_prefix(path_j, old_entry.path, i as usize);
                    }
                };
                Self::neq_old_from_path_disjoint(child, child_path, old_entry, regions);
            };
        }
    }

    pub proof fn is_at_eq_rec(
        subtree: OwnerSubtree<C>,
        root_path: TreePath<NR_ENTRIES>,
        dest_path: TreePath<NR_ENTRIES>,
        entry1: EntryOwner<C>,
        entry2: EntryOwner<C>,
    )
        requires
            subtree.inv(),
            PageTableOwner(subtree).pt_inv(),
            dest_path.inv(),
            root_path.inv(),
            Self::is_prefix_of(root_path, dest_path),
            root_path.len() <= INC_LEVELS - 1,
            root_path.len() == subtree.level,
            subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),
            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry1, dest_path)),
            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry2, dest_path)),
        ensures
            entry1 == entry2,
        decreases INC_LEVELS - root_path.len(),
    {
        if root_path == dest_path {
            assert(subtree.value == entry1);
            assert(subtree.value == entry2);
        } else if subtree.level == INC_LEVELS - 1 || !subtree.value.is_node() {
            proof_from_false()
        } else {
            assert(root_path.len() <= dest_path.len());
            if root_path.len() == dest_path.len() {
                assert(root_path.0.len() == dest_path.0.len());
                assert forall|i: int| 0 <= i < root_path.0.len() implies #[trigger] root_path.0[i]
                    == dest_path.0[i] by {
                    assert(root_path.index(i) == dest_path.index(i));
                };
                assert(root_path == dest_path);
                assert(false);
            }
            assert(root_path.len() < dest_path.len());
            let i = dest_path.index(root_path.len() as int);
            PageTableOwner(subtree).pt_inv_unroll(i as int);
            assert(Self::is_prefix_of(root_path.push_tail(i), dest_path));
            Self::is_at_eq_rec(
                subtree.children[i as int].unwrap(),
                root_path.push_tail(i as usize),
                dest_path,
                entry1,
                entry2,
            );
        }
    }

    pub proof fn view_rec_inversion(
        self,
        path: TreePath<NR_ENTRIES>,
        regions: MetaRegionOwners,
        m: Mapping,
    ) -> (entry: EntryOwner<C>)
        requires
            self.pt_inv(),
            path.len() == self.0.level,
            self.view_rec(path).contains(m),
            self.0.tree_predicate_map(path, Self::path_correct_pred()),
            self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
        ensures
            Self::is_prefix_of(path, entry.path),
            regions.slot_owners[frame_to_index(m.pa_range.start)].paths_in_pt == set![entry.path],
            m.va_range.start == vaddr_of::<C>(entry.path),
            m.page_size == page_size((INC_LEVELS - entry.path.len()) as PagingLevel),
            entry.is_frame(),
            m.property == entry.frame().prop,
            self.0.tree_predicate_map(path, Self::is_at_pred(entry, entry.path)),
            self.0.tree_predicate_map(path, Self::path_in_tree_pred(entry.path)),
            entry.inv(),
        decreases INC_LEVELS - path.len(),
    {
        broadcast use PageTableOwner::group_lemmas;

        if self.0.value.is_frame() {
            assert(Self::is_prefix_of(path, self.0.value.path));
            if self.0.level < INC_LEVELS - 1 {
                // Non-leaf frame: pt_inv gives children[i] is None,
                // so tree_predicate_map has no children to recurse into.
                assert forall|i: int| 0 <= i < NR_ENTRIES implies (
                #[trigger] self.0.children[i]) is None by {
                    self.pt_inv_non_node(i);
                };
            }
            assert(self.0.tree_predicate_map(
                path,
                Self::is_at_pred(self.0.value, self.0.value.path),
            ));
            assert(self.0.tree_predicate_map(path, Self::path_in_tree_pred(self.0.value.path)));
            self.0.value
        } else if self.0.value.is_node() {
            let i = self.view_rec_contains_choose(path, m);
            self.pt_inv_unroll(i);
            let entry = PageTableOwner(self.0.children[i].unwrap()).view_rec_inversion(
                path.push_tail(i as usize),
                regions,
                m,
            );
            Self::prefix_transitive(path, path.push_tail(i as usize), entry.path);
            assert forall|j: int|
                0 <= j < NR_ENTRIES
                    && #[trigger] self.0.children[j] is Some implies self.0.children[j].unwrap().tree_predicate_map(
            path.push_tail(j as usize), Self::is_at_pred(entry, entry.path)) by {
                if j != i {
                    self.pt_inv_unroll(j);
                    Self::prefix_push_different_indices(path, entry.path, i as usize, j as usize);
                    assert(!Self::is_prefix_of(path.push_tail(j as usize), entry.path));
                    Self::is_at_holds_when_on_wrong_path(
                        self.0.children[j].unwrap(),
                        path.push_tail(j as usize),
                        entry.path,
                        entry,
                    );
                }
            };
            assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry, entry.path)));

            assert forall|j: int|
                0 <= j < NR_ENTRIES
                    && #[trigger] self.0.children[j] is Some implies self.0.children[j].unwrap().tree_predicate_map(
            path.push_tail(j as usize), Self::path_in_tree_pred(entry.path)) by {
                if j != i {
                    self.pt_inv_unroll(j);
                    Self::prefix_push_different_indices(path, entry.path, i as usize, j as usize);
                    assert(!Self::is_prefix_of(path.push_tail(j as usize), entry.path));
                    Self::path_in_tree_holds_when_on_wrong_path(
                        self.0.children[j].unwrap(),
                        path.push_tail(j as usize),
                        entry.path,
                    );
                }
            };
            assert(self.0.tree_predicate_map(path, Self::path_in_tree_pred(entry.path)));
            entry
        } else {
            proof_from_false()
        }
    }

    pub proof fn view_rec_inversion_unique(
        self,
        path: TreePath<NR_ENTRIES>,
        regions: MetaRegionOwners,
        m1: Mapping,
        m2: Mapping,
    )
        requires
            self.pt_inv(),
            path.len() <= INC_LEVELS - 1,
            path.len() == self.0.level,
            self.view_rec(path).contains(m1),
            self.view_rec(path).contains(m2),
            m1.pa_range.start == m2.pa_range.start,
            m1.inv(),
            m2.inv(),
            self.0.tree_predicate_map(path, Self::path_tracked_pred(regions)),
            self.0.tree_predicate_map(path, Self::path_correct_pred()),
            self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
        ensures
            m1 == m2,
    {
        let entry1 = self.view_rec_inversion(path, regions, m1);
        let entry2 = self.view_rec_inversion(path, regions, m2);

        assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry1, entry1.path)));
        assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry2, entry2.path)));

        // Same paddr ⇒ same slot ⇒ same singleton paths_in_pt ⇒ same entry path.
        let idx = frame_to_index(m1.pa_range.start);
        assert(regions.slot_owners[idx].paths_in_pt == set![entry1.path]);
        assert(regions.slot_owners[idx].paths_in_pt == set![entry2.path]);
        assert(set![entry1.path].contains(entry2.path));
        assert(entry1.path == entry2.path);

        Self::is_at_eq_rec(self.0, path, entry1.path, entry1, entry2);
    }

    pub broadcast group group_lemmas {
        PageTableOwner::lemma_view_rec_contains,
        PageTableOwner::lemma_view_rec_contains_intro,
    }
}

impl<C: PageTableConfig> Inv for PageTableOwner<C> {
    open spec fn inv(self) -> bool {
        &&& self.0.inv()
        &&& self.pt_inv_at_depth((INC_LEVELS - self.0.level) as nat)
        &&& self.0.value.is_node()
        &&& self.0.value.path.len() <= INC_LEVELS - 1
        &&& self.0.value.path.inv()
        &&& self.0.value.path.len() == self.0.level
        &&& self.0.value.parent_level == (INC_LEVELS - self.0.level) as PagingLevel
        &&& self.0.value.node().tree_level == self.0.value.path.len()
        &&& self.0.tree_predicate_map(self.0.value.path, Self::path_correct_pred())
    }
}

impl<C: PageTableConfig> View for PageTableOwner<C> {
    type V = PageTableView;

    open spec fn view(&self) -> <Self as View>::V {
        let mappings = self.view_rec(self.0.value.path);
        PageTableView { mappings }
    }
}

} // verus!