Something is wrong with predicate triggers for functions

[marcoeilers]

Silicon triggers definitions of functions both when they are called directly and when predicates are unfolded that they depend on.

For example, in the Viper program below, we get the triggers (recurse s@$ x@2@00)) and (recurse%stateless x@2@00) (Mem%trigger ($Snap.second ($Snap.second s@$)) x@2@00 x@2@00) for the definition of recurse. However, the precondition of recurse contains multiple permissions, not just the one for the Mem predicate; that's (I think) why the trigger identifies some s@$ that the predicate snapshot is only a part of.

Thus, if we later unfold Mem and assume, for example, (Mem%trigger t x@1@15 x@1@15), where t is the snapshot of the Mem instance we're unfolding, if t happens to have the form ($Snap.second ($Snap.second s@$)) for any existing snapshot s@$, we will unfold the function definition *including * lots of assumptions about the (essentially arbitrary) snapshot s@$, which are not guarded by any condition about e.g. the precondition of recurse holding for said snapshot. That seems very unsound.

As a result (I believe), the following program verifies but shouldn't (see the assert in fooUnsound):

predicate f(r: Ref)
function getF(r: Ref): Int
    requires f(r)

method setF(r: Ref, v: Int)
    requires f(r)
    ensures f(r) && getF(r) == v


predicate Mem(x: Ref, y: Ref)
{
    f(x) && 0 <= getF(x)
}

predicate nothing() {
  forall r: Ref :: false ==> acc(f(r), 1/2)
}

function recurse(x: Ref): Int
requires nothing()
requires acc(f(x), 1/2)
requires acc(Mem(x, x), wildcard)
{
    (unfolding nothing() in 0) + (unfolding acc(Mem(x, x), wildcard) in getF(x))
}

method fooUnsound(x: Ref)
requires nothing()
requires acc(Mem(x, x), 1/2)
requires acc(f(x), 1/2)
requires getF(x) == 0
ensures  acc(Mem(x, x), 1/2)
{
    var oldResult: Int := recurse(x)
    assert oldResult == 0
    unfold acc(Mem(x, x), 1/2)
    assert false  // succeeds
    setF(x, getF(x) + 1)
    fold acc(Mem(x, x), 1/2)
    assert false
    var newResult: Int := recurse(x) // this call triggers the unsoundness
    assert newResult == 1
}

The solution might simply be to make the entire definitional axiom conditional on the function precondition holding.

[marcoeilers]

Okay, I no longer believe my explanation from above, that actually seems fine as long as the definitional axiom contains only definitions. So maybe the problem is that it doesn't, but that's not clear at all.