Skip to main content

lemma_idx_times_pow2_bound

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

Function lemma_idx_times_pow2_bound 

Source 
pub proof fn lemma_idx_times_pow2_bound<C: PageTableConfig>(start: Vaddr, end: Vaddr)
Expand description
requires
start
    == C::TOP_LEVEL_INDEX_RANGE_spec().start
        * (pow2(pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat) as int),
end
    == (C::TOP_LEVEL_INDEX_RANGE_spec().end
        * (pow2(pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat) as int) - 1)
        % 0x1_0000_0000_0000_0000int,
ensures
start < pow2(C::ADDRESS_WIDTH() as nat),
end < pow2(C::ADDRESS_WIDTH() as nat),
end
    == C::TOP_LEVEL_INDEX_RANGE_spec().end
        * pow2(pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat) - 1,

Two-in-one: start = idx.start * 2^off < 2^ADDRESS_WIDTH and end = (idx.end * 2^off - 1) % 2^64 < 2^ADDRESS_WIDTH.

The first follows from idx.start < 2^(ADDRESS_WIDTH - off). The second from idx.end <= 2^(ADDRESS_WIDTH - off) plus the no-wrap condition: idx.end * 2^off <= 2^ADDRESS_WIDTH ≤ 2^64, so the % 2^64 is a no-op when the value is positive.