pub open spec fn vaddr_shift_bits<const L: usize>(idx: int) -> nat
0 < L,
idx < L,
{ (12 + 9 * (L - 1 - idx)) as nat }