Skip to main content

lemma_same_node_vaddr_upper_bits_match

ostd::specs::mm::page_table

Function lemma_same_node_vaddr_upper_bits_match 

Source 
pub proof fn lemma_same_node_vaddr_upper_bits_match<C: PagingConstsTrait>(
    va1: Vaddr,
    va2: Vaddr,
    node_start: Vaddr,
    level: PagingLevel,
)
Expand description
requires
level <= C::NR_LEVELS(),
node_start <= va1,
va1 - node_start < page_size::<C>((level + 1) as PagingLevel),
node_start <= va2,
va2 - node_start < page_size::<C>((level + 1) as PagingLevel),
node_start as nat % page_size::<C>((level + 1) as PagingLevel) as nat == 0,
ensures
vaddr_upper_bits_spec::<C>(va1) == vaddr_upper_bits_spec::<C>(va2),

Architecture-parameterized view of the uninterpreted upper bits preserved by moving within one page-table node.