throw's payload is never narrowed: a violating value flows into Exn<T> with no obligation and no runtime guard

[aallan]

Found during the #1213 burndown (PR C5's scope-boundary check). throw's argument position carries no narrowing obligation at all:

effects(<Exn<Nat>>) ... throw(0 - 5)

verifies clean — 4/4 Tier 1, ZERO refine_bind obligations — and vera run returns 0 SILENTLY, the negative value having been narrowed into the @Nat payload with no static obligation and no runtime guard. The refined spelling (type Pos = { @Int | @Int.0 > 0 }, effects(<Exn<Pos>>), throw(0 - 5)) is identical: clean verification, silent run.

The contrast that localizes it: a USER effect's op argument in the same position is correctly obligated — op emit(Pos -> Unit) + Log.emit(0 - 5) → loud E505. So the shared binding-obligation machinery covers effect-op arguments generally; throw specifically bypasses it. Not refinement-specific, not Byte-specific.

Pre-existing (verified against the pre-C5 base). A silent verification hole — the class the burndown's completion bar treats as must-fix: check-green, verify-green (falsely), silently wrong at run.

Fix direction: throw's payload flows through the same binding-obligation family as every other narrowing site (the shared helper the C5 gate lives in covers let/call-arg/ctor-field/tuple/effect-op-arg/match/array/handler-init already — the question is why the throw lowering path skips it, likely because throw's Never return shape takes a different translation leg). The proving test is the E505 twin of the user-effect contrast above, plus the runtime-guard leg for the Tier-3 case.

[aallan]

The static half is merged into release/v0.1.10 via PR #1270 (2026-08-10T11:55Z): throw's payload — and, after the review round replaced the name-keyed gate with the structural one, every bare call resolving to an effect operation — now carries the standard binding obligation, so a provably-violating value is a loud E503/E505 and an undischargeable one is a disclosed tier3_unguarded. This issue stays OPEN for the residual: codegen emits no runtime guard on the payload (throw lowers straight to throw $exn_<family>), sized in the PR as a codegen change of its own (reuse the #1203 put-store guard emission plus the boundary-predicate lowering, then flip the verifier's guardedness). The KNOWN_ISSUES row states the interim honestly.

[aallan]

A second residual, measured during PR C1's rebase-interaction probe (pre-existing at ef7c04c0, i.e. present in the merged PR #1270 fix itself): the payload obligation does not survive monomorphization. The same provably-negative throw payload refutes as a loud E503 in a non-generic function but demotes to Tier-3 inside a monomorphized clone — measured with an imported forall<T> whose body throws into an Exn<Nat>, identical with and without an importer-side shadow. So the static half closed by #1270 covers non-generic bodies; clones keep the old silence-shaped demotion (disclosed, at least, but weaker than the direct case). Routing decision pending: either the clone-verification path re-runs the bare-op obligation walk under its pinned scopes (the #1241 machinery landing in PR C1 is the natural hook), or it joins the runtime-guard residual as this issue's documented scope. Both residuals stay on this issue.

[aallan]

PR C7 (branch fix/c7-widths) threads the payload cell metadata (CellNames on throw, from both registration paths) that this issue's runtime-guard residual will want — the guard emission now has a site handing it the resolved cell identity, and the width marking means the guarded value is at the declared width. It also unblocks the run-assertion extension PR #1270's review flagged (the satisfying-literal test now runs as well as verifies). The guard itself remains unimplemented; both residuals stand.