Closes #516 Stage 2 (Stage 3 -- per-kind Fix paragraphs -- remains).

Pre-fix, runtime traps surfaced only the kind taxonomy from Stage 1
(divide_by_zero / out_of_bounds / etc.) plus the trap message.  The
user got "Integer division by zero" with no indication of which of
their functions divided by zero -- they had to read the raw wasmtime
backtrace with hex offsets and translate WAT names back to source.

Stage 2 walks wasmtime.Trap.frames after classification, looks each
frame's WAT name up in a new CompileResult.fn_source_map (built
during codegen by _register_fn for top-level functions and by the
closure-lifting pass for $anon_N helpers), and produces a structured
backtrace: list of {func, file, line_start, line_end, is_builtin}
dicts, leaf-first to match wasmtime / gdb / Python convention.

Per-function granularity, not per-line: wasmtime-py doesn't expose
WAT-to-WASM debug-info plumbing, so byte-offset -> source-line
mapping isn't viable.  The issue's own success criterion is "even a
coarse 'trap inside cell_at at or after line 84' would be a big step
up", which is per-function.

Resolution rules in _resolve_trap_frames (vera/codegen/api.py):

* Built-ins are tagged as <builtin>, not dropped.  WAT functions
  named alloc / gc_collect / contract_fail, plus anything starting
  with exn_ / vera. / closure_sig_, are runtime infrastructure with
  no Vera source.  Surfacing them would claim a misleading
  file:line; tagging them keeps the chain visible without lying.

* Monomorphized generics suffix-strip at the rightmost $ (identity$Int
  -> identity).  $ cannot appear in user-written Vera identifiers, so
  any $ in a WAT name was inserted by the monomorphizer.

* Lifted closures register under anon_N with the source span of the
  original fn(...) syntactic site, so a trap inside a closure points
  at the closure body, not at the synthetic top-level wrapper.

* Unknown user-named frames are surfaced with <unknown> location, not
  dropped.  Better to show the WAT name with no location than lose
  the frame entirely; any future source-map gap is diagnosable from
  the unknown markers.

cmd_run text mode appends a "Source backtrace:" block after the
error line.  Leading runtime-helper frames are collapsed with a
"(suppressed N runtime-helper frames above first user code)" marker
so the user sees their own code at the top of the trace.  JSON mode
adds a frames array to each diagnostic with the full structured
backtrace (including built-ins, so machine consumers see the full
picture for telemetry).

Tests: 15 new tests across 3 classes in tests/test_runtime_traps.py:

* TestResolveTrapFrames516 (7) -- unit tests with a _FakeFrame shim:
  user-fn resolution, built-in tagging, built-in-prefix matching,
  monomorphized base-name fallback, unknown-name surfacing,
  defensive empty-frames behaviour, leaf-first ordering.

* TestTrapSourceBacktrace516 (5) -- end-to-end via cmd_run: text-mode
  surface, leaf-first ordering across stream output, JSON envelope
  frames array, contract-violation backtrace, direct execute()
  WasmTrapError.frames attachment.

* TestSourceMapPopulation516 (3) -- light-weight inspection of
  CompileResult.fn_source_map: top-level fns registered, lifted
  closures registered under anon_N, built-in helpers NOT registered
  (regression guard against bogus user-frame entries).

3,576 tests pass + 14 skipped (was 3,561+14).  mypy clean.  All 81
conformance + 33 examples pass.  uv.lock regenerated for version
bump.

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

Four CodeRabbit findings actioned plus filed #547 to track #516 Stage 3
(per-kind Fix paragraphs) per the workflow rule "PR-generated new
issues must be added to a tracker in the same PR".

Code fixes:

* vera/codegen/api.py _resolve_trap_frames: defensive leading-$
  strip on frame name before the builtin-allowlist check and the
  fn_source_map lookup.  Verified empirically that current
  wasmtime-py strips $ already (a divide-by-zero trap inside
  `(func $bad ...)` returns func_name='bad'), but the normalisation
  is one cheap line and protects against any future wasmtime
  version that leaves the $ in.  Without it, a regression there
  would silently break every backtrace lookup with no clear
  diagnostic.

