Pre-fix, WASM return_call reverted to plain call whenever a function
had needs_alloc=True, because return_call discards the current frame
and would skip the GC epilogue, leaking shadow-stack slots per
iteration.  This forced agents to restructure allocating tail-
recursive code into array_fold/array_map shapes or to hoist
allocations outside the recursion.

The fix preserves TCO AND the shadow-stack invariant: instead of
reverting, the post-process now PREPENDS a two-instruction $gc_sp
restore (local.get $gc_sp_save; global.set $gc_sp) immediately
before each return_call in an allocating function.  Args are
already on the WASM operand stack at the return_call site; the
restore only touches the $gc_sp global, so args transfer atomically
to the callee.  The callee's prologue saves a clean new $gc_sp
baseline, so per-iteration shadow-stack usage stays bounded at
caller's entry + n_arg_roots regardless of iteration count.

Postcondition-bearing functions still revert to plain call — the
runtime postcondition check needs to run after each call, and
return_call would skip it.  Dispatch precedence: postcondition-
revert > GC-aware-TCO-patch > untouched.

Tests:
- Updated TestTailCallOptimization517 — renamed the falls-back
  test to test_allocating_function_uses_gc_aware_tco_549 and
  inverted assertions; added test_allocating_function_with_
  postcondition_still_reverts for precedence.
- Updated TestGCShadowStackOverflow::test_shadow_stack_overflow_
  traps to use a non-tail-recursive shape that still genuinely
  overflows post-#549.
