Problem proving lemma with imperative features

[jad-hamza]

Thanks to Romain (J) for reporting

Stainless times out on the assertion arePositive(l).

import stainless.collection._

object Imperative {
  case class Test(var l: List[BigInt]) {

    def lemma(x: BigInt, amount: BigInt) = {
      require(arePositive(x :: l))

      assert(arePositive(x :: l))
      l = x :: l
      assert(arePositive(l))
    }

    def arePositive(l: List[BigInt]): Boolean = {
      l match {
        case Nil() => true
        case p :: ps => p >= 0 && arePositive(ps)
      }
    }
  }
}

The VC which corresponds to this assertion is:

arePositive(thiss, ::[BigInt](thiss.l, x)) ==> (arePositive(thiss, ::[BigInt](thiss.l, x)) ==> {
   val thiss: Test = Test(::[BigInt](thiss.l, x))
  arePositive(thiss, thiss.l)
})

Simplified, this corresponds to:

arePositive(thiss, x :: l) ==> {
   val thiss2: Test = Test(x :: l)
  arePositive(thiss2, x :: l)
})

So the issue comes from the fact that after transformation, arePositive has an extra argument which is the Test class itself. Our workaround for the moment is to pull arePositive out of the class (and then everything works as expected).

[vkuncak]

@jad-hamza : even though I thought that this is something we may not want to fix, I am wondering if it would not be useful for us to implement, for @pure functions, something that does dependency analysis on fields of parameters and the receiver and factors out the function to only take the values that it needs. But the question is how deep such analysis should go in terms of the call graph and in terms of the nesting of fields.