pub proof fn lemma_max_paddr_range()Expand description
ensures
MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX,