Function vaddr_range_spec 

pub open spec fn vaddr_range_spec<C: PageTableConfig>() -> RangeInclusiveView<Vaddr>

{
    let start = page_table_managed_start_spec::<C>();
    let end = (page_table_managed_end_spec::<C>() - 1) as Vaddr;
    RangeInclusiveView {
        start,
        end,
        exhausted: false,
    }
}

Canonical bounds of the VA range managed by a page-table config,