Function vaddr_leading_part_spec 

pub open spec fn vaddr_leading_part_spec<C: PagingConstsTrait>(va: Vaddr) -> Vaddr

{
    ((va >> nr_page_table_coverage_bits_spec::<C>())
        * pow2(nr_page_table_coverage_bits_spec::<C>() as nat)) as Vaddr
}

Contribution of the uninterpreted upper virtual-address bits to the concrete address.