Call by name arguments unsound

[andreagilot-da]

When running the following example, stainless times out as expected on foo because I use head on an empty list. Stainless however verifies foo2 which is exactly foo but with an additional call by value argument that is never used. The issues arises with timeouts, if the example is simplified and stainless is able to find a counterexample, then both will be invalid.

I am using the latest version of stainless-scalac.

[vkuncak]

The issue also arises in Scala 3. Here is a version of the example along with a test case that crashes in --eval.

Note that the ADT does not seem the simple algebraic one because C case is defined in terms of B.

import stainless.lang._
import stainless.collection._

sealed trait Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Trait
case class C(left: B, right: B) extends Trait

object Bug{
  def foo2(t: Trait, arg: => BigInt): List[BigInt] = {
    decreases(t)
    t match {
      case A() => Nil[BigInt]()
      case B(v, sub) => foo2(sub, arg)
      case C(l, r) => Cons(((foo2(l, arg) ++ (foo2(r, arg) :+ BigInt(1))) - BigInt(1)).head, Nil[BigInt]())
    }
  }

  val b: B = B(0, A())
  def test = foo2(C(b, b), 42)
}

[vkuncak]

Removing the recursion bouncing in the ADT using a pair makes Stainless detect it and correctly report an error:

import stainless.lang._
import stainless.collection._

sealed trait Trait
case class A() extends Trait
case class C(left: (BigInt, Trait), right: (BigInt, Trait)) extends Trait

object Bug{
  def foo2(t: Trait, arg: => BigInt): List[BigInt] = {
    decreases(t)
    t match {
      case A() => Nil[BigInt]()
      case C(l, r) => Cons(((foo2(l._2, arg) ++ (foo2(r._2, arg) :+ BigInt(1))) - BigInt(1)).head, Nil[BigInt]())
    }
  }
}

gives

warning:  - Result for 'precond. (call head[BigInt](-[BigInt](++[BigInt](foo...)' VC for foo2 @13:28:
warning: t.isInstanceOf[A] || -[BigInt](++[BigInt](foo2(t.left._2, () => arg()), :+[BigInt](foo2(t.right._2, () => arg()), BigInt("1"))), BigInt("1")) != Nil[BigInt]()
Test.scala:13:28: warning:  => INVALID
                 case C(l, r) => Cons(((foo2(l._2, arg) ++ (foo2(r._2, arg) :+ BigInt(1))) - BigInt(1)).head, Nil[BigInt]())
                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: Found counter-example:
warning:   arg: () => BigInt -> () => BigInt("0")
  t: Trait          -> C((BigInt("4"), A()), (BigInt("5"), A()))
Verified: 4 / 5

 stainless summary 

