SKILL doc fixes + ROADMAP browser-target tier from Conway's Life agent experiments

CHANGELOG.md

@@ -6,6 +6,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### Documentation
+- **SKILL.md** — three doc fixes surfaced by an agent writing Conway's Game of Life from scratch on current main.  `array_length`'s SKILL comment updated from *"returns Int (always >= 0)"* to *"returns Nat (the array length, flows to either Nat or Int positions)"* to match user-visible behaviour (the type checker permits `Int <: Nat` via verifier-enforced refinement, so the result flows freely into either).  `array_fold` example gains a three-line comment making the closure shape explicit (`fn(@Acc, @Elem -> @Acc)` with the rightmost-is-`.0` derivation), so agents no longer have to write a probe to determine the parameter order.  New "Tuples" subsection under "Composite types" showing `Tuple(...)` construction and `match` destructuring — previously SKILL mentioned `@Tuple<Int, String>` only as a type with no construction example, leading agents to hunt for tuple-literal syntax that doesn't exist and abandon valid approaches.
+
+### Tooling
+- **`scripts/check_skill_examples.py`** allowlist re-anchored after the SKILL line offsets shifted; one stale redundant entry pruned (the Non-exhaustive Match section had three allowlist entries but only two actual code blocks); one mis-anchored entry corrected (a "bare `@Int + @Int`" allowlist entry was parked on a parseable full-function example, suppressing it).
+
 ## [0.0.138] - 2026-05-07
 
 ### Fixed

KNOWN_ISSUES.md

