Function page_table_coverage_end_spec 

pub open spec fn page_table_coverage_end_spec<C: PageTableConfig>() -> int

{
    page_table_coverage_start_spec::<C>() as int
        + page_size::<C>((C::NR_LEVELS() + 1) as PagingLevel)
}

Exclusive end of the complete page-table index coverage for the configured upper bits. This mathematical boundary may be one past Vaddr::MAX.