Function vaddr_of 

pub open spec fn vaddr_of<C: PageTableConfig>(path: TreePath<NR_ENTRIES>) -> usize

{ (vaddr(path) + page_table_coverage_start_spec::<C>()) as usize }

Reconstructs a path address with the configuration’s derived upper-address contribution.