Quantifier with predicates/predicates with quantifiers interfere with each other
sakehl opened this issue · 4 comments
Hi, maybe I am understanding something incorrectly, but otherwise this might be a bug?
The following program does not verify. And it uses a predicate, and quantifies over this predicate.
However, in another program, which tries to do the same, but the quantifier is moved inside the predicate, it does verify. (Which I included below)
Using the Stable silicon version from the Viper IDE.
Code which does not verify
predicate arrR(x: Int, a: Option[Array], n: Int) {
a != (none1(): Option[Array]) && alen(optGet1(a)) == n && 0 <= x && x < n &&
acc(aloc(optGet1(a), x).int, write)
}
predicate arr(a: Option[Array], n: Int) {
a != (none1(): Option[Array]) && alen(optGet1(a)) == n &&
(forall i: Int ::
{ aloc(optGet1(a), i) }
0 <= i && i < alen(optGet1(a)) ==> acc(aloc(optGet1(a), i).int, write))
}
method main(tid: Int, n: Int, x0: Option[Array], x1: Option[Array], x2: Option[Array])
requires 0 < n
requires acc(arr(x1, n), write/2)
requires acc(arr(x2, n), write/2)
requires (forall j: Int ::
{ aloc(optGet1(x1), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x1, n), write/2) in
aloc(optGet1(x1), j).int) ==
j)
requires (forall j: Int ::
{ aloc(optGet1(x2), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x2, n), write/2) in
aloc(optGet1(x2), j).int) ==
2 * j)
requires (forall i: Int ::
{ arrR(i, x0, n) }
0 <= i && i < n ==> acc(arrR(i, x0, n), write))
ensures 0 < n
ensures acc(arr(x1, n), write/2)
ensures acc(arr(x2, n), write/2)
ensures (forall j: Int ::
{ aloc(optGet1(x1), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x1, n), write/2) in
aloc(optGet1(x1), j).int) ==
j)
ensures (forall j: Int ::
{ aloc(optGet1(x2), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x2, n), write/2) in
aloc(optGet1(x2), j).int) ==
2 * j)
ensures (forall i: Int ::
{ arrR(i, x0, n) }
0 <= i && i < n ==> acc(arrR(i, x0, n), write))
ensures (forall j: Int ::
{ aloc(optGet1(x0), j) }
0 <= j && j < n ==>
(unfolding acc(arrR(j, x0, n), write) in aloc(optGet1(x0), j).int) ==
3 * j)
{
{
var i: Int
var a1: Int
var a2: Int
i := 0
while (i < n)
invariant 0 < n
invariant acc(arr(x1, n), write/2)
invariant acc(arr(x2, n), write/2)
invariant (forall j: Int ::
{ aloc(optGet1(x1), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x1, n), write/2) in
aloc(optGet1(x1), j).int) ==
j)
invariant (forall j: Int ::
{ aloc(optGet1(x2), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x2, n), write/2) in
aloc(optGet1(x2), j).int) ==
2 * j)
invariant 0 <= i && i < n + 1
invariant (forall i1: Int ::
{ arrR(i1, x0, n) }
0 <= i1 && i1 < n ==> acc(arrR(i1, x0, n), write))
invariant (forall j: Int ::
{ aloc(optGet1(x0), j) } {arrR(j, x0, n)}
0 <= j && j < i ==>
(unfolding acc(arrR(j, x0, n), write) in
aloc(optGet1(x0), j).int) ==
3 * j)
{
unfold acc(arr(x1, n), write/2)
a1 := aloc(optGet1(x1), i).int
fold acc(arr(x1, n), write/2)
unfold acc(arr(x2, n), write/2)
a2 := aloc(optGet1(x2), i).int
fold acc(arr(x2, n), write/2)
unfold acc(arrR(i, x0, n), write)
aloc(optGet1(x0), i).int := a1 + a2
fold acc(arrR(i, x0, n), write)
i := i + 1
}
}
}
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)
}
}
domain Option[T1] {
function none1(): Option[T1]
function some(x: T1): Option[T1]
function option_get(opt: Option[T1]): T1
axiom {
(forall x: T1 ::
{ (some(x): Option[T1]) }
(none1(): Option[T1]) != (some(x): Option[T1]))
}
axiom {
(forall x: T1 ::
{ (some(x): Option[T1]) }
(option_get((some(x): Option[T1])): T1) == x)
}
axiom {
(forall opt: Option[T1] ::
{ (some((option_get(opt): T1)): Option[T1]) }
(some((option_get(opt): T1)): Option[T1]) == opt)
}
}
field int: Int
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)
}
function optGet1(opt: Option[Array]): Array
requires opt != (none1(): Option[Array])
decreases
ensures (some(result): Option[Array]) == opt
{
(option_get(opt): Array)
}
Code which does verify
predicate arrR(x: Int, a: Option[Array], n: Int) {
a != (none1(): Option[Array]) && alen(optGet1(a)) == n && 0 <= x && x < n &&
acc(aloc(optGet1(a), x).int, write)
}
predicate arr(a: Option[Array], n: Int) {
a != (none1(): Option[Array]) && alen(optGet1(a)) == n &&
(forall i: Int ::
{ aloc(optGet1(a), i) }
0 <= i && i < alen(optGet1(a)) ==> acc(aloc(optGet1(a), i).int, write))
}
method main(tid: Int, n: Int, x0: Option[Array], x1: Option[Array], x2: Option[Array])
requires 0 < n
requires acc(arr(x1, n), write/2)
requires acc(arr(x2, n), write/2)
requires (forall j: Int ::
{ aloc(optGet1(x1), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x1, n), write/2) in
aloc(optGet1(x1), j).int) ==
j)
requires (forall j: Int ::
{ aloc(optGet1(x2), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x2, n), write/2) in
aloc(optGet1(x2), j).int) ==
2 * j)
requires acc(arr(x0, n), write)
ensures 0 < n
ensures acc(arr(x1, n), write/2)
ensures acc(arr(x2, n), write/2)
ensures (forall j: Int ::
{ aloc(optGet1(x1), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x1, n), write/2) in
aloc(optGet1(x1), j).int) ==
j)
ensures (forall j: Int ::
{ aloc(optGet1(x2), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x2, n), write/2) in
aloc(optGet1(x2), j).int) ==
2 * j)
ensures acc(arr(x0, n), write)
ensures (forall j: Int ::
{ aloc(optGet1(x0), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x0, n), write) in aloc(optGet1(x0), j).int) ==
3 * j)
{
{
var i: Int
var a1: Int
var a2: Int
i := 0
while (i < n)
invariant 0 < n
invariant acc(arr(x1, n), write/2)
invariant acc(arr(x2, n), write/2)
invariant (forall j: Int ::
{ aloc(optGet1(x1), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x1, n), write/2) in
aloc(optGet1(x1), j).int) ==
j)
invariant (forall j: Int ::
{ aloc(optGet1(x2), j) }
0 <= j && j < n ==>
(unfolding acc(arr(x2, n), write/2) in
aloc(optGet1(x2), j).int) ==
2 * j)
invariant 0 <= i && i < n + 1
invariant acc(arr(x0, n), write)
invariant (forall j: Int ::
{ aloc(optGet1(x0), j) }
0 <= j && j < i ==>
(unfolding acc(arr(x0, n), write) in
aloc(optGet1(x0), j).int) ==
3 * j)
{
unfold acc(arr(x1, n), write/2)
a1 := aloc(optGet1(x1), i).int
fold acc(arr(x1, n), write/2)
unfold acc(arr(x2, n), write/2)
a2 := aloc(optGet1(x2), i).int
fold acc(arr(x2, n), write/2)
unfold acc(arr(x0, n), write)
aloc(optGet1(x0), i).int := a1 + a2
fold acc(arr(x0, n), write)
i := i + 1
}
}
}
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)
}
}
domain Option[T1] {
function none1(): Option[T1]
function some(x: T1): Option[T1]
function option_get(opt: Option[T1]): T1
axiom {
(forall x: T1 ::
{ (some(x): Option[T1]) }
(none1(): Option[T1]) != (some(x): Option[T1]))
}
axiom {
(forall x: T1 ::
{ (some(x): Option[T1]) }
(option_get((some(x): Option[T1])): T1) == x)
}
axiom {
(forall opt: Option[T1] ::
{ (some((option_get(opt): T1)): Option[T1]) }
(some((option_get(opt): T1)): Option[T1]) == opt)
}
}
field int: Int
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)
}
function optGet1(opt: Option[Array]): Array
requires opt != (none1(): Option[Array])
decreases
ensures (some(result): Option[Array]) == opt
{
(option_get(opt): Array)
}
So I still am running into this problem, but I've tried to minimize the example. The code below does not verify.
However if you remove the unrelated quantifier
requires (forall j: Int :: { aloc(x1, j) }
0 <= j && j < 10 ==> (unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int) == j)
from the requirements, it does verify. So the quantifiers seem to interfere with each other.
This code does not work
method test(x0: Array, x1:Array)
requires (forall j: Int :: {arrR(j, x0, 10)} 0 <= j && j < 10 ==> arrR(j, x0, 10))
requires arr(x1, 10)
requires (forall j: Int :: { aloc(x1, j) }
0 <= j && j < 10 ==> (unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int) == j)
requires (forall j: Int :: { aloc(x0, j) }
0 <= j && j < 10 ==> (unfolding arrR(j, x0, 10) in aloc(x0, j).int == 3 * j))
{
assert (unfolding arrR(0, x0, 10) in
aloc(x0, 0).int == 3 * 0)
}
predicate arrR(x: Int, a: Array, n: Int) {
alen(a) == n && 0 <= x && x < n && acc(aloc(a, x).int, write)
}
predicate arr(a: Array, n: Int) {
alen(a) == n && (forall i: Int :: { aloc(a, i) } 0 <= i && i < alen(a) ==> acc(aloc(a, i).int, write))
}
field int: Int
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)
}
}
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)
}
Part of the reason this happens is that arr
contains a quantified permission for field int
, and as a result, unfolding arr
in test
forces the use of Silicon's quantified permission algorithm for all usages of the int
field inside test
(when without that unfolding, there is no quantified permission for int
anywhere in test
, and it can use the simpler algorithm for non-quantified resources).
Then, for some reason, the QP algorithm seems to be incomplete in this setting, which it obviously shouldn't be. I'll try to figure out why.
Edit: A simple workaround would be to move the unfolding of arr
to a function (i.e., write a getter function that returns unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int
) and call that function from test
, which would allow Silicon to keep using the simpler non-QP algorithm in test
and avoid the incompleteness.
Also, thanks a lot for the minimized example!
PR #840 fixes the underlying issue.
Awesome, thanks a lot!