Test.scala:11:5:    foo2  body assertion: match exhaustiveness                      trivial                     0.0 
Test.scala:11:5:    foo2  non-negative measure                                      valid from cache            0.0 
Test.scala:13:28:   foo2  precond. (call head[BigInt](-[BigInt](++[BigInt](foo...)  invalid           nativez3  3.6 

In the original example, however, the counterexample is masked! It looks like something is off with the way ADTs are encoded in this case, even though there's no ADT encoding. @samarion have you seen anything like this?

[mario-bucev]

Another point that may be worth pointing out: if we replace the call-by-name parameter arg: => BigInt to arg: () => BigInt and leave the rest unchanged, a counter-example is found. However, if we proceed to desugar as the compiler would do (replacing the parameter and eta-expanding arg), then the function is incorrectly verified.

[samarion]

Very strange. Maybe if someone grabs some solver debug logs of the failing case I can try to make a guess.

[mario-bucev]

Another variant, this is correctly rejected:

import stainless.lang._
import stainless.collection._

object i1395b {
  sealed trait Trait
  case class A() extends Trait
  case class B(value: BigInt, sub: Trait) extends Trait
  case class C(left: B, right: B) extends Trait

  def foo2(t: Trait, arg: BigInt => BigInt): List[BigInt] = {
    decreases(t)
    t match {
      case A() => Nil[BigInt]()
      case B(v, sub) => foo2(sub, x => arg(x))
      case C(l, r) =>
        val h = foo2(l, x => arg(x)).head
        Cons(h, Nil[BigInt]())
    }
  }
}

but this incorrectly verifies:

import stainless.lang._
import stainless.collection._

object i1395b {
  sealed trait Trait
  case class A() extends Trait
  case class B(value: BigInt, sub: Trait) extends Trait
  case class C(left: B, right: B) extends Trait

  def foo2(t: Trait, arg: () => BigInt): List[BigInt] = {
    decreases(t)
    t match {
      case A() => Nil[BigInt]()
      case B(v, sub) => foo2(sub, () => arg())
      case C(l, r) =>
        val h = foo2(l, () => arg()).head
        Cons(h, Nil[BigInt]())
    }
  }
}

[samarion]

This might be an instance of this issue: https://github.com/epfl-lara/inox/issues/139

[mario-bucev]

The solver debug log for the precondition VC (for the variant https://github.com/epfl-lara/stainless/issues/1395#issuecomment-1494224828):

Click to expand

``` - Now solving 'precond. (call head$1[BigInt](foo2$0((scrut$5.left$2...)' VC for foo2$0 @24:17... - Original VC: val scrut$5: Trait$0 = t$67 !scrut$5.isInstanceOf[A$106] ==> (!scrut$5.isInstanceOf[B$77] ==> (scrut$5.isInstanceOf[C$9] ==> { val thiss$9: List$1[BigInt] = foo2$0(scrut$5.left$2, () => arg$1()) ((thiss$9 != Nil$0[BigInt]())): @ghost })) - Simplified VC: t$67.isInstanceOf[A$106] || t$67.isInstanceOf[B$77] || foo2$0(t$67.left$2, () => arg$1()) != Nil$0[BigInt]() Solving with: nativez3 -> registering free function start$3!2 ==> arg$1!1: () => BigInt -> instantiating matcher m$13!37 ==> arg$1!1() -> instantiating matcher m$14!46 ==> inv$7(t$67!0) -> instantiating matcher m$15!47 ==> foo2$0((left$9 t$67!0),lambda$0!31) -> instantiating matcher m$16!48 ==> inv$7((left$9 t$67!0)) -> instantiating matcher m$17!49 ==> inv$7((right$9 t$67!0)) -> instantiating matcher m$18!50 ==> inv$7((sub$10 t$67!0)) . start$3!2 . (=> start$3!2 (= b_free$0!28 (not b_next$0!29))) . (=> start$3!2 (= tp$3!20 b_and$0!30)) . (=> (not b_lambda$0!32) (not b$19!25)) . (=> (and start$3!2 (= arg$1!1 arg$1!1) t$76!33) tb$0!34) . (=> tb$0!34 (= result$0!35 true)) . (=> b$19!25 t$76!33) . (= b_and$0!30 (and (=> t$76!33 result$0!35) b_and$1!36)) . (=> b$19!25 m$13!37) . (=> b$19!25 true) . (=> b$19!25 (< (dynLambda$1!45 order$0!44 arg$1!1) (dynLambda$1!45 order$0!44 lambda$0!31))) . (=> start$3!2 (=> (not res$46!24) (not e$4!18))) . (=> start$3!2 (= res$46!24 (and (not ((_ is (A$118 () Trait$3)) t$67!0)) (not ((_ is (B$81 (Int Trait$3) Trait$3)) t$67!0))))) . (=> start$3!2 e$4!18) . (=> start$3!2 (and (inv$7!16 t$67!0) e$5!19)) . (=> start$3!2 tp$3!20) . (=> b$19!25 (= e$4!18 (= (foo2$0!17 (left$9 t$67!0) lambda$0!31) Nil$2))) . (=> b$20!26 (= e$5!19 (and (inv$7!16 (left$9 t$67!0)) tp$0!21 (inv$7!16 (right$9 t$67!0)) tp$1!22))) . (=> b$21!27 (= e$5!19 (and (inv$7!16 (sub$10 t$67!0)) tp$2!23))) . (= (and start$3!2 res$46!24) b$19!25) . (= (and start$3!2 ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) t$67!0)) b$20!26) . (= (and start$3!2 ((_ is (B$81 (Int Trait$3) Trait$3)) t$67!0)) b$21!27) . (=> start$3!2 m$14!46) . (=> b$19!25 m$15!47) . (=> b$20!26 m$16!48) . (=> b$20!26 m$17!49) . (=> b$21!27 m$18!50) - Running search... - Finished search with blocked literals - Running search without blocked literals (w/o lucky test) - Finished search without blocked literals - We need to keep going Unrolling generation [1] - 0 new clauses Unrolling types (0) -> extending lambda blocker: (= b_lambda$0!32 (or (and start$3!2 b_free$0!28) (and b$19!25 b$19!25 (= lambda$0!31 arg$1!1)) b_lambda$1!51)) Unrolling behind lambda$0!31|(and b$19!25 (= lambda$0!31 arg$1!1))() (3) . (= bs$1!53 (and d$1!52 b$19!25)) . (=> bs$1!53 (= (dynLambda$0!6 lambda$0!31) (dynLambda$0!6 arg$1!1))) . (=> (and b$19!25 (= lambda$0!31 arg$1!1) b$19!25) d$1!52) - 4 new clauses Unrolling ignored matchers (0) Unrolling ignored substitutions (0) Unrolling ignored grounds (0) - Finished unrolling - Running search... - Finished search with blocked literals - Running search without blocked literals (w/o lucky test) - Finished search without blocked literals - We need to keep going Unrolling generation [4] Unrolling behind inv$7((sub$10 t$67!0))() (2) . (=> d$2!54 (= (inv$7!16 (sub$10 t$67!0)) (or (not ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) (sub$10 t$67!0))) ((_ is (B$81 (Int Trait$3) Trait$3)) (left$9 (sub$10 t$67!0)))))) . (=> b$21!27 d$2!54) Unrolling behind inv$7((left$9 t$67!0))() (2) . (=> d$3!57 (= (inv$7!16 (left$9 t$67!0)) (or (not ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) (left$9 t$67!0))) ((_ is (B$81 (Int Trait$3) Trait$3)) (left$9 (left$9 t$67!0)))))) . (=> b$20!26 d$3!57) Unrolling behind inv$7((right$9 t$67!0))() (2) . (=> d$4!58 (= (inv$7!16 (right$9 t$67!0)) (or (not ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) (right$9 t$67!0))) ((_ is (B$81 (Int Trait$3) Trait$3)) (left$9 (right$9 t$67!0)))))) . (=> b$20!26 d$4!58) -> instantiating matcher m$19!87 ==> lambda$0!31() -> instantiating matcher m$20!94 ==> foo2$0((ite c$6!77 (sub$10 (left$9 t$67!0)) (left$9 (left$9 t$67!0))),(ite c$6!77 lambda$1!88 lambda$2!91)) -> instantiating matcher m$21!95 ==> head$1[BigInt](call$3!76) Unrolling behind foo2$0((left$9 t$67!0), lambda$0!31)() (30) . (=> (not b_lambda$2!86) (not b$25!82)) . (=> b$25!82 m$19!87) . (= bs$1!89 (and b$25!82 b$19!25)) . (=> bs$1!89 (= (= (dynLambda$0!6 lambda$0!31) (dynLambda$0!6 arg$1!1)) (= lambda$1!88 lambda$0!31))) . (=> b$25!82 true) . (=> b$25!82 (< (dynLambda$1!45 order$0!44 lambda$0!31) (dynLambda$1!45 order$0!44 lambda$1!88))) . (=> (not b_lambda$3!90) (not b$26!81)) . (=> b$26!81 m$19!87) . (= bs$1!92 (and b$26!81 b$19!25)) . (=> bs$1!92 (= (= (dynLambda$0!6 lambda$0!31) (dynLambda$0!6 arg$1!1)) (= lambda$2!91 lambda$0!31))) . (= bs$1!93 (and b$26!81 b$25!82)) . (=> bs$1!93 (= lambda$2!91 lambda$1!88)) . (=> b$26!81 true) . (=> b$26!81 (< (dynLambda$1!45 order$0!44 lambda$0!31) (dynLambda$1!45 order$0!44 lambda$2!91))) . (=> b$25!82 (= e$7!79 call$3!76)) . (=> b$23!83 (= e$6!80 Nil$2)) . (=> b$24!84 (= e$6!80 e$7!79)) . (=> b$24!84 (= c$6!77 ((_ is (B$81 (Int Trait$3) Trait$3)) (left$9 t$67!0)))) . (=> bm$0!85 (= call$3!76 (foo2$0!17 (ite c$6!77 (sub$10 (left$9 t$67!0)) (left$9 (left$9 t$67!0))) (ite c$6!77 lambda$1!88 lambda$2!91)))) . (=> b$26!81 (= e$7!79 (Cons$2 (head$1!75 call$3!76) Nil$2))) . (=> d$5!59 (= c$5!78 ((_ is (A$118 () Trait$3)) (left$9 t$67!0)))) . (=> d$5!59 (= (foo2$0!17 (left$9 t$67!0) lambda$0!31) e$6!80)) . (= (and d$5!59 c$5!78) b$23!83) . (= (and d$5!59 (not c$5!78)) b$24!84) . (= (and b$24!84 c$6!77) b$25!82) . (= (and b$24!84 (not c$6!77)) b$26!81) . (= (or b$25!82 b$26!81) bm$0!85) . (=> bm$0!85 m$20!94) . (=> b$26!81 m$21!95) . (=> b$19!25 d$5!59) Unrolling behind inv$7(t$67!0)() (2) . (=> d$6!96 (= (inv$7!16 t$67!0) (or (not ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) t$67!0)) ((_ is (B$81 (Int Trait$3) Trait$3)) (left$9 t$67!0))))) . (=> start$3!2 d$6!96) - 38 new clauses -> instantiating matcher m$22!112 ==> inv$7((left$9 (sub$10 t$67!0))) -> instantiating matcher m$23!113 ==> inv$7((right$9 (sub$10 t$67!0))) -> instantiating matcher m$24!114 ==> inv$7((sub$10 (sub$10 t$67!0))) -> instantiating matcher m$25!121 ==> inv$7((left$9 (left$9 t$67!0))) -> instantiating matcher m$26!122 ==> inv$7((right$9 (left$9 t$67!0))) -> instantiating matcher m$27!123 ==> inv$7((sub$10 (left$9 t$67!0))) -> instantiating matcher m$28!130 ==> inv$7((left$9 (right$9 t$67!0))) -> instantiating matcher m$29!131 ==> inv$7((right$9 (right$9 t$67!0))) -> instantiating matcher m$30!132 ==> inv$7((sub$10 (right$9 t$67!0))) Unrolling types (27) . (=> b$28!110 (= e$8!106 (and (inv$7!16 (left$9 (sub$10 t$67!0))) tp$4!107 (inv$7!16 (right$9 (sub$10 t$67!0))) tp$5!108))) . (=> b$29!111 (= e$8!106 (and (inv$7!16 (sub$10 (sub$10 t$67!0))) tp$6!109))) . (=> b$21!27 (= tp$2!23 (and (inv$7!16 (sub$10 t$67!0)) e$8!106))) . (= (and b$21!27 ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) (sub$10 t$67!0))) b$28!110) . (= (and b$21!27 ((_ is (B$81 (Int Trait$3) Trait$3)) (sub$10 t$67!0))) b$29!111) . (=> b$28!110 m$22!112) . (=> b$28!110 m$23!113) . (=> b$29!111 m$24!114) . (=> b$21!27 m$18!50) . (=> b$28!119 (= e$8!115 (and (inv$7!16 (left$9 (left$9 t$67!0))) tp$4!116 (inv$7!16 (right$9 (left$9 t$67!0))) tp$5!117))) . (=> b$29!120 (= e$8!115 (and (inv$7!16 (sub$10 (left$9 t$67!0))) tp$6!118))) . (=> b$20!26 (= tp$0!21 (and (inv$7!16 (left$9 t$67!0)) e$8!115))) . (= (and b$20!26 ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) (left$9 t$67!0))) b$28!119) . (= (and b$20!26 ((_ is (B$81 (Int Trait$3) Trait$3)) (left$9 t$67!0))) b$29!120) . (=> b$28!119 m$25!121) . (=> b$28!119 m$26!122) . (=> b$29!120 m$27!123) . (=> b$20!26 m$16!48) . (=> b$28!128 (= e$8!124 (and (inv$7!16 (left$9 (right$9 t$67!0))) tp$4!125 (inv$7!16 (right$9 (right$9 t$67!0))) tp$5!126))) . (=> b$29!129 (= e$8!124 (and (inv$7!16 (sub$10 (right$9 t$67!0))) tp$6!127))) . (=> b$20!26 (= tp$1!22 (and (inv$7!16 (right$9 t$67!0)) e$8!124))) . (= (and b$20!26 ((_ is (C$12 (Trait$3 Trait$3) Trait$3)) (right$9 t$67!0))) b$28!128) . (= (and b$20!26 ((_ is (B$81 (Int Trait$3) Trait$3)) (right$9 t$67!0))) b$29!129) . (=> b$28!128 m$28!130) . (=> b$28!128 m$29!131) . (=> b$29!129 m$30!132) . (=> b$20!26 m$17!49) -> extending lambda blocker: (= b_lambda$2!86 (or (and b$19!25 true) b_lambda$4!133)) Unrolling behind lambda$0!31|true() (3) . (= bs$1!136 (and d$7!135 b$19!25)) . (=> bs$1!136 (= (dynLambda$0!6 lambda$0!31) (dynLambda$0!6 arg$1!1))) . (=> b$25!82 d$7!135) -> extending lambda blocker: (= b_lambda$3!90 (or (and b$19!25 true) b_lambda$5!134)) Unrolling behind lambda$0!31|true() (1) . (=> b$26!81 d$7!135) - 6 new clauses Unrolling ignored matchers (0) Unrolling ignored substitutions (0) Unrolling ignored grounds (0) - Finished unrolling - Running search... - Finished search with blocked literals - Running search without blocked literals (w/o lucky test) - Finished search without blocked literals - Result for 'precond. (call head$1[BigInt](foo2$0((scrut$5.left$2...)' VC for foo2$0 @24:17: => VALID ```

There is an ADT invariant on Trait that specifies that, if this is a C, then its left and right are Bs.

[samarion]

Yeah that looks like the Inox issue I mentioned.

I expect that the example using a pair instead of the B type works because the counterexample is found before the bad unfolding takes place, whereas that counterexample is blocked in the bad case because the Trait type has to be unfolded for the invariant.

I gave some pointers about how to fix the underlying issue in https://github.com/epfl-lara/inox/issues/139, but it's unfortunately a bit involved.

[mario-bucev]

At a first glance, all ingredients seems to be present for the fix. I'll give it a try :) Thanks again for looking at this issue!

[vkuncak]

How did it go @mario-bucev ?

[vkuncak]

@sankalpgambhir to illustrate the consequence of SMT-style ADT restrictions, even a very mild departure from recursion going over top-level data type definition, as in the present example:

sealed trait Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Trait
case class C(left: B, right: B) extends Trait

requires Stainless to transform the ADT to make call inside C go to top-level type instead of subclass:

@invariant(inv)
abstract class Trait
case class C(left: Trait, right: Trait) extends Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Trait

with the definition of inv:

def inv(thiss: Trait): Boolean = thiss.isInstanceOf[C] ==> ({
  assert(thiss.isInstanceOf[C], "Cast error")
  thiss.left
}.isInstanceOf[B] && {
  assert(thiss.isInstanceOf[C], "Cast error")
  thiss.right
}.isInstanceOf[B])

[vkuncak]

This and the underlying Inox issue should not be forgotten