pub proof fn lemma_nr_pte_index_bits_bounded<C: PagingConstsTrait>()Expand description
ensures
0 <= nr_pte_index_bits::<C>() <= C::BASE_PAGE_SIZE().ilog2(),pub proof fn lemma_nr_pte_index_bits_bounded<C: PagingConstsTrait>()0 <= nr_pte_index_bits::<C>() <= C::BASE_PAGE_SIZE().ilog2(),