Stainless crash: `Variable ... is not defined in context` when lifting two `while` loops

[sfiruch]

Claude reports:

object CrashRepro {
  def f(t: Int, rob: Int, lim: Int): Int = {
    require(rob >= 0 && t >= 0 && lim >= 0)
    var cT = 0
    var vT = rob
    if (t != 0) {
      cT = 0
      vT = cT + rob
      var cont = true
      (while (cont && vT <= t && vT <= lim) {
        decreases(lim - vT + (if (cont) 1 else 0))
        if (vT < lim) { cT = cT + 1; vT = cT + rob } else { cont = false }
      }).invariant(cT >= 0 && vT >= rob)
    }
    var i = 0
    var acc = 0
    (while (i < 8) {
      decreases(8 - i)
      acc = acc + (if (vT > i) 1 else 0)
      i = i + 1
    }).invariant(i >= 0 && acc >= 0)
    vT + cT + acc
  }
}

• Stainless: 0.9.9.3 (stainless-dotty-standalone-0.9.9.3.jar, Scala 3.7.2)
• JVM: any (reproduced on Zulu OpenJDK 26.0.1)
• OS: reproduced on Windows 11; not OS-specific.

How to reproduce

stainless --config-file=false CrashRepro.scala

Observed behaviour

Stainless aborts with:

[ Fatal  ] CrashRepro.scala:33:7: Variable cT 2 is not defined in context:
[ Fatal  ] Kind: error: argument types (call fWhile(cT, lim, rob, t, vT, i, acc, vT))
[ Fatal  ] Functions: fWhile
...

inox.package$FatalError: Variable cT 2 is not defined in context
    at inox.Reporter.fatalError(Reporter.scala:56)
    at stainless.verification.TypeChecker.inferType(TypeChecker.scala:723)
    at stainless.verification.TypeChecker.checkType(TypeChecker.scala:1262)
    ...

Expected behaviour

The program should either verify normally or report a legitimate user error — not
abort with an internal "not defined in context" failure.

What seems to be going on

The function f contains two while loops. Both are lifted to a helper named
fWhile — i.e. the generated names collide (no disambiguating suffix). From the error
dump, the two call sites have different signatures:

• inner loop (inside the if): fWhile(lim, rob, t, cT, vT, cont) — 6 args
• trailing loop (after the if): fWhile(cT, lim, rob, t, vT, i, acc, vT) — 8 args

Resolving one call against the other fWhile definition leaves cT undefined in the
calling context, which is what the type-checker reports.

Minimisation notes

All of the following are required; removing any one makes the error disappear:

• two local vars where one is defined in terms of the other (vT = cT + rob);
• both reassigned inside a while loop that is nested inside an if;
• a boolean loop-guard var (cont) updated in the loop body;
• one of the outer vars (vT) read by a second while loop after the if.

In particular, collapsing to a single var (dropping vT), or deleting the trailing
while loop, both make it compile cleanly.

[samuelchassot]

@kasiaMarek would it be solved by #1731? Or can it be solved at the same time?

[kasiaMarek]

@kasiaMarek would it be solved by #1731? Or can it be solved at the same time?

It may get fixed, I'll check.

Update: Still fails but with a different error 😄.

[kasiaMarek]

I look a bit at this issue (after #1731 ). The problem is that the definition of one of the inner functions ends up in the refinement.

Here is a small repro:

object CrashRepro:
  def foo(b : Boolean) =
    val y = 
      if b then
        val x = 42
        def bar() = x
        bar()
      else 0
    def baz() = y
    baz()

Since, I don't think I will have the time to fix it soon. Here is the description of the issue in more detail. Since bar() and baz() will be considered the same level of nesting (neither nested in a nested function), FunctionClosure will try to bring them to top-level at the same time. The issues span from x and bar being defined inside val (this is the same thing that happens in the original issue after some transformations).

• The first issue is that for y we create a parameter to baz, with refinement y = if b then { val x = 42; ...} else 0. So the definition of bar() will end up in the refinement. Due to freshenLocals (line 103 in FunctionClosure), in the definition of rhs of baz this local definition will be freshened and that occurrence of ApplyLetRec will have a local function id not included in closed (won't match the pattern in line 266). This is a new issue after fix an issue with function closure with refinement types #1731.
• The second issue (which was already present in some form before fix an issue with function closure with refinement types #1731). Is that when collecting variables for baz (see: transFree) x will be on that list, yet it is not in scope cannot to be passed as an argument to baz.
• Even if we remove x from variables passed to baz, when later transforming the refinement of y (see: ClosingTransformer), the maps that correlate arg to param will correlate the param x to bar with the old x in the definition of foo not the freshened, local one in the refinement of y. Which will result in trying to pass to bar (in the refinement of y) x that is defined in foo, so again not in scope.

I think the easiest solution would be to lift each function one by one. This way if we first lift bar, the refinement of y will already have the correct call to the top-level definition of bar. This, unfortunately, requires some adjustments to s.tree and t.tree type, since the previous assumption that the transformed (once) function has no local defs is invalid.