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,