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.index(0)) * 0x80_0000_0000int <= vaddr(path),
vaddr(path) + page_size((INC_LEVELS - path.len()) as PagingLevel)
    <= (path.index(0) + 1) * 0x80_0000_0000int,

The VA of any path is within the 2^39-sized cell of its top-level index: path[0] * 2^39 <= vaddr(path) and vaddr(path) + page_size <= (path[0]+1) * 2^39. Pure VA arithmetic (x86 4-level paging). Used by view_rec_top_index_va_bound.