pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_large_enough()Expand description
ensures
#[trigger] FRAME_METADATA_RANGE.end
>= FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE,