Function vaddr_to_paddr_for 

pub open spec fn vaddr_to_paddr_for<A: ArchAddressSpaceModel>(va: Vaddr) -> Paddr

{ (va - A::linear_mapping_base_vaddr_spec()) as usize }

Convert a linear-mapped virtual address back to a physical address.