Skip to main content

axiom_top_level_index_range_bounds

ostd::mm::page_table

Function axiom_top_level_index_range_bounds 

Source 
pub proof fn axiom_top_level_index_range_bounds<C: PageTableConfig>()
Expand description
ensures
(C::TOP_LEVEL_INDEX_RANGE_spec().start as int)
    < (pow2(
        (C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()))
            as nat,
    ) as int),
C::TOP_LEVEL_INDEX_RANGE_spec().end as int
    <= pow2(
        (C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()))
            as nat,
    ) as int,
pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) <= C::ADDRESS_WIDTH() as int,
pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) >= 0,
(C::TOP_LEVEL_INDEX_RANGE_spec().start as int)
    < (C::TOP_LEVEL_INDEX_RANGE_spec().end as int),
C::ADDRESS_WIDTH() as int <= 64,

Trait-level invariant the upstream enforces via const assertions in vaddr_range’s prologue. Captured here as an axiom so we can use it in proofs (Verus has no const { ... } form for trait constants).

idx.start < 2^(ADDRESS_WIDTH - offset) and idx.end <= 2^(...) together bound the positional VA at pt_va_range_start / pt_va_range_end by 2^ADDRESS_WIDTH.