Function is_valid_range_spec 

pub open spec fn is_valid_range_spec<C: PageTableConfig>(r: Range<Vaddr>) -> bool

{
    page_table_managed_start_spec::<C>() <= r.start < r.end
        <= page_table_managed_end_spec::<C>()
}

Models is_valid_range using managed bounds.