ROADMAP is future work; HISTORY is what we did; CHANGELOG is the
detailed account.  The previous Stage-12-launch edit blurred the
boundary by dragging a four-pattern campaign-recap into "What's
next" with references to closed issues (#515, #570, #487, #593,
#588) -- that material belongs in HISTORY's Stage 12 framing,
where it already lives.

Changes:

* "Where we are" -- trimmed to a single line scoreboard
  (3,766 tests, 86 conformance, 34 examples, 13 spec chapters).
  The retrospective VeraBench paragraph and the duplicate
  Conway-runs-cleanly note removed; both are HISTORY material.
* "What's next" -- replaced the four-pattern campaign-recap
  paragraph with one short forward-looking framing: stabilisation
  closes out N concrete issues, agent-integration is next.
* Stabilisation tier rows -- dropped retrospective references to
  #593 (closure-return shadow-push, fixed in v0.0.138) and #588
  (walker missing branches, fixed in v0.0.137).  The forward-looking
  rationale stands on its own.
* Verification-depth row -- generalises the obligation infrastructure
  reference instead of name-checking the closed #520 / #551 fixes
  that built it.

No content moved; the historical material lives in HISTORY.md
Stage 12 and CHANGELOG.md v0.0.137 / v0.0.138 entries.

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

The previous trim (33c8090) didn't go far enough -- ROADMAP was still
a wall of text with retrospective evidence, meta-explanation, and
descriptive intros that weren't forward-looking.  This pass cuts:

* Top intro: 3 paragraphs of meta-framing -> 1 sentence pointing at
  HISTORY + CHANGELOG.
* "What's next" prose recap removed.  The Stabilisation tier table
  *is* what's next; no preamble needed.
* "The ordering principle" / "What moves when" meta-paragraphs --
  collapsed to one short sentence inline below the agent-integration
  tier table.
* Phase 1b VeraBench results dump (lines 70-99 -- six-model results
  table, key-findings narrative) removed.  Those are RESULTS, not
  forward work; they live in the vera-bench repo.  Replaced with
  forward item: "Expand benchmark coverage (pass@k, more models)".
* Phase 1a-complete pointer dropped (redundant with doc-level
  HISTORY pointer at the top).
