Unfold, fold, and unfolding must have a strictly positive permission amount

[marcoeilers]

This addresses viperproject/silver#444 on the Carbon side and depends on a change in Silver to introduce a new kind of error and adapt test annotations.

@gauravpartha: I've implemented this now by introducing a completely new check that perm > none instead of replacing or modifying the existing perm >= none checks in the QuantifiedPermModule. Is this a good way of doing things in Carbon?
I tried a different version first (it's on branch meilers_unfold_none) where I instead check in QuantifiedPermModule if we're currently folding or unfolding a predicate, and then if that's the case I check the error type and make the comparison strict. That had two drawbacks: a) it felt awkward because exhaleExp and inhaleAux suddenly use some random state in the FuncPredModule, and b) it results in a different order of errors than in Silicon.
I could also imagine a third version where all methods (exhaleExp, exhaleExpBeforeAfter, exhale, exhaleConnective, invokeExhaleOnComponents, inhaleAux, ...) all get an additional boolean parameter to specify whether a value of zero is okay, and then that gets set to false in foldPredicate or unfoldPredicate. That also didn't feel good to me because I pass this one value through fifteen methods, but maybe that's preferable to duplicating the check like in this PR. What do you think?

I should mention: Both other options (where we check that the permission is non-zero when exhaling or inhaling the predicate) also have the issue that they result in a different order of checks for folds than in Silicon: For folds, we would exhale the predicate body before inhaling the predicate and checking that the permission is non-zero. Thus, if some pure constraint in the predicate is not satisfied, we'd get an error about that first, before the error for the zero-permission. In Silicon, the zero-error always comes first, which feels better to me.

[gauravpartha]

I agree that the choice that you implemented makes most sense. In particular, I think it's important that the order of errors matches Silicon (one can even make an argument that a semantics for verifier implementations should force an order on certain errors, which makes this point even stronger). Apart from that this solution is the easiest to comprehend when looking at the code and most directly reflects a description of the semantics.

Regarding the other two choices:

• I agree that relying on hard-to-explain state in modules is suboptimal. We removed one such instance that was extremely hard to understand for something that is simple (#451).
• I may be missing something regarding adding the checks in inhale and exhale as implemented on the other branch (meilers_unfold_none): Why does that work? If the predicate has no accessibility predicates we would not do any checks at all in that case, correct (which would not be desired)?

[marcoeilers]

Thanks!

• I may be missing something regarding adding the checks in inhale and exhale as implemented on the other branch (meilers_unfold_none): Why does that work? If the predicate has no accessibility predicates we would not do any checks at all in that case, correct (which would not be desired)?

This does not target the inhale or exhale of the predicate body (which was hopefully unaffected), but of the predicate itself, which we always either inhale for fold or exhale for unfold.