Skip to main content

lemma_vaddr_strict_bound

ostd::specs::mm::page_table

Function lemma_vaddr_strict_bound 

Source 
pub proof fn lemma_vaddr_strict_bound(path: TreePath<NR_ENTRIES>)
Expand description
requires
path.inv(),
path.len() <= INC_LEVELS - 1,
ensures
vaddr(path) < 0x1_0000_0000_0000int,

The positional VA of every valid path fits in the current paging address space. The concrete x86 bound is retained for callers that combine it with canonical leading bits.