pub open spec fn pa_is_valid_kernel_address(pa: int) -> bool
{ PHYSICAL_BASE_ADDRESS_SPEC() <= pa < PHYSICAL_BASE_ADDRESS_SPEC() + PAGE_SIZE() * MAX_NR_PAGES() as int }