Unsound package algorithm for magic wands

[tdardinier]

The package algorithm used by Silicon computes a footprint for a wand that may conditions on facts that are not framed by the wand's footprint, which is unsound, as the example below (which is verified by Silicon) illustrates:

field f: Bool
 
method main(x: Ref, a: Ref, b: Ref)
 requires acc(x.f) && acc(a.f) && acc(b.f)
 ensures false
{
    package acc(x.f) && (x.f ? acc(a.f, 1/2) : acc(b.f, 1/2)) --* acc(a.f, 1/2) && acc(b.f, 1/2)
    assert (perm(a.f) == 1/1 && perm(b.f) == 1/2) || (perm(a.f) == 1/2 && perm(b.f) == 1/1)
    x.f := perm(a.f) != 1/1
    apply acc(x.f) && (x.f ? acc(a.f, 1/2) : acc(b.f, 1/2)) --* acc(a.f, 1/2) && acc(b.f, 1/2)
}

The footprint computed by Silicon for the wand acc(x.f) && (x.f ? acc(a.f, 1/2) : acc(b.f, 1/2)) --* acc(a.f, 1/2) && acc(b.f, 1/2) is x.f ? acc(b.f, 1/2) : acc(a.f, 1/2), which is not a theoretically valid footprint, since it conditions on the value of x.f, even though it holds no permission to it.

Note that Carbon suffers from the same issue.