Speculative. No current user driver — filed during a 2026-05-04 audit while closing #551 (originally framed as a soundness fix; turned out to be checker-prevented).

What this would change

Today vera/types.py:132 defines NUMERIC_TYPES = frozenset({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. Refinement-type aliases (type MyByte = { @Byte | true }) don't bypass — base_type() strips refinements before the check. So @Byte + @Byte, @Byte - @Byte, @Byte * @Byte, -@Byte, etc. all produce E140 at type-check time.

Allowing Byte arithmetic would mean:

1. Widen NUMERIC_TYPES to include BYTE.
2. Verifier obligations on Byte: underflow (lhs >= rhs for sub) AND overflow (lhs + rhs <= 255 for add, lhs * rhs <= 255 for mul). Both directions, because Byte is [0, 255] (closed range, unlike Nat which is [0, ∞)).
3. Codegen guards on Byte: lower bound (mirror Nat underflow guard from Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520, but i32.lt_u since Byte is unsigned i32 in WASM) AND upper bound (compare against 255 after widening to i64 to avoid intermediate i32 overflow).
4. Spec updates: spec/04 §4.4 and spec/11 §11.2.1 need to extend the unsigned-arithmetic obligation language from Nat-only to Nat + Byte, with the upper-bound case spelled out.
5. Tests: parameterise the existing TestNatSubtractionObligation520 and TestNatSubtractionRuntimeGuard520 tests over both types, plus add overflow-guard tests for ADD and MUL.

Why this is speculative (no current driver)

The day-to-day Vera use cases that could need byte arithmetic — base64 / URL / hex encoding, JSON char classification, HTML escape, parser lookup tables — are already implemented in the standard library as host imports (base64_encode, url_encode, etc., written in Python/JS). User code calls those, not byte primitives. The byte_to_int → @Int arithmetic → int_to_byte round-trip handles the rare custom case verbosely but correctly.

The use cases where byte arithmetic would be idiomatic but currently is not:

• Custom parsers for binary formats (network protocols, image data, file headers). Not currently in scope for Vera; agents writing parsers today reach for stdlib (CSV parsing and generation #236 CSV, JSON, etc.) or call out to host code.
• Character math ('a' + 1 == 'b', ASCII case folding). Vera uses string_char_code which returns @Nat — already in Nat-arithmetic land, no Byte involvement.
• Hash / checksum / XOR primitives. Cryptography is deliberately out of scope today (Cryptographic hashing (SHA-256, HMAC) #235 tracker). Even if it lands, primitives might be exposed as host imports rather than Vera-level byte ops.
• Color / pixel arithmetic (RGBA blend, alpha). Niche; no Vera precedent.

Trade-offs

Pros:

• LLM agents porting b1 - b2 from Rust/Go/C don't need byte_to_int noise in the translation.
• Eliminates the round-trip-bug class (byte_to_int(int_to_byte(...)) patterns).
• Symmetric with @Nat's unsigned arithmetic story (Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520).

Cons:

• Two range guards instead of one (under + over). Doubles the requires surface for every binary operator. Adds verifier complexity.
• WASM codegen complexity: i32 + i32 might overflow i32 itself before the <= 255 clamp; need careful widening to i64 inside the guard.
• Mixed-type (Byte + Int) still needs conversions, so it doesn't fully eliminate conversion noise.
• Wraparound semantics unfamiliar to users coming from C / Rust u8 (where wrap is silent and well-defined).
• The current "Byte is convert-only" idiom is deliberate, not an oversight.

Trigger condition

Open this issue when:

• A real Vera program (or proposed feature) requires byte arithmetic at the user-code level — e.g., a binary-format parser the stdlib doesn't cover.
• Or the agent porting bench (VeraBench tier ?) shows a measurable adoption tax from byte_to_int round-trips on byte-heavy benchmarks.

Until one of those signals appears, the current design (Byte excluded from arithmetic) is the right call for Vera's LLM-target audience.

Action when the time comes

• Confirm a real user-code use case needs byte arithmetic at the language level (not satisfied by a stdlib primitive).
• Decide on overflow semantics: trap (current @Nat convention), saturate (clamp to 0/255), or wrap (C / Rust u8 style).
• Widen NUMERIC_TYPES in vera/types.py:132 to include BYTE.
• Extend _is_unsigned_typed / _has_nat_origin in vera/verifier.py (rename or parameterise).
• Extend _is_static_nat_typed / _has_nat_origin_codegen in vera/wasm/operators.py.
• Add overflow obligation for + and *: lhs + rhs <= 255, lhs * rhs <= 255.
• Codegen: emit guarded sequences for + and * in addition to -.
• Update spec §4.4 and §11.2.1 to extend the unsigned-arithmetic language to Byte.
• Parameterise existing TestNatSubtractionObligation520 and TestNatSubtractionRuntimeGuard520 over Nat + Byte.
• Add overflow-direction tests.

Related

• Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 — @Nat subtraction underflow (parent — the architecture this would extend).
• @Byte subtraction silent underflow (follow-up to #520) #551 — Closed as not-a-bug; the original "Byte underflow soundness hole" framing turned out to be checker-prevented. This issue captures the speculative feature the original was conflated with.
• Generalize @Nat invariant check to all binding sites (broader generalisation of #520) #552 — Generalise @Nat invariant check to all binding sites. If Byte arithmetic lands, the same generalisation extends.
• Generic functions bypass E502 underflow obligation (follow-up to #520) #555 — Generic functions bypass E502. Same.