The semantics of permission introspection in the body of unfolding expressions is unclear

[gauravpartha]

It is currently unclear how permission introspection should behave inside the body of unfolding expressions, i.e., what the permission mask should be when evaluating the body. We have had some discussions on the challenges (with Peter, Alex, Thibault) and this issue documents some of the high-level points.

Intuitively, one might expect unfolding P(x) in e to evaluate e in the state where permission to P(x) is exhaled and permission to body(P(x)) is inhaled. However, this view breaks down when considering exhale statements. The core reason is that permission introspection within exhale statements is aware of previous side-effects in the exhale, which means that it would be inconsistent to use the permission mask right before the exhale for unfolding expressions. For example, exhale acc(P(x)) && perm(P(x)) == none is expected to verify in a state with full permission to P(x), and thus exhale acc(P(x)) && unfolding Q(y) in perm(P(x)) == none is expected to verify in a state with full permission to P(x) and at least full permission to Q(y). To show why this leads to challenges in the general case, let us consider some examples.

Consider exhale P(x) && unfolding P(x) in e. Here, we can't define the behaviour of unfolding to exchange P(x) for body(P(x)), because P(x) has already been removed by the exhale. There are multiple options one could imagine here. Let us discuss two.

One option could be that one does not remove P(x) inside the unfolding and instead directly obtains the permission to the body of P(x) because P(x) has already been removed (while the unfolding would remove the permission to P(x) in the case exhale unfolding P(x) in e). This is strange, because perm(P(x)) before the unfolding says that there is no permission to P(x) but now we get permission inside P(x) due to the unfolding expression. One would have to also think about the case when one has more than full permission to P(x) before the exhale (i.e., where exhaling the first conjunct does not remove all available permission to P(x)). Finally, I think @tdardinier mentioned that this option would not be easily expressible in a more abstract semantics.

A second option could be to not obtain permission to body(P(x)) in the unfolding expression, because there is no permission left to P(x).

Fractional amount in unfoldings

Before a decision is made, one should also reconsider whether it makes sense for unfolding expressions to allow specifying the fractional amount that should be unfolded. One could argue that the precise fractional amount does not matter, similarly to how the precise fractional amount of permissions in function preconditions does not matter (regarding the latter, a use case was discussed where the precise fractional amount did matter, but this would be resolved with an asserting A in e expression as explored in #663)

State of the back-ends

Carbon currently does not have a consistent treatment of permission introspection inside unfolding expressions (in most cases, the unfolding expression has no effect on permission introspection). Changing Carbon to make unfolding expressions have an effect on perm expressions in the general case will require fundamental changes, since Carbon currently translates unfolding expressions to Boogie expressions where the unfolding is ignored (the unfolding mainly has an effect for the well-definedness check that is translated to a Boogie statement).
Silicon seems to generally follow the approach of exchanging the predicate for its body when evaluating the unfolding body.