Allow controlling stuckness at the language level

Currently, the safety result of Iris is that each expression is either a value or can reduce. However, there are cases where one wants to have expressions that are not values but also cannot reduce (e.g. when modelling untrusted code that is allowed to get stuck or for modeling "no behavior"). Currently, Iris provides the MaybeStuck WP which does not require proving safety. However, using MaybeStuck is very coarse grained: If any part of the program uses the MaybeStuck WP, one looses the safety guarantees for the whole program as composing a MaybeStuck WP with a NotStuck WP results in a MaybeStuck WP.

This MR extends the language interface with a stuck_allowed e σ predicate (name open for debate) that specifies expressions that are not required to be reducible. One can obtain the NotStuck WP by defining stuck_allowed e σ as False and the MaybeStuck WP by defining stuck_allowed e σ as True.

Open questions:

• Naming
• What are the right set of axioms?
• Discussing TODOs in the code
• Should the MaybeStuck be removed in this MR or in a follow up MR?
• The MaybeStuck WP allows having both MaybeStuck and NotStuck WP for the same language while the solution in this MR fixes the notion of stuckness of a language. Is this a problem?
• Should we add a Abort NB expression to HeapLang to replace the diverge library?