lemma_vaddr_to_paddr_properties

ostd::specs::arch::kspace

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,