Unsoundness with quantifiers (choose nothing and always succeed)

[jad-hamza]

I don't remember why this example with assert(false) is in the valid benchmarks? https://github.com/epfl-lara/stainless/blob/5b7b3a0c01c23486fea44abb2255f0963a242708/frontends/benchmarks/verification/valid/Countable2.scala

This should be rejected? (probably the assertion line 33)

Also quantifiers for the type-checker should probably be hidden under an --unsafe-quantifier flag.

[mario-bucev]

A variation:

import stainless.lang._
import stainless.annotation._

// A variant of Countable2
object ChooseNothing {
  def theorem() = {
    val e: Nothing = choose((x: Nothing) => true)
    assert(false)
  }
}

[vkuncak]

So, it looks like choose generates a quantified VC, so it relates to quantifiers. Then, either

• Inox does not report the outcome of such quantified query correctly (it's fine if it is conservative!), or
• We do not correctly check the outcome of Inox
• We do not give correct query to Inox (some assumption is lost), or @mario-bucev maybe report whether Inox gives a definite answer (as opposed to Uknown) and query it gets in the tiny variation example above.

[vkuncak]

This issue is mentioned in the following soundness test case in verification/false-invalid/Countable2.scala and shows how hard it is to know emptiness of types.

object Countable2 {
  // an instance of Countable[T] gives a bijection between T and BigInt
  abstract class Countable[T] {
    @law
    def isBijective = {
      forall((t: T) => g(f(t)) == t) &&
      forall((h: BigInt) => f(g(h)) == h)
    }

    def f(x: T): BigInt
    def g(x: BigInt): T
  }

  type Empty = Countable[BigInt => BigInt]

  // there is no element of Countable[BigInt => BigInt]
  // (since there is no bijection between BigInt and BigInt => BigInt)
  def lemma(e: Empty) = {
    assert(e.isBijective)
    val f: (BigInt => BigInt) => BigInt = e.f _
    val g: BigInt => (BigInt => BigInt) = e.g _
    def d(x: BigInt): BigInt = g(x)(x) + 1
    assert(d(f(d)) == g(f(d))(f(d)) + 1)
    assert(d(f(d)) == d(f(d)) + 1)
    false
  }.holds

  def theorem() = {
    if (forall((x: Empty) => false))
      assert(false) // Inox assumes every type is not empty
    else {
      val e: Empty = choose((x: Empty) => true)
      assert(lemma(e))
      assert(false)
    }
  }
}