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(),