viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

Some plugin interactions seem to be broken in ViperServer #184

Closed marcoeilers closed 10 months ago

marcoeilers commented 10 months ago

The following program verifies with standard Silicon and Carbon, but does not verify in VSCode (with an up to date version of Viper):

adt List[T] {
    Nil()
    Cons(elem: T, next: List[T])
}

adt Pair[S,T] {
    MkPair(fst: S, snd: T)
}

domain ListDomain[T] {
    function length(List[T]): Int

    axiom {
        length((Nil(): List[T])) == 0
    }

    axiom {
        forall l: List[T], e: T :: length(Cons(e, l)) == 1 + length(l)
    }
}

method zip(l1: List[Int], l2: List[Int]) returns (res: List[Pair[Int, Int]])
    decreases l1
    ensures length(l1) == length(l2) ==> length(res) == length(l1)
{

    if(l1 == Nil() || l2 == Nil()) {
        res := Nil()
    } else {
        var rest: List[Pair[Int, Int]] := zip(l1.next, l2.next)
        res := Cons(MkPair(l1.elem, l2.elem), rest)
    }
}

I'm reasonably sure that the problem is that the ADT plugin does not generate the well-foundedness axioms for the List type, and that may be because it does not get a config object that says that the termination plugin is active. So this seems potentially related to #165.

marcoeilers commented 10 months ago

Fixed in #186