v0.0.125: per-kind Fix paragraphs for runtime traps (#547)#548
Conversation
) Closes #547. Finishes #516 Stage 3. Pre-fix, runtime traps surfaced the kind taxonomy + description + source backtrace (Stages 1+2) but no actionable remediation paragraph. Compile-time errors carry description / rationale / fix / spec_ref through the standard `Diagnostic` shape; runtime traps now match that surface with a Vera-native Fix paragraph appended after the source backtrace. Refactor: `_classify_trap` returns `(kind, description, fix)` instead of `(kind, message)`. The previous shape crammed Fix- shaped hints inline in the message (e.g. "Out-of-bounds memory access (if the trapping frame is gc_collect, see #515; otherwise check array indexing or string slicing)"); Stage 3 splits them into clean fields. New per-kind table `_TRAP_FIX_PARAGRAPHS` in vera/codegen/api.py carries the canonical content. Per-kind Fix paragraph content: * divide_by_zero — "Add a precondition `requires(divisor != 0)` on the function performing the division, or guard the division site with a non-zero check. The Z3 verifier will then prove the division is safe at every call site at compile time." * out_of_bounds — names the two most-likely user causes (array indexing, string slicing) and the runtime-helper escape hatch (file an issue if the trap is inside `gc_collect` / `alloc`). * stack_exhausted — references #517 (the open TCO issue) so an agent reading the Fix knows this is a known limitation rather than a bug they should report; will be rewritten when #517 ships to reference `return_call` as a supported feature. * unreachable — names the most-likely cause (non-exhaustive `match`) and the resolution path (add the missing arm). * overflow — names the i64 range and the canonical remediation (precondition guarded by Z3). * contract_violation, unknown — empty string (the contract message itself already explains what failed; unknown by definition has no specific suggestion). WasmTrapError gains a `fix: str` field alongside the existing kind / frames / stdout / stderr. Default "" for backward compat. CLI surface: text mode appends a Fix: block after the Source backtrace: block, with the paragraph wrapped to ~76 columns (matching the compile-time Diagnostic rendering style). JSON mode adds a `fix` key to each trap diagnostic alongside description / trap_kind / frames — always present for schema stability (mirrors the always-present `frames` decision from CodeRabbit round 5 on the v0.0.124 PR), possibly empty. Empty- string Fix paragraphs suppress the text-mode block entirely (no empty Fix: header noise) but still surface as "" in JSON. Tests: 6 new tests in TestTrapFixParagraphs547, plus the existing 7 TestClassifyTrap tests updated for the new 3-tuple return shape with per-kind Fix-paragraph content assertions. TestWasmTrapError gained `fix` field round-trip + default-value assertions. 3,604 tests pass + 14 skipped (was 3,598 + 14). mypy clean; 81 conformance + 33 examples pass. Manual smoke output: Error: Integer division by zero Source backtrace: in divide (/tmp/divtrap.vera:1-5) in main (/tmp/divtrap.vera:7-11) Fix: Add a precondition `requires(divisor != 0)` on the function performing the division, or guard the division site with a non-zero check. The Z3 verifier will then prove the division is safe at every call site at compile time. Doc sweep: * KNOWN_ISSUES.md — #516 row removed (Stage 3 closes it). * ROADMAP.md — #516 / #547 dropped from the bug-killing campaign queue; intro updated to "nine remain"; priority rows renumbered (#517 promoted to position 1). * HISTORY.md — single-sentence v0.0.125 row. * CHANGELOG.md — new v0.0.125 section with full per-kind paragraph documentation. * By the numbers — v0.0.124 column refreshed to v0.0.125. uv.lock regenerated for the version bump. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (2)
📝 WalkthroughWalkthroughRuntime-trap diagnostics now include per-kind remediation text: Changes
Sequence Diagram(s)sequenceDiagram
participant Program
participant Runtime
participant Classifier as _classify_trap
participant Error as WasmTrapError
participant CLI
Program->>Runtime: execute wasm
Runtime->>Classifier: classify trap (raw info)
Classifier-->>Runtime: (kind, description, fix)
Runtime->>Error: raise WasmTrapError(kind, description, fix, frames)
Error-->>CLI: exception surfaced
CLI->>CLI: render text (emit "Fix:" block if fix != "")
CLI->>CLI: render JSON (include "fix" field)
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related issues
Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #548 +/- ##
=======================================
Coverage 91.04% 91.04%
=======================================
Files 58 58
Lines 22126 22139 +13
Branches 259 259
=======================================
+ Hits 20144 20157 +13
Misses 1975 1975
Partials 7 7
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@HISTORY.md`:
- Line 262: Update the Stage 11 row for version v0.0.125 (the line starting "|
v0.0.125 | 28 Apr | **Runtime traps now carry per-`kind` `Fix:` paragraphs**
([`#547`](https://github.com/aallan/vera/issues/547), closes
[`#516`](https://github.com/aallan/vera/issues/516) Stage 3). |") to the canonical
one-clause/one-link shape: keep only the single outcome clause "Runtime traps
now carry per-`kind` `Fix:` paragraphs" and a single issue link (pick the
primary one, e.g., [`#547`]), removing the extra follow-up clause, the "closes
[`#516`]" reference and "Stage 3" text so the row matches the template `| vX.Y.Z |
DD Mmm | **<one-clause outcome>** ([`#NNN`](url)). |`.
In `@tests/test_runtime_traps.py`:
- Around line 1559-1563: The assertion for fix_body_lines currently allows up to
80 chars which is too loose given textwrap.fill(..., width=76, initial_indent="
", subsequent_indent=" ") adds two indent chars; update the assertion that
iterates over fix_body_lines to require len(ln) <= 78 and update the failure
message accordingly (refer to the loop over fix_body_lines and the assertion
that raises "Fix-block line too long").
- Around line 1387-1393: The test should assert the "Fix:" paragraph comes after
the full rendered backtrace (i.e., after the last frame), not just after the
"Source backtrace:" heading: compute the last frame position from captured.err
(e.g., last_frame_pos = captured.err.rfind("\n File ")), assert last_frame_pos
> backtrace_pos to confirm frames exist, then assert fix_pos > last_frame_pos
instead of 0 <= backtrace_pos < fix_pos; use the existing variables
backtrace_pos, fix_pos, and captured.err to implement this check.
In `@vera/codegen/api.py`:
- Around line 591-594: The unknown-trap branch currently adds a "WASM trap: "
prefix when returning the exception, causing duplicate prefixes if str(exc)
already contains that text; change the tuple return so it uses the raw exception
string (str(exc)) instead of f"WASM trap: {exc}" and keep the same third element
_TRAP_FIX_PARAGRAPHS["unknown"] so callers still receive the same metadata.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 418826c6-bcb5-4df8-bbb8-bdefd9ef7139
⛔ Files ignored due to path filters (6)
docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**docs/sitemap.xmlis excluded by!docs/**uv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (11)
CHANGELOG.mdHISTORY.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdpyproject.tomltests/test_runtime_traps.pyvera/__init__.pyvera/cli.pyvera/codegen/api.py
💤 Files with no reviewable changes (1)
- KNOWN_ISSUES.md
All four CodeRabbit findings actioned. * HISTORY v0.0.125 row trimmed to a single-link single-clause shape: `**Runtime traps now carry per-kind Fix: paragraphs** ([#547]).` Removed the second issue link ([#516] Stage 3) and the "closes ... Stage 3" clause. This is the SIXTH time on the same drift across releases — memory note hardened with a stricter template (ONE link, ONE clause, ZERO separators) and a numbered checklist so future-me defaults to the terse shape on first draft. * tests/test_runtime_traps.py test_fix_paragraph_wraps_at_76_columns_in_text_mode line-length bound tightened from `<= 80` to `<= 76`. CodeRabbit suggested `<= 78` based on the assumption that textwrap.fill adds the initial_indent / subsequent_indent ON TOP of width — verified empirically (Python -c) that textwrap COUNTS the indent as part of width, so the strict ceiling is 76 (76 wrap = 2 indent + 74 body for fully-wrapped lines). Comment explains the strict- ceiling reasoning and the single-token caveat. * tests/test_runtime_traps.py test_text_mode_shows_fix_block_after_backtrace position assertion strengthened: was `backtrace_pos < fix_pos` (Fix: comes after the heading), now also asserts `backtrace_pos < last_frame_pos < fix_pos` so a regression that put Fix: between the header and the frames would fail. Frame format is `\n in <funcname> (file:N)`; rfind locates the last occurrence. CodeRabbit's exact regex (`\n File `) used the Python traceback format, not ours — adapted to our actual output shape. * vera/codegen/api.py _classify_trap unknown branch: `f"WASM trap: {exc}"` -> `str(exc)`. The wasmtime exception text already contains "wasm trap:" in its "Caused by:" tail, and a synthetic mock starting with "wasm trap: ..." would produce a double-prefix message ("WASM trap: wasm trap: ...") with the old shape. Test test_unknown_trap_surfaces_raw_message still passes (the substring "novel reason" is preserved either way). 3,590 tests pass + 14 skipped (unchanged — no new tests, just strengthened assertions). mypy clean. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
HISTORY.md (1)
262-262:⚠️ Potential issue | 🟡 MinorRephrase this HISTORY row in user-facing terms.
per-kindandFix:`` are still implementation/UI-surface details. A Stage 11 HISTORY row here should read as the user-visible outcome only, e.g. “Runtime traps now include actionable fix suggestions”.Suggested edit
-| v0.0.125 | 28 Apr | **Runtime traps now carry per-`kind` `Fix:` paragraphs** ([`#547`](https://github.com/aallan/vera/issues/547)). | +| v0.0.125 | 28 Apr | **Runtime traps now include actionable fix suggestions** ([`#547`](https://github.com/aallan/vera/issues/547)). |Based on learnings: In
HISTORY.mdStage 11, rows must stay as single-line user-facing summaries; UI surface strings and implementation details belong inCHANGELOG.md.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@HISTORY.md` at line 262, Update the HISTORY.md table row for v0.0.125 so it reads as a single-line, user-facing summary instead of including UI/implementation details; replace the existing cell text "| v0.0.125 | 28 Apr | **Runtime traps now carry per-`kind` `Fix:` paragraphs** ([`#547`](https://github.com/aallan/vera/issues/547)). |" with a plain user-facing sentence such as "| v0.0.125 | 28 Apr | Runtime traps now include actionable fix suggestions ([`#547`](https://github.com/aallan/vera/issues/547)). |" so it omits references to `per-`kind`` and ``Fix:`` and stays in the single-line HISTORY format.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@vera/codegen/api.py`:
- Around line 500-507: Update the "stack_exhausted" message in the mapping (the
string value keyed by "stack_exhausted" in api.py) to remove the incorrect
recommendation about using an "accumulator-shaped helper" (which still consumes
WASM frames without `return_call`); instead advise restructuring recursion to an
explicit iterative approach or splitting work into bounded chunks, or waiting
for issue `#517`; keep the rest of the explanatory text intact and adjust wording
to avoid implying accumulator recursion flattens the WASM stack.
---
Duplicate comments:
In `@HISTORY.md`:
- Line 262: Update the HISTORY.md table row for v0.0.125 so it reads as a
single-line, user-facing summary instead of including UI/implementation details;
replace the existing cell text "| v0.0.125 | 28 Apr | **Runtime traps now carry
per-`kind` `Fix:` paragraphs**
([`#547`](https://github.com/aallan/vera/issues/547)). |" with a plain user-facing
sentence such as "| v0.0.125 | 28 Apr | Runtime traps now include actionable fix
suggestions ([`#547`](https://github.com/aallan/vera/issues/547)). |" so it omits
references to `per-`kind`` and ``Fix:`` and stays in the single-line HISTORY
format.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 5a30597e-cf82-48ed-8f98-27d2d575a3a6
📒 Files selected for processing (4)
HISTORY.mdTESTING.mdtests/test_runtime_traps.pyvera/codegen/api.py
Both CodeRabbit findings actioned. * vera/codegen/api.py _TRAP_FIX_PARAGRAPHS["stack_exhausted"]: rewrote to drop the misleading "accumulator-shaped helper that keeps the stack flat" advice. Without TCO (which #517 will provide), accumulator-style recursion still pushes a fresh WASM frame per tail call — telling users to "use an accumulator- shaped helper" doesn't actually save them from the stack- exhaustion trap. The new paragraph names the actually- effective workarounds: iterate via array_fold / array_map (which compile to WASM loops, not recursion), split work into bounded chunks of <5K frames, or wait for #517. Existing test still passes (the substring assertion `"return_call" in fix` is preserved by the rewritten text). * HISTORY.md v0.0.125 row: trimmed UI/implementation-detail language ("per-`kind` `Fix:` paragraphs") to outcome-shaped language ("actionable fix suggestions"). Now reads `**Runtime traps now include actionable fix suggestions** ([#547])` — parallels v0.0.124's `**Runtime traps now include a source backtrace**` for a clean Stage 2 / Stage 3 progression. The convention across the table is "name the outcome, not the mechanism" — `per-kind` is mechanism (different kinds get different paragraphs); `Fix:` is UI (the literal CLI heading). The user-facing change is "runtime traps now suggest fixes". 3,590 tests pass + 14 skipped, mypy clean. Co-Authored-By: Claude <noreply@anthropic.invalid>
Closes #547. Finishes #516 Stage 3.
What changed
Pre-fix, runtime traps surfaced
kindtaxonomy + description + source backtrace (Stages 1+2 in v0.0.120 / v0.0.124), but no actionable remediation paragraph. Compile-time errors carrydescription/rationale/fix/spec_refthrough the standardDiagnosticshape; runtime traps now match that surface with a Vera-nativeFix:paragraph appended after the source backtrace.Before (v0.0.124):
After (v0.0.125):
JSON envelope adds:
Refactor
_classify_trapreturns(kind, description, fix)instead of(kind, message). The previous shape crammed Fix-shaped hints inline in the message (e.g."Out-of-bounds memory access (if the trapping frame is gc_collect, see #515; otherwise check array indexing or string slicing)"); Stage 3 splits them into clean fields so consumers can render description and fix independently. New per-kind table_TRAP_FIX_PARAGRAPHSinvera/codegen/api.pycarries the canonical content.WasmTrapErrorgains afix: strfield alongside the existingkind/frames/stdout/stderr. Default""for backward compatibility with directWasmTrapError(...)constructors that don't pass the keyword.Per-kind Fix paragraph content
kinddivide_by_zerorequires(divisor != 0)... The Z3 verifier will then prove the division is safe at every call site at compile time."out_of_boundsgc_collect/alloc).stack_exhaustedunreachablematch) and the resolution path.overflowcontract_violation""— the contract message itself already explains what failed.unknown""— by definition no specific suggestion possible.CLI surface
Fix:block after theSource backtrace:block, with the paragraph wrapped to ~76 columns (matching the compile-timeDiagnosticrendering style). Empty-string Fix paragraphs suppress the block entirely (no emptyFix:header noise).fixkey to each trap diagnostic alongsidedescription/trap_kind/frames— always present for schema stability (mirrors the always-presentframesdecision from round-5 of v0.0.124: trap source backtrace (#516 Stage 2) #546), possibly empty.Tests
TestTrapFixParagraphs547(6 tests) — text-modeFix:block surfacing with position-ordering invariant (Fix:appears after backtrace), text-mode block suppression forcontract_violation, JSON-modefixfield always-present, JSONfixfield empty-but-present forcontract_violation, table-completeness assertion (every kind in the taxonomy has a_TRAP_FIX_PARAGRAPHSentry — adding a new kind without its Fix paragraph fails this test immediately), and column-wrap invariant (~76 chars max per line, two-space indent underFix:heading).TestClassifyTrap(7 tests) updated for the new 3-tuple return shape; per-kind assertions now also verify the Fix paragraph content matches expected substrings ("requires(divisor != 0)"fordivide_by_zero,"#517"+"return_call"forstack_exhausted, etc.).TestWasmTrapErrorextended to verify thefixfield round-trips through the constructor and defaults to"".Documentation
Test plan
pytest tests/ -q— 3,590 passed, 14 skipped (was 3,584 + 14)mypy vera/— cleanpython scripts/check_conformance.py— all 81 passpython scripts/check_examples.py— all 33 passpython scripts/check_doc_counts.py— consistent (3,604 tests)python scripts/check_version_sync.py— version 0.0.125 consistentCo-Authored-By: Claude noreply@anthropic.invalid
Summary by CodeRabbit
New Features
Documentation
Tests