Open
Description
Created by @mschwerhoff on 2017-06-11 21:05
Last updated on 2017-06-25 17:08
Carbon and Silicon currently differ in their handling of (un)folding a wildcard fraction of a predicate. Consider the following examples:
field f: Int
predicate P(x: Ref, y: Ref) { acc(x.f) && acc(y.f) }
method test01(x: Ref, y: Ref) {
inhale P(x, y)
unfold acc(P(x, y), wildcard)
assert perm(x.f) == perm(y.f)
}
method test02(x: Ref, y: Ref) {
inhale acc(x.f) && acc(y.f)
fold acc(P(x, y), wildcard)
assert perm(x.f) == perm(y.f)
}
The two asserts fail in Carbon but verify in Silicon. My explanation is that the way a predicate body is scaled differs between the two: when folding acc(P(x, y), wildcard), Carbon takes the body and multiplies each permission expression by wildcard, thus exhaling acc(x.f, wildcard) && acc(y.f, wildcard). Silicon, on the other hand, uses only a single wildcard value to scale the predicate body: it basically exhales let k = wildcard in acc(x.f, k) && acc(y.f, k).