Incompleteness: Asserting a syntactically identical assertion fails

[ArquintL]

In the following example, the asserted assertion in UseStepsSamePackage and UseStepsSamePackage2 is syntactically identical to the postcondition of the immediately preceding call and the immediately preceding inhale stmt, resp.
However, SE and VCG both fail to verify the assert stmt.

Moving the existential into a heap-dependent function solves the issue as a workaround.

function Add_pure(x: Int, y: Int): Int
{
    x + y
}

method ComputeSteps(target: Int) returns (r1: Array)
  requires target >= 0
  ensures array_perm(r1, write)
  ensures len(r1) > 0
  ensures forall t2: Int :: { Add_pure(target, t2) } exists idx: Int :: { at(r1, idx) } target < t2 ==> 0 <= idx && idx < len(r1) && Add_pure(target, t2) == at(r1, idx) + t2
{
  r1 := NewArray(1)
  at(r1, 0) := target
}

method UseStepsSamePackage(target: Int)
requires 0 <= target
{
    var r1: Array
	r1 := ComputeSteps(target)
	assert forall t2: Int :: { Add_pure(target, t2) } exists idx: Int :: { at(r1, idx) } target < t2 ==> 0 <= idx && idx < len(r1) && Add_pure(target, t2) == at(r1, idx) + t2
}

method UseStepsSamePackage2(target: Int)
requires 0 <= target
{
    var r1: Array
	inhale array_perm(r1, write)
    inhale len(r1) > 0
    inhale forall t2: Int :: { Add_pure(target, t2) } exists idx: Int :: { at(r1, idx) } target < t2 ==> 0 <= idx && idx < len(r1) && Add_pure(target, t2) == at(r1, idx) + t2
	assert forall t2: Int :: { Add_pure(target, t2) } exists idx: Int :: { at(r1, idx) } target < t2 ==> 0 <= idx && idx < len(r1) && Add_pure(target, t2) == at(r1, idx) + t2
}

// taken from https://viper.ethz.ch/examples/arraylist-quantified-permissions.html
domain Pair[T1,T2] {
  function first(p : Pair[T1,T2]): T1
  function second(p: Pair[T1,T2]): T2
}

domain Array {
  function loc(a: Array, i: Int): Ref
  function len(a: Array): Int
  function inv_loc(r:Ref) : Pair[Array,Int]

  axiom loc_injective {
    forall a: Array, i: Int :: {loc(a, i)}
      0 <= i && i < len(a) ==>
      first(inv_loc(loc(a, i))) == a && second(inv_loc(loc(a, i))) == i
  }

  axiom length_nonneg {
    forall a: Array :: len(a) >= 0
  }
}

field val: Int

define at(a, i) (loc(a, i).val)
define array_perm(a, p) (forall i: Int :: {at(a, i)} 0 <= i && i < len(a) ==> acc(at(a, i), p))

method NewArray(length: Int) returns (a: Array)
requires 0 <= length
ensures  array_perm(a, write)
ensures  len(a) == length
{
    // get arb array
    var arbArray: Array
    a := arbArray
    inhale len(a) == length
    inhale forall i:Int :: 0 <= i && i < len(a) ==> acc(loc(a,i).val)
}

[marcoeilers]

I don't think Viper can do much about this; this is basically just a limitation of e-matching.
To get this to verify, you basically need to move the triggering term for the outer forall out of the existential, so that the forall is triggered immediately, and then make sure that the assumed existential triggers the inner forall in the assertion you're proving.

This here verifies:

method UseStepsSamePackage2(target: Int)
requires 0 <= target
{
    var r1: Array
	inhale array_perm(r1, write)
    inhale len(r1) > 0
    inhale forall t3: Int :: { Add_pure(target, t3) } target < t3 ==> exists idx: Int :: { at(r1, idx) }  0 <= idx && idx < len(r1) && Add_pure(target, t3) == at(r1, idx) + t3
    var t2: Int
    assert  let t2sum == (Add_pure(target, t2)) in target < t2 ==> exists idx: Int :: { at(r1, idx) }  0 <= idx && idx < len(r1) && t2sum == at(r1, idx) + t2
}

(The t2sum is extracted to always trigger the forall, and I have to phrase the proof obligation about a specific variable for some reason, and move the target < t2 implication for some reason I don't understand.)

[ArquintL]

Thanks so much! That's very insightful =)