* vera/cli.py JSON envelope: always include the "frames" key (even
  as an empty list) instead of the old `if exc.frames:` guard.
  Matches the always-present `trap_kind` shape; consumers can
  iterate `diag["frames"]` directly without `.get(..., [])`
  ceremony.  Schema stability for a structural field outweighs the
  envelope-minimalism win.

Test fixes:

* tests/test_runtime_traps.py
  test_lifted_closure_registered_under_anon_id: was checking only
  that an anon_N key exists; now also asserts the registered span
  value (file = "<unknown>" via the compile-from-string path,
  line_start = 4, line_end = 6 — the exact lines of the inline
  closure literal in the test fixture).  A future bug that
  registered the wrong AST node (e.g. picking up the enclosing
  array_map call instead of the AnonFn) would fail this test
  with a clear coordinate mismatch instead of silently surfacing
  the wrong file:line on a real trap inside the closure body.

* tests/test_runtime_traps.py: added
  test_contract_violation_json_mode_includes_frames as a JSON
  variant of the existing text-mode contract-violation backtrace
  test.  Pins the JSON envelope's frames array AND the JSON-mode-
  no-stderr-leak invariant from #543.  Without it, a future
  refactor could surface the backtrace in text mode but drop it
  from the JSON path, and CI would stay green.

Docs:

* TESTING.md: 3,590 -> 3,591 total tests; test_runtime_traps.py
  row updated 39->40 / 1,021->1,098 lines.
* ROADMAP.md, README.md, HISTORY.md: 3,590 -> 3,591 across all
  three references.

#547 (Stage 3) is filed with concrete content (per-kind Fix
paragraph drafts, refactor scope for _classify_trap, CLI surface
plan, test plan).  Will be picked up after #517 (TCO) lands so
the stack_exhausted Fix paragraph can reference return_call as
shipped instead of "see #517 for the planned fix".

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

Three of four CodeRabbit findings actioned plus two new tests for
the suppression-marker code path that round 4's TESTING.md update
implied existed.

Actioned:

* HISTORY.md v0.0.124 row trimmed to a single concise sentence.
  The previous wording carried implementation detail
  (WasmTrapError.frames, Source backtrace: block, JSON envelope
  shape, granularity rationale) that belongs in CHANGELOG, not in
  the HISTORY one-line-summary table.  This is the *third* time
  the user has corrected the same drift (memory note tagged at
  v0.0.121 noted it was "the third time" then; this is now four).

* ROADMAP.md opening line "Vera v0.0.119 delivers..." -> "Vera
  v0.0.124 delivers...".  The compiler-pipeline blurb itself is
  unchanged (no pipeline additions since v0.0.119); the version
  number was just stale.

* tests/test_runtime_traps.py: added
  test_text_mode_collapses_leading_runtime_helper_frames and
  test_text_mode_does_not_collapse_when_all_frames_are_builtins.
  Pre-fix the suppression-marker logic in cli.py was untested
  (real GC / allocator traps with builtin-leaf frames are
  timing-sensitive and not deterministically reproducible from a
  Vera fixture); new tests monkeypatch vera.codegen.execute to
  raise a WasmTrapError with synthetic frame chains, so the pure
  suppression logic is exercised against deterministic input.
  First test: 2 builtin leaf frames + 1 user frame -> assert
  "suppressed 2 runtime-helper frames" appears, builtin frames
  collapsed, user frame surfaced at top.  Second test: builtin-
  only chain -> assert NO suppression marker, both helpers
  displayed (the "only collapse if a user frame remains" guard).

* TESTING.md: row description updated to name _resolve_trap_frames,
  cmd_run, "leaf-first" ordering, and "suppression marker"
  explicitly per CodeRabbit's request.  Coverage is now accurate
  (was previously claiming "order" without naming "leaf-first";
  not claiming suppression-marker coverage which now exists).

Not actioned:

