Skip to main content

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
valid_frame_paddr(page),
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,