Function lemma_paddr_to_vaddr_properties 

pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)

requires

pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,

ensures

#[trigger] paddr_to_vaddr(pa) == model::paddr_to_vaddr_for::<CurrentArch>(pa),

LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(pa) < VMALLOC_BASE_VADDR,

#[trigger] vaddr_to_paddr(paddr_to_vaddr(pa)) == pa,

Relates the current linear mapping to its architecture model and inverse.