Function nr_pte_index_bits_spec 

pub open spec fn nr_pte_index_bits_spec<C: PagingConstsTrait>() -> usize

{ nr_subpage_per_huge::<C>().ilog2() as usize }

Number of virtual-address bits used to select an entry within one page-table node.