Function certify_size_bound 

pub fn certify_size_bound(ranks: &[u64]) -> Option<SizeBound>

Verify that ranks is a valid non-increasing measure and read off the SizeBound it certifies. Returns None if the measure ever increases (then it is not a termination measure and certifies nothing). The bound levels · max_width is a structural consequence of the annotation, so the checker never re-derives the proof — it only counts.