- tests/test_stress.py — switched the existing 1K-iter deep-tail
  test from string-pool literals (didn't actually set needs_alloc)
  to genuine array allocation; added a 1M-iter companion
  parametrised over default/eager-GC.

Closes #549.

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

The #549 post-process inserts `local.get $gc_sp_save; global.set
$gc_sp` immediately before each `return_call` site in an allocating
function.  Pre-fix the two inserted lines were appended as raw
strings with no leading whitespace, so the rendered WAT looked
misaligned when the `return_call` was nested inside an `if/else`
(operators.py prepends 2 spaces to every instruction inside a
then/else arm; functions.py later prepends 4 more at the body-level
stringify step — so a nested return_call carries 6 leading spaces
while my inserted lines only got 4).

Functionally inert — WAT parses by tokens, not whitespace — but
visually misleading for anyone reading the WAT for debugging.

Fix: copy the leading whitespace from the original return_call
line and apply it to both inserted lines so the restore sequence
visually nests at the same depth as the return_call it precedes.

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

Surfaced during #549 review when the user pointed out that the
compiler currently stamps WAT indentation onto instruction strings
inline at ~14 emission sites scattered across vera/wasm/ and
vera/codegen/.  This is implicit-by-convention: any new emission
site that doesn't know about it produces visually-misaligned WAT
(as #549's GC-aware TCO post-process did initially.

Vera source has vera fmt because consistent presentation matters
for a debuggable surface.  Same principle applies to compiler-
emitted WAT — the primary surface agents read when debugging
codegen bugs.  Logged as #672 for a single-pass formatter that
walks s-expression and control-flow depth and applies canonical
indentation.

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

1. **Ruff S101** (CI failure) — two `assert gc_sp_save is not None`
   in `vera/codegen/functions.py` flagged by the `Security lint
   (ruff S rules)` job.  Both are pure mypy type-narrowing asserts
   (the variable is `int | None` and we're inside an
   `if ctx.needs_alloc:` block where it's guaranteed non-None).
   Added `# noqa: S101` to both sites, matching the existing
   project precedent in `vera/codegen/api.py` (five similar sites).

2. **Finding 1: HISTORY.md footer release count** (valid) — the
   table-footer total still read "153 tagged releases" after the
   v0.0.154 row landed.  Bumped to 154 to match the README figure.

3. **Finding 2: postcondition test tightened** (valid) — the
   test only asserted `return_call $build` is absent; a future
   regression that mistakenly took BOTH the postcondition-revert
   and the GC-aware patch paths would slip through.  Added a
   structural assertion that no `local.get N; global.set $gc_sp`
   pair precedes any plain `call $build` site, pinning the
   dispatch precedence (post_instrs revert and GC-aware patch are
   mutually exclusive, not additive).  Cannot forbid the sequence
   outright because the GC epilogue at function-end legitimately
   contains it.

4. **Finding 3: GC-aware TCO test now matches exact prologue local**
   (valid) — previously the test only required `local.get <any>`
   two lines before `return_call`.  Now we parse the GC prologue
   (`global.get $gc_sp; local.set <N>`) at function entry to
   capture the exact `$gc_sp_save` local index, then require the
   preamble at each return_call site uses *that same* local.  A
   typo or off-by-one in the patch code that picked up an
   unrelated local would now fail.

5. **Finding 4: shadow_stack_overflow_traps WAT structural check**
   (partially valid, added) — `_run_trap` alone proves "something
   trapped" but not "the shadow-stack-overflow guard fired
   specifically."  Added a structural assertion that the
   distinctive `global.get $gc_stack_limit` token appears in the
   `$overflow` function body, catching a hypothetical regression
   where the guard is silently dropped but `_run_trap` still
   passes via an unrelated trap class.

TESTING.md test_codegen.py line count updated to reflect the new
test additions (107 lines).

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

**Finding 1: TESTING.md stress count inconsistency** (valid) —
header table said `test_stress.py` has 16 instances but the
detailed section still read "8 initial test programs" and
"14 parametrised instances".  Fixed cohesively:
- `### The 8 initial test programs` → `### The 9 initial test
  programs` so the section claim matches the header.
- Added entry **9. `test_tco_with_allocation_1m_iterations`** so
  the section actually enumerates what it claims to.
- Updated test #3's stale narrative — this PR switched its body
  from `let @string = "stress"` (which doesn't trigger
  needs_alloc because string-pool literals don't allocate) to
  `let @array<Int> = [_, _]` (genuine heap alloc).  Old text
  asserted == 6,000 from `string_length("stress")`; new text
  asserts == 2,000 from `array_length([_, _])`.  Without this
  update the doc described a test that no longer exists.
- "Six of the eight" → "Seven of the nine" in the eager-GC lane
  paragraph (math now adds up to 16 with the 9th test).
- CLI examples and Budget line updated from 14/8 to 16/9.

**Finding 2: boundary-safe regex in WAT searches** (valid) — the
three #549 tests used plain `.find("(func $build")` and
`"return_call $build" in body` substring matches.  Today's test
source defines only `$build` and `$f` so there's no false-match
risk, but a future symbol like `$build_helper` would match
falsely.  Switched all three tests to `re.search` with
boundary-safe patterns:
- `re.search(r"\(func \$build\b", ...)` for function-start.
- `re.search(r"return_call \$build\b", ...)` for return_call
  sites (trailing `\b` excludes `$build_anything`).
- `re.search(r"\bcall \$build\b", ...)` for plain call sites
  (leading `\b` rules out `return_call $build`; trailing `\b`
  rules out `$build_anything`).
- Same boundary-safe extraction applied to `$overflow` in
  `test_shadow_stack_overflow_traps`.

Note on CR's literal suggested pattern `r'\b\(func \$build\b'`:
the leading `\b\(` is incorrect — `\b` requires a word-char on
one side, but `(` is preceded by whitespace or newline (both
non-word) at WAT indentation depths, so that anchor wouldn't
match.  Dropped the leading anchor; kept the substantive
trailing `\b`.

Scope decline: did NOT update the pre-existing tests in the
file that use the same substring-search pattern (the #517 tests
on lines 1899/1934/1949/1968/2016/2027 etc.).  Those existed
before this PR and changing them is out of scope for #549.
CR's relayed wording said "apply the same replacement to the
analogous checks later in the file" — interpreted as the
analogous checks in MY new/modified tests, not the entire pre-
existing test suite.

Validation: pytest passes (3862/3862), mypy clean, ruff S
rules clean, doc-counts consistent (test_codegen.py grew by
+39 lines from the regex switchover; TESTING.md updated to
match).

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