marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Invariants with append #201

Open alex28sh opened 2 months ago

alex28sh commented 2 months ago

Hello, I'm having issues with invariants verification, when append operations are present. For example, I cannot verify 'Invariant(Forall(int, lambda d_2j: (Implies(((0) <= (d_2j)) and ((d_2j) < (d_1i)) and starts__with(xs[d_2j], p, 0), Exists(int, lambda x: x >= 0 and x < len(filtered) and filtered[x] == d_2j)), [[xs[d_2j]]])))' 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 commented 2 months ago

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 commented 2 months ago

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