AMD64_PDPMASK
a = (pdpe & AMD64_PG_1GB_FRAME) + (va & AMD64_PDPMASK);
return (AMD64_NBPDP - (va & AMD64_PDPMASK));
_Static_assert(PDPMASK == AMD64_PDPMASK, "PDPMASK mismatch");