Function vaddr_to_paddr 

pub open spec fn vaddr_to_paddr(va: Vaddr) -> usize

recommends

LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,

{ model::vaddr_to_paddr_for::<CurrentArch>(va) }

Converts a virtual address in the linear mapping to a physical address.