Skip to main content

axiom_leading_bits_only_when_high_half

ostd::mm::page_table

Function axiom_leading_bits_only_when_high_half 

Source 
pub proof fn axiom_leading_bits_only_when_high_half<C: PageTableConfig>()
Expand description
ensures
C::LEADING_BITS_spec() != 0usize
    ==> (C::VA_SIGN_EXT()
        && (((C::TOP_LEVEL_INDEX_RANGE_spec().start as int)
            * (pow2(pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat) as int))
            / (pow2((C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1),

Per-config relationship between LEADING_BITS_spec and the sign-ext branch of vaddr_range: a non-zero LEADING_BITS requires both VA_SIGN_EXT and that bit ADDRESS_WIDTH - 1 of pt_va_range_start is set. Equivalently (contrapositive), if either of those fails, then LEADING_BITS == 0.

For UserPtConfig (LB=0) the conclusion is vacuous; for KernelPtConfig (LB=0xffff, idx.start=256, off=39, ADDRESS_WIDTH=48), 2^47 / 2^47 % 2 == 1 and VA_SIGN_EXT == true — so the implication holds.