Function vaddr_upper_bits_spec 

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

{ va >> page_table_vaddr_bits_spec::<C>() }

Bits of va above the complete configured page-table coverage.