Function leading_bits_spec 

pub open spec fn leading_bits_spec<C: PageTableConfig>() -> usize

{
    let bits = nr_page_table_coverage_bits_spec::<C>();
    let start = C::TOP_LEVEL_INDEX_RANGE().start
        * pow2(pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat);
    if C::VA_SIGN_EXT()
        && (start / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1
    {
        (pow2((usize::BITS - bits) as nat) - pow2((C::ADDRESS_WIDTH() - bits) as nat))
            as usize
    } else {
        0
    }
}

Upper VA bits selected by the same sign-extension rule as executable vaddr_range. The bit boundary is the complete page-table coverage, as in vaddr_leading_part_spec.