Close #466 and remove stale ergonomic framing from ROADMAP

CHANGELOG.md

@@ -10,11 +10,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 - **SKILL.md documentation sweep** ([#513](https://github.com/aallan/vera/issues/513)) — eight sections added or rewritten to close agent-surfaced documentation gaps: Array literals (`[]` / `[1, 2, 3]` / type inference), Closures and captured bindings (syntax + De Bruijn shift rule + the primitives-only capture limitation + tail-recursion-with-explicit-parameters workaround), full string escape-sequence table (`\n` / `\t` / `\r` / `\0` / `\\` / `\"` / `\u{XXXX}`) with explicit unsupported list and fallback notes, Nullary vs Unit-taking function signature variants, Stored function values and `apply_fn`, Known Bugs and Workarounds section pointing at KNOWN_ISSUES.md. Additions validated against `scripts/check_skill_examples.py`; ALLOWLIST regenerated (68 unique entries, AST-verified zero duplicate keys).
 
 ### Tracked bugs
-- Four compiler bugs surfaced by an agent writing Conway's Game of Life against v0.0.119, filed + added to KNOWN_ISSUES.md + reprioritised in ROADMAP.md's implementation-order table:
+- Five compiler/runtime bugs surfaced by an agent writing Conway's Game of Life against v0.0.119, filed + added to KNOWN_ISSUES.md + reprioritised in ROADMAP.md's implementation-order table:
   - [#514](https://github.com/aallan/vera/issues/514) — closure codegen mis-emits environment when capturing heap-allocated outer bindings (Array, String, ADT). Primitive captures work; any heap capture fails at WASM validation. Root cause refined from earlier "nested closures" symptom.
   - [#515](https://github.com/aallan/vera/issues/515) — `$gc_collect` walks past `$heap_ptr` to the linear-memory bound and traps mid-sweep.
   - [#516](https://github.com/aallan/vera/issues/516) — runtime traps bubble up as raw wasmtime stack traces; CLI mis-labels every trap as "Runtime contract violation".
   - [#517](https://github.com/aallan/vera/issues/517) — no tail-call optimization; the documented tail-recursion iteration idiom blows the WASM call stack at ~tens of thousands of frames.
+  - [#522](https://github.com/aallan/vera/issues/522) — `IO.print` output lost on trap: `host_print` in `vera/codegen/api.py` appends to a Python `io.StringIO` that is only returned to the CLI after successful execution, so on the trap path the captured buffer is dropped as the exception unwinds in `execute()`. Proposed fix (not yet implemented): flush the buffer on trap before re-raising, and/or tee the host print into `sys.stdout` live. Paired with #516 in the ROADMAP queue (both are crash-debugging UX). SKILL.md Known Bugs table extended accordingly.
 
 ## [0.0.119] - 2026-04-23
 

KNOWN_ISSUES.md

@@ -15,6 +15,7 @@ Bugs and limitations tracked against the [issue tracker](https://github.com/aall
 | Closures mis-emit the environment when capturing **heap-allocated** outer bindings (`String`, any `Array<T>`, any ADT, any opaque handle like `Map`/`Set`/`Decimal`/`Regex`). `vera check` and `vera compile` succeed; `vera run` fails with "unknown table 0: table index out of bounds" or "type mismatch: expected i32, found i64" depending on the captured type. Primitive captures (`Int`, `Nat`, `Bool`, `Byte`, `Float64`) work correctly. Workaround: lift the closure body to a top-level recursive function and thread the heap value as an explicit parameter rather than via capture. The previously-documented "nested closures" and "captured-scalar through array_map" symptoms are both narrow manifestations of this same root cause. | [#514](https://github.com/aallan/vera/issues/514) |
 | `$gc_collect` itself faults with out-of-bounds memory access under sustained allocation pressure — the collector walks past `$heap_ptr` to the linear-memory bound and traps. Symptom: `memory fault at wasm address 0x... in linear memory of size 0x...` with `gc_collect` at the top of the stack. Reproduces with Conway's Game of Life on a 40×20 grid over 200 generations. Workaround: reduce allocation pressure (avoid `Option<Nat>` in hot paths; prefer `array_mapi` over repeated `array_append`) | [#515](https://github.com/aallan/vera/issues/515) |
 | Runtime traps from the WASM runtime bubble up as raw wasmtime stack traces with hex offsets. CLI mis-labels every `Trap`/`WasmtimeError` as "Runtime contract violation" even when the actual cause is out-of-bounds memory access, integer overflow, or an unreachable. No Vera-native diagnostic, no source line, no actionable "Fix:" suggestion — contrary to the rest of the toolchain | [#516](https://github.com/aallan/vera/issues/516) |
+| `IO.print` output is lost when the program traps. The `host_print` implementation in `vera/codegen/api.py` appends to a Python `io.StringIO` that is only returned to the CLI via `ExecuteResult.stdout` after successful execution; on the `except` path the buffer is discarded as the exception unwinds. Agents inserting instrumentation prints to debug a suspected crash see no output and conclude their changes weren't exercised. Fix: flush `output_buf` to `sys.stdout` in `execute()`'s trap-handling path before re-raising, and/or tee `host_print` writes into `sys.stdout` live | [#522](https://github.com/aallan/vera/issues/522) |
 | No tail-call optimization. Tail-recursive functions (the documented-idiomatic Vera loop pattern) blow the WASM call stack at ~tens of thousands of frames, trapping with `call stack exhausted`. The SKILL.md "Iteration" section positions tail recursion as the replacement for `for`/`while`, but the compiled artefact doesn't match — for any iteration deeper than ~5–10K the documented idiom silently fails. Fix is emitting WASM `return_call` in tail positions (tail-call proposal is supported by wasmtime and V8) | [#517](https://github.com/aallan/vera/issues/517) |
 | `@Nat` subtraction silently underflows to a negative i64 — the type system accepts `@Nat - @Nat : @Nat` but the runtime produces negative values in `@Nat` slots. Downstream code relying on the `Nat >= 0` invariant (including Tier-1-verified contracts) can then produce memory-safety issues via out-of-bounds `Array` indexing. Refinement-type soundness hole. Four possible fixes (trap on underflow, saturating arithmetic, promote to `@Int`, or require a compile-time non-negativity proof); option 4 is most Vera-native | [#520](https://github.com/aallan/vera/issues/520) |
 

ROADMAP.md

@@ -20,26 +20,23 @@ This section captures the concrete **implementation order** for the next few wee
 
 ### The ordering principle
 
-The near-term queue mixes issues from two categories:
+The current near-term queue is a **bug-killing campaign**. After the Stage 11 stdlib push closed most of the ergonomic gaps (missing primitives, typed accessors, ASCII character utilities — see [HISTORY.md](HISTORY.md) for the release history), the dominant source of agent friction shifted from "the language can't do this" to "the language compiles and verifies my program but the compiled artefact misbehaves at runtime."
 
-- **Capability-expansion** — unlocks *new kinds of programs that aren't possible today*. No hand-rolled workaround exists; the language literally can't do the thing.
-- **Error-reduction / ergonomic** — the program is already possible but verbose, bug-prone, or fragile. Hand-rolled recursive accumulators, manual ASCII range checks, nested Option/Json unwraps. Examples: [#466](https://github.com/aallan/vera/issues/466) (array utilities), [#470](https://github.com/aallan/vera/issues/470) / [#471](https://github.com/aallan/vera/issues/471) (string + char), [#366](https://github.com/aallan/vera/issues/366) (JSON accessors).
+A second Game of Life agent run against v0.0.119 surfaced five fresh compiler/runtime bugs in a single afternoon ([#514](https://github.com/aallan/vera/issues/514), [#515](https://github.com/aallan/vera/issues/515), [#516](https://github.com/aallan/vera/issues/516), [#517](https://github.com/aallan/vera/issues/517), [#522](https://github.com/aallan/vera/issues/522)), plus [#520](https://github.com/aallan/vera/issues/520) from targeted testing. Combined with the pre-existing GC and translator bugs ([#346](https://github.com/aallan/vera/issues/346), [#347](https://github.com/aallan/vera/issues/347), [#348](https://github.com/aallan/vera/issues/348), [#475](https://github.com/aallan/vera/issues/475), [#487](https://github.com/aallan/vera/issues/487), [#490](https://github.com/aallan/vera/issues/490)), that's twelve open bug issues — all listed below, in priority order — and one enhancement ([#507](https://github.com/aallan/vera/issues/507)) at the tail.
 
-Both matter, but they're asymmetric in timing: capability gaps are *blocking* (entire program categories don't exist), ergonomic gaps are *annoying* (programs compound verbosity). Blocking issues front-load more value per hour because they unlock whole genres of program. The current state of the language is "most programs possible, some categories blocked" — so capability-expansion goes first, ergonomic polish follows.
+The agent's self-observation on why this matters:
 
-Empirical confirmation from a model writing Conway's Game of Life in Vera while this queue was being planned:
+> *The gap between "the type system is happy" and "the compiled artefact actually runs" is wider than you'd expect from a language with SMT-verified contracts. The verifier can prove your termination argument is sound while the codegen silently miscompiles your closure environment out from under you.*
 
-> "The bug fix plus `IO.sleep` and Random are transformative. With `IO.sleep` I can write a proper animation loop… With Random I can generate a random soup initial state instead of hardcoding a glider and blinker, which is dramatically more interesting to watch. The program goes from 'dump 20 static frames' to 'animated random cellular automaton that runs in your terminal.' From [#466](https://github.com/aallan/vera/issues/466), `array_any` is useful for detecting extinction, and `array_contains` could simplify some checks, but neither is essential. From [#470](https://github.com/aallan/vera/issues/470), `string_pad_start` would let me right-align the generation counter — minor polish."
-
-This reshaped the ordering: capability issues move up, ergonomic issues move down. Completed items are noted in [HISTORY.md](HISTORY.md).
+Closing that gap is the highest-leverage agent-adoption work available. Priority order below is by "impact on an agent trying to write a non-trivial program today," not by implementation difficulty.
 
 ### Implementation order
 
 | Order | Issue | Why now |
 |:---:|---|---|
 | 1 | [#514](https://github.com/aallan/vera/issues/514) — Nested closures + captured-scalar indirection codegen bugs | Two linked WASM codegen bugs surfaced by an agent writing Conway's Game of Life. Shape (a): nested closures fail at compile time; shape (b): a closure capturing a scalar that flows into `array_map` via a helper traps at runtime. The natural two-dimensional-map idiom (`array_map(rows, fn(row) { array_map(cols, fn(col) { ... }) })`) trips both. The language's headline ergonomic feature (higher-order array ops) is broken for the common nested case. |
 | 2 | [#515](https://github.com/aallan/vera/issues/515) — `$gc_collect` itself faults under sustained allocation pressure | GC walks past `$heap_ptr` to the linear-memory bound and traps. `gc_collect` at the top of the stack means the collector, not the program, is the crashing frame. 40×20×200 Conway reliably reproduces. A collector that faults mid-sweep is unshippable for any program with meaningful allocation pressure. |
-| 3 | [#516](https://github.com/aallan/vera/issues/516) — Runtime traps need Vera-native diagnostics | Runtime traps bubble up as raw wasmtime stack traces; CLI mis-labels every trap as "Runtime contract violation". Closes the "type-checks clean, runtime crashes opaque" gap that agent feedback is calling out. Three-stage scope: categorise the trap reason, source-map the Vera function that trapped, specialise help for common trap classes. |
+| 3 | [#516](https://github.com/aallan/vera/issues/516) + [#522](https://github.com/aallan/vera/issues/522) — Crash-debugging UX | Two paired issues. #516: runtime traps bubble up as raw wasmtime stack traces; CLI mis-labels every trap as "Runtime contract violation". Three-stage scope: categorise the trap reason, source-map the Vera function that trapped, specialise help for common trap classes. #522: `host_print` writes to a Python `io.StringIO` that's only returned to the CLI after successful execution, so any `IO.print` preceding a trap is discarded as the exception unwinds in `execute()` — instrumentation prints disappear exactly when they are most needed. Fix is flushing the captured buffer on the trap path (and/or teeing `host_print` into `sys.stdout` live). Together they close the "type-checks clean, runtime crashes opaque, can't even instrument" gap that agent feedback is calling out. |
 | 4 | [#517](https://github.com/aallan/vera/issues/517) — Tail-call optimization missing | The documented `for`/`while`-replacement idiom (tail-recursive functions) silently fails for iteration deeper than ~5–10K — WASM `call stack exhausted`. Emit `return_call` in tail positions; wasmtime and V8 already support the tail-call proposal. Discovered during the same Game of Life run that surfaced #514/#515/#516 — the agent blew the stack trying to stress-test the GC bug with 100K recursive iterations. |
 | 5 | [#520](https://github.com/aallan/vera/issues/520) — `@Nat` subtraction silent underflow (soundness hole) | Type system accepts `@Nat - @Nat : @Nat` but runtime emits a plain `i64.sub` with no underflow check — negative values can end up in `@Nat` slots. Any Tier-1-verified contract that relied on `Nat >= 0` is then logically undermined, and `Array[@Nat]` indexing with a negative `@Nat` becomes a memory-safety issue. The refinement-type layer's central promise ("this value is non-negative") doesn't hold. Probably fixable with a compile-time non-negativity proof obligation at subtraction sites (option 4 in the issue). |
 | 6 | [#475](https://github.com/aallan/vera/issues/475) — WASM call translator bug cleanup | Three Critical severity pre-existing bugs from the v0.0.113 calls.py decomposition: `_translate_handle_exn` missing catch-arm result type for expression-bodied handlers; `_translate_string_slice` i64→i32 narrowing before clamping (wraps to negative, then clamps to 0); `_translate_char_code` missing bounds check (out-of-range index reads arbitrary memory — real safety hole). Plus 7 Major-severity bugs. Correctness debt sitting since mid-April. Small, focused, independent fixes. |