Function vaddr_replace_pte_index_spec

pub open spec fn vaddr_replace_pte_index_spec<C: PagingConstsTrait>(
    va: Vaddr,
    level: PagingLevel,
    index: int,
) -> Vaddr

Expand description

{
    (va as int + (index - pte_index_spec::<C>(va, level)) * page_size::<C>(level))
        as Vaddr
}

Replace one page-table index while leaving the other address components unchanged.

vaddr_replace_pte_index_spec