Make the release body fit, and widen the gates to the drift they missed

.github/workflows/release.yml

@@ -162,6 +162,7 @@ jobs:
         run: |
           python scripts/release.py notes \
             --version "$VERSION" \
+            --repo "$GITHUB_REPOSITORY" \
             --output release/RELEASE_NOTES.md
           python scripts/release.py manifest \
             --dist-dir dist \

.gitignore

@@ -72,3 +72,9 @@ node_modules/
 # and verifies, so it produces neither; `pytest tests/` leaves the tree clean.)
 /hello.txt
 /examples/hello.txt
+
+# `scripts/check_corpus_differential.py` checks the base revision out here
+# by default, keyed by SHA and reused across runs.  Output, not source, and
+# deliberately repository-local rather than under a shared temporary
+# directory (its contents end up on the base side's PYTHONPATH).
+/.corpus-differential/

CLAUDE.md

@@ -80,6 +80,8 @@ python scripts/build_site.py          # Regenerate AI-readable site assets (llms
 python scripts/check_site_assets.py   # Verify site assets are up-to-date + docs/index.html ↔ docs/index.md state coherent facts (#1154)
 python scripts/check_version_sync.py  # Verify version consistency
 python scripts/check_doc_counts.py    # Verify documentation counts match codebase
+python scripts/check_doc_counts.py --check-bug-issues # Also check KNOWN_ISSUES' Bugs table against the open `bug` issues (GitHub API; release-PR time, not pre-commit)
+python scripts/check_corpus_differential.py --base-ref origin/main  # Compile the corpus at two revisions; report programs whose WAT moved (burndown instrument, not a hook)
 python scripts/check_licenses.py      # Verify all package licenses are MIT-compatible
 python scripts/check_wheel_availability.py # Verify every runtime dep has wheels for all supported platforms (README §Supported platforms)
 python scripts/check_limitations_sync.py              # Verify limitation tables are in sync

FAQ.md

@@ -279,7 +279,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 14-chapter formal specification
-- 11,786 tests, including a 244-program conformance suite
+- 11,940 tests, including a 244-program conformance suite
 - 42 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation

KNOWN_ISSUES.md

