Knownfolded permissions unexpectedly recorded even though unfolding is not executed

[gauravpartha]

Carbon verifies the following program currently:

method unexpected(x: Ref) {
    inhale acc(x.f,1/2) && x.f == 2
    inhale x.f == 3 || (x.f < 0 ==> unfolding P(x) in true) //Point A
    inhale acc(P(x),1/2)  //Point B
    exhale acc(x.f, 1/2)  //Point C
    inhale acc(x.f, 1/2)
    assert x.f == 2       //Point D
}

The assertion at point A is well-defined, because x.f < 0 is false and thus, the right hand side of the implication need not be checked.
Since x.f < 0 is false, the unfolding expression should not be executed (there would also be no way to execute it, since P(x) is not even held!). Nevertheless, right after the inhale at point A, Carbon records that x.f is knownfolded w.r.t. P(x). As a result, after inhaling P(x) at point B and exhaling all direct permission to x.f at point C, Carbon keeps the information x.f is still 2. Therefore, Carbon verifies the assert statement at point D.

Note that the inhale at point B is required for the assertion to go through, because Carbon takes knownfolded permissions into account only for predicates that are owned (which makes Carbon’s encoding sound w.r.t. a model that allows looking into arbitrarily deep into predicates). So, even though Carbon looks into a predicate at a point where it does not even own the predicate, Carbon only uses this information once a predicate is owned (assuming there was no exhale before obtaining the predicate).

I think this is unexpected behaviour, because it makes the recording of knownfolded permission unpredictable. If Carbon uses unfolding expressions to look into predicates, then Carbon should do so only if the unfolding expression is actually executed. Moreover, even if one allowed looking into predicates without executing unfolding expressions, it should be more predictable than what is done now. For example, if one removes the disjunction and only keeps the right disjunct, then Carbon does not record knownfolded permissions. At a high level this is because inhale with definedness checks and inhale without definedness checks are not in-sync (which I am planning to fix in #407).

I also think think that if one swaps the statements in Point A and Point B, then Carbon should also not verify the example (for the same reasons).

[gauravpartha]

#407 has now been merged and fixes the issue in the concrete program given above.

However, similar issues as the above can still occur. For such issues to not occur, one must ensure that free assumptions for an expression e (e.g., recording known-folded permissions) are only ever made if definedness of e is checked. In particular, in the above program a free assumption on the subexpression unfolding P(x) in true is made even though its definedness is never checked (due to short-circuiting).

Here is an example that also leads to an unexpected verification success:

method unexpected_exhale(x: Ref) {
    inhale acc(x.f,1/2) && x.f == 2
    exhale (x.f < 0 ==> unfolding P(x) in true)
    inhale acc(P(x),1/2)
    exhale acc(x.f, 1/2)
    inhale acc(x.f, 1/2)
    assert x.f == 2
}

Here the second inhale from the initial program was replaced by an exhale. The assertion succeeds because Carbon records knownfolded permission to P(x) at the exhale.