lemma_meta_to_paddr_biinjective

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

Function lemma_meta_to_paddr_biinjective 

Source 
pub broadcast proof fn lemma_meta_to_paddr_biinjective(vaddr: Vaddr)
Expand description
requires
FRAME_METADATA_RANGE().start <= vaddr && vaddr < FRAME_METADATA_RANGE().end,
vaddr % META_SLOT_SIZE() == 0,
ensures
#[trigger] frame_to_meta(meta_to_frame(vaddr)) == vaddr,