A law whose goal is an unfolded loop state with a large fuel numeral still overflows the stack (2.0.24), in term_snf rather than the renderer

[nohzafk]

The fix for #895 covers the renderer. A proof goal that is an unfolded loop
state with a large fuel numeral still overflows the stack, in
term_snf -> term_wnf -> term_higher.

That is the case in your closing note on #895: the crash bites a real proof,
not a diagnostic.

Repro

crash_fuel.bend, 20 lines, Base only:

import Base

type S is Data:
  A{s: String, k: Nat}
  B{s: String, e: Bool, k: Nat}

def go(fuel: Nat, st: S) -> Nat:
  match fuel st:
    case 0n _:
      0n
    case 1n+f A{+s, k}:
      go(f, B{s, String.eq(s, "q"), k})
    case 1n+f B{+s, True{}, k}:
      go(f, A{s, k})
    case 1n+f B{+s, False{}, k}:
      go(f, A{s, k})

law done:
  for s: String
  {go(U32.to_nat(4294967295), A{s, 0n}) == 0n : Nat}

def done(s):
  {==}

$ bend crash_fuel.bend
RangeError: Maximum call stack size exceeded.
    at term_higher (/$bunfs/root/bend:361:32)
    at term_wnf (/$bunfs/root/bend:2323:24)
    at term_snf (/$bunfs/root/bend:2496:22)

Only the fuel numeral changes. Everything else in the file stays the same.

fuel in the law	2.0.20	2.0.24
4n, 40n, 1000n, 10000n	expected/observed	expected/observed
100000n	RangeError	RangeError
4294967295n	RangeError	RangeError

Darwin arm64, bun 1.3.14, bend 2.0.24 installed with bend update.

A numeral in a goal is fine now

Your renderer fix holds. This law has a large numeral in the goal, no loop
and no match:

law big:
  for x: Nat
  {Nat.add(x, 4294967295n) == 4294967295n : Nat}

2.0.24: expected : Nat.add(x, 4294967295n) / observed : 4294967295n
2.0.20: RangeError

So the remaining crash is a different path, and it needs the goal to be an
unfolded loop state. With input that is ground, the loop runs to its exit and
no numeral is left in the goal. With input that is abstract, the loop stops at
the first comparison, and the goal is the state constructor with the stuck
comparison inside it and the fuel as a numeral:

expected : go(4294967294n, B{String.eq.fin(String.cmp(s, "q")), 0n})

Why it blocks real work

A fuel counter is the only loop shape the language allows, and App.run
enters its loop with U32.to_nat(4294967295). So the proof that cannot be
written is the one about a program that runs longer than a moment.

The workaround costs the statement, not the proof. I state the law over
run(200n, state) instead of over the function callers use:

law chain_symbolic:
  for +a: String
  for +b: String
  {R.run(200n, R.MN{...}) == ... : R.RRes}

200 steps is more than the graph needs, so nothing is weakened -- but the
statement is no longer about the function whose fuel is fixed at 4294967295
inside its body. With the small fuel the proof goes through, and the same
theorem one node longer stops cleanly at a comparison between two abstract
names. The crash is the only reason the statement had to move.

Relation to #895

#895 was closed with: the renderer walks a Nat literal as its Succ chain, an
iterative renderer is not worth the checker code, and "we will revisit if the
stack guard bites a real proof rather than the renderer."

The renderer fix works. This is the other path, and it is a proof:

• Both crashes walk term_snf. A failing law over a Nat literal from about 12200n crashes the error renderer with RangeError instead of printing expected/observed #895 ends in expr_show (the diagnostic);
  this one ends in term_wnf -> term_higher (normalizing the goal for the
  check itself).
• In 2.0.24 the pure-numeral goal above prints its mismatch, so the renderer
  is no longer the one that dies.
• The goal here is not a hint about a variable: it is the loop's state with
  the fuel reduced, which is what a proof about that loop has to be written
  against.

Question

Is the walk on the fuel numeral inside term_higher, or on the state? If the
numeral is the cause, a bound on that traversal would give expected/observed
here as well, which is what #895 asked for on the renderer path.

---

The reproducer and the measurements were run by me with an AI assistant. The
commands are reproducible from the files above.