Function lemma_same_node_vaddr_leading_part_match 

pub proof fn lemma_same_node_vaddr_leading_part_match<C: PagingConstsTrait>(
    va1: Vaddr,
    va2: Vaddr,
    node_start: Vaddr,
    level: PagingLevel,
)

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_leading_part_spec::<C>(va1) == vaddr_leading_part_spec::<C>(va2),

Moving within one page-table node preserves the upper virtual-address contribution.