Function pte_index_spec 

pub open spec fn pte_index_spec<C: PagingConstsTrait>(
    va: Vaddr,
    level: PagingLevel,
) -> usize

{
    (va >> pte_index_bit_offset_spec::<C>(level))
        & ((nr_subpage_per_huge::<C>() - 1) as usize)
}

Page-table index selected by va at level.