#551 was filed during #520's design discussion as a "mechanical
follow-up" assuming `@Byte - @Byte` underflow was a runtime hole.
Investigation shows the type checker rejects the construct before
it can reach the verifier or codegen — so there is no runtime hole
and no fix to apply.

vera/types.py:132 defines NUMERIC_TYPES = {INT, NAT, FLOAT64} —
Byte is *deliberately* not in that set.  The arithmetic check at
vera/checker/expressions.py:252 (binary) and :384 (unary negation)
rejects any operand whose base type isn't in NUMERIC_TYPES,
producing E140.  Refinement-type aliases don't bypass —
base_type() strips refinements before the check.

The runtime hole described in #551 doesn't exist because there's
no AST shape `BinaryExpr(SUB, @byte, @byte)` for the verifier or
codegen to ever see.

The separable design question that #551 conflated with — "should
Vera allow Byte arithmetic at all?" — is genuinely speculative
(no current user driver; day-to-day use cases route through stdlib
host imports like base64_encode / url_encode).  Captured as #564
with the full design analysis.  Labeled `bookmark` so the rationale
is preserved for whoever picks up the question if a real driver
emerges.

Changes
-------

tests/test_checker.py
- New TestByteArithmeticRejection551 (5 tests):
  * test_byte_subtraction_rejected_e140 — pins the SUB rejection.
  * test_byte_addition_rejected_e140 — covers the broader ADD case.
  * test_byte_unary_negation_rejected_e147 — pins the unary path.
  * test_refinement_alias_does_not_bypass — ensures `type
    MyByte = { @byte | true }` doesn't provide an escape hatch.
  * test_byte_to_int_then_arithmetic_works — pins the canonical
    workaround idiom.
  These pin current behaviour so a future widening of
  NUMERIC_TYPES (e.g. resolving #564 affirmatively) can't silently
  re-open the hole without a corresponding extension of the
  verifier obligation + codegen guard from #520.

spec/04-expressions.md §4.4
- Drop the "Byte enforcement tracked as #551" caveat.  Replace
  with note that Byte is excluded from arithmetic at the
  type-check layer (vera/types.py); user code that needs
  byte-level arithmetic uses byte_to_int / int_to_byte
  conversions.  Reference #564 as the speculative tracker.

spec/11-compilation.md §11.2.1
- Same fix as spec/04: remove "tracked separately in #551"
  caveat; explain that the underflow obligation needs no Byte
  extension today because the checker prevents Byte arithmetic.
  Reference #564.

ROADMAP.md
- Campaign tracker (line 25): append the #551 housekeeping note
  to the existing chronicle; bump count "eight remain" → "seven
  remain"; remove #551 from the inline list.
- Priority table: drop row 2 (#551) entirely; renumber rows
  3-6 to 2-5.
- New `## Speculative` section between `## Continuous: quality
  and security hardening` and `## Completed phases`.  Lists #564
  with its trigger condition (real Vera program needs byte-level
  arithmetic, or VeraBench shows adoption tax from byte_to_int
  round-trips).  Frames the section's purpose: deferred decisions
  with no current user driver, distinct from campaign / milestones
  / continuous hardening.

TESTING.md / ROADMAP.md
- Doc-counts bumps for the new test class:
  * Tests headline: 3,640 → 3,645 (3,631 passed, 14 skipped).
  * test_checker.py row: 508 → 513 / 5,656 → 5,766.
  * ROADMAP by-the-numbers footer: 3,640 → 3,645.

No version bump
---------------

This is housekeeping with no shipped behaviour change — the
checker's E140 rejection of @byte arithmetic was already in place;
this PR documents that rejection in the spec, pins it with
regression tests, and clears the misconceived bug tracker.

Verification
------------
- 5 new TestByteArithmeticRejection551 tests pass.
- Doc-counts / limitations-sync / version-sync / spec-examples
  all green.

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

…GELOG entry

Three findings; one real, one wrong-but-superseded, one declined.

ROADMAP.md (line numbers → symbol references)
- Drop `vera/types.py:132` parenthetical from line 25 (campaign
  tracker housekeeping note) and line 261 (Speculative section
  entry).  Symbol-level reference (`NUMERIC_TYPES`) is durable
  across code reorganisations; line numbers drift silently.
  CodeRabbit's first finding was correct; second finding ("change
  132 to 131") was based on an older snapshot — the actual line
  is 132 but Finding 1 supersedes by removing the number entirely.

tests/test_checker.py
- Apply the same line-number-removal to TestByteArithmeticRejection551
  class docstring: `vera/types.py:132` → `vera/types.py`; the
  `expressions.py:252 (binary) and :384 (unary negation)` reference
  becomes `_check_binary` arithmetic branch and `_check_unary` NEG
  branch (still pinpoints the location, doesn't drift).

CHANGELOG.md
- Add entry under [Unreleased] / Documentation explaining the #551
  closure and #564 filing.  CI lint
  (scripts/check_changelog_updated.py) flagged spec/ edits as
  substantive changes requiring a CHANGELOG entry — fair gate; spec
  text changes ARE shipped at next version bump.  Without this, the
  unreleased state would have looked like "no changes" while
  spec/04 §4.4 and spec/11 §11.2.1 were materially different.

TESTING.md
- Bump test_checker.py lines 5,766 → 5,767 (one-line shift from the
  docstring rewrite).

Skipped: HISTORY.md update
- CodeRabbit also asked to add a 2026-05-04 entry to HISTORY.md.
  Skipped because HISTORY.md tracks per-release rows (v0.0.126,
  v0.0.127) — not per-event housekeeping.  No version is bumped by
  this PR (no shipped behaviour change), so a new HISTORY.md row
  would break the per-release shape.  The campaign tracker in
  ROADMAP.md already records the 2026-05-04 closure date with full
  rationale; that's the right place for housekeeping events.

Verification
- 5 TestByteArithmeticRejection551 tests still pass; doc-counts /
  limitations-sync / version-sync / spec-examples all green.

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

User-flagged: SKILL.md doesn't tell agents that @byte arithmetic
isn't supported.  Real documentation gap; closing it before this
PR ships avoids a future "I tried @Byte.0 + @Byte.1 and got E140
— why isn't this in SKILL?" loop.

CodeRabbit re-flagged the HISTORY.md ask via a different anchor
(round 1 had it as outside-diff; round 2 puts it inline at line
25).  Same finding; same answer; declining again with stronger
reasoning.

SKILL.md
- Append a clarifying paragraph to the Numeric conversions
  section: "Byte is excluded from arithmetic operators (+, -, *,
  /, %, unary -) at type-check time — @Byte.0 + @Byte.1 produces
  E140.  For byte-level math, convert to Int via byte_to_int, do
  the arithmetic in @int, and convert back via int_to_byte if
  needed.  The forward-looking design question of allowing direct
  @byte arithmetic (with verified underflow + overflow guards) is
  tracked speculatively as #564".

scripts/check_skill_examples.py
- Allowlist line shifts: 34 entries auto-updated by
  scripts/fix_allowlists.py --fix.  Each FRAGMENT entry shifted
  by +2 lines (the new paragraph's two lines), no duplicate keys
  introduced (verified via ast-walk script).

Skipped (again): HISTORY.md update for #551 closure
- HISTORY.md is a per-release ledger.  Its rows are version-tagged
  (v0.0.126, v0.0.127, ...) and serve as the immutable record
  of "what shipped when."  Adding a row for "2026-05-04
  housekeeping #551 closure" would break the per-release shape
  because no version was bumped (no shipped behaviour change).

  The closure IS recorded in three places already:
  1. CHANGELOG.md [Unreleased] entry — will roll into the next
     release row whenever v0.0.128 ships.
  2. ROADMAP.md campaign tracker (line 25) — date-stamped event
     log for in-flight campaign work.
  3. The closed issue itself with detailed comment, plus #564
     speculative tracker.

  HISTORY.md is the wrong venue: it tracks releases.  When
  v0.0.128 lands, the [Unreleased] CHANGELOG content (including
  this housekeeping note) will be folded into a single HISTORY
  row per the established convention.

Verification
- check_doc_counts / check_spec_examples / check_skill_examples /
  check_limitations_sync all green.

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

…entries

Real pre-existing technical debt CodeRabbit caught: four SKILL
allowlist entries labeled `FRAGMENT` that actually point at
*full functions* with complete contracts.  Verified each entry by
walking the SKILL.md block at its line:

| Allowlist line | SKILL.md content | Pre-fix label |
|---|---|---|
| 1396 | `private fn try_div(...)` Exn handler example | "Async effect declarations list" |
| 1485 | `private fn classify(...)` Inference effect example | "Effect handler syntax template" |
| 1552 | `private fn run_counter(...)` State handler example | "Handler syntax template, not real code" |
| 1863 | `public fn process(...)` with where-block helper | "Wrong: missing index on slot reference" (label nonsense too) |

Each of these blocks parses cleanly without an allowlist entry —
verified by removing the entries and re-running the parser:

    Before: Parsed OK: 52 / Allowlisted: 66 / FAILED: 0
    After:  Parsed OK: 56 / Allowlisted: 62 / FAILED: 0

Total Vera blocks unchanged at 118; the 4 blocks shifted from
"allowlisted" to "parseable" — which is the correct
classification.  The allowlist's mapping semantics
(intentionally-unparseable fragments only) are now respected for
those four entries.

scripts/check_skill_examples.py
- Remove the 4 mis-classified `FRAGMENT` entries (lines for
  SKILL.md offsets 1396, 1485, 1552, 1863).  Allowlist drops from
  66 → 62 entries; no duplicate keys (verified via ast-walk
  script).

Out of scope for this PR
- An audit of *all* `FRAGMENT` allowlist entries (62 remaining)
  to identify other potential mis-classifications would expand
  the change surface beyond #551 / #565's housekeeping focus.
  The four Rabbit named were the specific ones in this round's
  finding.  If the broader audit is worth doing, file as a
  separate cleanup issue (would naturally pair with #538, the
  larger "replace line-numbered allowlists with inline HTML
  comment fences" refactor).

Verification
- check_skill_examples.py: 0 failures, all 118 Vera blocks pass.
- check_doc_counts / check_limitations_sync / check_version_sync:
  all green.

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