Function top_level_index_width_spec 

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

{ (C::ADDRESS_WIDTH_spec() - pte_index_bit_offset_spec::<C>(C::NR_LEVELS())) as usize }

Number of effective virtual-address bits used by the top-level page-table index.