Pancake annotation positions

From a pure usability perspective, the current annotations have to sit inside a function body or a loop body like:
```c
fun main() {
/@ requires ... @/
/@ ensures ... @/

// blah..

while {
/@ invariant .. @/
}

}
```
which works as it is; but a bit counter-intuitive. A nicer way would be to put the annotations outside the bodies.

No file, test, or entry point is named. First clarify the desired syntax and how requires, ensures, and invariant annotations should relate to function and loop bodies; done means an agreed design is implemented and its behavior is covered by tests.

Written by the indexing model from the issue text.