pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_page_aligned()Expand description
ensures
#[trigger] FRAME_METADATA_RANGE.start % PAGE_SIZE == 0,FRAME_METADATA_RANGE.end % PAGE_SIZE == 0,