lemma_paddr_to_meta_biinjective

ostd::mm::frame::meta::mapping

Function lemma_paddr_to_meta_biinjective 

Source 
pub broadcast proof fn lemma_paddr_to_meta_biinjective(paddr: Paddr)
Expand description
requires
paddr % PAGE_SIZE() == 0,
paddr < MAX_PADDR(),
ensures
#[trigger] meta_to_frame(frame_to_meta(paddr)) == paddr,