Function lemma_paddr_to_vaddr_properties_for 

pub proof fn lemma_paddr_to_vaddr_properties_for<A: ArchAddressSpaceModel>(pa: Paddr)

requires

pa < A::vmalloc_base_vaddr_spec() - A::linear_mapping_base_vaddr_spec(),

ensures

A::linear_mapping_base_vaddr_spec() <= paddr_to_vaddr_for::<A>(pa)
    < A::vmalloc_base_vaddr_spec(),

vaddr_to_paddr_for::<A>(paddr_to_vaddr_for::<A>(pa)) == pa,

Maps a physical offset into the linear mapping window and back without loss.