lemma_meta_to_frame_soundness

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

Function lemma_meta_to_frame_soundness 

Source 
pub broadcast proof fn lemma_meta_to_frame_soundness(meta: Vaddr)
Expand description
requires
meta % META_SLOT_SIZE() == 0,
FRAME_METADATA_RANGE().start <= meta
    && meta < FRAME_METADATA_RANGE().start + MAX_NR_PAGES() * META_SLOT_SIZE(),
ensures
#[trigger] meta_to_frame(meta) % PAGE_SIZE() == 0,
meta_to_frame(meta) < MAX_PADDR(),