Skip to main content

lemma_next_slot_pte_index

ostd::specs::mm::page_table

Function lemma_next_slot_pte_index 

Source 
pub proof fn lemma_next_slot_pte_index<C: PagingConstsTrait>(
    va: Vaddr,
    next: Vaddr,
    level: PagingLevel,
)
Expand description
requires
1 <= level <= C::NR_LEVELS(),
va < next <= va + page_size::<C>(level),
next % page_size::<C>(level) == 0,
ensures
next
    == (nat_align_down(va as nat, page_size::<C>(level) as nat) + page_size::<C>(level))
        as Vaddr,
pte_index_spec::<C>(next, level) == 0
    ==> {
        &&& pte_index_spec::<C>(va, level) + 1 == nr_subpage_per_huge::<C>()
        &&& next % page_size::<C>((level + 1) as PagingLevel) == 0

    },
pte_index_spec::<C>(next, level) != 0
    ==> pte_index_spec::<C>(va, level) + 1 < nr_subpage_per_huge::<C>(),

At the next aligned boundary, a terminal index carries into the parent slot.