axiom_kernel_range_valid

ostd::mm::kspace::kvirt_area

Function axiom_kernel_range_valid 

Source 
pub proof fn axiom_kernel_range_valid(r: Range<Vaddr>)
Expand description
ensures
(KERNEL_BASE_VADDR <= r.start && r.end <= KERNEL_END_VADDR && r.start < r.end
    && r.start % PAGE_SIZE == 0 && r.end % PAGE_SIZE == 0)
    ==> is_valid_range_spec::<KernelPtConfig>(&r),

Kernel ranges within [KERNEL_BASE_VADDR, KERNEL_END_VADDR] with alignment are valid for KernelPtConfig (which uses sign-extended high-half addresses).