Viper allows predicates whose fractional amount is not self-framing

Carbon and Silicon check for each predicate whether the body is self-framing. However, (in cases where the amounts of permission involved rule out aliasing possibilities) this check might not imply that every fractional amount of this body is self-framing. As a result, both verify the following program (explanation below the listing), but I think they should report an error:

field f: Int
field g: Int

predicate R(x: Ref, y: Ref) {
    acc(x.f) && acc(y.f) && (x == y ==> y.g > 0)
}

method main(a: Ref) 
    requires acc(a.g) && acc(a.f)
    ensures false
{
    a.g := 1
    fold acc(R(a,a), 1/2) // Point A
    a.g := -1 //Point B
    unfold acc(R(a,a),1/2) // Point C
}

The body of R(x,y) is self-framing (because the first two conjuncts ensure that x != y). However, the body of acc(R(x,y),1/2) is not self-framing (note that the field accessed on the right of the implication is different; no permissions to it are held in the predicate body). The example exploits this to prove false in main. At point A, the predicate instance acc(R(a,a),1/2) is folded whose body is not self-framing, which is possible because the permission to a.g is held outside the predicate instance. At point B, a heap assignment is executed such that the body of acc(R(a,a),1/2) is violated. This violation leads to a contradiction after the unfold at point C.

In summary, since the Viper verifiers frame predicates around operations such as heap assignments, predicate instances must be self-framing. Here, there are predicate instances, which are not self-framing and thus I think the Viper verifiers should report an error.

A natural solution would be to check whether a predicate body is self-framing for every fraction. However, this might be too restrictive, because there may be programs in practice where the current self-framing check (which just checks whether the body is self-framing for fraction 1) is sufficient but where the stronger check for every fraction may fail. For instance, the current self-framing check is likely sufficient if no predicate instance with fraction less than 1 is used. Moreover, if function calls are used in predicate instances with preconditions that specify concrete fractions, then the stronger condition will not hold.

Start by reproducing the program in the issue with both Carbon and Silicon, focusing on the fold at Point A and unfold at Point C. Then trace the self-framing checks for predicate instances with fractional amounts; done means the verifiers reject this unsound example while preserving valid uses that the issue identifies as potentially affected.