Summary

Vera lacks tail-call optimization. Recursive functions written in tail-call form still grow the WASM call stack and trap with call stack exhausted at modest recursion depths (~tens of thousands of frames, depending on parameter count and the size of each frame). This undercuts the "iteration is tail recursion" idiom that SKILL.md documents as the canonical loop pattern.

Reproducer

private fn count_down(@Nat -> @Nat)
  requires(true) ensures(true) effects(pure)
{
  if @Nat.0 == 0 then { 0 } else { count_down(@Nat.0 - 1) }
}

public fn main(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{
  nat_to_int(count_down(50000))
}

wasm trap: call stack exhausted

The function is textbook tail-recursive (the recursive call is the last expression on the else branch, no work after it). With TCO it should iterate in constant stack space and return 0. Without TCO it uses one WASM stack frame per iteration and traps once the stack is full.

Why this matters

SKILL.md "Iteration" section positions tail recursion as the replacement for for/while:

Vera has no for or while loops. Iteration is always expressed as tail-recursive functions.

And the example it shows is a recursive loop(limit, counter) that calls itself on @Nat.1, @Nat.0 + 1. For any program that iterates more than ~5-10K times the documented idiom silently fails — whereas a language targeting LLM authors absolutely needs the documented idiom to work. The Conway's Game of Life agent run that surfaced #514 and #515 also hit this limit indirectly when it tried to stress-test with 100,000 recursive iterations to isolate the GC crash cause.

Scope

Two paths, each independently valuable:

1. Emit WASM return_call for tail positions. WASM's tail-call proposal is standard and supported by wasmtime. This would fix the common case automatically and align the runtime behaviour with the documented idiom.

2. Detect tail position in the compiler (vera/wasm/calls.py and friends) and emit return_call only when the call really is in tail position — not behind an if arm when the other arm does work, not inside a let that binds the result, etc. The tail-position analysis is standard and small.

Notes

wasmtime has enabled --wasm-features=tail-call for a while; modern Node.js / V8 also support it. So the change is purely in the code generator, not in the runtime dependencies.

Discovered during the Game of Life agent run that also filed #514, #515, #516. That same run is now working around the missing TCO by cutting recursion depth, which was why it couldn't run a 100K-iteration isolation test for the GC bug — it blew the stack instead.