* README.md "Fix:" claim — the README's "Every error includes...
  how to fix it" sentence at line 74 is in the "Errors are
  instructions" section illustrated by an E001 example.  The claim
  is about compile-time errors (E001-E702 with stable Diagnostic
  shape carrying description / rationale / fix / spec_ref) and has
  been accurate since v0.0.43 when stable error codes shipped.
  Runtime trap diagnostics are a separate surface that's still in
  progress (Stage 2 shipped; Stage 3 tracked as #547).  The
  CodeRabbit instruction was to edit "the sentence containing
  'Vera is in **active development** at v0.0.124'" but there's no
  Fix-claim adjacent to that sentence (it's at line 74, the
  flagged line is 184) and the actual Fix-claim it's about
  isn't invalidated by Stage 3 still being open.  Replying inline
  on the PR with this analysis.

Doc counts: 3,591 -> 3,593 across TESTING.md / ROADMAP.md /
README.md / HISTORY.md (two new tests added in this round).

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

All four CodeRabbit findings actioned.  Three are stale-comment
fixes pointing at the previous commit's prelude-detection refactor
that left explanatory comments referring to the old `decl.span is
None` heuristic; one is the fifth-time HISTORY drift on the same
v0.0.124 row.

Stale-comment fixes (all three reflect the actual current criterion
"prelude detection is by registration-flow position in compile_program,
not by AST-level span absence" — the failure mode being avoided is
that inject_prelude calls parse_to_ast on inline Vera source, so its
synthetic FnDecls do have spans, just spans pointing at synthetic
source coordinates):

* tests/test_runtime_traps.py — TestResolveTrapFrames516
  test_prelude_function_tagged_as_builtin docstring updated.
* vera/codegen/api.py — CompileResult.prelude_fn_names field
  comment updated; explicitly notes detection is registration-flow
  not span-based, with the failure mode that motivated the change.
* vera/codegen/core.py — both _fn_source_map and _prelude_fn_names
  field comments updated; documents the post-inject_prelude loop
  in compile_program as the actual registration site, retains the
  monomorphized-name suffix-strip rule documentation, retains the
  built-in helper exclusion rationale.

HISTORY trim (5th time on the same drift):

* HISTORY.md v0.0.124 row collapsed to a single outcome sentence:
  "Runtime traps now include a source backtrace ([#516] Stage 2)."
  The Stage 3 / #547 follow-up reference moved into the CHANGELOG
  (new "Stage 3 follow-up" subsection in the v0.0.124 entry) where
  forward-looking process information belongs.  Per the memory note
  hardened in the previous round: "more than one ` — ` separator OR
  more than one sentence = already drifted, cut".  The row now has
  zero separators and one sentence — within bounds.

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

…in walk + monomorphized-prelude skip

All five CodeRabbit findings actioned.  The two structural ones are
shape-of-the-shipped-API decisions worth getting right before this
PR lands; the three smaller ones are correctness / cleanliness /
test-coverage tightening.

* `TrapFrame` dataclass replaces `list[dict[str, object]]`
  (vera/codegen/api.py).  New `@dataclass(frozen=True)` with five
  fields (func / file / line_start / line_end / is_builtin) and a
  `to_dict()` method for JSON serialisation at the envelope
  boundary.  `_resolve_trap_frames` now returns `list[TrapFrame]`;
  `WasmTrapError.frames` is `list[TrapFrame]`.  Mypy can now type-
  check field access — the previous stringly-typed dict allowed
  silent typos like `frame["fucn"]`.  Safe to change shape now
  because the API hasn't shipped externally yet (Stage 2 is in
  this still-open PR).

