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