stainless Call by name arguments unsound

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.

Mar 29 '23 11:03 andreagilot-da

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)
}

Mar 31 '23 15:03 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?

Mar 31 '23 15:03 vkuncak

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.

Mar 31 '23 15:03 mario-bucev

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

Apr 03 '23 09:04 samarion

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]())
    }
  }
}

Apr 03 '23 12:04 mario-bucev

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

Apr 03 '23 12:04 samarion

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.

Apr 03 '23 13:04 mario-bucev

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.

Apr 03 '23 15:04 samarion

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!

Apr 04 '23 06:04 mario-bucev

How did it go @mario-bucev ?

Apr 16 '23 19:04 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])

Nov 25 '23 16:11 vkuncak

This and the underlying Inox issue should not be forgotten

Mar 01 '24 12:03 vkuncak

stainless stainless copied to clipboard

Call by name arguments unsound

stainless
stainless copied to clipboard