Function lemma_vaddr_of_eq_int 

pub proof fn lemma_vaddr_of_eq_int<C: PageTableConfig>(path: TreePath<NR_ENTRIES>)

requires

path.inv(),

path.len() <= INC_LEVELS - 1,

ensures

vaddr_of::<C>(path) == vaddr(path) + page_table_coverage_start_spec::<C>(),

vaddr_of::<C>(path) in int equals the unconditional sum — no usize wrap. Holds because vaddr(path) < 2^48 (any valid path) and LEADING_BITS < 2^16, so the sum is < 2^64 = usize::MAX + 1.