pub proof fn lemma_linear_mapping_base_vaddr_properties()Expand description
ensures
LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0,LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR,