pub proof fn lemma_max_paddr_range()Expand description
ensures
MAX_PADDR <= VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,pub proof fn lemma_max_paddr_range()MAX_PADDR <= VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,