Function lemma_vaddr_to_paddr_properties_for

pub proof fn lemma_vaddr_to_paddr_properties_for<A: ArchAddressSpaceModel>(va: Vaddr)

Expand description

requires

A::linear_mapping_base_vaddr_spec() <= va < A::vmalloc_base_vaddr_spec(),

ensures

vaddr_to_paddr_for::<A>(va)
    < A::vmalloc_base_vaddr_spec() - A::linear_mapping_base_vaddr_spec(),

paddr_to_vaddr_for::<A>(vaddr_to_paddr_for::<A>(va)) == va,

Maps a linear-mapped virtual address to a physical offset and back without loss.

lemma_vaddr_to_paddr_properties_for