Assert c.isInstanceOf[Type] invalid, even though c is a parameter of type Type

[Sporarum]

Stainless version:

[  Info  ] Stainless verification tool (https://github.com/epfl-lara/stainless)
[  Info  ] Version: 0.9.1
[  Info  ] Built at: 2021-09-28 12:09:18.155
[  Info  ] Bundled Scala compiler version: 2.13.6

Command: (with empty cache)
stainless minimised.scala

Problematic lines:

def helper(c: Transfinite): Unit = {
    decreases(c.l, 0)
    assert(c.isInstanceOf[Transfinite]) // Invalid !
    ...
}

Content of minimised.scala:

import stainless.lang._

abstract sealed class Ordinal{
    def l: BigInt = { this match {
        case Nat() => BigInt(0)
        case Transfinite(in) => in.l + 1
    }
    }.ensuring( res => res >= 0 )
}

case class Nat() extends Ordinal
case class Transfinite(in: Ordinal) extends Ordinal //removing Ordinal removes location information

object lemmas {

    def bar(a: Ordinal): Unit = {
        decreases(a.l, 1)

        def helper(c: Transfinite): Unit = {
            decreases(c.l, 0)
            assert(c.isInstanceOf[Transfinite])

            bar(c.in)
        }
        
        a match {
            case b: Transfinite =>
                helper(b)
            case Nat() =>

        }
    }
    
}

Ouptut:

[  Info  ] Starting verification...
[  Info  ] Verified: 5 / 12
[Warning ]  - Result for 'body assertion' VC for helper @21:20:
[Warning ] c.isInstanceOf[Transfinite]
[Warning ] minimised.scala:21:20:  => INVALID
                       assert(c.isInstanceOf[Transfinite])
                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^
[Warning ] Found counter-example:
[Warning ]   c: Ordinal -> Nat()
[  Info  ] Verified: 11 / 12
[  Info  ]   ┌───────────────────┐
[  Info  ] ╔═╡ stainless summary ╞══════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └───────────────────┘                                                                      ║
[  Info  ] ║                           bar      non-negative measure   valid              nativez3  0.1 ║
[  Info  ] ║ minimised.scala:26:9:     bar      match exhaustiveness   valid from cache             0.0 ║
[  Info  ] ║ minimised.scala:28:17:    bar      measure decreases      valid              nativez3  0.1 ║
[  Info  ] ║                           helper   non-negative measure   valid              nativez3  0.1 ║
[  Info  ] ║ minimised.scala:21:20:    helper   body assertion         invalid            nativez3  0.1 ║
[  Info  ] ║ minimised.scala:23:13:    helper   measure decreases      valid              nativez3  0.1 ║
[  Info  ] ║ minimised.scala:23:17:    helper   cast correctness       valid              nativez3  0.0 ║
[  Info  ] ║ minimised.scala:4:5:      l        non-negative measure   valid              nativez3  0.5 ║
[  Info  ] ║ minimised.scala:4:23:     l        match exhaustiveness   valid              nativez3  0.0 ║
[  Info  ] ║ minimised.scala:5:23:     l        postcondition          valid              nativez3  0.1 ║
[  Info  ] ║ minimised.scala:6:33:     l        measure decreases      valid              nativez3  0.1 ║
[  Info  ] ║ minimised.scala:6:33:     l        postcondition          valid              nativez3  0.0 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 12   valid: 11   (1 from cache) invalid: 1    unknown: 0    time:     1.1           ║
[  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════╝
[  Info  ] Shutting down executor service.

(also note the valid from cache after having deleted the cache)

[samarion]

This seems like an issue in the interaction between Stainless and Inox.

In order to fix the issue, we should probably make sure that the Inox UnrollingSolver calls declare on all free variables in constraints (in assertCnstr). This might also require adding a cache layer for declared variables to avoid generating declaration clauses multiple times.

The valid from cache message might occur because two VCs with the same constraint are generated when verifying the program, so only one will be checked.

[mario-bucev]

It seems to only affect inner functions:

import stainless.lang._

object i1214b {
  abstract sealed class Ordinal
  case class Nat() extends Ordinal
  case class Transfinite(in: Ordinal) extends Ordinal 

  def free(c: Transfinite): Unit = {
    assert(c.isInstanceOf[Transfinite]) // Verifies
  }

  def bar(): Unit = {
    def inner(c: Transfinite): Unit = {
      assert(c.isInstanceOf[Transfinite]) // Does not verify
    }
  }
}

Looking at the trees, RefinementLifting may be the place where to look for:

// Symbols before RefinementLifting
def free$0(c$5: { v$21: Ordinal$0 | v$21 is Transfinite$0 }): Unit = {
  assert(c$5.isInstanceOf[{ v$23: Ordinal$0 | v$23 is Transfinite$0 }])
  ()
}

def bar$0: Unit = {
  def inner$0(_$c$3: { v$24: Ordinal$0 | v$24 is Transfinite$0 }): Unit = {
    assert(_$c$3.isInstanceOf[{ v$26: Ordinal$0 | v$26 is Transfinite$0 }])
    ()
  }
  ()
}

// Symbols after RefinementLifting
def free$0(c$5: Ordinal$0): Unit = {
  require(c$5 is Transfinite$0)
  assert(c$5 is Transfinite$0)
  ()
}

def bar$0: Unit = {
  def inner$0(_$c$3: Ordinal$0): Unit = {
    assert(_$c$3 is Transfinite$0)
    ()
  }
  ()
}