Loop invariant not preserved when unfolding inside a quantifier

[vakaras]

The following example:

field val: Int

function left(index: Int): Int
    requires index >= 0

function right(index: Int): Int
    requires index >= 0

predicate ArraySegmentTree(data: Seq[Ref], idx: Int) {
    idx >= 0
    && idx < |data|
    && acc(data[idx].val)
    && ( (left(idx) >= 0 && left(idx) < |data| ) ==> ArraySegmentTree(data, left(idx)))
    && ( (right(idx) >= 0 && right(idx) < |data|) ==> ArraySegmentTree(data, right(idx)))
}

method from_array_to_tree(data: Seq[Ref], lo: Int, hi: Int)
    requires |data| > 0
    requires lo >= 0
    requires hi == |data|
    requires hi > lo
    // requires forall k: Int, l: Int :: 0 <= k && k < l && l < |data| ==> data[k] != data[l]
{
    var i: Int := lo
    while (i < hi)
        invariant lo <= i && i <= hi
        // invariant forall k: Int, l: Int :: 0 <= k && k < l && l < |data| ==> data[k] != data[l]
        // invariant forall j: Int :: lo <= j && j < i ==>  acc(data[j].val)
        // invariant forall j: Int :: {data[j]} lo <= j && j < i  ==> data[j].val >= 0
        invariant forall j: Int :: lo <= j && j < i ==> ArraySegmentTree(data, j)
        invariant forall j: Int :: {data[j]} lo <= j && j < i  ==> unfolding ArraySegmentTree(data, j) in data[j].val >= 0
    {
        i := i
    }
}

fails with the following error:

Loop invariant (forall j: Int :: { data[j] } lo <= j && j < i ==> (unfolding acc(ArraySegmentTree(data, j), write) in data[j].val >= 0)) might not be preserved. Assertion (forall j: Int :: { data[j] } lo <= j && j < i ==> (unfolding acc(ArraySegmentTree(data, j), write) in data[j].val >= 0)) might not hold. (x2.vpr@31.19--31.123)

[mschwerhoff]

Could have the same root cause as issue #228.

[vakaras]

If I understand #228 correctly, putting the unfolding into a function call should help, right? However, the following still fails with the same error:

field val: Int

function left(index: Int): Int
    requires index >= 0

function right(index: Int): Int
    requires index >= 0

predicate ArraySegmentTree(data: Seq[Ref], idx: Int) {
    idx >= 0
    && idx < |data|
    && acc(data[idx].val)
    && ( (left(idx) >= 0 && left(idx) < |data| ) ==> ArraySegmentTree(data, left(idx)))
    && ( (right(idx) >= 0 && right(idx) < |data|) ==> ArraySegmentTree(data, right(idx)))
}

function get_val(data: Seq[Ref], idx: Int): Int
    requires ArraySegmentTree(data, idx)
{
    unfolding ArraySegmentTree(data, idx) in data[idx].val
}

method from_array_to_tree(data: Seq[Ref], lo: Int, hi: Int)
    requires |data| > 0
    requires lo >= 0
    requires hi == |data|
    requires hi > lo
{
    var i: Int := lo
    while (i < hi)
        invariant lo <= i && i <= hi
        invariant forall j: Int :: lo <= j && j < i ==> ArraySegmentTree(data, j)
        invariant forall j: Int :: {get_val(data, j)} lo <= j && j < i  ==> get_val(data, j) >= 0
    {
        i := i
    }
}

EDIT: Interestingly, if I change the trigger to {data[j]}, then it succeeds.