Function valid_frame_paddr_for 

pub open spec fn valid_frame_paddr_for<A: ArchAddressSpaceModel>(pa: Paddr) -> bool

{ pa % A::C::BASE_PAGE_SIZE() == 0 && pa < A::max_paddr_spec() }

A physical address that can identify a base-page frame for architecture A.