lemma_vaddr_to_paddr_properties

ostd::specs::arch

Function lemma_vaddr_to_paddr_properties 

Source 
pub broadcast proof fn lemma_vaddr_to_paddr_properties(va: Vaddr)
Expand description
requires
LINEAR_MAPPING_BASE_VADDR() <= va < VMALLOC_BASE_VADDR(),
ensures
#[trigger] vaddr_to_paddr(va) < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
#[trigger] paddr_to_vaddr(vaddr_to_paddr(va)) == va,