Incompleteness when unfolding a predicate under a quantifier.

[viper-admin]

Created by @vakaras on 2018-07-23 16:31

In the example below, the second call to fails fails with an error that the precondition loc(fruits, j).val) >= 0 does not hold. However, if unfolding is pulled out to be the top level expression (method works), the example verifies successfully.

#!silver
field val: Int
domain Array {
    function loc(arr: Array, pos: Int): Ref
    function len(arr: Array): Int
    function arrayref(ref: Ref): Array
    function arraypos(ref: Ref): Int
    axiom len_nonneg {
        forall a: Array :: {len(a)} len(a) >= 0
    }
    axiom array_diff {
        forall a: Array, p: Int :: {loc(a, p)} arrayref(loc(a, p)) == a && arraypos(loc(a, p)) == p
    }
}

predicate arrayacc(a: Array) {
    forall i: Int :: { loc(a, i) } 0 <= i && i < len(a) ==> acc(loc(a, i).val)
}

method fails(fruits: Array, rdperm: Perm)
    requires none < rdperm && rdperm < write
    requires acc(arrayacc(fruits), rdperm)
    requires forall j: Int :: { loc(fruits, j) } 0 <= j && j < len(fruits) ==>
        (unfolding acc(arrayacc(fruits), rdperm) in loc(fruits, j).val) >= 0
{
    fails(fruits, rdperm / 2)
    //:: UnexpectedError: precondition does not hold.
    fails(fruits, rdperm / 2)
}

method works(fruits: Array, rdperm: Perm)
    requires none < rdperm && rdperm < write
    requires acc(arrayacc(fruits), rdperm)
    requires unfolding acc(arrayacc(fruits), rdperm) in
        forall j: Int :: { loc(fruits, j) } 0 <= j && j < len(fruits) ==>
        (loc(fruits, j).val) >= 0
{
    works(fruits, rdperm / 2)
    works(fruits, rdperm / 2)
}

[gauravpartha]

Here is another incompleteness with unfolding within a quantifier (havoc_qp5.vpr from the quasihavoc examples in the Silver tes suite after desugaring quasihavoc to exhale + inhale), where the assertion fails to verify:

method foo(x: Ref, y: Ref, s: Seq[Ref], t: Seq[Ref])
    requires |s| == |t| && |s| >= 2
    requires forall i: Int, j: Int :: 0 <= i && i < j && j < |s| ==> s[i] != s[j]
    requires forall i: Int :: 0 <= i && i < |s| ==>
                Pair(s[i], t[i])
    requires forall i: Int :: 0 <= i && i < |s| ==>
                unfolding Pair(s[i], t[i]) in s[i].f == i
    requires x == s[0] && y == t[0]
{
    exhale acc(Pair(x,y))
    inhale acc(Pair(x,y))
    unfold Pair(x, y)

    assert forall i: Int :: 1 <= i && i < |s| ==>
            unfolding Pair(s[i], t[i]) in s[i].f == i
}