Consider enforcing termination checking

[utaal]

@parno notes that no termination checking weakens the guarantees provided by verification, as a missing iteration counter increment, for example, may cause a verifiable program to stall in a case that could have been easily caught by the termination check.

Introducing an optional termination check is on the roadmap. We can consider a flag that enforces termination checking of all exec functions.

There is also the option to default to termination checking on, to avoid the pitfall @parno describes. I believe that requires further design to allow to selectively disable it (possibly in a manner similar to dafny's decreases *).

[utaal]

• Implementing termination checks for loops is a pre-requisite to this.

[utaal]

Discussion at the [Verus all-hands]:

• What should the default be? Terminating or non-terminating?
• Termination-by-default might be easier because presumably most functions are terminating even in a project (say) like a forever-running server, where only the outermost functions are non-terminating
• what if someone is using a mostly-Rust program, and then for that lightweight verification, we aren’t sure how termination should work
• Default experience: termination checking; some attribute that means “this might not terminate” (apply on per-function or while-loop basis)
• Don’t use decreases * as the keyword, that is confusing; use may_not_terminate or similar to not be confusing
• Concurrency: proving termination is not easy; so being able to mark things aggressively non-terminating is important; but we should ignore this concern for now, and default should be enabling termination checking.

[utaal]

From triage:
More sources of non-termination than just checking for decreases clauses on loop and recursion.
Already supported for recursion, and loops. No enforcement yet.
How to do UX?
error (initially warning) in the absence of a decreases clause in exec code, and crate-level attributes to opt-in or opt-out of total correctness.

@matthias-brun, @jaylorch: consider opting out for individual function, i.e. main, with an attributes. Folks are not against the idea.

@jaylorch: find a name flaggable by the auditor.