Function lemma_vaddr_upper_part_is_align_down

pub proof fn lemma_vaddr_upper_part_is_align_down<C: PagingConstsTrait>(va: Vaddr)

Expand description

ensures

vaddr_upper_part_spec::<C>(va)
    == nat_align_down(
        va as nat,
        page_size::<C>((C::NR_LEVELS() + 1) as PagingLevel) as nat,
    ),

Upper address bits contribute the aligned base of the complete paging body.

lemma_vaddr_upper_part_is_align_down