@inlineOnce on recursive functions

[jad-hamza]

Since I've enabled inlining (once) of recursive functions in themselves, this example fails:

import stainless.annotation._
import stainless.collection._
import stainless.lang._

object InlineOnce {
  def test(l: List[BigInt]): Unit = {
    require(arePositive(l) && !l.isEmpty)
    assert(arePositive(l.tail))
  }

  @inlineOnce
  def arePositive(l: List[BigInt]): Boolean = {
    decreases(l)
    l.isEmpty || (l.head >= 0 && arePositive(l.tail))
  }
}

After inlining, arePositive(l) becomes equivalent (ignoring small lists) to:

l.head >= 0 && l.tail.head >= 0 && arePositive(l.tail.tail)

The VC for the assertion looks like (again ignoring small lists):

(l.head >= 0 && l.tail.head >= 0 && arePositive(l.tail.tail)) ==>
(l.tail.head >= 0 && l.tail.tail.head >= 0 && arePositive(l.tail.tail.tail)) ==>

The problem is that unrolling arePositive(l.tail.tail) will only give us arePositive(l.tail.tail....tail.tail) for an even number of tails, wihle we need in the conclusion arePositive on an odd number of tails. I think we already had this discussion and that might have been the reason we disabled inlining (once) in own body.

I could revert @inlineOnce to have the old behavior of not inlining in the own function, and introduce another annotation @inlineOnceSelf for inlining in own body.

[samarion]

Just curious, in which situations are we expecting @inlineOnceSelf to make a big difference?

[jad-hamza]

I wanted it when verifying a recursive function, and marked it as @inlineOnce @opaque, in order to make the specification of the recursive call "immediately available" without unrolling. I don't know if it was really required for the verification to go through, but I thought it could help.

[samarion]

If we ever migrate to using refinement types instead of post-conditions, we could implement this "immediate inlining of post-conditions" in a cleaner way at the Inox level.