* Exception-chain walk for `.frames` via new
  `_find_frames_in_exception_chain` helper (vera/codegen/api.py).
  Some wasmtime call paths wrap a `Trap` (which carries `frames`)
  inside a `WasmtimeError` (which doesn't); inspecting only the
  outer exception silently drops the backtrace.  The helper walks
  `__cause__` / `__context__` until a frame sequence is found —
  same pattern as the existing `_VeraExit` chain walk in
  `execute()`.  Folded into the resolver itself rather than at the
  call site so direct callers (tests, future LSP) get the chain
  walk for free.

* Skip monomorphized prelude registration (vera/codegen/core.py).
  After Pass 1.5 (monomorphize), each clone's `_register_fn` would
  re-add prelude entries to `_fn_source_map` with the same bogus
  coordinates the post-prelude loop just scrubbed out for the base
  names (e.g. `option_unwrap_or$Int` -> the original generic's
  prelude span).  Now: after registering each `mdecl`, suffix-strip
  at the rightmost `$` and if the base is in `_prelude_fn_names`,
  pop the entry from `_fn_source_map`.  The trap resolver already
  handled this correctly via the same suffix-strip rule, so this
  is cleanliness rather than a correctness fix — but cleaner to
  not have dead entries in the map.

* New `test_json_mode_preserves_full_frame_chain_including_builtins`
  in tests/test_runtime_traps.py — JSON-mode sibling of the text-
  mode collapse tests.  Pins the contract that JSON mode preserves
  the FULL backtrace (helpers included, leaf-first order) while
  text mode collapses for display.  Without this, a refactor
  could accidentally apply the text-mode collapse to JSON output
  too and downstream consumers (telemetry, LSP) would silently
  start receiving filtered chains.  Same monkeypatch strategy as
  the text-mode tests so a single mock surface exercises both
  paths.

* Stale span-based comment fixed in test (line 1341-1344).  The
  `test_no_spurious_entries_for_builtins` docstring still claimed
  built-ins are detected via "decl.span is None" — leftover from
  round 4.  Replaced with the accurate explanation: WASM helpers
  ($alloc, $gc_collect, $contract_fail, $exn_*, $vera.*) are
  emitted directly into WAT by the assembly module and never go
  through `_register_fn`, which is why they don't appear in the
  source map.  Prelude functions go through `_register_fn` and
  are then moved to `_prelude_fn_names` by the post-prelude loop
  — that path is covered separately by
  `test_prelude_functions_registered_as_builtins`.

Cli.py + tests updated to use `frame.func` / `frame.file` etc.
instead of `frame["func"]` / `frame.get("func")` ; the JSON
envelope serialises via `[f.to_dict() for f in exc.frames]` so
the wire format stays unchanged.  Mypy clean; full suite passes
3,584 + 14 skipped (was 3,583 + 14).

Doc counts: 3,597 -> 3,598 across TESTING.md / ROADMAP.md /
README.md / HISTORY.md (one new test added).

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

All three CodeRabbit findings actioned.

* ROADMAP Milestone 3c "expand from 30 to 50+ examples" -> "expand
  from 33 to 50+ examples" plus a parenthetical pointing future
  updates at scripts/check_doc_counts.py as the canonical source.
  The "30" figure dated to v0.0.101 / Stage 9; we've shipped three
  examples since (string_utilities + two others) without bumping
  this baseline.

* tests/test_runtime_traps.py: renamed
  test_frames_preserved_in_outermost_first_order ->
  test_frames_preserved_in_leaf_first_order.  The previous name
  was the literal opposite of what the test asserts — the body
  asserts ["inner", "outer"] (leaf-first / innermost-first) and
  the inline comment correctly says "wasmtime returns inner-first;
  we preserve that order so the human reading the backtrace sees
  the leaf first".  Docstring rewritten to use the correct
  terminology with a note explaining why we follow wasmtime / gdb
  (leaf-first) rather than Python's traceback convention (root-
  first).  Body, assertion, and inline comment unchanged — only
  the name and docstring drifted.

* vera/cli.py: moved the suppression message to fire AFTER the
  "Source backtrace:" header rather than before it.  Reads more
  naturally: the suppression line is metadata about the backtrace
  below it, so it belongs under the heading.  Pre-fix:

      (suppressed 2 runtime-helper frames above first user code)
    Source backtrace:
      in main  (foo.vera:1-3)

  Post-fix:

    Source backtrace:
      (suppressed 2 runtime-helper frames above first user code)
      in main  (foo.vera:1-3)

* tests/test_runtime_traps.py
  test_text_mode_collapses_leading_runtime_helper_frames: added
  a position-ordering assertion so a future reorder regression
  fails immediately.  Substring checks alone wouldn't catch it.
  New assertion: header_pos < suppress_pos < main_pos.

Doc counts: TESTING.md test_runtime_traps.py line count refreshed
1,440 -> 1,465 (the new ordering assertion added 25 lines).  Full
suite still 3,598 / 3,584 passed + 14 skipped.

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