Function paddr_to_vaddr_for 

pub open spec fn paddr_to_vaddr_for<A: ArchAddressSpaceModel>(pa: Paddr) -> Vaddr

{ (pa + A::linear_mapping_base_vaddr_spec()) as usize }

Convert a physical address through architecture A’s linear mapping.