Termination of `next` for `Range`

[Lysxia]

(Context: trying to prove termination of simple for loops.)

In theory, fixing this is as simple as adding an extern_spec. The difficulty is that the impl is polymorphic in the index type:

impl<A: Step> Iterator for Range<A> {
  fn next ...
}

So the termination of next depends on the termination of Step::forward_checked.

[jhjourdan]

We more and more need first-class tags for proof modes.

This would cover:

• Termination
• panic freedom vs. UB freedom only
• ghost mode vs. program mode
• SC vs. Weak memory
• others?

Then we would use these in specifications. This would solve this issue, but also simplify the specs for closures, better handle the case of ghost s non-ghost functions, etc...