lemma_meta_to_frame_soundness

ostd::specs::mm::frame::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,