vabits_actual
#define vabits_actual (64 - ((read_tcr() >> 16) & 63))
#define vabits_actual ((u64)VA_BITS)