Closes #517.  Spawns #549 for the GC-aware-TCO follow-up.

Pre-fix, every Vera `call` site emitted a plain WASM `call`
regardless of tail-position status, so a tail-recursive function
pushed one WASM frame per iteration and trapped with `call stack
exhausted` at ~tens of thousands of frames.  The documented
"iteration is tail recursion" idiom from SKILL.md silently failed
past ~5-10K iterations.

Fix is a per-fn analyzer (vera/codegen/tail_position.py) that marks
id(FnCall) AST nodes in syntactic tail position; _translate_call
emits `return_call $foo` instead of `call $foo` when the call's id
is in the marked set AND the callee's WASM return type matches the
caller's (required for WASM return_call semantics — the signature
must match).

Tail-position analyzer rules:
* Body trailing expression IS in tail position
* If parent is tail and is IfExpr: both branches tail (cond NOT)
* If parent is tail and is MatchExpr: every arm body tail (scrutinee NOT)
* If parent is tail and is Block: trailing expr tail (statements NOT)
* All other constructs: NOT tail-transparent

Allocating-function fallback (#549 follow-up):
* WASM return_call discards the current frame, which means the GC
  epilogue (restore $gc_sp, unwind shadow stack) never runs.  For
  an allocating function, that leaks shadow-stack slots once per
  iteration and would eventually trap on the next $alloc once
  gc_sp passes the worklist boundary — strictly WORSE than the
  pre-fix "stack exhausted" trap.
* Post-process at the end of _compile_fn reverts every
  return_call → call when ctx.needs_alloc is True.  Allocating
  functions pay the WASM frame cost in exchange for correct
  shadow-stack management until #549 ships GC-aware tail calls.

Verified:
* 50K count_down (issue's canonical reproducer) returns 0 cleanly
* 1M count_down also returns 0 cleanly (constant stack space)
* Test fixtures in tests/test_runtime_traps.py updated to keep
  trap-bearing calls in NON-tail position via let-binding —
  otherwise TCO discards main's frame and the existing backtrace
  assertions wouldn't see main in the resolved chain.

Tests: 9 new in TestTailCallOptimization517 (50K + 1M behavioural,
return_call structural assertion, non-tail plain-call assertion,
allocating-function fallback, 4 analyzer unit tests for each
tail-transparent construct).

Documentation:
* stack_exhausted Fix paragraph rewritten to reflect post-fix
  reality ("Vera compiles tail-position calls to return_call ...
  if you're still hitting this trap the recursion isn't actually
  in tail position; restructure with an accumulator parameter").
* KNOWN_ISSUES: #517 row removed; new #549 row tracking the
  GC-aware TCO follow-up for allocating functions.
* ROADMAP: #517 dropped from queue (intro updated, eight remain
  in campaign), priority rows renumbered.
* HISTORY: terse v0.0.126 row per the hardened memory rules
  ("Tail-recursive iteration runs in constant stack space"
  ([#517])).

3,613 tests pass (was 3,604; 9 new) + 14 skipped.  mypy clean.
81 conformance + 33 examples pass.  uv.lock regenerated.

Co-Authored-By: Claude <noreply@anthropic.invalid>

…est strengthening

Four CodeRabbit findings actioned.  The first is a real Major-
severity correctness bug that would have shipped as a soundness
hole; the other three are test/doc quality improvements.

* vera/codegen/functions.py: postcondition-aware tail-call
  fallback.  Pre-fix, body_instrs revert (return_call -> call) was
  gated only on ctx.needs_alloc.  But _compile_postconditions
  also emits instructions AFTER body_instrs (local.set $ret,
  condition check, trap on failure, local.get $ret to push back),
  and WASM return_call discards the current frame — so any
  function with a non-trivial ensures clause AND a tail-recursive
  call would silently skip the postcondition check on every
  iteration, violating the contract.  Moved the revert to AFTER
  _compile_postconditions runs and added the post_instrs check:
  now reverts return_call when EITHER ctx.needs_alloc OR
  post_instrs is non-empty.

  This was a soundness hole — the v0.0.126 PR as it stood would
  have shipped a runtime where ensures clauses on tail-recursive
  functions silently passed regardless of the actual return
  value.  Caught by CodeRabbit before merge.

* tests/test_codegen.py: new
  test_postcondition_function_falls_back_to_plain_call.
  Constructs a tail-recursive function with a non-trivial
  ensures clause (`@Nat.result >= 0`) and asserts that the
  recursive call site emits plain `call`, not `return_call`.
  Pins the new fallback condition so a future revert of the
  postcondition check would fail this test loudly rather than
  silently regressing the soundness.

* tests/test_codegen.py: strengthened
  test_no_return_call_for_non_tail_position.  Was asserting only
  the negative (caller's let-bound call is NOT return_call).
  Added the positive sibling assertion: count_down's recursive
  call IS return_call.  Without the positive check, a buggy
  analyzer that marked NOTHING would silently pass the negative
  assertion while regressing the actual TCO behaviour — both
  branches need explicit pinning.

* tests/test_codegen.py: strengthened
  test_analyzer_does_not_mark_call_args.  Was asserting only
  len(sites) == 1.  Now locates the specific FnCall AST nodes
  (outer `inner(...)` and inner-arg `arg_producer()`) by
  walking the parsed AST, asserts id(outer) IN sites AND
  id(arg) NOT IN sites, and pins the exact set
  (`sites == {id(outer)}`).  A buggy analyzer that marked the
  WRONG call would have passed the old `len == 1` assertion
  while regressing the analyzer's tail-position detection.

* TESTING.md: corrected the Tests row from 3,613 / 3,590
  passed / 14 skipped to 3,614 / 3,600 passed / 14 skipped.
  3,590 was the previous release's passed count; the v0.0.126
  PR added 9 new tests (now 10 with the postcondition test
  added in this round) but I forgot to update the breakdown in
  the same commit.  Aggregate and breakdown are now in sync
  and pytest-collected total matches.

3,600 tests pass + 14 skipped (was 3,599 + 14, +1 for the new
postcondition test).  mypy clean.

Co-Authored-By: Claude <noreply@anthropic.invalid>

Both CodeRabbit findings actioned.

* TESTING.md test_codegen.py row description updated to mention
  both stress tests: "50K- and 1M-iteration stress" instead of
  just "1M-iteration stress".  The 50K test is the issue's
  canonical reproducer (count_down(50000)) and the 1M test pins
  constant-stack-space behaviour on top.  Both ship; the
  description now reflects both.  Also expanded the analyzer
  unit-test list inline ("Block-trailing / IfExpr-both-branches
  / MatchExpr-arm-bodies / let-value-NOT-marked /
  call-args-NOT-marked") so the test inventory matches the
  shipped contract per CodeRabbit's pattern from previous PRs.

* tests/test_codegen.py: new test_analyzer_marks_match_arm_bodies.
  Pre-fix, the analyzer (vera/codegen/tail_position.py) had
  MatchExpr handling but no explicit test pinning the behaviour;
  a regression that dropped or mis-handled the MatchExpr case
  would have slipped past CI silently.  New test constructs a
  function whose body is a match with two arms — one arm wraps
  its tail call around a non-tail argument call — and asserts:

  - Both arm-body calls (the outer arm_handler(...) on each arm)
    are in sites.
  - The nested argument call (arg_producer(())) inside the None
    arm is NOT in sites.
  - sites is exactly {id(none_arm_call), id(some_arm_call)} —
    exhaustive cardinality + identity check.

  Same exhaustiveness pattern as the round-1 strengthening of
  test_analyzer_does_not_mark_call_args (assert specific ids,
  not just count).

3,601 tests pass (was 3,600; +1 for the MatchExpr analyzer test)
+ 14 skipped.  mypy clean.

Co-Authored-By: Claude <noreply@anthropic.invalid>

CodeRabbit's single finding actioned with three new tests covering
the non-tail roots inside tail-transparent constructs.  Each test
mirrors the existing analyzer-test pattern (parse_to_ast, walk
the AST to locate the specific FnCall, assert id() NOT in sites,
plus an exhaustive sites == set() check).

* test_analyzer_does_not_mark_call_in_block_statement — pins
  ExprStmt-position calls (the LetStmt.value case is already
  covered by test_analyzer_does_not_mark_let_value_calls).  A
  Block with a leading ExprStmt(FnCall(...)) and a trailing
  IntLit must mark NOTHING — statements are not tail-transparent.

* test_analyzer_does_not_mark_call_in_if_condition — pins
  IfExpr.condition position.  An if-expression's condition is
  evaluated and consumed before either branch runs, so a call
  there is non-tail regardless of whether the if-expression
  itself is in tail position.

* test_analyzer_does_not_mark_call_in_match_scrutinee — pins
  MatchExpr.scrutinee position.  Same reasoning: the scrutinee
  is evaluated and consumed by the match-dispatch (constructor
  tag check + field binding) before any arm runs.

Each test would catch a regression where the analyzer started
visiting non-transparent positions with the parent's tail
status — which would silently emit return_call in those
positions, discard the current frame, and skip the work that
should have consumed the call's result (the if-dispatch, the
match-dispatch, or the trailing block expression).

The TCO test inventory now covers every transparent /
non-transparent position individually:
* Transparent (tail propagates): Block trailing expr, IfExpr
  branches, MatchExpr arm bodies.
* Non-transparent (tail does NOT propagate): LetStmt.value,
  ExprStmt.expr, IfExpr.condition, MatchExpr.scrutinee,
  FnCall.args.

3,604 tests pass + 14 skipped (was 3,601, +3 for these
negative tests).  mypy clean.

Co-Authored-By: Claude <noreply@anthropic.invalid>

Single CodeRabbit finding actioned.  TESTING.md test_codegen.py
row description now lists the three round-3 negative analyzer
tests explicitly:

* ExprStmt-statement-NOT-marked
* IfExpr-condition-NOT-marked
* MatchExpr-scrutinee-NOT-marked

Appended to the existing analyzer-unit-test inventory after the
positive coverage (Block-trailing / IfExpr-both-branches /
MatchExpr-arm-bodies) and the previously-listed negative cases
(let-value-NOT-marked / call-args-NOT-marked).

The inventory now exhaustively names every position the analyzer
visits or skips — matches the shipped test contract:

* Transparent (tail propagates inward, marked tests):
  Block-trailing, IfExpr-both-branches, MatchExpr-arm-bodies.
* Non-transparent (tail does NOT propagate, NOT-marked tests):
  let-value, call-args, ExprStmt-statement, IfExpr-condition,
  MatchExpr-scrutinee.

Co-Authored-By: Claude <noreply@anthropic.invalid>