pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)Expand description
requires
pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(pa) < VMALLOC_BASE_VADDR,#[trigger] vaddr_to_paddr(paddr_to_vaddr(pa)) == pa,