Skip to main content

lemma_leading_bits_properties

ostd::specs::mm::page_table::vaddr_range_proofs

Function lemma_leading_bits_properties 

Source 
pub proof fn lemma_leading_bits_properties<C: PageTableConfig>()
Expand description
ensures
page_table_coverage_start_spec::<C>()
    == leading_bits_spec::<C>() * pow2(nr_page_table_coverage_bits_spec::<C>() as nat),
page_table_coverage_start_spec::<C>()
    + pow2(nr_page_table_coverage_bits_spec::<C>() as nat) <= pow2(usize::BITS as nat),
C::VA_SIGN_EXT()
    && (C::TOP_LEVEL_INDEX_RANGE().start
        * pow2(pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat)
        / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1
    ==> page_table_coverage_start_spec::<C>()
        == pow2(usize::BITS as nat) - pow2(C::ADDRESS_WIDTH() as nat),
leading_bits_spec::<C>()
    < pow2((usize::BITS - nr_page_table_coverage_bits_spec::<C>()) as nat),

Derives the sign-extension mask and its width from the paging constants.