Function lemma_paddr_to_vaddr_aligned_for 

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

requires

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

pa % A::C::BASE_PAGE_SIZE() == 0,

ensures

paddr_to_vaddr_for::<A>(pa) % A::C::BASE_PAGE_SIZE() == 0,

Preserves base-page alignment when mapping a physical offset into the linear window.