(Un)folding no longer allows `none` in viper

[pieter-bos]

See also:

• Unfolding with no permissions and predicate well-definedness viperproject/silver#444
• New error reason for unfolding or folding with non-positive permission amount. viperproject/silver#744

We should consider what to do with this:

• On a technical level we can just map through the error, I guess in the blame of fold/unfold/unfolding
• We should consider whether the behaviour of Scale should change - my current interpretation of this is that e.g. [none](a == 1) is equivalent to true, not a == 1, and not disallowed as a well-formedness condition.
  • e.g. I think in parallel blocks we encode stuff as [1 / N]predicates() instead of N > 0 ==> [1 / N]predicates(), so that should then also change. this is nonsense
• An alternative is to simply always encode a branch, i.e. unfold [p]x() -> if(p > 0) unfold [p](x)