Skip to main content

lemma_vaddr_range_bounds_spec_unfold

ostd::mm::page_table

Function lemma_vaddr_range_bounds_spec_unfold 

Source 
pub proof fn lemma_vaddr_range_bounds_spec_unfold<C: PageTableConfig>()
Expand description
ensures
vaddr_range_bounds_spec::<C>()
    == {
        let idx = C::TOP_LEVEL_INDEX_RANGE_spec();
        let off = pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat;
        let lb = C::LEADING_BITS_spec() as int;
        let base = lb * 0x1_0000_0000_0000int;
        let start = (base + (idx.start as int) * pow2(off)) as usize;
        let end_inclusive = (base + (idx.end as int) * pow2(off) - 1) as usize;
        (start, end_inclusive)
    },

Reveal the body of vaddr_range_bounds_spec at a call site without making the function itself open (which causes z3-context pollution in cursor invariants).