Implement delay/Later<Clock,T> guarded feedback typing per D-095
Ships D-095's Later introduction/elimination judgment and, in the
same change per the standing D-093/D-094 commitment, FIX-ω's branch
(b) resolution — not deferred a fourth time.
- strata-hir: TypeKind::Later{domain, inner}, a peer of Stamped. No
grammar changes — delay(init, next) already parsed as an ordinary
Call.
- strata-check: CheckedExprKind::Delay, promoted from Call the way
D-092 promoted Index. The self-reference mechanism needed a real
judgment call the design doc's "synthetic name" language didn't
literally specify a syntax for: since v0 ships zero new grammar,
`next` refers to the delay's own result via the enclosing `let`'s
own name, bound at type T (not Later<T>) inside next's scope,
reusing that same LocalId under BindingKind::Register — which makes
lowering free, since a Binding(target_id) inside next already
resolves to a register read with no new lowering logic. This forces
delay(init, next) to be written as a direct `let name = ...`
initializer (delay_call_not_let_initializer rejects anything else).
Elimination: a Later value crossing into a same-domain `reg <-
expr;` update is accepted (with CDC crossing-checked); used anywhere
else as if it were T — output, return, comparison — is rejected
with later_value_used_before_clock_edge.
The one-delay-per-component restriction did not fall out for free:
delay_calls_seen is incremented before descending into a call's own
args, so both a second top-level delay and a delay nested inside
another delay's init/next are caught by the same counter check.
FIX-ω (branch b): reject_linear_in_feedback_next, a flat structural
membership walk (mem_tainted/ghost_tainted-shaped, not a counting
one) rejects any reference to a still-live linear-tracked binding
anywhere in next's subtree, called eagerly once per delay call site
rather than lazily through linear_uses's per-target sweep — fires
even in a component with zero linear lets in scope, and avoids
re-diagnosing the same next subtree once per unrelated linear
target.
- strata-arch-ir/strata-circt: no new node type, confirmed both by
code (a checked delay unpacks directly into a CheckedRegister +
CheckedRegisterUpdate before ever reaching this lowerer) and by
compiling the good fixture and inspecting the MLIR directly: two
plain seq.firreg ops, zero Later leakage into the output.
Verified end-to-end via the real CLI: the FIX-ω case rejects with
linear_reference_in_feedback_next, the early-use case rejects with
later_value_used_before_clock_edge, and the good fixture checks clean
and compiles to exactly the plain register shape D-095 §6 promised.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
54efc08232versecafe committed on 8/20/2026, 5:29:35 AMparentcec995b