Function lemma_aligned_vaddr_slack 

pub proof fn lemma_aligned_vaddr_slack<C: PagingConstsTrait>(
    va: Vaddr,
    level: PagingLevel,
)

requires

1 <= level <= C::NR_LEVELS() + 1,

va % page_size::<C>(level) == 0,

ensures

va + page_size::<C>(level) <= usize::MAX + 1,

A power-of-two-aligned address leaves one complete slot before machine-word wrap.