Open invariants in async/await and async blocks.

[FeizaiYiHao]

I'm planning to add support for open invariants in async functions and add support for async blocks. Please let me know if these makes sense.

Open invariants

Conceptually, as long as any open_invariants block doesn't contain yield points, we'd be fine.
The only yield point in Rust is await. Luckily, Rust does not allow yield points in non-async functions. Even if a regular function has an async block, which may contain await, the block returns a future that is lazy and will not do anything unless it is called await in some async functions.
Therefore, as long as open_invariants does not call async functions or await, the execution wouldn't yield.
So all we need to do is to traverse the expressions and statements in each open_invariants block and make sure there are no calls to async functions or await.

Async blocks

On a high level, I think it should work similarly to async functions (so with postconditions), since async functions are desugared into a function with a large async block. I'm not sure how to handle this elegantly. Should it be handled similarly to closure?

[tjhance]

Invariants: Yeah, this sounds right to me. Conceptually, I'd consider a yield to be an operation that is "opens_invariants any", which effectively rules it out from being used in open_invariant blocks, or in functions with anything less than the default "opens_invariants any" in its signature.

Async blocks: This will probably require a bit more investigation. As I understand it, these are like closures, but they're a different "kind" of closure, and I don't know much about them right now.