vaddr_make

ostd::specs::mm::page_table

Function vaddr_make 

Source 
pub open spec fn vaddr_make<const L: usize>(idx: int, offset: usize) -> usize
Expand description
recommends
0 < L,
idx < L,
0 <= offset < 512,
{ (vaddr_shift::<L>(idx) * offset) as usize }