If a heap-dependent function which requires a QP in its precondition is used in a trigger, then any method call (that uses resources in its specifications) between a quantifier using the function in its trigger and the usage of the function intended to trigger the quantifier will cause the trigger not to be matched.
The problem is that although the function framing axiom can in principle get the proof to go through, this depends on learning equality between the QP "chunks" before and after the method call; this is in turn implied by an extensionality axiom for the QP "chunk" (the generated "condqp" function one can see in the Boogie output) but that only triggers if the QP was used in both relevant states; here it is only used in one.
Various variations of the example do verify, as indicated also in the comments; the code verifies if one does any of the following:
- remove the intervening method call
- make the function to be frame depend only on non-quantified resources
- explicitly assert the function to be framed before the method call
What does not make the example verify (4.) is to make the method call depend on provably disjoint resources from the function; just changing the heap (via the corresponding exhale/inhale) is enough for the failure.
Silicon verifies all versions of this example, including the original.
I haven't thought up a possible fix yet. One might be to do translate such functions in triggers specially so that the corresponding terms needed for framing get generated (essentially having a variant of the existing axiom trigger on pairs of states if one used the function and the other used the function in a trigger). I'm not sure how this might affect performance for other examples (seems like it might be OK to me, but I could try it). Maybe there are other possibilities (eventually I'd like to think about overhauling the QP framing approach anyway, but that's a longer discussion).
field val : Int
function to_frame(s:Set[Ref], i:Int) : Bool
requires forall r: Ref :: r in s ==> acc(r.val) // 2. removing this
method reads(s:Set[Ref], x:Ref)
requires acc(x.val, 1/2) && !(x in s)
requires forall r: Ref :: r in s ==> acc(r.val, 1/2) // 4. commenting this does *not* get the proof through
ensures acc(x.val, 1/2)
ensures forall r: Ref :: r in s ==> acc(r.val, 1/2) // 4. commenting this does *not* get the proof through
method test(s:Set[Ref], x: Ref)
requires acc(x.val) && !(x in s)
requires forall r: Ref :: r in s ==> acc(r.val)
{
assume forall i:Int :: {to_frame(s,i)} to_frame(s,i)
// assert to_frame(s,42) // 3. adding this
reads(s, x) // 1. removing this
assert to_frame(s,42)
}
If a heap-dependent function which requires a QP in its precondition is used in a trigger, then any method call (that uses resources in its specifications) between a quantifier using the function in its trigger and the usage of the function intended to trigger the quantifier will cause the trigger not to be matched.
The problem is that although the function framing axiom can in principle get the proof to go through, this depends on learning equality between the QP "chunks" before and after the method call; this is in turn implied by an extensionality axiom for the QP "chunk" (the generated "condqp" function one can see in the Boogie output) but that only triggers if the QP was used in both relevant states; here it is only used in one.
Various variations of the example do verify, as indicated also in the comments; the code verifies if one does any of the following:
What does not make the example verify (4.) is to make the method call depend on provably disjoint resources from the function; just changing the heap (via the corresponding exhale/inhale) is enough for the failure.
Silicon verifies all versions of this example, including the original.
I haven't thought up a possible fix yet. One might be to do translate such functions in triggers specially so that the corresponding terms needed for framing get generated (essentially having a variant of the existing axiom trigger on pairs of states if one used the function and the other used the function in a trigger). I'm not sure how this might affect performance for other examples (seems like it might be OK to me, but I could try it). Maybe there are other possibilities (eventually I'd like to think about overhauling the QP framing approach anyway, but that's a longer discussion).