Function vaddr_at 

pub open spec fn vaddr_at(path: TreePath<NR_ENTRIES>, leading_bits: int) -> usize

{ (vaddr(path) + leading_bits * 0x1_0000_0000_0000int) as usize }

Virtual address of path with leading_bits placed in bits [48, 64).

Adds the upper-address contribution to the positional path address. 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.