Function lemma_vaddr_path_aligned 

pub proof fn lemma_vaddr_path_aligned<C: PageTableConfig>(
    path: TreePath<NR_ENTRIES>,
    va: Vaddr,
)

requires

path.inv(),

path.len() <= C::NR_LEVELS(),

forall |k: int| {
    0 <= k < path.len()
        ==> #[trigger] path[k]
            == pte_index_spec::<C>(va, (C::NR_LEVELS() - k) as PagingLevel)
},

ensures

vaddr(path) + vaddr_upper_part_spec::<C>(va)
    == nat_align_down(
        va as nat,
        page_size::<C>((C::NR_LEVELS() - path.len() + 1) as PagingLevel) as nat,
    ),

A path of concrete PTE indices identifies the aligned slot containing the address.