Suboptimal behaviour with quantifiers — better autotriggers possible?

[mschwerhoff]

The following example was originally reported by @bobismijnnaam as Silicon issue #574. Observe that requires-clause and assert-statement contain literally the same assertion.

domain VectorIndex {

  function vrange(lo: Int, hi: Int): VectorIndex
}

domain VectorExpression[T] {

  function vseq(xs: Seq[T]): VectorExpression[T]

  function vsum(is: VectorIndex, xs: VectorExpression[T]): T

} 

//  a field 
field variance: Int

method query(calculatorSpec: Ref)
  requires calculatorSpec != null
  requires acc(calculatorSpec.variance, 1/2)
  requires (exists xs: Seq[Int] :: 
    (0 < |xs| 
      ==> (exists varredXs: Seq[Int] ::
          |varredXs| == |xs| 
          && 
          (
            (forall i: Int :: 0 <= i && i < |xs| ==> varredXs[i] == xs[i]) 
              && 
              calculatorSpec.variance == vsum(vrange(0, |xs|), vseq(varredXs))
              )
              ) 
      ))
{
  assert  
    (exists xs: Seq[Int] :: 
      (0 < |xs| 
        ==> (exists varredXs: Seq[Int] ::
            |varredXs| == |xs| 
            && 
            (
              (forall i: Int :: 0 <= i && i < |xs| ==> varredXs[i] == xs[i]) 
                && 
                calculatorSpec.variance == vsum(vrange(0, |xs|), vseq(varredXs))
                )
                ) 
        ))
}

As is, both Silicon and Carbon fail to verify the code. Adding triggers to both expressions (requires-clause and assert-statement) helps:

exists xs: Seq[Int] :: {|xs|}
  ...
  exists varredXs: Seq[Int] :: {|varredXs|}
    ...
    forall i: Int :: {varredXs[i]}{xs[i]} ...

I haven't had a closer look yet. Neither at the resulting Z3/Boogie code, nor at which triggers are strictly necessary to make the example verify.

Since the assertions are syntactically identical (and no heap or other updates happen in between), it is a bit unfortunate that the example doesn't verify directly. Maybe we can do better here. E.g. I'm not sure if we compute triggers for existentials, if none are provided.

[bobismijnnaam]

From my brief prodding of the example including triggers, only the triggers on the existentials in the requires clause are necessary for viper to verify the example.