Unrelated fold removes knowledge of quantifier with predicate unside
Opened this issue · 2 comments
sakehl commented
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 commented
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 commented
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).