lemma_frame_to_meta_soundness

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