lemma_frame_to_meta_soundness

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

Function lemma_frame_to_meta_soundness 

Source 
pub broadcast proof fn lemma_frame_to_meta_soundness(page: Paddr)
Expand description
requires
page % PAGE_SIZE() == 0,
page < MAX_PADDR(),
ensures
#[trigger] frame_to_meta(page) % META_SLOT_SIZE() == 0,
FRAME_METADATA_RANGE().start <= frame_to_meta(page)
    && frame_to_meta(page)
        < FRAME_METADATA_RANGE().start + MAX_NR_PAGES() * META_SLOT_SIZE(),