Tetris experiment: 2 codegen bugs + 6 friction features + ROADMAP updates by aallan · Pull Request #623 · aallan/vera

aallan · 2026-05-07T19:18:00Z

Summary

An agent attempting to write terminal Tetris on Vera 0.0.138 surfaced two new closure-codegen bugs and a substantial friction list. This PR files all of it as GitHub issues and lands the entries in KNOWN_ISSUES.md / ROADMAP.md.

Bugs reproduced on current main and filed (added to KNOWN_ISSUES.md)

#615 — Non-contiguous outer-Int capture in closures miscompiles. Closure that references @Int.k while skipping @Int.j (0 < j < k) emits malformed WASM: tail-shaped expressions trap at instantiation, body shapes with subsequent let-pushes silently produce wrong values. vera check is silent. Hit everywhere in the Tetris collision check; required helper-function workarounds throughout.
#614 — Closure capturing data ADT and passing it to a function call emits malformed WASM (unknown table 0: table index out of bounds). vera check is silent. Single-variant ADTs reproduce identically. Hypothesised same root cause as Non-contiguous capture of outer Int slots in closure miscompiles (trap or silent wrong result) #615 in the closure-lifter env-struct serialisation — one fix may close both.

Both promoted to the top of the stabilisation tier in ROADMAP.md (#615 first, since silent miscompute is the most severe failure mode).

Friction features filed (added to appropriate ROADMAP phases)

#616 — nat_add / nat_sub_sat / nat_mul built-ins (Phase 4c). Most painful gap by frequency.
#617 — Anonymous tuples with destructuring (Speculative; deferred per the friction doc).
#618 — IO.read_char / Terminal effect (Phase 2c). Pairs with Browser runtime: implement IO.sleep via JSPI (or Asyncify fallback) so animations don't freeze the tab #609 / Browser runtime: interpret a minimal ANSI escape subset so terminal-style Vera programs render unchanged #610 for browser real-time programs.
#619 — Single-keyword pure / io shorthand for the vacuous contract preamble (Phase 4d).
#620 — Optional field names in data declarations (Phase 4d). Cosmetic, slot semantics unchanged.
#621 — debug effect permitted in any effect row, including pure (Phase 3c).
#622 — SKILL.md polish: array_join cross-reference + decreases-with-+1 idiom example (Phase 3c, documentation-only).

ROADMAP changes

Stabilisation tier expanded from 7 to 9 items; Closure capturing data ADT and passing it to a function call inside body emits malformed WASM #614 and Non-contiguous capture of outer Int slots in closure miscompiles (trap or silent wrong result) #615 inserted at the top. Agent-integration tier renumbered.
Phase 2c gains IO.read_char — single-character input portable across terminal and browser targets #618. Phase 3c gains debug effect permitted in any effect row (including pure) for diagnostic stderr output #621 + SKILL.md polish: array_join cross-reference + decreases-with-+1 idiom example #622. Phase 4c gains Built-in nat_add / nat_sub_sat / nat_mul to eliminate the Nat round-trip dance #616.
New Phase 4d "Language ergonomics" with Single-keyword pure / io shorthand for the vacuous contract preamble #619 + Optional field names in data declarations (cosmetic, for --explain-slots and error messages) #620 (strict-superset additions surfaced by real-program friction).
Speculative tier gains Anonymous tuples / pairs with destructuring (deferred design decision) #617 with explicit trigger condition.

Note on coordination with #613

This branch is on the un-trimmed ROADMAP because PR #613 (the trim) is still open. The new tier-table rows added here are conflict-free with #613 — the trim only touches the prose around the table, not the table rows themselves. Whichever lands first, the other rebases cleanly.

Test plan

All three repros reproduce on current main (ec46cf8):
- Bug 1 traps with unknown table 0: table index out of bounds at offset 1374.
- Bug 2a traps identically at offset 1385.
- Bug 2b silently returns fits = false instead of fits = true.
Bug 2a workaround (touch all outer slots) returns result: [13, 24, 35, 46] correctly.
python scripts/check_doc_counts.py — consistent (38 KNOWN_ISSUES entries, was 36)
python scripts/check_limitations_sync.py — consistent
python scripts/check_site_assets.py — up to date
All filed issues are linked back from ROADMAP / KNOWN_ISSUES; cross-references are correct (Closure capturing data ADT and passing it to a function call inside body emits malformed WASM #614 ↔ Non-contiguous capture of outer Int slots in closure miscompiles (trap or silent wrong result) #615 mention each other).

Summary by CodeRabbit

Documentation

Expanded known issues documentation with newly identified issues, including detailed descriptions and workarounds to assist users
Refreshed product roadmap with updated implementation priorities and newly added planned features across multiple upcoming development milestones and future work

…ates An agent attempting to write terminal Tetris on Vera 0.0.138 surfaced two new closure-codegen bugs and a substantial friction list. This PR files all of it as GitHub issues and lands them in KNOWN_ISSUES.md / ROADMAP.md in the right places. Bugs (filed + reproduced on current main, added to KNOWN_ISSUES.md): * #615 -- Non-contiguous outer-Int capture in closures miscompiles. Closure that references @Int.k while skipping @Int.j (0 < j < k) emits malformed WASM: tail-shaped expressions trap at instantiation, body shapes with subsequent let-pushes silently produce wrong values. vera check is silent. Hit *everywhere* in the Tetris collision-check; required helper-function workarounds throughout. * #614 -- Closure capturing data ADT and passing it to a function call emits malformed WASM (unknown table 0: table index out of bounds). vera check is silent. Single-variant ADTs reproduce identically. Hypothesised same root cause as #615 in the closure-lifter env-struct serialisation -- one fix may close both. Both promoted to top of stabilisation tier in ROADMAP.md (#615 first since silent miscompute is the most severe failure mode). Friction features (filed as separate issues, added to ROADMAP.md): * #616 -- nat_add / nat_sub_sat / nat_mul built-ins (Phase 4c). Most painful gap by frequency: today, adding two Nats requires a five-line int_to_nat round-trip with an unreachable None arm. * #617 -- Anonymous tuples with destructuring (Speculative). The friction doc explicitly de-prioritises this -- the slot system needs a story for tuples, and the existing workarounds (Array<Int> / single-variant ADT) work today. * #618 -- IO.read_char / Terminal effect (Phase 2c). Tetris is fundamentally real-time but IO.read_line is line-buffered, forcing the agent to ship a turn-based variant. Pairs with #609 / #610 for browser real-time programs. * #619 -- Single-keyword pure / io shorthand for the vacuous contract preamble (Phase 4d). Strict superset of existing syntax. * #620 -- Optional field names in data declarations (Phase 4d) for --explain-slots and error-message use. Slot semantics unchanged. * #621 -- debug effect permitted in any effect row (Phase 3c). Single privileged escape hatch for diagnostic stderr; effect-system and verifier-invisible; strippable in production. * #622 -- SKILL.md polish: array_join cross-reference + decreases-with-+1 idiom example (Phase 3c, documentation-only). ROADMAP changes: * Stabilisation tier expanded from 7 to 9 items; #614 and #615 inserted at the top. Agent-integration tier renumbered 8/9/10 to 10/11/12. * Phase 2c gains #618 (IO.read_char / Terminal effect). * Phase 3c gains #621 (debug effect) + #622 (SKILL polish). * Phase 4c gains #616 (nat_add / nat_sub_sat / nat_mul). * New Phase 4d "Language ergonomics" with #619 (pure shorthand) + #620 (optional field names). * Speculative tier gains #617 (tuples) with explicit trigger condition. KNOWN_ISSUES.md gains entries for #614 and #615 in the Bugs section. Source friction documents from the Tetris experiment are referenced in each issue; one reproducer per bug archived in /tmp/tetris-repros/ during this session and confirmed reproducing on commit ec46cf8. Co-Authored-By: Claude <noreply@anthropic.invalid>

coderabbitai · 2026-05-07T19:18:12Z

📝 Walkthrough

Walkthrough

KNOWN_ISSUES.md and ROADMAP.md updated to document closure-capture WASM miscompilation failures, reorder stabilisation-tier priorities with the new issues elevated, and add planned work items for Milestones 2–4 covering IO, debugging, standard library completeness, and speculative language features.

Changes

Project Status & Tracking Documentation

Layer / File(s)	Summary
Known Closure-Capture Issues `KNOWN_ISSUES.md`	Two new "Bugs" table entries (`#614`, `#615`) document closure-capture failures: ADT data passed into function calls within closures emit malformed WASM at instantiation; non-contiguous capture of same-typed outer slots can miscompile or trap. Both include reproduction and workaround details.
Stabilisation-Tier Prioritisation `ROADMAP.md`	Implementation order table reordered: `#615` moved to top priority, `#614` elevated, followed by reordered codegen/runtime/stress/browser validation items (`#602`, `#604`, `#596`, `#597`, `#609`, `#610`, `#595`).
Milestone 2-4 Roadmap Enhancements `ROADMAP.md`	Milestone 2 adds IO.read_char and Terminal effect for raw-mode interactive input (`#618`). Milestone 3 adds debug effect for stderr diagnostics and SKILL.md documentation polish (`#621`, `#622`). Milestone 4 extends standard library with built-in enhancements (`#616`) and language ergonomics including pure/io shorthand and optional data field names (`#619`, `#620`).
Speculative Features `ROADMAP.md`	"Speculative" section adds item `#617` for anonymous tuples and destructuring syntax.

Estimated code review effort

🎯 1 (Trivial) | ⏱️ ~3 minutes

Possibly related issues

Non-contiguous capture of outer Int slots in closure miscompiles (trap or silent wrong result) #615: Directly addressed in this PR as the primary closure-capture WASM miscompilation bug now documented in KNOWN_ISSUES.md and prioritised at the top of the stabilisation tier.

Possibly related PRs

aallan/vera#483: Both PRs modify ROADMAP.md's near-term implementation priorities and "What's next" ordering for stabilisation-tier issues.

Suggested labels

docs

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title accurately describes the main changes: two codegen bugs (`#614`, `#615`) filed and documented in KNOWN_ISSUES.md, six friction features added to the roadmap, and comprehensive ROADMAP.md updates reflecting issue prioritisation and new phases.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests
Commit unit tests in branch claude/tetris-experiment-bugs-and-friction

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

coderabbitai

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@ROADMAP.md`:
- Line 194: The list item for issue `#621` contains a trailing table delimiter
character '|' at the end of the line (the stray pipe), which triggers accidental
table syntax in Markdown; remove the trailing '|' from the "[`#621`] ... |" list
entry so the item ends cleanly without the pipe character (update the line
containing the "#621" bullet to delete the final '|').

🪄 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: 5807b642-c790-4b2e-8034-221e614e5ee8

📥 Commits

Reviewing files that changed from the base of the PR and between ec46cf8 and 0ab1059.

📒 Files selected for processing (2)

KNOWN_ISSUES.md
ROADMAP.md

aallan · 2026-05-07T19:20:12Z

Folding into #613 — the user correctly pointed out everything should be in one PR. Reopening this work as additional commits on the claude/roadmap-trim-retrospective branch backing #613, after critically re-evaluating each friction item against Vera's design principles (mandatory contracts, De Bruijn slot indexing, effect-row visibility) rather than just transcribing the friction-doc proposals.

codecov · 2026-05-07T19:23:19Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 90.92%. Comparing base (ec46cf8) to head (0ab1059).

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #623   +/-   ##
=======================================
  Coverage   90.92%   90.92%           
=======================================
  Files          59       59           
  Lines       22997    22997           
  Branches      259      259           
=======================================
  Hits        20910    20910           
  Misses       2080     2080           
  Partials        7        7

Flag	Coverage Δ
javascript	`57.36% <ø> (ø)`
python	`94.74% <ø> (ø)`

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@nat

Fold the Tetris-experiment work into this PR (was opened as #623, which is now closed in favour of bundling here). Bugs (filed + reproduced on current main, added to KNOWN_ISSUES.md): * #615 -- Non-contiguous outer-Int capture in closures miscompiles (silent wrong result OR trap, depending on body shape). Hit *everywhere* in the Tetris collision-check; required helper-function workarounds throughout. * #614 -- Closure capturing data ADT and passing it to a function call emits malformed WASM. Single-variant ADTs reproduce identically. Hypothesised same root cause as #615 in the closure-lifter env-struct serialisation. Both promoted to top of stabilisation tier in ROADMAP (#615 first since silent miscompute is the most severe failure mode). Friction items: each evaluated against Vera's design principles rather than just transcribed from the friction document. Kept as-is (no design tension): * #618 -- IO.read_char / Terminal effect (Phase 2c) * #622 -- SKILL.md polish: array_join cross-reference + decreases idiom example (Phase 3c) Reframed against design principles: * #616 -- nat ops. Ship total nat_add + nat_mul (Phase 4c); reject saturating nat_sub_sat -- saturating papers over the underflow obligation that refinement types are designed to surface. The underflow case is fixed cheaper by #552 generalising @nat invariant checking. * #620 -- optional field names in data declarations (Phase 4d, new "Cosmetic / advisory additions" phase). Issue body now carries four load-bearing guardrails: names never bindable in patterns, semantics-irrelevant, no compiler enforcement, mixed/anonymous forms must coexist. Sharpens the "cosmetic only" framing so this cannot drift into named-binding territory. * #621 -- debug effect. Reframed as a *visible* first-class effect uniquely composable with pure (effects(pure | <Debug>)), not the effect-system-invisible version the friction doc proposed. The invisible version contradicted the load-bearing effect-row visibility property; the visible version preserves the design while still solving the closure-debugging friction. Closed as design-rejected: * #617 -- anonymous tuples with let (x, y) = ... destructuring. Destructuring sugar introduces named locals, which contradict Vera's De Bruijn slot indexing. The friction doc itself de-prioritised this; the data Pair { Pair(A, B) } workaround is the design-aligned answer. * #619 -- pure / io single-keyword shorthand. Directly undermines the mandatory contract preamble's role as a forcing function. 60 lines of vacuous preamble for 20 helpers is the design working as intended -- it makes "vacuous because lazy" and "vacuous because thoughtful" typographically distinct. ROADMAP changes: * Stabilisation tier expanded from 7 to 9 items; #614 / #615 inserted at top. Agent-integration tier renumbered 8/9/10 -> 10/11/12. * Phase 2c gains #618. * Phase 3c gains #621 + #622. * Phase 4c gains #616 (nat_add + nat_mul; nat_sub_sat rejected). * New Phase 4d "Cosmetic / advisory additions" with #620. KNOWN_ISSUES.md gains entries for #614 and #615 in the Bugs section. Co-Authored-By: Claude <noreply@anthropic.invalid>

coderabbitai Bot reviewed May 7, 2026

View reviewed changes

Comment thread ROADMAP.md

aallan closed this May 7, 2026

aallan deleted the claude/tetris-experiment-bugs-and-friction branch May 7, 2026 19:28

aallan mentioned this pull request May 7, 2026

ROADMAP refactor + Tetris experiment: 2 codegen bugs + design-reviewed friction items #613

Merged

9 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Tetris experiment: 2 codegen bugs + 6 friction features + ROADMAP updates#623

Tetris experiment: 2 codegen bugs + 6 friction features + ROADMAP updates#623
aallan wants to merge 1 commit into
mainfrom
claude/tetris-experiment-bugs-and-friction

aallan commented May 7, 2026 •

edited by coderabbitai Bot

Loading

Uh oh!

coderabbitai Bot commented May 7, 2026 •

edited

Loading

Walkthrough

Changes

Estimated code review effort

Possibly related issues

Possibly related PRs

Suggested labels

Uh oh!

coderabbitai Bot left a comment

Uh oh!

Uh oh!

aallan commented May 7, 2026

Uh oh!

codecov Bot commented May 7, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

aallan commented May 7, 2026 • edited by coderabbitai Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Bugs reproduced on current main and filed (added to KNOWN_ISSUES.md)

Friction features filed (added to appropriate ROADMAP phases)

ROADMAP changes

Note on coordination with #613

Test plan

Summary by CodeRabbit

Documentation

Uh oh!

coderabbitai Bot commented May 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Walkthrough

Changes

Estimated code review effort

Possibly related issues

Possibly related PRs

Suggested labels

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

aallan commented May 7, 2026

Uh oh!

codecov Bot commented May 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

aallan commented May 7, 2026 •

edited by coderabbitai Bot

Loading

coderabbitai Bot commented May 7, 2026 •

edited

Loading

codecov Bot commented May 7, 2026 •

edited

Loading