@@ -10,6 +10,8 @@ Bugs and limitations tracked against the [issue tracker](https://github.com/aall
 | Conservative GC scan can spuriously retain heap objects via the host-handle field of a wrapper ADT (#573 latent). Phase 2b scans wrapper payloads word-by-word; the `handle` at offset 4 is a small i32 that stays below `gc_heap_start` (~147 KiB) for typical programs, so the heap-range check rejects it. Long-running programs (>100K host-store allocations in a single `execute()`) could see a handle exceed the threshold and (with the right alignment) be falsely classified as a heap pointer, retaining an unrelated heap object. Retention bug, not correctness — no use-after-free, no corruption. Issue body lists four candidate fix designs (self-describing wrappers, header skip-scan flag, wrap-table cross-reference, max-handle lower-bound check). | [#578](https://github.com/aallan/vera/issues/578) |
 | macOS malloc abort during wasmtime cleanup after Ctrl-C arrives in a host import (observed with `IO.sleep`).  The Python-side `KeyboardInterrupt` traceback half is fixed in v0.0.137 (host_sleep converts to `_VeraExit(130)` for clean exit), but a follow-on `pointer being freed was not allocated` / `Abort trap: 6` from the wasmtime/ctypes teardown path can still fire if the program was in certain heap states.  Filed upstream against wasmtime-py as [bytecodealliance/wasmtime-py#336](https://github.com/bytecodealliance/wasmtime-py/issues/336) — root cause is `wasmtime/_func.py` catching `Exception` rather than `BaseException` in the trampoline, letting `KeyboardInterrupt` escape into Rust with an undefined ABI return value.  Independent of #593 (which turned out to be a closure-return shadow-push asymmetry, not a Ctrl-C / cleanup issue).  No data-integrity impact; only the cleanup path. | [#595](https://github.com/aallan/vera/issues/595) |
 | `Inference.complete` / `Http.get` / `Http.post` decode network response bodies with strict UTF-8 (`vera/codegen/api.py:756 / :2809 / :2841`). If a remote API returns a response containing non-UTF-8 bytes, the user sees a Python `UnicodeDecodeError` message leaked into the `Result::Err` string. Lower-severity sibling of #589 — the sites are wrapped in `try/except Exception` so no Python traceback escapes wasmtime's trampoline (the failure surfaces as a Vera-level `Err`, not a crash), but the error message contains Python-internals noise rather than a Vera-native diagnostic. Practical trigger probability is low (HTTP/JSON APIs almost universally use UTF-8), but the defensive-coding hygiene gap mirrors #589 and should be closed. Decision pending: `errors="replace"` (preserve data, lose signal) vs explicit invalid-UTF-8 detection with a Vera-native `Err` (preserve signal, lose data). | [#591](https://github.com/aallan/vera/issues/591) |
+| String interpolation of a `String`-returning function call generates invalid WASM (i64/i32 type mismatch).  `vera check` and `vera verify` pass; the trap surfaces only at instantiation with a WASM byte offset rather than a source line.  Trigger is narrow: function call (not a slot ref or literal) whose return type is `@String`, used as the interpolation expression directly without an intervening `let`-binding.  Workaround: let-bind first, or use `string_concat` instead of interpolation. | [#602](https://github.com/aallan/vera/issues/602) |
+| Five prelude combinators (`option_unwrap_or`, `result_unwrap_or`, `option_map`, `option_and_then`, `result_map`) are silently skipped from every WASM compile due to two backend gaps: (1) the `_unwrap_or` variants take a bare type variable `@T` as a parameter which the WASM backend can't lower; (2) the `_map` / `_and_then` variants use `apply_fn` inside a `match` arm which the WASM codegen doesn't support yet (already noted as a known gap in `vera/wasm/README.md:643`).  Python target works in full; only `--target browser` (and any future native target sharing the WASM codegen) is affected.  The `apply_fn` path would unblock 3 of 5 functions in one stroke. | [#604](https://github.com/aallan/vera/issues/604) |
 
 ## Limitations
 
@@ -39,6 +41,10 @@ Bugs and limitations tracked against the [issue tracker](https://github.com/aall
 | Inference: no token/temperature controls (`max_tokens` hardcoded) | [#370](https://github.com/aallan/vera/issues/370) |
 | Inference: no user-defined handlers (`handle[Inference]`) | [#372](https://github.com/aallan/vera/issues/372) |
 | No float array host-alloc (`_alloc_result_ok_float_array`) | [#373](https://github.com/aallan/vera/issues/373) |
+| Browser runtime: `runtime.mjs` doesn't export the internal string-marshalling helpers (`allocString`, `readString`, `allocArrayOfStrings`), so JavaScript can't pass `String` arguments into Vera functions.  Forces all browser programs into the "compute everything upfront, drain stdout once" pattern; rules out streaming or interactive simulations driven from JS. | [#603](https://github.com/aallan/vera/issues/603) |
+| Terminal-vs-browser IO seam in the "write once, run anywhere" framing.  A program built for terminal ergonomics (`IO.sleep` for animation pacing, ANSI escapes for cursor control) compiles cleanly to `--target browser` but doesn't run meaningfully — `IO.sleep` busy-waits on the main thread ([#609](https://github.com/aallan/vera/issues/609) tracks the JSPI-driven yield fix), ANSI escapes render as literal text in the DOM ([#610](https://github.com/aallan/vera/issues/610) tracks an ANSI-subset interpreter for the browser runtime).  Closing both — neither requires a language change — would let typical terminal Vera programs render unchanged on either target.  Vera's design point ("pure core, effects at the boundary") is still right; the boundary just differs between targets. | [#608](https://github.com/aallan/vera/issues/608) (umbrella) |
+| Documentation: bidirectional `Int <: Nat` subtyping (with verifier-enforced refinement) is implemented in the type checker but not surfaced in user-facing docs — agents discover it by surprise when `array_length` (formally `@Int`) flows freely into `@Nat` positions. | [#607](https://github.com/aallan/vera/issues/607) |
+| Documentation: `decreases` rule for effectful recursive functions is correct in SKILL.md but buried inside a paragraph, requiring agents to triangulate between FizzBuzz (no `decreases`) and the State combinator example (with `decreases`) to find it. | [#605](https://github.com/aallan/vera/issues/605) |
 
 ## Refactoring needed
 
@@ -57,6 +63,7 @@ Internal test-quality items that don't affect correctness today but would make t
 | Gap | Issue |
 |-----|-------|
 | `TestHostPrintInvalidUtf8589` (`tests/test_runtime_traps.py`) has 6 structural source-greps and 1 end-to-end synthetic-WAT test for `host_print`. The other 5 decode sites (`host_stderr`, `host_contract_fail`, `_read_wasm_string`, `markdown.py::_read_string`, `_extract_string`) are pinned only by structural tests. A refactor that centralises the decodes into a `_safe_decode()` helper would break the structural greps even with preserved behaviour. End-to-end tests using synthetic WAT modules per site (~5 × 20 lines) would survive the refactor. Lowest-cost form: parametrize the existing test over an `(import_name, type_signature, payload_construction)` tuple. | [#592](https://github.com/aallan/vera/issues/592) |
+| `scripts/fix_allowlists.py --fix` uses a line-offset bulk-shift heuristic that doesn't reliably re-anchor when a documentation file receives multiple edits at different positions in one session.  Hit twice during PR #601's workflow — required manual line-number patching plus one mis-anchored entry that was only caught by CodeRabbit on PR review.  A content-fingerprint anchor (hash the surrounding ~5 lines of each entry) would be robust to multi-edit sequences. | [#606](https://github.com/aallan/vera/issues/606) |
 
 ## CI workarounds