stainless
stainless copied to clipboard
epfl-lara
Function equivalence with comparefuns crashes
Hi @drganam @vkuncak, can Stainless generate equivalence lemmas for functions when one of the function calls other functions? (here replace vs slowReplace).
I get a crash on this example (from a FV student)
stainless Test.scala --solvers=smt-z3 --timeout=10 --comparefuns=replace --models=slowReplace --batched --debug=trees --debug-phases=Trace
import stainless.collection._
object Test {
def split[T](l: List[T], x: T): List[List[T]] = l match {
case Nil() => List[List[T]](List[T]())
case Cons(y, ys) if x == y =>
Nil[T]() :: split(ys, x)
case Cons(y, ys) =>
val r = split(ys, x)
(y :: r.head) :: r.tail
}
def join[T](ll: List[List[T]], l: List[T]): List[T] = ll match {
case Nil() => Nil[T]()
case Cons(l1, Nil()) => l1 // if you miss this case, Stainless finds a counter-example to theorem
case Cons(l1, ls) => l1 ++ l ++ join(ls, l)
}
def replace[T](l1: List[T], x: T, l2: List[T]): List[T] = l1 match {
case Nil() => Nil[T]()
case Cons(y, ys) if x == y => l2 ++ replace(ys, x, l2)
case Cons(y, ys) => y :: replace(ys, x, l2)
}
def theorem[T](l1: List[T], x: T, l2: List[T]): Unit = {
if (!l1.isEmpty) theorem(l1.tail, x, l2) // recursive proof
}.ensuring(_ =>
join(split(l1, x), l2) == replace(l1, x, l2)
)
// could be checked for equivalence with `replace` thanks to --comparefuns
def slowReplace[T](l1: List[T], x: T, l2: List[T]): Unit = join(split(l1, x), l2)
}
stainless Test.scala --solvers=smt-z3 --timeout=10 --comparefuns=replace --models=slowReplace --batched --debug=trees
Show output
[ Debug ] Symbols before Trace
[ Debug ]
[ Debug ] -------------Functions-------------
[ Debug ] @library
[ Debug ] def head[T](thiss: List[T]): T = {
[ Debug ] require(@ghost (thiss \u2260 Nil[T]()))
[ Debug ] thiss match {
[ Debug ] case Cons(h, _) =>
[ Debug ] h
[ Debug ] }
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def isEmpty[T](thiss: List[T]): Boolean = thiss match {
[ Debug ] case Nil() =>
[ Debug ] true
[ Debug ] case _ =>
[ Debug ] false
[ Debug ] }
[ Debug ]
[ Debug ] def join[T](ll: List[List[T]], l: List[T]): List[T] = ll match {
[ Debug ] case Nil() =>
[ Debug ] Nil[T]()
[ Debug ] case Cons(l1, Nil()) =>
[ Debug ] l1
[ Debug ] case Cons(l1, ls) =>
[ Debug ] ++[T](++[T](l1, l), join[T](ls, l))
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def ++[T](thiss: List[T], that: List[T]): List[T] = {
[ Debug ] thiss match {
[ Debug ] case Nil() =>
[ Debug ] that
[ Debug ] case Cons(x, xs) =>
[ Debug ] Cons[T](x, ++[T](xs, that))
[ Debug ] }
[ Debug ] } ensuring {
[ Debug ] (res: List[T]) => @ghost ((content[T](res) == content[T](thiss) \u222A content[T](that) && size[T](res) == size[T](thiss) + size[T](that)) && (that \u2260 Nil[T]() || res == thiss))
[ Debug ] }
[ Debug ]
[ Debug ] def replace[T](l1: List[T], x: T, l2: List[T]): List[T] = l1 match {
[ Debug ] case Nil() =>
[ Debug ] Nil[T]()
[ Debug ] case Cons(y, ys) if x == y =>
[ Debug ] ++[T](l2, replace[T](ys, x, l2))
[ Debug ] case Cons(y, ys) =>
[ Debug ] val rassoc$4: T = y
[ Debug ] ::[T](replace[T](ys, x, l2), rassoc$4)
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def size[T](thiss: List[T]): BigInt = {
[ Debug ] thiss match {
[ Debug ] case Nil() =>
[ Debug ] 0
[ Debug ] case Cons(h, t) =>
[ Debug ] 1 + size[T](t)
[ Debug ] }
[ Debug ] } ensuring {
[ Debug ] (x$1: BigInt) => @ghost (x$1 >= 0)
[ Debug ] }
[ Debug ]
[ Debug ] def split[T](l: List[T], x: T): List[List[T]] = l match {
[ Debug ] case Nil() =>
[ Debug ] Cons[List[T]](Nil[T](), Nil[List[T]]())
[ Debug ] case Cons(y, ys) if x == y =>
[ Debug ] val rassoc$1: List[T] = {
[ Debug ] val rassoc$1: List[T] = Nil[T]()
[ Debug ] assert(rassoc$1 is Nil, "Inner refinement lifting")
[ Debug ] rassoc$1
[ Debug ] }
[ Debug ] ::[List[T]](split[T](ys, x), rassoc$1)
[ Debug ] case Cons(y, ys) =>
[ Debug ] val r: List[List[T]] = split[T](ys, x)
[ Debug ] val rassoc$2: T = y
[ Debug ] val rassoc$3: List[T] = ::[T](head[List[T]](r), rassoc$2)
[ Debug ] ::[List[T]](tail[List[T]](r), rassoc$3)
[ Debug ] }
[ Debug ]
[ Debug ] def slowReplace[T](l1: List[T], x: T, l2: List[T]): Unit = {
[ Debug ] val tmp: List[T] = join[T](split[T](l1, x), l2)
[ Debug ] ()
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def ::[T](thiss: List[T], t: T): List[T] = Cons[T](t, thiss)
[ Debug ]
[ Debug ] @library
[ Debug ] def content[T](thiss: List[T]): Set[T] = thiss match {
[ Debug ] case Nil() =>
[ Debug ] {}
[ Debug ] case Cons(h, t) =>
[ Debug ] {h} \u222A content[T](t)
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def tail[T](thiss: List[T]): List[T] = {
[ Debug ] require(@ghost (thiss \u2260 Nil[T]()))
[ Debug ] thiss match {
[ Debug ] case Cons(_, t) =>
[ Debug ] t
[ Debug ] }
[ Debug ] }
[ Debug ]
[ Debug ] def theorem[T](l1: List[T], x: T, l2: List[T]): Unit = {
[ Debug ] if (\u00ACisEmpty[T](l1)) {
[ Debug ] theorem[T](tail[T](l1), x, l2)
[ Debug ] } else {
[ Debug ] ()
[ Debug ] }
[ Debug ] } ensuring {
[ Debug ] (x$1: Unit) => join[T](split[T](l1, x), l2) == replace[T](l1, x, l2)
[ Debug ] }
[ Debug ]
[ Debug ] -------------Sorts-------------
[ Debug ] @library
[ Debug ] abstract class List[T]
[ Debug ] case class Nil[T]() extends List[T]
[ Debug ] case class Cons[T](h: T, t: List[T]) extends List[T]
[ Debug ]
[ Debug ] @synthetic
[ Debug ] abstract class Object
[ Debug ] case class Open(value: BigInt) extends Object
[ Debug ]
[ Debug ]
[ Debug ]
[ Debug ]
[ Debug ] Symbols after Trace
[ Debug ]
[ Debug ] -------------Functions-------------
[ Debug ] @library
[ Debug ] def head[T](thiss: List[T]): T = {
[ Debug ] require(@ghost (thiss \u2260 Nil[T]()))
[ Debug ] thiss match {
[ Debug ] case Cons(h, _) =>
[ Debug ] h
[ Debug ] }
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def isEmpty[T](thiss: List[T]): Boolean = thiss match {
[ Debug ] case Nil() =>
[ Debug ] true
[ Debug ] case _ =>
[ Debug ] false
[ Debug ] }
[ Debug ]
[ Debug ] def join[T](ll: List[List[T]], l: List[T]): List[T] = ll match {
[ Debug ] case Nil() =>
[ Debug ] Nil[T]()
[ Debug ] case Cons(l1, Nil()) =>
[ Debug ] l1
[ Debug ] case Cons(l1, ls) =>
[ Debug ] ++[T](++[T](l1, l), join[T](ls, l))
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def ++[T](thiss: List[T], that: List[T]): List[T] = {
[ Debug ] thiss match {
[ Debug ] case Nil() =>
[ Debug ] that
[ Debug ] case Cons(x, xs) =>
[ Debug ] Cons[T](x, ++[T](xs, that))
[ Debug ] }
[ Debug ] } ensuring {
[ Debug ] (res: List[T]) => @ghost ((content[T](res) == content[T](thiss) \u222A content[T](that) && size[T](res) == size[T](thiss) + size[T](that)) && (that \u2260 Nil[T]() || res == thiss))
[ Debug ] }
[ Debug ]
[ Debug ] def replace[T](l1: List[T], x: T, l2: List[T]): List[T] = l1 match {
[ Debug ] case Nil() =>
[ Debug ] Nil[T]()
[ Debug ] case Cons(y, ys) if x == y =>
[ Debug ] ++[T](l2, replace[T](ys, x, l2))
[ Debug ] case Cons(y, ys) =>
[ Debug ] val rassoc$4: T = y
[ Debug ] ::[T](replace[T](ys, x, l2), rassoc$4)
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def size[T](thiss: List[T]): BigInt = {
[ Debug ] thiss match {
[ Debug ] case Nil() =>
[ Debug ] 0
[ Debug ] case Cons(h, t) =>
[ Debug ] 1 + size[T](t)
[ Debug ] }
[ Debug ] } ensuring {
[ Debug ] (x$1: BigInt) => @ghost (x$1 >= 0)
[ Debug ] }
[ Debug ]
[ Debug ] def split[T](l: List[T], x: T): List[List[T]] = l match {
[ Debug ] case Nil() =>
[ Debug ] Cons[List[T]](Nil[T](), Nil[List[T]]())
[ Debug ] case Cons(y, ys) if x == y =>
[ Debug ] val rassoc$1: List[T] = {
[ Debug ] val rassoc$1: List[T] = Nil[T]()
[ Debug ] assert(rassoc$1 is Nil, "Inner refinement lifting")
[ Debug ] rassoc$1
[ Debug ] }
[ Debug ] ::[List[T]](split[T](ys, x), rassoc$1)
[ Debug ] case Cons(y, ys) =>
[ Debug ] val r: List[List[T]] = split[T](ys, x)
[ Debug ] val rassoc$2: T = y
[ Debug ] val rassoc$3: List[T] = ::[T](head[List[T]](r), rassoc$2)
[ Debug ] ::[List[T]](tail[List[T]](r), rassoc$3)
[ Debug ] }
[ Debug ]
[ Debug ] def slowReplace[T](l1: List[T], x: T, l2: List[T]): Unit = {
[ Debug ] val tmp: List[T] = join[T](split[T](l1, x), l2)
[ Debug ] ()
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def ::[T](thiss: List[T], t: T): List[T] = Cons[T](t, thiss)
[ Debug ]
[ Debug ] @library
[ Debug ] def content[T](thiss: List[T]): Set[T] = thiss match {
[ Debug ] case Nil() =>
[ Debug ] {}
[ Debug ] case Cons(h, t) =>
[ Debug ] {h} \u222A content[T](t)
[ Debug ] }
[ Debug ]
[ Debug ] @library
[ Debug ] def tail[T](thiss: List[T]): List[T] = {
[ Debug ] require(@ghost (thiss \u2260 Nil[T]()))
[ Debug ] thiss match {
[ Debug ] case Cons(_, t) =>
[ Debug ] t
[ Debug ] }
[ Debug ] }
[ Debug ]
[ Debug ] def theorem[T](l1: List[T], x: T, l2: List[T]): Unit = {
[ Debug ] if (\u00ACisEmpty[T](l1)) {
[ Debug ] theorem[T](tail[T](l1), x, l2)
[ Debug ] } else {
[ Debug ] ()
[ Debug ] }
[ Debug ] } ensuring {
[ Debug ] (x$1: Unit) => join[T](split[T](l1, x), l2) == replace[T](l1, x, l2)
[ Debug ] }
[ Debug ]
[ Debug ] @derived(Test.slowReplace$Test.replace)
[ Debug ] @derived(slowReplace)
[ Debug ] def Test.slowReplace$Test.replace[T](l1: List[T], x: T, l2: List[T]): Unit = {
[ Debug ] ()
[ Debug ] } ensuring {
[ Debug ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2)
[ Debug ] }
[ Debug ]
[ Debug ] -------------Sorts-------------
[ Debug ] @library
[ Debug ] abstract class List[T]
[ Debug ] case class Nil[T]() extends List[T]
[ Debug ] case class Cons[T](h: T, t: List[T]) extends List[T]
[ Debug ]
[ Debug ] @synthetic
[ Debug ] abstract class Object
[ Debug ] case class Open(value: BigInt) extends Object
[ Debug ]
[ Debug ]
[ Debug ]
[ Debug ]
[ Debug ]
[ Debug ] Ensuring well-formedness after phase Trace...
[ Error ] Type error: {
[ Error ] ()
[ Error ] } ensuring {
[ Error ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2)
[ Error ] }, expected Unit,
[ Error ] found <untyped>
[ Error ]
[ Error ] Typing explanation:
[ Error ] {
[ Error ] ()
[ Error ] } ensuring {
[ Error ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2)
[ Error ] } is of type <untyped>
[ Error ] () is of type Unit
[ Error ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2) is of type <untyped>
[ Error ] slowReplace[T](l1, x, l2) == replace[T](l1, x, l2) is of type <untyped>
[ Error ] slowReplace[T](l1, x, l2) is of type <untyped>
[ Error ] l1 is of type List[T]
[ Error ] x is of type T
[ Error ] l2 is of type List[T] because slowReplace was instantiated with T:=T with type (List[T],T,List[T]) => Unit
[ Error ] replace[T](l1, x, l2) is of type <untyped>
[ Error ] l1 is of type List[T]
[ Error ] x is of type T
[ Error ] l2 is of type List[T] because replace was instantiated with T:=T with type (List[T],T,List[T]) => List[T]
[ Fatal ] Well-formedness check failed after phase Trace
[ Error ] Stainless terminated with an error.
[ Error ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error ] You may use --debug=stack to have the stack trace displayed in the output.
This works somewhat in Dragana's branch. Needs to be rebased. Dragana might appreciate help with that.
On Tue, May 17, 2022, 16:54 Jad Hamza @.***> wrote:
Hi @drganam https://github.com/drganam @vkuncak https://github.com/vkuncak, can Stainless generate equivalence lemmas for functions when one of the function calls other functions? (here replace vs slowReplace). I get a crash on this example (from a FV student)
stainless Test.scala --solvers=smt-z3 --timeout=10 --comparefuns=replace --models=slowReplace --batched --debug=trees --debug-phases=Trace
import stainless.collection._ object Test {
def split[T](l: List[T], x: T): List[List[T]] = l match { case Nil() => ListList[T] case Cons(y, ys) if x == y => NilT :: split(ys, x) case Cons(y, ys) => val r = split(ys, x) (y :: r.head) :: r.tail }
def join[T](ll: List[List[T]], l: List[T]): List[T] = ll match { case Nil() => NilT case Cons(l1, Nil()) => l1 // if you miss this case, Stainless finds a counter-example to theorem case Cons(l1, ls) => l1 ++ l ++ join(ls, l) }
def replace[T](l1: List[T], x: T, l2: List[T]): List[T] = l1 match { case Nil() => NilT case Cons(y, ys) if x == y => l2 ++ replace(ys, x, l2) case Cons(y, ys) => y :: replace(ys, x, l2) }
def theorem[T](l1: List[T], x: T, l2: List[T]): Unit = { if (!l1.isEmpty) theorem(l1.tail, x, l2) // recursive proof
}.ensuring(_ => join(split(l1, x), l2) == replace(l1, x, l2) )
// could be checked for equivalence with
replacethanks to --comparefuns def slowReplace[T](l1: List[T], x: T, l2: List[T]): Unit = join(split(l1, x), l2)}
stainless Test.scala --solvers=smt-z3 --timeout=10 --comparefuns=replace --models=slowReplace --batched --debug=trees Show output
[ Debug ] Symbols before Trace [ Debug ] [ Debug ] -------------Functions------------- [ Debug ] @library [ Debug ] def head[T](thiss: List[T]): T = { [ Debug ] @.*** (thiss \u2260 NilT)) [ Debug ] thiss match { [ Debug ] case Cons(h, ) => [ Debug ] h [ Debug ] } [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def isEmpty[T](thiss: List[T]): Boolean = thiss match { [ Debug ] case Nil() => [ Debug ] true [ Debug ] case _ => [ Debug ] false [ Debug ] } [ Debug ] [ Debug ] def join[T](ll: List[List[T]], l: List[T]): List[T] = ll match { [ Debug ] case Nil() => [ Debug ] NilT [ Debug ] case Cons(l1, Nil()) => [ Debug ] l1 [ Debug ] case Cons(l1, ls) => [ Debug ] ++[T](++[T](l1, l), join[T](ls, l)) [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def ++[T](thiss: List[T], that: List[T]): List[T] = { [ Debug ] thiss match { [ Debug ] case Nil() => [ Debug ] that [ Debug ] case Cons(x, xs) => [ Debug ] Cons[T](x, ++[T](xs, that)) [ Debug ] } [ Debug ] } ensuring { [ Debug ] (res: List[T]) => @ghost ((contentT == contentT \u222A contentT && sizeT == sizeT + sizeT) && (that \u2260 NilT || res == thiss)) [ Debug ] } [ Debug ] [ Debug ] def replace[T](l1: List[T], x: T, l2: List[T]): List[T] = l1 match { [ Debug ] case Nil() => [ Debug ] NilT [ Debug ] case Cons(y, ys) if x == y => [ Debug ] ++[T](l2, replace[T](ys, x, l2)) [ Debug ] case Cons(y, ys) => [ Debug ] val rassoc$4: T = y [ Debug ] ::[T](replace[T](ys, x, l2), rassoc$4) [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def size[T](thiss: List[T]): BigInt = { [ Debug ] thiss match { [ Debug ] case Nil() => [ Debug ] 0 [ Debug ] case Cons(h, t) => [ Debug ] 1 + sizeT [ Debug ] } [ Debug ] } ensuring { [ Debug ] (x$1: BigInt) => @ghost (x$1 >= 0) [ Debug ] } [ Debug ] [ Debug ] def split[T](l: List[T], x: T): List[List[T]] = l match { [ Debug ] case Nil() => [ Debug ] Cons[List[T]](NilT, NilList[T]) [ Debug ] case Cons(y, ys) if x == y => [ Debug ] val rassoc$1: List[T] = { [ Debug ] val rassoc$1: List[T] = NilT [ Debug ] assert(rassoc$1 is Nil, "Inner refinement lifting") [ Debug ] rassoc$1 [ Debug ] } [ Debug ] ::[List[T]](split[T](ys, x), rassoc$1) [ Debug ] case Cons(y, ys) => [ Debug ] val r: List[List[T]] = split[T](ys, x) [ Debug ] val rassoc$2: T = y [ Debug ] val rassoc$3: List[T] = ::[T](headList[T], rassoc$2) [ Debug ] ::[List[T]](tailList[T], rassoc$3) [ Debug ] } [ Debug ] [ Debug ] def slowReplace[T](l1: List[T], x: T, l2: List[T]): Unit = { [ Debug ] val tmp: List[T] = join[T](split[T](l1, x), l2) [ Debug ] () [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def ::[T](thiss: List[T], t: T): List[T] = Cons[T](t, thiss) [ Debug ] [ Debug ] @library [ Debug ] def content[T](thiss: List[T]): Set[T] = thiss match { [ Debug ] case Nil() => [ Debug ] {} [ Debug ] case Cons(h, t) => [ Debug ] {h} \u222A contentT [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def tail[T](thiss: List[T]): List[T] = { [ Debug ] @.*** (thiss \u2260 NilT)) [ Debug ] thiss match { [ Debug ] case Cons(, t) => [ Debug ] t [ Debug ] } [ Debug ] } [ Debug ] [ Debug ] def theorem[T](l1: List[T], x: T, l2: List[T]): Unit = { [ Debug ] if (\u00ACisEmptyT) { [ Debug ] theorem[T](tailT, x, l2) [ Debug ] } else { [ Debug ] () [ Debug ] } [ Debug ] } ensuring { [ Debug ] (x$1: Unit) => join[T](split[T](l1, x), l2) == replace[T](l1, x, l2) [ Debug ] } [ Debug ] [ Debug ] -------------Sorts------------- [ Debug ] @library [ Debug ] abstract class List[T] [ Debug ] case class NilT extends List[T] [ Debug ] case class Cons[T](h: T, t: List[T]) extends List[T] [ Debug ] [ Debug ] @synthetic [ Debug ] abstract class Object [ Debug ] case class Open(value: BigInt) extends Object [ Debug ] [ Debug ] [ Debug ] [ Debug ] [ Debug ] Symbols after Trace [ Debug ] [ Debug ] -------------Functions------------- [ Debug ] @library [ Debug ] def head[T](thiss: List[T]): T = { [ Debug ] @.*** (thiss \u2260 NilT)) [ Debug ] thiss match { [ Debug ] case Cons(h, ) => [ Debug ] h [ Debug ] } [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def isEmpty[T](thiss: List[T]): Boolean = thiss match { [ Debug ] case Nil() => [ Debug ] true [ Debug ] case _ => [ Debug ] false [ Debug ] } [ Debug ] [ Debug ] def join[T](ll: List[List[T]], l: List[T]): List[T] = ll match { [ Debug ] case Nil() => [ Debug ] NilT [ Debug ] case Cons(l1, Nil()) => [ Debug ] l1 [ Debug ] case Cons(l1, ls) => [ Debug ] ++[T](++[T](l1, l), join[T](ls, l)) [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def ++[T](thiss: List[T], that: List[T]): List[T] = { [ Debug ] thiss match { [ Debug ] case Nil() => [ Debug ] that [ Debug ] case Cons(x, xs) => [ Debug ] Cons[T](x, ++[T](xs, that)) [ Debug ] } [ Debug ] } ensuring { [ Debug ] (res: List[T]) => @ghost ((contentT == contentT \u222A contentT && sizeT == sizeT + sizeT) && (that \u2260 NilT || res == thiss)) [ Debug ] } [ Debug ] [ Debug ] def replace[T](l1: List[T], x: T, l2: List[T]): List[T] = l1 match { [ Debug ] case Nil() => [ Debug ] NilT [ Debug ] case Cons(y, ys) if x == y => [ Debug ] ++[T](l2, replace[T](ys, x, l2)) [ Debug ] case Cons(y, ys) => [ Debug ] val rassoc$4: T = y [ Debug ] ::[T](replace[T](ys, x, l2), rassoc$4) [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def size[T](thiss: List[T]): BigInt = { [ Debug ] thiss match { [ Debug ] case Nil() => [ Debug ] 0 [ Debug ] case Cons(h, t) => [ Debug ] 1 + sizeT [ Debug ] } [ Debug ] } ensuring { [ Debug ] (x$1: BigInt) => @ghost (x$1 >= 0) [ Debug ] } [ Debug ] [ Debug ] def split[T](l: List[T], x: T): List[List[T]] = l match { [ Debug ] case Nil() => [ Debug ] Cons[List[T]](NilT, NilList[T]) [ Debug ] case Cons(y, ys) if x == y => [ Debug ] val rassoc$1: List[T] = { [ Debug ] val rassoc$1: List[T] = NilT [ Debug ] assert(rassoc$1 is Nil, "Inner refinement lifting") [ Debug ] rassoc$1 [ Debug ] } [ Debug ] ::[List[T]](split[T](ys, x), rassoc$1) [ Debug ] case Cons(y, ys) => [ Debug ] val r: List[List[T]] = split[T](ys, x) [ Debug ] val rassoc$2: T = y [ Debug ] val rassoc$3: List[T] = ::[T](headList[T], rassoc$2) [ Debug ] ::[List[T]](tailList[T], rassoc$3) [ Debug ] } [ Debug ] [ Debug ] def slowReplace[T](l1: List[T], x: T, l2: List[T]): Unit = { [ Debug ] val tmp: List[T] = join[T](split[T](l1, x), l2) [ Debug ] () [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def ::[T](thiss: List[T], t: T): List[T] = Cons[T](t, thiss) [ Debug ] [ Debug ] @library [ Debug ] def content[T](thiss: List[T]): Set[T] = thiss match { [ Debug ] case Nil() => [ Debug ] {} [ Debug ] case Cons(h, t) => [ Debug ] {h} \u222A contentT [ Debug ] } [ Debug ] [ Debug ] @library [ Debug ] def tail[T](thiss: List[T]): List[T] = { [ Debug ] @.*** (thiss \u2260 NilT)) [ Debug ] thiss match { [ Debug ] case Cons(, t) => [ Debug ] t [ Debug ] } [ Debug ] } [ Debug ] [ Debug ] def theorem[T](l1: List[T], x: T, l2: List[T]): Unit = { [ Debug ] if (\u00ACisEmptyT) { [ Debug ] theorem[T](tailT, x, l2) [ Debug ] } else { [ Debug ] () [ Debug ] } [ Debug ] } ensuring { [ Debug ] (x$1: Unit) => join[T](split[T](l1, x), l2) == replace[T](l1, x, l2) [ Debug ] } [ Debug ] [ Debug ] @derived(Test.slowReplace$Test.replace) [ Debug ] @derived(slowReplace) [ Debug ] def Test.slowReplace$Test.replace[T](l1: List[T], x: T, l2: List[T]): Unit = { [ Debug ] () [ Debug ] } ensuring { [ Debug ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2) [ Debug ] } [ Debug ] [ Debug ] -------------Sorts------------- [ Debug ] @library [ Debug ] abstract class List[T] [ Debug ] case class NilT extends List[T] [ Debug ] case class Cons[T](h: T, t: List[T]) extends List[T] [ Debug ] [ Debug ] @synthetic [ Debug ] abstract class Object [ Debug ] case class Open(value: BigInt) extends Object [ Debug ] [ Debug ] [ Debug ] [ Debug ] [ Debug ] [ Debug ] Ensuring well-formedness after phase Trace... [ Error ] Type error: { [ Error ] () [ Error ] } ensuring { [ Error ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2) [ Error ] }, expected Unit, [ Error ] found
[ Error ] [ Error ] Typing explanation: [ Error ] { [ Error ] () [ Error ] } ensuring { [ Error ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2) [ Error ] } is of type [ Error ] () is of type Unit [ Error ] (res: Unit) => slowReplace[T](l1, x, l2) == replace[T](l1, x, l2) is of type [ Error ] slowReplace[T](l1, x, l2) == replace[T](l1, x, l2) is of type [ Error ] slowReplace[T](l1, x, l2) is of type [ Error ] l1 is of type List[T] [ Error ] x is of type T [ Error ] l2 is of type List[T] because slowReplace was instantiated with T:=T with type (List[T],T,List[T]) => Unit [ Error ] replace[T](l1, x, l2) is of type [ Error ] l1 is of type List[T] [ Error ] x is of type T [ Error ] l2 is of type List[T] because replace was instantiated with T:=T with type (List[T],T,List[T]) => List[T] [ Fatal ] Well-formedness check failed after phase Trace [ Error ] Stainless terminated with an error. [ Error ] Debug output is available in the file stainless-stack-trace.txt. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues [ Error ] You may use --debug=stack to have the stack trace displayed in the output.— Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/1264, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA5CDN33LQXAXNTODJSHM63VKOXKZANCNFSM5WFHFQXA . You are receiving this because you were mentioned.Message ID: @.***>
I can help with rebasing, I've become a skilled craftsman in that regard hehe :p Edit: https://github.com/drganam/stainless/pull/1
Sorry for not seeing this sooner.
Shouldn't return type of slowReplace be List[T] and not Unit?
This works for List[T], no need for function matching even :)
Looks like a very nice addition to our new fancy EC test suite!
