Add checked if/match statements, generalize linear reconciliation to N arms

D-094 §7's own deferred follow-up: strata_hir::StatementKind had no
If/Match variant, so bare if (no else) and match-as-statement both
fell to Unsupported, poisoning the whole component and forcing linear
bindings live across them into the conservative never-consumed
fallback. This gives both real checked representation.

strata-hir: StatementKind::If{condition,then_block,else_block} and
StatementKind::Match{scrutinee,arms}. lower_block routes bare-if/match
statement-position expressions through new lowering functions, except
when an if/else sits in tail-value position — that path is untouched,
preserving D-094's landed Select behavior exactly. else-if chains
reuse the same machinery via a synthetic single-statement wrapper
block.

strata-check: reconcile_arms generalizes Select's two-arm rule to N
arms (same UseCount shape on every arm = one safe use; any divergence
rejects, naming which arms differ; any Many propagates without
re-firing) — Select's own reconciliation now calls this shared
function, verified byte-identical for the 2-arm case against the full
existing suite. block_linear_uses folds a target's uses across a
whole block's statements, not just a tail expression, handling nested
If/Match via reconcile_arms so arbitrary nesting works by
construction. A bare if gets a synthetic always-Zero arm standing in
for the untaken path — consuming a linear binding only inside the
taken path is exactly the same leak shape already rejected for
asymmetric Select arms.

Conditional register/mem lowering: the pre-existing NestedState guard
(block_depth > 1) already covers this — a register update reached
through the new If/Match branches is correctly excluded from
arch-ir/CIRCT lowering rather than silently treated as unconditional.
No new arch-ir Mux concept needed; verified end-to-end that check
succeeds and compile fails gracefully with lowering_rejected/
NestedState, not a crash.

Updated linear_let_live_across_unchecked_bare_if_is_conservatively_
rejected to assert the precise linear_branch_mismatch now that bare
if is really checked, instead of the old generic fallback — matching
the CDC/mem precedent for correcting stale tests rather than leaving
them inaccurate.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
cec995bda4versecafe committed on 8/20/2026, 4:57:33 AMparentfc26a6c
7 files changed+489-71