Updating --conditionalizePermissions

[marcoeilers]

Silicon's experimental --conditionalizePermissions flag performs a program transformation that rewrites access predicates under conditions, i.e., b ==> acc(e.f, r), into unconditional access predicates with conditional permission amounts, i.e., acc(e.f, b ? r : none), with the intention of preventing Silicon from branching on the value of b to reduce the number of branches.

This PR updates the rewriter to add features and fix some issues to make it more generally usable:

• Instead of throwing a runtime error when encountering a wand (which cannot have a conditional permission amount), it simply does not perform the rewriting for wands (i.e., it will output a mostly unchanged b ==> P --* Q.
• Similarly, it does not perform the rewriting if r is a wildcard (since that leads to completeness issues), or when e is a complex expression that is not always well-defined, since the well-definedness of e may depend on condition b: Given acc(e.f, b ? r : none), Silicon checks that e is well-defined in the current context in general, not only if b is true.
• It fixes previous issues when transforming quantifiers or let-expressions, where the transformer would turn transform triggers and bound expressions, respectively, into implications, which results in invalid code.
• It adds a phase that transforms impure ternary expressions b ? P : Q into a conjunction of implications b ==> P && !b ==> Q, which is then transformed as described above (ternary expressions were previously left untransformed).

Finally, it fixes an issue that occurs when packaging a wand that contains a quantified permission with a complex permission amount (which is technically a different issue, but will happen more often when using the transformation).