systematic inline defs handling and interaction with @opaque. Do not repeat while loop transform

[vkuncak]

Currently, inline defs are kept and verified like normal functions and their use appers verified a bit as if annotated by @inlineOnce. However, it would be relatively simple and useful to give users other options.

inline directs scalac to make the call non-modular. This is orthogonal to whether the verification should be modular, which we control using annotations such as @opaque, @inline, @inlineOnce, see annotations at https://github.com/epfl-lara/stainless/blob/main/frontends/library/stainless/annotation/annotations.scala

Currently, we inline such methods before vcgen, turning require into assert and ensuring into assume.
Given:

  inline def g(x: BigInt) = {
    require(x > 0)
    x + 1
  }.ensuring(_ > 3)

  @main
  def f =
    g(3)
    42

invoking

stainless Test.scala --debug=trees --debug-phases=AssertionInjector

gives

[ Debug  ] def g(x: BigInt): BigInt = {
[ Debug  ]   require(x > BigInt("0"))
[ Debug  ]   x + BigInt("1")
[ Debug  ] }.ensuring {
[ Debug  ]   (_$1: BigInt) => _$1 > BigInt("3")
[ Debug  ] }

[ Debug  ] def f: Int = {
[ Debug  ]   val x$proxy1: BigInt = BigInt("3")
[ Debug  ]   assert(x$proxy1 > BigInt("0"), "Inlined precondition")
[ Debug  ]   val _$1: BigInt = x$proxy1 + BigInt("1")
[ Debug  ]   assume(_$1 > BigInt("3"))
[ Debug  ]   val tmp: BigInt = _$1
[ Debug  ]   42
[ Debug  ] }

Adding @opaque to g results in

[ Error  ] Test.scala:8:14: Can't inline opaque or extern function, use @inlineOnce instead
             inline def g(x: BigInt) = {

However, it seems useful for orthogonality of verification to treat g as opaque, so it would be good to

• support opaque annotation on inline, with the effect same as if the def was not inline

In the other direction, there is an opportunity to treat inline functions as transparent, as receipies for code and verification that should be applied every time. This can work around the limitations of higher-order verification. I propose that when requested using a new annotation @transparent on the inline function:

• inline function should not be verified in isolation
• the inlined body should not insert assume statements, so that any assertions in it are verified on each use

Here is another example of the use. This program verifies. Note that the inner function representing while loop is generated both for the inline function itself, and for its use:

  inline def initArray(a: Array[Int], v: Int): Unit =
    var i = a.length - 1
    (while i > 0 do
      decreases(i)
      a(i) = v
      i -= 1).invariant(0 <= i && i < a.length)

  def f =
    val a = new Array[Int](100)
    initArray(a, 42)

trees:

@derived(f)
def fWhile(i: Int, a: Array[Int]): (Unit, Int, Array[Int]) = {
  require((0 <= i && i < a.length) &&& (i > 0))
  decreases(i)
  val a: Array[Int] = a
  val i: Int = i
  val ix: Int = i
  val a: Array[Int] = {
    assert(ix >= 0 && ix < a.length, "Array index out of range")
    a.updated(ix, 42)
  }
  val tmp: Unit = ()
  val a: Array[Int] = a
  val tmp: Unit = ()
  val tmp: Unit = ()
  val i: Int = i - 1
  val tmp: Unit = ()
  if (i > 0) {
    fWhile(i, a)
  } else {
    ((), i, a)
  }
}.ensuring {
  (_res: (Unit, Int, Array[Int])) => {
    val a: Array[Int] = _res._3
    val i: Int = _res._2
    (0 <= i && i < a.length) &&& !(i > 0)
  }
}

def initArray(a: Array[Int], v: Int): (Unit, Array[Int]) = {
  val a: Array[Int] = a
  val i: Int = a.length - 1
  val t: (Unit, Int, Array[Int]) = if (i > 0) {
    initArrayWhile(v, i, a)
  } else {
    ((), i, a)
  }
  val res: Unit = t._1
  val a: Array[Int] = t._3
  val i: Int = t._2
  (res, a)
}

@derived(initArray)
def initArrayWhile(v: Int, i: Int, a: Array[Int]): (Unit, Int, Array[Int]) = {
  require((0 <= i && i < a.length) &&& (i > 0))
  decreases(i)
  val a: Array[Int] = a
  val i: Int = i
  val ix: Int = i
  val a: Array[Int] = {
    assert(ix >= 0 && ix < a.length, "Array index out of range")
    a.updated(ix, v)
  }
  val tmp: Unit = ()
  val tmp: Unit = ()
  val i: Int = i - 1
  val tmp: Unit = ()
  if (i > 0) {
    initArrayWhile(v, i, a)
  } else {
    ((), i, a)
  }
}.ensuring {
  (_res: (Unit, Int, Array[Int])) => {
    val a: Array[Int] = _res._3
    val i: Int = _res._2
    (0 <= i && i < a.length) &&& !(i > 0)
  }
}

def f: Unit = {
  val a: Array[Int] = {
    assert(100 >= 0, "Non-negative array size")
    Array(0, ..., 0) (of size 100)
  }
  val i: Int = a.length - 1
  val t: (Unit, Int, Array[Int]) = if (i > 0) {
    fWhile(i, a)
  } else {
    ((), i, a)
  }
  val res: Unit = t._1
  val a: Array[Int] = t._3
  val i: Int = t._2
  res
}