* Milestone 1 / Milestone 2 descriptive intros that were partly
  retrospective ("This milestone follows the critical dependency
  chain that has driven the project... Map / JSON / HTTP /
  Inference are complete...") trimmed to the forward-looking goal
  statement only.
* Phase 2b Http intro trimmed: "shipped in v0.0.99" -> "extend the
  existing GET/POST surface".
* "Completed phases" footer paragraph (810+ commits / 138 releases /
  3766 tests / etc) removed entirely -- pure retrospective summary
  duplicating HISTORY.
* Phase 3c stale "33 to 50+ examples" -> "50+".  Also drops the
  parenthetical about check_doc_counts.py (tooling note, not
  roadmap content).
* Speculative-section meta-explanation trimmed.
* Continuous-hardening intro trimmed.

Net: 263 -> 200 lines (-76 / +13).  No forward-looking content
removed; only retrospective state, evidence dumps, and meta-prose.

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

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>

Pushback during PR review surfaced that "optional field names in data
declarations" has already been considered and rejected in April 2026
as #183 ("Human-readable slot annotations: display layer for @T.n
references"), with three explicit reasons:

1. They can lie -- advisory labels with no enforcement become a
   liability when they drift from semantics.
2. They don't help LLMs *generate* correct indices, only help humans
   *read* generated code.
3. They add comment-rot maintenance burden.

#183's replacement was #445 (vera check --explain-slots), which
shipped in v0.0.108 and is the project's design-aligned answer to
the slot-readability friction class.

The "four load-bearing guardrails" reframe in #620 didn't escape
those reasons -- guardrail 3 ("the compiler does not -- and must
not -- warn on misleading names") explicitly enshrined the first
rejection reason as a feature.  The "single point of truth" framing
(names in constructor declaration, not on slot references) is a
minor mitigation versus #183's per-use-site annotations but a
smaller failure surface, not a different failure mode.

Removed Phase 4d entirely from ROADMAP (it had only #620).  Closure
comment on #620 cites #183 verbatim and explains why the syntactic
difference doesn't escape the rejection.

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

User pushback on #620 (which I closed as duplicate of #183) prompted
re-evaluation of every other newly opened friction issue against
DESIGN.md principles.  All four remaining feature issues fail the
hard look:

* #616 (nat_add / nat_mul / nat_sub_sat) -- Closed as redundant.
  Empirically tested: Nat + Nat -> Nat and Nat * Nat -> Nat work
  directly today, type-check, verify at Tier 1, and run.  Bidirectional
  Int <: Nat subtyping handles them.  The friction is a documentation
  gap that #607 already tracks.  Adding new built-ins for what + and *
  already do violates DESIGN.md principle 6 (constrained expressiveness)
  and principle 3 (one canonical form).
* #618 (IO.read_char / Terminal effect) -- Closed.  Strategic answer
  for real-time terminal programs is --target browser, already
  prioritised in the stabilisation tier as #609 (JSPI sleep) + #610
  (ANSI subset interpreter).  IO.read_char alone is half-useless without
  set_raw_mode (still line-buffered); the full Terminal effect is
  OS-specific and substantial.  Browser path is the design-aligned
  choice and avoids per-OS gotchas.
* #621 (Debug effect) -- Closed.  Closure-must-be-pure is principle 2
  working as intended.  The Vera-aligned debugging path is "extract
  closure to top-level helper, vera test, IO.print from caller" --
  same workaround needed for #614/#615 anyway.  General future answer
  is #294 (effect row polymorphism).  A Debug effect adds a parallel
  mechanism redundant with both -- principle 6 violation.
* #622 (SKILL polish) -- Closed.  Both proposed additions are already
  in SKILL.md: string_join is in the bolded prefix-convention block at
  line 729 plus a worked example at line 982; the decreases-with-+1
  idiom is shown in a worked example at line 1614.  The friction-doc
  author themselves admitted they "didn't read carefully enough first
  time".  Padding SKILL.md with redundant cross-references would
  violate principle 6's documentation analogue.

Net result of the Tetris experiment after design review:
* Two real codegen bugs filed and added to KNOWN_ISSUES.md (#614, #615)
  + stabilisation-tier entries.
* Zero of the seven friction features survive design review:
  - 5 closed (#617 De Bruijn, #619 mandatory contracts, #620 dup of
    #183, plus #616, #618, #621, #622 from this commit).
  - 1 reframed earlier and now also closed (#616).
  - 1 reframed earlier and now also closed (#621).

The friction document was a useful map of where agents hit Vera's
design constraints, but every feature it proposed either:
- Solved a documentation problem (#607 / #622)
- Was already considered and rejected (#620 dup of #183)
- Contradicted a load-bearing design principle (#617, #619, #621)
- Was redundant with an existing or planned mechanism (#616, #618)

ROADMAP cleanup: removed entries for the four newly-closed issues
(Phase 2c #618, Phase 3c #621 + #622, Phase 4c #616).

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

CodeRabbit's stated rule ("HISTORY.md strictly tied to tagged release
versions") is incorrect -- non-versioned `| -- |` rows appear
throughout HISTORY.md, accepted convention for changes that landed
between version bumps.  But the underlying point is valid: existing
`| -- |` rows all describe work that shipped (bug fixes, CI tooling,
GC widening, etc).  The #595 close-note I added is qualitatively
different: nothing of ours shipped, only an upstream wasmtime-py PR
merged.  The issue's own close-comment is the canonical record;
HISTORY duplicating it just adds noise.

Removed the row from HISTORY.  Folded a brief mention into the
existing CHANGELOG [Unreleased] "Changed: ROADMAP.md" entry which
already documents this PR's roadmap edits, so the close-note lives
alongside the rest of the ROADMAP-cleanup record.

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