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,