Function vaddr_make 

pub open spec fn vaddr_make<const L: usize>(idx: int, offset: usize) -> usize

recommends

0 < L,

idx < L,

offset < NR_ENTRIES,

{ (page_size_spec::<PagingConsts>((L - idx) as PagingLevel) * offset) as usize }