Function page_table_managed_start_spec 

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

{
    (page_table_coverage_start_spec::<C>()
        + C::TOP_LEVEL_INDEX_RANGE().start * page_size::<C>(C::NR_LEVELS())) as Vaddr
}

Start of the managed virtual-address range, restricted by TOP_LEVEL_INDEX_RANGE.