Invariants with append

[alex28sh]

Hello, I'm having issues with invariants verification, when append operations are present. For example, I cannot verify 'Invariant(Forall(int, lambda d_2_j_:
(Implies(((0) <= (d_2_j_)) and ((d_2_j_) < (d_1_i_)) and starts__with(xs[d_2_j_], p, 0),
Exists(int, lambda x: x >= 0 and x < len(filtered) and filtered[x] == d_2_j_)),
[[xs[d_2_j_]]])))'
How can such issues be resolved?

@Pure
def starts__with(s : List[int], p : List[int], i : int) -> bool :
    Requires(Acc(list_pred(s), 1/2))
    Requires(Acc(list_pred(p), 1/2))
    Requires(i >= 0 and i <= len(p) and i <= len(s))
    Ensures(Implies(len(p) == i and len(s) >= len(p), Result()))
    Ensures(Implies(len(s) < len(p), not Result()))
    return len(s) >= len(p) and Forall(int, lambda x: Implies(x >= i and x < len(p), s[x] == p[x]))

def filter__by__prefix(xs : List[List[int]], p : List[int]) -> List[int]:
    Requires(Acc(list_pred(xs)))
    Requires(Acc(list_pred(p)))
    Requires(Forall(xs, lambda x : Acc(list_pred(x))))
    Ensures(Acc(list_pred(p)))
    Ensures(Acc(list_pred(xs)))
    Ensures(Acc(list_pred(Result())))
    filtered = list([int(0)] * 0) # type : List[int]
    d_1_i_ = int(0) # type : int
    d_1_i_ = 0
    while (d_1_i_) < (len(xs)):
        Invariant(Acc(list_pred(filtered)))
        Invariant(Acc(list_pred(xs), 1/2))
        Invariant(Acc(list_pred(p), 1/2))
        Invariant(((0) <= (d_1_i_)) and ((d_1_i_) <= (len(xs))))
        Invariant(Forall(xs, lambda x : Acc(list_pred(x))))
        Invariant(Forall(int, lambda d_2_j_: Implies(d_2_j_ >= 0 and d_2_j_ < len(filtered), filtered[d_2_j_] >= 0 and filtered[d_2_j_] < d_1_i_)))
        Invariant(Forall(int, lambda d_2_j_:
            (Implies(((0) <= (d_2_j_)) and ((d_2_j_) < (d_1_i_)) and starts__with(xs[d_2_j_], p, 0), 
                    Exists(int, lambda x: x >= 0 and x < len(filtered) and filtered[x] == d_2_j_)), 
            [[xs[d_2_j_]]])))
        if starts__with((xs)[d_1_i_], p, 0):
            filtered = (filtered) + [d_1_i_]
        d_1_i_ = (d_1_i_) + (1)
    return filtered

[marcoeilers]

Hi!
I can maybe have a closer look tonight, but in general, Forall-Exists properties are hard to prove in SMT-based verifiers, because essentially the prover has to automatically find some value x for each d_2_j s.t. the property holds.
One way to make it easier is to is to give that value to the prover explicitly. So you could maintain some additional sequence or map of values that contains, for each d_2_j, the relevant x, and then rewrite the existential using that value.

[alex28sh]

Actually, I solved this issue by wrapping Exists(int, lambda x: x >= 0 and x < len(filtered) and filtered[x] == d_2_j_) into a separate pure function