Incorrect encoding when the predicate argument in an unfold statement contains a permission introspection of the same predicate

[Dev-XYS]

The following program demonstrates the bug.

predicate P(x: Perm)
{
    x == none ==> false
}

method foo()
{
    inhale P(write)
    unfold P(perm(P(write)))
    assert false  // successfully verified
}

Predicate P is false if the argument x is none, and otherwise trivially true. The first statement of the method inhales P(write), which should be equivalent to inhale true, not affecting the program state. In the second statement, instead of unfolding P(write) directly, we use the expression perm(P(write)) as the argument of the predicate location, which should evaluate to write. Therefore, the statement should just be unfold P(write), and inhale true as a result. However, according to Carbon’s implementation, it subtracts 1 from the mask of P(write), and uses the resultant mask to evaluate perm(P(write)) in inhale (by substitution), leading to the inhale of the body of P(none), which is false.

[Dev-XYS]

The same bug is also present in fold encoding. See #577.