Unsound capture of mutable variables in closures

[vkuncak]

Stainless freezes the value of a closure incorrectly at creation time, resulting in unsoundness.
For example, it verifies this.

import stainless.annotation.*
object Lambda4 {
  def app[@mutable A](mkA: A, ping: A => Unit, get: A => BigInt): BigInt = {
    val f: A => BigInt = ((a: A) => {ping(a); get(a)+1})
    f(mkA)
  } ensuring(res => true)

  case class Cell[T](var content: T)

  def test = {
    val c = Cell[BigInt](42)
    val d = Cell[BigInt](7)
    val myPing = {
      (c1 : Cell[BigInt]) => c1.content = c1.content + d.content
    }
    d.content = 1000
    val res: BigInt = app(c, myPing, _.content)
    assert(c.content == 49)
    assert(res == 50)
  }
}

edit: of course Stainless needs @mutable parameter on A in app; I had inadvertedly removed it as I was testing it in REPL. The use in REPL confirms that the program crashes at run time due to assertion viaolation, yet it verifies with stainless Version: 0.9.7-7-g99a3f92

[vkuncak]

In my view, we should just disable capturing of mutable objects inside closures.
If you need to capture something, you need to do it through objects of some other class, and then aliasing checks need to apply.

We should also check what happens if we do similar construction using inner classes.

[vkuncak]

While one can imagine generalization to allow this, I believe that we should for now use the basic type systems to enforce that functions are only working on their arguments and do not capture anything mutable. For more general case, I propose to use a different type, see #1369

[mario-bucev]

Note that the assertion is correctly rejected if we were to replace the lambda with an inner function