Skip to main content

lemma_vaddr_of_eq_int

ostd::specs::mm::page_table

Function lemma_vaddr_of_eq_int 

Source 
pub proof fn lemma_vaddr_of_eq_int<C: PageTableConfig>(path: TreePath<NR_ENTRIES>)
Expand description
requires
path.inv(),
path.len() <= INC_LEVELS - 1,
ensures
vaddr_of::<C>(path) as int
    == vaddr(path) as int + C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int,

vaddr_of::<C>(path) in int equals the unconditional sum — no usize wrap. Holds because vaddr(path) < 2^48 (any valid path) and LEADING_BITS < 2^16, so the sum is < 2^64 = usize::MAX + 1.