Skip to main content

lemma_vaddr_top_index_cell

ostd::specs::mm::page_table

Function lemma_vaddr_top_index_cell 

Source 
pub proof fn lemma_vaddr_top_index_cell(path: TreePath<NR_ENTRIES>)
Expand description
requires
path.inv(),
1 <= path.len() <= INC_LEVELS - 1,
ensures
(path[0]) * page_size::<PagingConsts>(NR_LEVELS as PagingLevel) <= vaddr(path),
vaddr(path) + page_size::<PagingConsts>((INC_LEVELS - path.len()) as PagingLevel)
    <= (path[0] + 1) * page_size::<PagingConsts>(NR_LEVELS as PagingLevel),

The VA of any path is within the cell selected by its top-level index.