AMD64_PML4SHIFT
pml4eindex = (va >> AMD64_PML4SHIFT) & (AMD64_NPML4EPG - 1);
_Static_assert(PML4SHIFT == AMD64_PML4SHIFT, "PML4SHIFT mismatch");