Unrelated fold removes knowledge of quantifier with predicate unside

[sakehl]

The following program does not verify. Whilst if you remove fold acc(hide1(x1, n, i),1/2) from line 21, it does verify. And I believe that line 21 should be unrelated to the given verification failure:

Silicon 1.1-SNAPSHOT (ad3593f7)
Silicon found 1 error in 3.18s:
  [0] Assert might fail. Assertion (forall j: Int :: { hide0(x0, n, j) } 0 <= j && j < n ==> (unfolding acc(hide0(x0, n, j), write) in aloc(x0, j).int) == 0) might not hold. (qpreds_quant1.vpr@23.11--25.56)

File

method main1(tid: Int, n: Int, x0: Array, x1: Array, i: Int)
  requires x0 != x1
  requires alen(x0) == n && alen(x1) == n
  requires (forall j: Int :: { hide0(x0,n,j) }
          0 <= j && j < n ==> acc(hide0(x0,n,j), write)
  )
  requires (forall j: Int ::
          { hide1(x1,n,j) }
          0 <= j && j < n ==> acc(hide1(x1,n,j), 1/2)
  )
  requires (forall j: Int :: { hide0(x0,n,j) }
          0 <= j && j < n ==> (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)
  
  requires i >= 0 && i < n
{
  assert (forall j: Int :: { hide0(x0,n,j) }
      0 <= j && j < n ==>
      (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)

  unfold acc(hide1(x1, n, i),1/2)
  fold acc(hide1(x1, n, i),1/2)

  assert (forall j: Int :: { hide0(x0,n,j) }
      0 <= j && j < n ==>
      (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)
}


////////////////////////// Other functions 
domain Array  {

  function array_loc(a: Array, i: Int): Ref 

  function alen(a: Array): Int 

  function loc_inv_1(loc: Ref): Array 

  function loc_inv_2(loc: Ref): Int 

  axiom {
    (forall a: Array, i: Int ::
      { array_loc(a, i) }
      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
  }

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

field int: Int

predicate hide0(x: Array, n: Int, i: Int) {
  n > 0 && i >= 0 && i < n && alen(x) == n &&
  acc(aloc(x, i).int, write)
}

predicate hide1(x: Array, n: Int, i: Int) { 
  n > 0 && i >= 0 && i < n && alen(x) == n && 
  acc(aloc(x, i).int, write)
}


function aloc(a: Array, i: Int): Ref
  requires 0 <= i
  requires i < alen(a)
  decreases 
  ensures loc_inv_1(result) == a
  ensures loc_inv_2(result) == i
{
  array_loc(a, i)
}

[sakehl]

Additionally, if you write

assert (forall j: Int :: { aloc(x0, j) }
      0 <= j && j < n ==>
      (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)

I.e. For the trigger of the quantifier, you use the function inside the unfolding.

In this case, the quantifier does not seem to trigger at all.

Although maybe this is just not allowed and fine, was not sure about this.

[marcoeilers]

Apparently this was also fixed by PR #846 (although there are some fundamental issues here that we're essentially just working around with a bunch of caching).