@@ -21,8 +21,6 @@ Defects in shipped compiler, runtime, or tooling behaviour — this table matche
 | The checker resolves a bare call to a SIBLING function's `where` helper. Spec §5 makes a helper local to its parent, and the checker's own `_lookup_function_scoped` implements that — it walks the enclosing frame stack and reads each frame's direct helpers — but it then falls back to `env.lookup_function`, and `vera/registration.py` has recursed every helper into that flat `TypeEnv`. So a top-level `other()` calling `helperx(7)`, where `helperx` is a helper of an unrelated `holder`, is **check-green and verify-green** and then refused by codegen (`Function 'helperx' is not defined in this module and was not found in any imported module`) — the helper is emitted as `holder$where$helperx`, so the bare call has no target. Loud, never a wrong answer. The op-name variant is the one that matters for the #1284 ownership predicate: with the helper named `get` and the sibling reading a `State<Int>` cell by bare `get(())`, the checker binds the HELPER and reports `[E202] Argument 0 of 'get' has type Unit, expected Int` where spec §7.4 resolves the operation — so the checker rejects a program codegen compiles correctly, the two tables disagreeing in the CHECKER's direction for the first time. Codegen's `_scoped_fns` (#1299) implements the spec rule; the fix here is a checker change, whose new rejections need their own blast-radius pass. | [#1307](https://github.com/aallan/vera/issues/1307) |
 | `md_parse` diverges between the native and browser runtimes on **211 of 1,471** adversarial inputs (14.3%) and **329 of 4,858** blank-line-separated sections of the project's own documentation (6.8%), measured at [PR #1303](https://github.com/aallan/vera/pull/1303) by comparing the two ADTs directly rather than their renders. The second denominator is the repository's own Markdown, so it moves whenever a document gains or loses a section; 11 of those 4,858 also differ in the rendered output. Nine classes, each with a one-line repro. The largest by a wide margin — 173 of the 211 — is *plain-text run grouping*: the browser emits one `MdText` per scan segment where the reference coalesces adjacent runs, so `**unclosed` is `[MdEmph([]), MdText("unclosed")]` natively and `[MdText("*"), MdText("*unclosed")]` in the browser. That class is invisible to `md_render` (the runs concatenate to the same text) but not to a Vera program that matches on the ADT, which is what makes it a §12.9.3 violation rather than a cosmetic one. The rest are render-visible: emphasis/strong scanning (`***both***` renders `**both****` natively, `***both***` in the browser); list-continuation indent width, where the reference strips exactly two (or three) characters and the browser strips all leading whitespace (`- a\n   b` → `- a  b` vs `- a b`); a `+` bullet, unrecognised in the browser; an `n)` ordered marker, likewise; a loose list, one list natively and two in the browser (`- a\n\n- b`); nesting past two levels, flattened in the browser (`- a\n  - b\n    - c`); a thematic break with internal spaces (`*   *   *`); and a table without a separator row (`\| a \| b \|\n- li`). Neither implementation is the specification — §9.7.3 pins the ADT, not the grammar that produces it — so closing this means choosing a parse for each class and stating it, then mirroring. Successor to [#1294](https://github.com/aallan/vera/issues/1294), which closed the `md_render` half; the parity suite pins the shapes they do agree on, so a regression on one of those goes red. | [#1301](https://github.com/aallan/vera/issues/1301) |
 | A postcondition may name a `State<T>` the function's effect row never declares, and `vera check` accepts it: `ensures(new(State<Bool>) == false)` under `effects(<State<Int>>)` reports OK, then `vera compile` fails with **E699** — the internal-compiler-error diagnostic whose own text says the type checker should have rejected the input, which is exactly the situation. Both forms land there for the same reason (no cell of that family exists, so `old()` finds no snapshot local and, since [#1285](https://github.com/aallan/vera/issues/1285), `new()` finds no getter). Loud and never a wrong answer, so this is diagnostic quality rather than soundness — but it is a check-green program that cannot compile, reported against the compiler instead of against the program, with a bug-report request the user should not act on. Before #1285 the `new()` side was worse than loud: the name-keyed lookup found the row's other getter and silently read the wrong cell. Fix direction: validate an `OldExpr`/`NewExpr`'s effect reference against the declared row where the checker already validates the rest of the clause, one rule for both forms; `test_a_family_the_row_does_not_declare_is_loud_on_both_sides` pins today's E699 and is the test to flip. | [#1298](https://github.com/aallan/vera/issues/1298) |
-| Spec Chapter 10 is a second, hand-maintained copy of `vera/grammar.lark`, and the rule-name alignment gate `scripts/check_grammar_alignment.py` compares only rule-name headers — three classes of drift pass it unseen. **Terminals, both directions**: the header pattern requires a lowercase lead, so a fabricated terminal added to §10.2 leaves the gate green, and no declared-versus-referenced audit exists in either direction. **Rule references**: restoring a removed ambiguity to a production's right-hand side is invisible, because only headers are compared. **Production bodies**: the class most grammar edits actually fall into. Two instances are live in the chapter on `main` today, both body-level and both this issue's to close: typed holes (`"?" -> hole_expr`, in `grammar.lark` since 2026-03-30) appear nowhere in `primary_expr`, and §10.2's `BLOCK_COMMENT: /\{-[\s\S]*?-\}/` is non-nesting, contradicting both §1.3 ("They nest") and the implementation, which parses `{- a {- b -} c -}` clean. Never a wrong answer from a program — the defect is that the published grammar misdescribes the one the parser has. Fix direction: extend the gate side-aware (terminal audit both ways, reference-set comparison), or fold Chapter 10 toward the DESIGN Grammar row's actual promise of a single-sourced shared grammar rather than a hand-maintained copy held honest by ever-wider cross-checks; the two live instances are fixable independently of which direction wins. | [#1290](https://github.com/aallan/vera/issues/1290) |
-| `.github/workflows/release.yml`'s `Tag and create GitHub Release` step fails with `HTTP 422: Validation Failed — body is too long (maximum is 125000 characters)` when the CHANGELOG section `scripts/release.py notes` extracts into `RELEASE_NOTES.md` exceeds GitHub's release-body limit. It fired on v0.1.10, whose notes extract to roughly 148,700 bytes — the #1213 burndown's 44-issue section, some 23,000 characters past the limit — and it fired at the worst point in the pipeline: **after** PyPI had accepted the immutable archives and **after** the tag was created, leaving the release half-cut with no repeatable path back. The v0.1.10 GitHub Release was completed by hand, mirroring the step exactly: the run's artifacts downloaded and hash-verified three ways, then `gh release create --verify-tag --latest` with the wheel, sdist and SHA256SUMS, and a generated body — the section's bold bullet lead-ins as a headline index plus a link to the canonical section at the tag. Rare, since it needs a release this large, but rarity is not the mitigating factor here; the landing point is. Fix direction: make the step total — before `gh release create`, regenerate oversized notes into that index form so the release always carries a body that fits, with the full notes staying in `CHANGELOG.md`, which is already the release notes of record. | [#1288](https://github.com/aallan/vera/issues/1288) |
 | `ch05_closure_nat_return` (a run-level conformance program in the pre-commit + CI gate) trapped **once** in a full `check_conformance.py` run (`unreachable` in `main` — the sentinel `assert` or a GC shadow-stack guard) and has not reproduced in ~960 attempts across isolated, parallel, eager-GC, and hash-seed-swept executions; the emitted WAT is deterministic and correct. Suspected rare runtime/GC/wasmtime interaction, tracked so a future intermittent CI red resolves here instead of starting fresh. | [#996](https://github.com/aallan/vera/issues/996) |
 
 ## Limitations

README.md

@@ -263,7 +263,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.1.11: 2,000+ commits, 209 releases, 11,786 tests, 95% Python code coverage, 244 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.1.11: 2,000+ commits, 209 releases, 11,940 tests, 95% Python code coverage, 244 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/).
 

RELEASING.md

@@ -93,7 +93,16 @@ The release-prep PR must:
 2. Turn the accumulated `[Unreleased]` notes into a dated `## [X.Y.Z]`
    section with at least one bullet and update the CHANGELOG compare links.
 3. Add the release's one-line HISTORY entry and regenerate site assets.
-4. Pass the ordinary protected-branch CI and review process.
+4. Reconcile `KNOWN_ISSUES.md`'s Bugs table with the tracker, by running
+   `python scripts/check_doc_counts.py --check-bug-issues`.  The convention
+   is one row per open `bug`-labelled issue, and the check needs the GitHub
+   API — it sends `GH_TOKEN` or `GITHUB_TOKEN` when either is set, and is
+   rate limited per IP when neither is, so export one before running it —
+   so it is opt-in rather than part of the pre-commit hook: mid-cycle
+   the two legitimately disagree, since a bug filed against an open PR's
+   branch has an issue before it has a row.  At release time they should
+   agree — that is the point at which the file is the published list.
+5. Pass the ordinary protected-branch CI and review process.
 
 After merge, `release.yml` detects the version increase on `main`. It then:
 

ROADMAP.md

@@ -12,7 +12,7 @@ Ordering derives from the design principles ([DESIGN.md](DESIGN.md)): verificati
 
 ## Where we are
 
-11,786 tests, 244 conformance programs, 42 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire.
+11,940 tests, 244 conformance programs, 42 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire.
 
 ## Stage 19 — The verification completeness sprint