Egg invariant: unsatisfiable invariant of locally declared classes that depend on mutable local state

[vkuncak]

/* Curious case of Egg invariant. 

   When a class is defined inside a method, the context is captured inside an invariant.
   If this context is mutable and is changed before class declaration, the captured
   check is wrong and an attempt to construct class instance fails.

   The context should probably not be captured when there is no syntactic dependency.

   If there is a syntactic dependency that is mutable, probably we should just throw
   unless there is a clear way to handle such mutable context.
 */

import stainless.lang.*
import stainless.annotation.*
import StaticChecks.*

object EggInvariant {
  case class Mut(var x: Int)

  def test = {
    val m = Mut(2)
    m.x = 1
    assert(m.x == 1)

    final case class Egg(n: Int)

    Egg(3)
  }
}

The generated invariant is:

@invariant
@derived(test)
def inv(thiss: Egg): Boolean = {
  val m: Mut = Mut(2)
  @ghost (m.x == 1)
}

[mario-bucev]

One way to "fix" this is to run a check to ensure the path condition does not refer to mutable variables or mutable types.