Follow-up to #520. Once #520 lands compile-time proof obligation + Tier-3 runtime trap for @Nat - @Nat underflow, the same soundness hole remains for @Byte - @Byte.

@Byte values are 0..=255 (unsigned, single octet). Subtraction with a < b underflows the same way @Nat - @Nat does, and the runtime currently emits a plain i64.sub with no guard. A negative @Byte slot violates the byte type's range invariant and propagates into anything that assumed bytes-are-non-negative (string indexing, array indexing into @Array<@Byte>, byte→string conversions).

Scope

Mirror the #520 implementation:

1. Verifier: emit lhs >= rhs proof obligation for BinaryExpr(Sub, lhs, rhs) when both operands are @Byte.
2. Codegen: at Tier 3, emit a guarded subtraction that traps with WasmTrapError(kind="underflow") (same trap kind as @Nat — both are unsigned underflow; a single Fix paragraph covers both).
3. Tests: positive (verifies with requires), negative (fails to verify), runtime (Tier-3 traps cleanly).
4. Conformance: ch??_byte_underflow.vera showing the canonical requires a >= b pattern.
5. Audit existing @Byte - @Byte sites (none expected in current corpus, but verify).

Why follow-up rather than bundled into #520

Keeps the #520 PR focused on the more commonly-used type (@Nat). Once #520 lands, the verifier helper and codegen guard are reusable — this becomes a small mechanical follow-up.

Acceptance

• All @Byte - @Byte sites either verify at Tier 1 (with explicit requires) or carry runtime guards at Tier 3.
• Trap diagnostic names the fix.
• ROADMAP / HISTORY entries follow the campaign's one-line discipline.

Related

• Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 — @Nat subtraction silent underflow (parent)