Calculus annotations: disallow unsound recursion

[Philipp15b]

We should also add checks that prevent users doing unsound recursive calls.

For example, this example is unsound w.r.t. wp semantics:

@wp
proc unsound() -> (x: Bool)
    pre ?(true)
    post ?(x == false)
{
    x = unsound()
}

The reason is that the call encoding implicitly assumes doing Park induction is valid, but it's not valid w.r.t. the least fixed point semantics and lower bounds (proc).

So we should disallow calls in:

• procs w.r.t. wp and ert (because of lfp semantics)
• coprocs w.r.t. wlp (because of gfp semantics)

It might be possible to relax these conditions, for example if we know that the call graph is acyclic. But I'm not sure about that right now.