Function lemma_align_down_indices 

pub proof fn lemma_align_down_indices<C: PagingConstsTrait>(
    va: Vaddr,
    level: PagingLevel,
)

requires

1 <= level <= C::NR_LEVELS(),

ensures

({
    let aligned = nat_align_down(va as nat, page_size::<C>(level) as nat) as Vaddr;
    &&& aligned % C::BASE_PAGE_SIZE() == 0
    &&& vaddr_upper_bits_spec::<C>(aligned) == vaddr_upper_bits_spec::<C>(va)
    &&& forall |i: int| {
        1 <= i <= C::NR_LEVELS()
            ==> #[trigger] pte_index_spec::<C>(aligned, i as PagingLevel)
                == if i < level { 0 } else { pte_index_spec::<C>(va, i as PagingLevel) }
    }

}),

Aligning down preserves all indices at and above the slot and the upper address bits.