Support for labelled assertions and requires in functions

[MikaelMayer]

Summary

There are labelled assertions in statements, but not in expressions. Similarly, it's not possible to reveal "labelled requires" in functions.

Background and Motivation

We often see a conversion from method to functions to ease reasoning.
However, labelling assertion is not possible in expressions. In the following example:

predicate P(x: int)

function test(): (i: int)
  ensures P(i)
  requires rule: forall i | i % 2 == 0 :: P(i)
{
  assert rule2: forall i | i % 4 == 0 :: P(i) by {
    reveal rule;
  }
  assert P(12) by {
    reveal rule;
  }
  12
}

assert rule2: is not permitted, and if removed, reveal rule; is not permitted either.
It ought to be available.

Proposed Feature

• Labelled assertions in expressions
• Support for revealing labelled requires in functions

Alternatives

Not having labelled assertions is not a problem for small codebases, but bigger codebases start to have this issue.
The workaround for not having labelled assertions is to have non-labelled assertions, but as functions grow, verification can become not durable. Not only that, but to figure out what assertions actually speed up proof, one absolutely needs to isolate assertions so that they don't interfere with other mechanisms.
Another workaround is to convert a function to a method, but it's not always possible, especially if the function was called by other functions.