Function lemma_vaddr_strict_bound Copy item path

path.inv(),

path.len() <= INC_LEVELS - 1,

(vaddr(path) as int) < 0x1_0000_0000_0000int,

vaddr(path) < 2^48 for every valid path: each term in the positional sum is i_k * 2^(12 + 9·k) with i_k < 512 = 2^9, so the sum is strictly less than 2^48.